技術的概要：エージェンティック・モデル・チェッキング

問題定義

大規模言語モデル（LLM）によって生成されたシステムコードの検証は、形式検証における既存の困難さを増幅させる独自の課題を提示する。LLM は C や Rust などの言語で、オペレーティングシステム、コンパイラ、ドライバのための膨大なコードを生成できるが、生成されたコードベースには明示的な形式仕様がないことが頻繁である。さらに、LLM 生成コードにおける安全性契約は、関数の境界で強制されるのではなく、呼び出しサイトにおいて暗黙的に符号化されることが多い。

この暗黙的な符号化は、特定の失敗モードをもたらす。ヘルパー関数（例えば、バイトインデックス付きリーダー、オフセット算術ライター）は、不変条件を維持するために周囲の呼び出し元のロジックに依存し、しばしば境界やオーバーフローガードを欠く。その結果、コードは形式化された入力に対しては正しく機能するが、敵対的または作為的な入力に対しては失敗する。従来の検証ツールはここで苦戦する。なぜなら、それらは文脈なしにヘルパーを破損として過剰に報告するか（過剰報告）、現在の呼び出し元がトリガーしないためバグを見逃す（報告不足）かのいずれかだからである。さらに、既存の LLM ベースの検証アプローチは、算術およびメモリの安全性において健全性を欠くことが多く、従来の帰納的チェッカーはシステムコードの規模とループの多さに対処できず、具体的な反例を生成する能力を欠いている。

手法：エージェンティック・モデル・チェッキング

著者は、「エージェントが提案し、ソルバーが検証する」という原則の下、LLM エージェントと有界モデル・チェッキング（BMC）バックエンドを結合する検証パラダイムであるエージェンティック・モデル・チェッキングを提案する。

BMC-Agentとして具体化されたこのシステムは、LLM エージェントが意味判断を必要とするタスクを処理し、決定論的な BMC バックエンド（C 用 CBMC、Rust 用 Kani）が健全性に関連するすべての決定を処理するパイプラインを通じて動作する。

中核的なアーキテクチャのコミットメント

1. トップダウン仕様の推論:

   • エージェントは、呼び出し元の文脈からトップダウンで関数ごとの事前条件と事後条件を推論する。
   • 仕様は、バックエンドのネイティブな assume/assert プリミティブに決定論的に変換される制限されたドメイン固有言語（DSL）で生成される。
   • システムは、単なるクラッシュ回避から行動の忠実さへと検証を昇華させるため、防御的なパニックフリーチェックに加えて機能的正確性の仕様（参照等価性式、代数的恒等式など）を生成する。

2. 構成的検証:

   • 検証は関数ごとに分解される。各関数は、推論された仕様に対して孤立してチェックされる。
   • 呼び出された関数（callee）は、その事後条件によって制約されたスタブに置き換えられる。これは、callee の事後条件が呼び出し元の仮定となるアサーム・ギャランティの規律を実装する。
   • このアプローチは、プログラム全体の状態爆発を防ぎ、検証をプログラム全体ではなく、単一関数の状態空間のサイズに合わせてスケーリング可能にする。

3. 多段階の反例検証:

   • BMC 反例は即座にバグ報告として扱われるわけではない。それらは、インツリー内のアクティブなクラッシュを潜在的な失敗やモデル化のアーティファクトから区別するために、厳格な検証パイプラインを通過する。
     • 入力到達可能性: 呼び出しグラフを遡って証人入力を伝播させ、呼び出し元がその値を供給できるかどうかを判定する。
     • callee の実現可能性: 実際の callee ボディを用いて BMC を再実行し、証人が実装を通じて到達可能であることを確認する。
     • 動的再生: ホストシステムで証人を実行するハーネスをコンパイルし、シグナル（SIGSEGV、SIGABRT など）を捕捉して動的クラッシュを確認する。
     • リアリズム監査: LLM エージェントが完全な文脈（仕様、ハーネス、証人状態）をレビューし、発見を現実的か非現実的かに分類し、フレームワーク不変のアーティファクト（初期化されていないグローバル変数、不可能なハードウェア状態など）をフィルタリングする。

4. 適応的洗練ループ（仕様のレベルでの CEGAR）:

   • 反例が偽陽性（例えば、ループアンワインドのアーティファクト）として分類された場合、システムは単にそれを抑制するのではなく、LLM が事前条件の強化、callee 契約の強化、またはソルバーパラメータの調整などの洗練を提案する。
   • 健全性ガードが、これらの洗練が実際のバグを隠蔽しないことを保証する。
   • 承認された洗練は、知識ベース（仕様ストアとパターンライブラリ）に永続化され、すべての呼び出し元に伝播される。これにより、CEGAR が述語抽象から、構成的伝播を伴う仕様のレベルへと拡張される。

主要な貢献

論文は、6 つの主要な貢献を概説している。

1. エージェンティック・モデル・チェッキング・パラダイム: LLM エージェントが意味タスク（仕様推論、チェック選択、分類）を管理し、BMC バックエンドが健全性を保証するフレームワーク。これにより、LLM 生成の C および Rust コードの仕様なし検証が可能になる。
2. トップダウン仕様層: DSL を介して CBMC/Kani に変換され、関数ごとの事前/事後条件を推論し、意味的に正当化された算術チェック（オーバーフロー、ポインタチェックなど）を選択するメカニズム。
3. 構成的検証アーキテクチャ: アサーム・ギャランティ契約の下で関数を孤立してチェックし、呼び出しグラフの層全体で並列化するスケーラブルなアプローチ。
4. 検証パイプライン: 到達可能性、実現可能性、動的再生、リアリズム監査の 4 段階のプロセス。発見を「確認された動的」や「確認されたシステムエントリー」などの証拠階層に分類する。
5. 多レベル洗練ループ: 偽陽性の反例を利用して構成的な洗練を駆動し、実行間で永続化する仕様レベルへの CEGAR の昇華を行うシステム。
6. BMC-Agent の実装と評価: 多様なコーパスで評価された動作するツール。実際の欠陥を確認し、ファズされたライブラリに対して有界なクリーン検証を生成し、機能的等価性を証明する能力を実証している。

評価結果

著者は、C と Rust にまたがる 4 つのコーパスで BMC-Agent を評価した。

• VibeOS (C): 15,000 行の LLM 生成 ARM64 カーネル。BMC-Agent は 12 モジュールにわたって34 の現実的なバグを確認した。このうち 16 は動的に再現（SIGSEGV/SIGABRT）され、14 はシステムエントリーポイントとして確認され、4 は形式モデル違反であった。
• 成熟した OSS ライブラリ (C): jq、OpenSSL、libcurl、libxml2、protobuf upb を評価。ツールは jq で2 つの未定義動作の欠陥を暴露し（GHSA として提出）、重度にファズされたパーサー表面（例：OpenSSL ASN.1 の 24 個のリーフ関数のうち 15 個）で有界なクリーン検証を生成した。
• Realtek r8125 ドライバ (C): rtl8125 ツールの ioctl において、特定のオーバーフローチェックをフラグセレクタを介して有効にすることでトリガーされるCAP_NET_ADMIN によってゲートされた MMIO 境界チェックバイパスを発見した。
• claudes-c-compiler (Rust): 50,000 行の LLM 生成 C コンパイラ。BMC-Agent は25 の実際のバグを確認した。これらは主にパニッククラスの欠陥（スライス OOB、整数オーバーフロー）および 1 つの機能的正確性違反であり、公開 API のバイトヘルパーで発生した。また、ELF ハッシュおよびヘッダー書き込みヘルパーに対して有界な機能的等価性を確立した。

結果からの主要な観察:

• ツールの精度は、フレームワークのアーティファクトをフィルタリングするリアリズム段階の検出器、標準構成でデフォルトオフのチェックを有効にする関数ごとのフラグ選択、そして反復パターンを永続的な不変条件に変換するフィードバックループに起因している。
• Rust コンパイラのケースでは、バグは特定のアンチパターンに従っていた。LLM は境界チェックなしでヘルパー関数を書き、不変条件を維持するために呼び出し元に依存していた。これにより、形式化された入力では機能するが敵対的な入力では失敗するコードが生成され、これは典型的な人間が書いたコンパイラ論理エラーとは異なるプロファイルであった。

意義と主張

この論文は、エージェンティック・モデル・チェッキングが、契約の推論を自動化し、それらを健全で有界なモデル・チェッキングと結合することによって、LLM 生成システムコードにおける「仕様ギャップ」に対処すると主張している。

• 健全性対スケーラビリティ: 健全性を BMC に委譲し、意味判断にはエージェントを使用することで、純粋な LLM 推論の非健全性を回避しつつ、プログラム全体検証のスケーラビリティの限界を克服する。
• 実行可能な検証: 多段階の検証パイプラインにより、報告されたバグが単なる理論的な反例ではなく、到達可能性と動的影響によって分類され、アクティブなクラッシュと潜在的な強化タスクを区別することを保証する。
• 構成的伝播: システムが仕様を洗練し、それを呼び出しグラフ全体に伝播させる能力により、偽陽性の反例から学習し、手動介入なしに時間とともに検証の品質を向上させることができる。

著者は今後の作業については慎重であり、広範な定量的評価（スケーリングにおける精度/再現率）、仕様の正確性仮定のより深い分析、トークン最適化によるコスト削減が次のステップであることを指摘している。彼らは、現在の結果が欠陥の確認とクリーンな表面の検証におけるパイプラインの能力を実証しているが、制限なくすべての LLM 生成コードを検証するという一般的な問題を解決したとは主張していないことを強調している。