安全クリティカルなシステム開発において、形式検証は信頼性を確保する重要な手法であるが、線形時相論理（LTL）などの形式論理の使用には高度な専門知識が必要であり、形式検証の適用範囲を制限している。テンプレートベースの翻訳アプローチは信頼性と引き換えに表現力を犠牲にし、ニューラル手法は流暢さを達成するものの正しさの保証を提供しない。この矛盾を解決するため、研究者らは学習翻訳と形式検証を統合するニューロシンボリックアーキテクチャ「NeuroNL2LTL」を提案した。
NeuroNL2LTLの中心的な設計は、翻訳プロセスを中間表現を経由させることである。この中間表現からLTLへのマッピングは構造保存的であり、生成される仕様は充足可能性と非自明性のチェックを受ける。さらに、最小編集修復メカニズムにより、ほぼ正しい出力が下流ツールに到達する前に自動修正される。これにより、ニューラルモデルの柔軟性を活用しつつ、シンボリック検証による硬い保証を提供する。
本論文の最も重要な革新は「検証器インザループ訓練」である。従来のニューラル翻訳モデルは参照訳との類似度のみを最適化するが、NeuroNL2LTLは検証結果を強化学習の報酬信号として使用し、ニューラルコンポーネントが形式正しさを直接目標として最適化される。これにより、モデルは訓練段階で論理的に検証可能な仕様を生成することを学習する。
評価のために、著者らは航空宇宙、ロボティクス、自動運転を含む12領域にわたる20万件以上の要件を含むテストセットを構築した。実験の結果、NeuroNL2LTLは意味的等価性で28%を達成し、同時に86%の出力が充足可能性検証に合格することを保証した。28%という意味的等価率は一見低いが、LTL翻訳の複雑さと厳密性を考慮すると、ニューロシンボリック手法の可能性を示している。さらに重要なのは、システムがほとんどの出力の論理的充足性を保証し、下流の検証ツールに信頼できる入力を提供することである。
翻訳に加えて、NeuroNL2LTLはLTLから文脈に基づく説明を生成し、専門的な論理訓練を受けていない領域専門家が仕様を理解し検証するのを支援する。これにより形式検証の敷居が下がり、より多くのエンジニアが形式手法の恩恵を受けられる。
結論として、この研究は形式検証がニューラル仕様システムの訓練目標と実行時フィルターの両方として機能し、統計的信頼性ではなく論理的保証に基づく信頼性を持つニューラルツールの構築を可能にすることを示した。これは安全クリティカル分野における自然言語インターフェースの新たな道を開き、形式検証の産業応用を促進する可能性がある。