FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning

本論文は、大規模システムにおける形式手法の適用を可能にする「FM-Agent」を提案し、LLM を活用して自然言語仕様に基づく構成論的推論と自動テスト生成を実現することで、開発者が検証済みの大規模コードからも多数の深刻なバグを発見できることを示しています。

要約

🏗️ 1. 背景：AI が作った「巨大な城」の欠陥

最近、AI（大規模言語モデル）が人間に代わって、数万行にも及ぶ巨大なソフトウェア（コンパイラやオペレーティングシステムなど）を自動で作る時代が来ました。
しかし、AI は時々「幻覚（ハルシネーション）」を起こし、バグ（欠陥）を含んだコードを書いてしまいます。

【問題点】
巨大な城（システム）を建設する際、従来の検査方法には限界がありました。

• 人間が仕様書を書くのは無理: 城の隅々まで正確な「設計図（仕様書）」を人間が手書きするのは、あまりに時間がかかりすぎます。
• AI が作ったコードは理解しにくい: 自分が書いたコードでもないのに、AI が作ったコードの「意図」を理解して仕様書を書くのは、人間にとってさらに困難です。
• バグの特定が難しい: 「ここが間違っている」と言われても、「なぜ間違っているのか」がわからないと、修理できません。

🕵️‍♂️ 2. FM-Agent の登場：「上からの視点」でチェックする探偵

この論文が提案するFM-Agentは、AI 自身を使って、この巨大なシステムのバグを自動で見つけ出す「探偵」です。

🔑 3 つの重要なアイデア（魔法の杖）

この探偵は、従来の方法とは違う 3 つの「魔法」を使います。

① 「上からの視点」で仕様書を作る（トップダウン方式）

• 従来の方法（ボトムアップ）: 「この小さな部品（関数）がどう動くか」を見て仕様書を作る。→ 欠点: 部品自体にバグがあれば、仕様書も間違った方向に進んでしまう。
• FM-Agent の方法: 「この部品は、上の親（呼び出し元）から見てどう動くべきか」を考えます。
  • 例え話: 料理人が「卵を割る」という作業をします。もし卵にヒビが入っていても、料理人は「卵を割る」という目的を忘れないでください。FM-Agent は、その「目的（親からの期待）」を AI に読み取らせ、バグのある実装に惑わされない仕様書を作ります。

② 自然言語で「論理」を解く

• 従来の方法: 仕様書は「数式」や「特殊な記号」で書かれなければなりません。
• FM-Agent の方法: 仕様書を**「普通の言葉（自然言語）」**で書きます。
  • 例え話: 「もし入力が空っぽなら、エラーを返す」という指示を、数式ではなく「もし中身がなければ、怒って帰る」という言葉で AI に理解させます。AI は言葉もコードも理解できるので、この「言葉で考える論理」が得意なのです。

③ 「バグの証拠」を自動で作り出す

• 従来の方法: 「ここがバグかもしれない」と言われても、実際に再現できないと信じてもらえません。
• FM-Agent の方法: 「バグがあるかもしれない」と判断したら、「そのバグを誘発させるためのテスト（実験）」を自動で作ります。
  • 例え話: 「この橋は危ないかもしれない」と言われたら、FM-Agent は「じゃあ、この重りを乗せてみよっか」と実際に実験し、橋が崩れるかどうかを確認します。崩れれば「バグ発見！」と確実な報告ができます。

🚀 3. 実際の成果：巨大なシステムを 2 日でチェック

このシステムを使って、実際に 4 つの巨大なプロジェクト（最大で 14 万行のコード）を 2 日間でチェックしました。

• 対象: AI が作った C 言語のコンパイラ、OS、データベースなど。
• 結果: 開発者がすでにテスト済みだったにもかかわらず、522 個の新しいバグを発見しました！
• バグの例:
  • コンパイラが正しいコードを誤って拒否してしまう。
  • OS がメモリを壊してクラッシュする。
  • データベースが間違った答えを返す。

これらは、単なる「小さなミス」ではなく、システム全体を止めてしまう深刻な問題ばかりでした。

🌟 まとめ：なぜこれがすごいのか？

FM-Agent は、**「AI が作ったコードを、AI が『意図』を汲み取りながら、言葉で論理的にチェックし、実際に実験してバグを証明する」**という、これまでにないアプローチを実現しました。

• 人間の手間を減らす: 仕様書を人間が書く必要がありません。
• スケールする: 巨大なシステムでも、並列処理で短期間にチェックできます。
• 実用的: 「バグがあるかも」だけでなく、「実際にこうすればバグが出る」という証拠まで提示します。

これは、AI が作るソフトウェアの品質を担保し、私たちが安心して AI 開発されたシステムを使えるようになるための、重要な第一歩と言えます。

技術概要

FM-Agent: 大規模システム向け形式手法の拡張

LLM ベースのホアスタイル推論による自動検証フレームワーク

本論文は、大規模システム（最大 14 万行のコード）における自動的な構成的検証（compositional reasoning）を実現する初のフレームワーク「FM-Agent」を提案しています。LLM（大規模言語モデル）を活用し、自然言語仕様に基づいたホア論理（Hoare Logic）の推論を行うことで、LLM によって生成されたコードや大規模システムに含まれるバグを効率的に発見します。

以下に、問題定義、手法、主要な貢献、評価結果、および意義について詳細をまとめます。

---

1. 背景と課題 (Problem)

LLM を支援としたソフトウェア開発は急速に普及しており、コンパイラなど 10 万行を超える大規模システムを自動生成できるようになりました。しかし、LLM のハルシネーション（幻覚）により生成されたコードにはバグが含まれる可能性が高く、その正しさを検証することが急務です。

既存の自動検証技術には以下の課題があります：

• スケーラビリティの欠如: 複雑な制御フローや状態操作、深い関数間依存関係を持つ大規模システムでは、既存の自動推論技術は拡張性に欠けます。
• 仕様の作成コスト: 構成的検証の基礎となるホア論理は、各関数に対して形式仕様（前条件・後条件）を定義する必要があります。これには専門知識と多大な人的コストが伴います。
• LLM 生成コードの特性: LLM が生成したコードの場合、開発者が関数の意図を深く理解していないため、正確な仕様を手動で記述することが困難です。また、既存の手法が実装コードから仕様を導出する場合、実装自体にバグがあると、そのバグが仕様にも反映されてしまい、検証が失敗します。

2. 提案手法：FM-Agent (Methodology)

FM-Agent は、LLM を活用して関数レベルの仕様を自動生成し、ホア論理の推論規則を自然言語に拡張して適用する 3 つの主要コンポーネントで構成されます。

2.1 主要な洞察 (Key Insights)

1. 呼び出し元からの期待動作の把握: 関数の実装（バグを含む可能性あり）ではなく、その関数を呼び出す側（Caller）の実装や意図から、関数が「どうあるべきか（期待動作）」を推測する。
2. 自然言語推論の精度: LLM は小さなコードブロックの実行結果を高精度に予測できるため、形式式ではなく自然言語の仕様に対してもホアスタイルの推論が可能である。
3. システム入力と内部動作の相関: システム全体の入力と内部関数の振る舞いの相関を LLM が捉えることで、バグをトリガーするシステムレベルのテストケースを生成できる。

2.2 アーキテクチャとワークフロー

FM-Agent は以下の 3 つのステップで動作します。

1. 仕様生成器 (Specification Generator)

   • トップダウン・パラダイム: 従来のボトムアップ（実装から仕様を導出）ではなく、エントリーポイント（システム入口）から開始し、呼び出し元（Caller）の意図に基づいて被呼び出し関数（Callee）の仕様を生成します。
   • 期待仕様 (Expected Specification): 呼び出し元がcalleeに求める前条件と後条件を自然言語で定義します。複数の呼び出し元がある場合は、それらを統合して包括的な仕様を生成します。
   • 並列処理: 関数呼び出しグラフを解析し、依存関係のない関数群（レイヤー）を特定することで、複数の関数仕様の生成を並列に行い、スケーラビリティを確保します。

2. コード推論器 (Code Reasoner)

   • 自然言語ホア論理: 生成された自然言語仕様（前条件・後条件）に対して、LLM を用いてホア論理の推論規則を拡張適用します。
   • 構成的検証: 各関数の実装が仕様に合致しているか、関数ごとに独立して検証します。関数内のステートメントごとに、前条件から後条件を推論し、最終的な戻り値が仕様を満たすかを確認します。
   • ループ処理: ループ不変条件（Loop Invariant）の生成よりも、まずループ後の後条件を推測し、それを検証するアプローチを採用しています。

3. バグ検証器 (Bug Validator)

   • テストケース生成: 推論器がバグの可能性を特定した場合、LLM を用いてそのバグをトリガーするシステムレベルのテストケースを自動生成します。
   • 実行と確認: 生成されたテストケースを実行し、クラッシュや誤った出力が発生するかを確認します。一定回数（N 回）試行してもバグが再現しない場合は、ハルシネーションによる誤検知とみなして除外します。

3. 主要な貢献 (Key Contributions)

• 初の大規模システム向け自動構成的検証フレームワーク: 14 万行規模のシステムを対象に、完全自動化された構成的検証を実現しました。
• トップダウンな仕様生成: 実装のバグに惑わされず、開発者の意図（呼び出し元の文脈）を反映した仕様を自動生成する新しいパラダイムを提案しました。
• 自然言語に基づくホア推論: 形式仕様記述言語に依存せず、自然言語の仕様に対して LLM を用いて推論を行う手法を確立しました。
• システムレベルのバグ特定: 関数単位のテストではなく、システム入力からバグを再現するテストケースを生成し、バグの根本原因を明確にします。

4. 評価結果 (Results)

4 つの異なるドメイン（コンパイラ、機械学習フレームワーク、OS、データベース）で、LLM によって自動生成された大規模システム（合計 27.7 万行、8,549 関数）に対して評価を行いました。

• 発見されたバグ数: 開発者が既にユニットテストや差分チェック、マルチエージェントレビューなどを実施していたシステムにおいて、522 個の新たなバグを発見しました。
  • CCC (C コンパイラ): 339 個（IR レベルの誤生成、ランタイム出力の誤り、コンパイルクラッシュなど）
  • VibeTensor (ML フレームワーク): 141 個（誤ったテンソル値、メモリリーク、クラッシュなど）
  • VibeOS (OS カーネル): 23 個（メモリ破損、無限ループ、PID カウンタの誤動作など）
  • Bespoke OLAP (SQL エンジン): 19 個（クエリ結果の誤り、プロセスクラッシュなど）
• スケーラビリティ: 最大 14.3 万行のシステム（CCC）を含む全システムについて、約 2 日間で検証を完了しました。
• アブレーション研究: トップダウン手法やホアスタイル推論を除去した場合、発見できるバグ数は大幅に減少（CCC で 339 個→57 個）し、提案手法の有効性が確認されました。

5. 意義と将来展望 (Significance)

• LLM 生成コードの品質保証: 開発者がコードを深く理解していない状況でも、LLM 自身が「意図」と「実装」の不一致を検出できるため、LLM エージェントによる開発の信頼性を高める重要な手段となります。
• 形式手法の実用化: 従来の形式検証は手動仕様記述の重荷により大規模システムに適用されていませんでした。FM-Agent はこのボトルネックを解消し、形式手法を大規模システムに拡張する道を開きました。
• 既存ツールとの共存: FM-Agent は完全な健全性（Soundness）を保証するものではなく、既存の形式検証ツールを代替するものではありません。しかし、大規模システムにおけるバグ発見に特化した実用的なアプローチとして、既存の検証手法を補完する役割を果たします。
• 将来の方向性: 並行プログラムの検証（Rely-Guarantee 論理など）への拡張や、LLM 自体の出力に対する推論への応用などが期待されます。

結論として、FM-Agent は、LLM 時代における大規模ソフトウェアの信頼性向上に向けた画期的なアプローチであり、自然言語と形式手法を融合させることで、これまで困難だった大規模システムの自動検証を可能にしました。