Harnessing Code Agents for Automatic Software Verification
本論文は、汎用的なLLMコードエージェントを、固定された人間設計の戦略で制約するのではなく、健全性を保証する検証ハーネスで包み込むことが、複雑なソフトウェアシステムの完全かつ全自動な形式検証を可能にし、専門家の介入なしにCoqおよびLean 4における数千の補題に対して100%の証明カバレッジを達成できることを実証するものである。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
超高層ビルを建設しようとしていると想像してください。しかし、その設計図は、世界でも一握りの専門家にしか読めないほど複雑で厳格な言語で書かれています。もし数学的な計算でたった一つの小さなミスをしただけでも、建物全体が崩壊してしまうかもしれません。これが、**形式ソフトウェア検証（formal software verification）**の世界です。これは、コンピュータコードにバグがないことを数学的に証明するプロセスです。
数十年にわたり、これはボトルネックとなってきました。ソフトウェアが完璧であることを証明することは可能ですが、それには人間の専門家による、気の遠くなるような長年の地道な作業が必要です。それは、都市のすべてのレンガを一つずつ手作業でチェックするために、建築家チームを雇うようなものです。
この論文は、「Aria」と呼ばれる新しい手法を紹介しています。コンピュータに「人間の建築家のように考える方法」を教えようとする（これは過去に失敗してきました）のではなく、著者たちは賢いコンピュータ・エージェントに「サンドボックス（砂場）」を与え、自力で解決策を見つけ出させたのです。
仕組みは以下の通りです。簡単な比喩を用いて説明します。
1. 問題点： 「専門家」というボトルネック
形式検証を、大規模で多段階の論理パズルを解くことだと考えてください。
- 従来の方法： 人間の専門家を雇います。彼らはパズルを見つめ、何時間も考え、解決策を書き留めます。
- 限界： 専門家はコストがかかり、時間がかかります。彼らは一日に数個のパズルしか解けません。
- 失敗したAIの試み： 以前のAIを用いた試みは、ロボットに厳格なチェックリストを与えるようなものでした。「ステップ1：このパーツを見る。ステップ2：この動きを試す」。ロボットはルールに従いましたが、チェックリストがあまりに硬直的であったため、行き詰まってしまいました。それは簡単なパズルしか解けなかったのです。
2. 解決策： 「コード・エージェント」と「安全ハーネス」
著者たちは異なるアプローチを試みました。AIにチェックリストを与えるのではなく、汎用プログラミング・アシスタント（「Claude Code」のような超優秀なインターン）と、厳格な安全ハーネスを与えたのです。
- エージェント（インターン）： あなたはAIにパズル全体（「補題/lemma」）を渡し、「これを解いてみて」と言います。AIはあらゆることを試す自由があります。ルールを確認し、動きを試し、失敗し、コードの別の部分を見たり、全く新しい戦略を試したりすることができます。それは人間の硬直した計画に従っているのではなく、自分自身の判断力を使っているのです。
- ハーネス（安全検査官）： これが最も重要な部分です。AIは間違いを犯すことが許されますが、システムにそれを「こっそり通す」ことはできません。
- AIが証明を書くと、「ハーネス」がそれを厳格なマシンチェッカー（「Coqカーネル」）に通します。
- 間違っていた場合： マシンは「ダメです。ステップ4が間違っています。理由はこれです」と伝えます。
- ループ： AIはそのフィードバックを聞き、間違いを修正し、再び試行します。単一のパズルに対して、最大30回までこれを繰り返すことができます。
- ルール： 証明が受理されるのは、マシンチェッカーが「はい、これは100%正しいです」と言った場合のみです。AIは嘘をつくことも、ステップを飛ばすこともできません。
3. 結果： 「不可能」なパズルを解く
著者らはこのシステムを、ソフトウェア界で最も難しい論理パズルの一つである「Iris」というライブラリでテストしました。
- 挑戦： Irisは、複雑な並行ソフトウェア（オペレーティングシステムやセキュアなライブラリなど）を検証するために使用されます。これはソフトウェア検証における「エベレスト」と見なされています。
- 成果： AIは、人間の助けなしに、**100%**のパズルを解きました。
- Irisコアライブラリ内の4,257個の複雑な補題を証明しました。
- 人気のあるプログラミング言語の安全性ルールであるRustの標準ライブラリにおいて、217個の補題を証明しました。
- 以前のAIシステムが8回中7回失敗した別のライブラリにおいても、318個のパズルを解きました。
- さらに、別のタイプの数学システム（Lean）でも動作し、これが特定のツールに限ったトリックではないことを証明しました。
4. なぜ機能するのか（「秘伝のソース」）
論文は、鍵となったのはAIをより賢くすることではなく、AIとチェッカーの関係性を変えたことだと主張しています。
- 信頼は無料： 多くのAIタスクでは、AIが「幻覚（ハルシネーション）」を起こしてデタラメを言っていないか心配する必要があります。しかし、このシステムでは「安全ハーネス」が絶対的な審判として機能します。AIが「解きました」と言っても、審判がそれをチェックします。もし間違っていれば、審判は拒絶します。AIがブラフで切り抜けることは不可能なのです。
- 硬直したルールがない： AIに（人間のステップバイステップの計画を強制するのではなく）独自の戦略を選ばせることで、AIは自身の「直感」を用いて、硬直したシステムが見逃していたショートカットや解決策を見つけ出すことができました。
5. ブラッシュアップ（磨き上げ）
時として、AIは正しいものの、乱雑な（例えば、非常に分かりにくいスタイルで書かれた数学の証明のような）解決策を見つけることがあります。システムには「ポリッシャー（磨き上げ）」エージェントが含まれており、それが乱雑な証明をクリーンでプロフェッショナルなスタイルへと書き換え、厳格なマシンチェックを通過しながらも、まるで人間の専門家が書いたかのような外観に整えます。
まとめ
この論文は、賢く自由な思考を持つAIエージェントを、厳格で一切の妥協を許さない安全ハーネスと組み合わせることで、複雑なソフトウェアにバグがないことを自動的に証明できるようになったと主張しています。それは、あらゆる方法を試すことが許された天才的でクリエイティブなインターンを雇い、同時に、完璧さ以外は一切受け付けないロボットに監視させているようなものです。その結果はどうでしょうか？ AIは、人間が自動化不可能だと言ってきた問題を含め、与えられたすべての問題を解き明かしたのです。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。