Natural Language based Specification and Verification

技術概要：自然言語に基づく仕様と検証（NLForge）

問題定義
C および C++ プログラムにおけるメモリ安全性違反（無効な参照外し、解放後の使用、範囲外アクセスなど）は、ソフトウェアの脆弱性の主要な源泉のままです。これらのエラーは、割り当て、解放、初期化、エイリアシングに関わる複雑な関数間相互作用に起因することが多く、従来の静的解析ツールはスケーラブルな検証において困難に直面しています。大規模言語モデル（LLM）はバグの特定において強力な能力を示していますが、形式的検証を通じて新たな脆弱性の導入を防止する点では重大な課題に直面しています。既存の検証パイプラインは通常、ループ不変条件や事前・事後条件などの厳格な形式言語による仕様を必要とし、高い注釈付けの負担を生み出します。LLM を用いてこれらの形式仕様を合成しようとする先行試みは、限られた成功しか収めていません。さらに、最近のベンチマークは、単一関数検証から構成的な多関数推論へ移行する際、LLM の性能が文脈ウィンドウの制限とグローバルな意味的一貫性を維持する難しさにより急激に低下することを示しています。

手法：NLForge
著者は、厳格な形式アーティファクトではなく自然言語仕様を生成・推論するために LLM を活用する構成的検証フレームワークであるNLForgeを提案します。このシステムは、プログラムの呼び出しグラフに対するボトムアップ、被呼び出し関数優先の分析に基づいて動作します。

1. パイプラインアーキテクチャ:

   • 前処理: システムは C/C++ コードから関数定義、シグネチャ、呼び出し箇所を抽出して呼び出しグラフを構築します。未解決の呼び出しは外部スタブを介して処理されます。
   • ボトムアップ分析: フレームワークは、トポロジカル順序（呼び出し元より先に被呼び出し関数を処理する）で呼び出しグラフに対して分析パスのシーケンスを実行します。
   • 自然言語サマリー: 形式論理を生成する代わりに、LLM は特定の属性について構造化された自然言語サマリー（自然言語記述を含む型付き JSON としてエンコード）を生成します。
     • 割り当て/解放/初期化: ヒープオブジェクトの作成、解放効果、および出力パラメータの初期化を要約します。
     • メモリ安全性契約: 事前条件（例：非 null、未解放、バッファサイズ）および事後条件を推論します。
     • リークおよび整数サマリー: 未解決の義務と整数オーバーフローのリスクを追跡します。
   • 構成的チェック: 最終的な検証パスにおいて、LLM は自身の推論した事前条件と被呼び出し関数の自然言語サマリーを用いて関数を分析します。モデルは、被呼び出し関数の完全な実装をインライン化することなく、被呼び出し関数の契約に対する安全性要件をチェックする推論エージェントとして機能し、潜在的な実行状態を維持します。

2. 設計の根拠:
   このアプローチは、コードとドキュメントでトレーニングされた LLM は、厳格な形式表記よりも自然言語サマリーをより一貫して生成、解釈、洗練できるという観察に基づいています。この設計は、検証問題を再利用可能な意味サマリーに分解することを目的としており、モデルが各呼び出し元の生ソースコードを再分析するのではなく、被呼び出し関数に関する明示的に述べられた仮定の下で関数について推論することを可能にします。

主な貢献

• 構成的フレームワーク: LLM を用いてメモリ安全性属性を推論・検証する、C/C++ 向けのボトムアップ関数間検証フレームワーク。
• 自然言語中間表現: 外部の記号チェッカー向けの形式仕様生成に焦点を当てた先行研究とは対照的に、検証の中間表現として自然言語意味サマリーを導入すること。
• 段階的分析パイプライン: 割り当て、解放、初期化、および呼び出し元側の義務といった再利用可能なサマリーにメモリ安全性推論を分解し、これらを後続の段階で LLM にフィードバックすること。
• 実証的評価: SV-COMP 2026 ベンチマークにおける、構成的推論と非構成的な全体プログラムプロンプトベースラインとの比較研究。

結果
著者は、4 つの LLM バックボーン（Claude Sonnet-4.6、GPT-5.4、Gemini-3.1-flash-lite、Qwen3.5-27B-UD-Q4）を用いて SV-COMP 2026 メモリ安全性ベンチマークのサブセットで NLForge を評価し、従来の検証ツール（CPAchecker、Symbiotic、Ultimate Automizer）と比較しました。

• RQ1（検証者としての LLM）: LLM ベースの分析は高い再現率とカバレッジを示し、真陽性の大部分を特定しました（例：Sonnet-4.6 は valid-memsafety において 99.8% の再現率を達成）。しかし、従来のツールに比べて偽陽性が著しく多く、現時点では単独の健全な検証者として機能することはできません。従来のツールは偽陽性を避けるために困難なケースで「不明（UNK）」を返すことがよくありますが、LLM はより高いエラー率で決定的な回答を提供します。
• RQ2（構成的検証）: 構成的アプローチは、特に複雑な実世界の制御フローおよびデータ構造ベンチマークにおいて、非構成的ベースラインを大幅に上回りました。
  • 構成的実行は、すべてのモデルにおいて真陽性を 3,390 から 3,476 に増加させ、偽陰性を 301 から 216 に削減しました。
  • 改善はより小さなモデルで最も顕著でした（例：Qwen3.5-27B-Q4 は偽陰性を 218 から 97 に削減）また、強い関数間推論を必要とするベンチマークにおいて顕著でした。
  • 合成された局所的な Juliet テストでは、改善が一貫しませんでした。これは、非構成的モデルが局所的なパターンを直接活用できたためです。

意義と主張
本論文は、検証における LLM の活用方法の転換を主張しています。外部エンジン向けの形式アーティファクトの生成者としてのみ扱うのではなく、構造化された再利用可能な自然言語サマリーに対する推論エージェントとして使用することへの移行です。

• 実用性: 自然言語は、特に全体プログラムプロンプティングがモデルの推論予算や文脈ウィンドウを超えてしまうタスクにおいて、構成的検証を可能にする実用的な中間仕様層として機能します。
• 限界: 著者は、自然言語の非形式性が較正の問題（より高い偽陽性）をもたらすことを認めており、このアプローチは生成されたサマリーの品質に敏感であると指摘しています。サマリー内のエラーは伝播し、増幅する可能性があります。
• 将来展望: この研究は、LLM がまだ健全な形式的検証の代替手段ではないものの、スケーラブルなバグ発見検証への有望な方向性を提供することを示唆しています。将来の研究は、較正の改善、サマリーと記号チェックの組み合わせ、間接呼び出しやヒープ不変条件などの複雑な機能のより堅牢な処理に焦点を当てるべきです。

本研究は、LLM がメモリ安全性を検証できるかという問いではなく、どのような表現と分解の下でそれらがより信頼性が高くなるかという問いが重要であると結論付けており、自然言語がモジュール化されたプログラム構造と LLM の推論能力の間のギャップを効果的に埋め得ることを浮き彫りにしています。