AIはコードを書けても、リポジトリを証明し切れない。Veroが示す「87.3%の罠」
AIコーディングエージェントが、あるリポジトリの形式仕様を87.3%通過したとします。
かなり完成に近いように見えます。残りを少し直せば終わりそうです。
しかし、形式検証では最後の12.7%が残っている限り、そのリポジトリ全体について「仕様を満たす」とは証明できません。しかも残った箇所は、簡単な証明の取りこぼしではなく、複数モジュールをつなぐ共有不変条件や、何段にも重なる補助定理を必要とする難所かもしれません。
2026年8月13日に公開された論文「Vero: Can AI Agents Build Formally Verified Software Repositories?」は、この完成直前に見える失敗を、43件の複数モジュールリポジトリで測りました。
最も強い評価構成は、個別仕様の87.3%を通過しました。それでも、コードと証明を両方完成できたのは43件中27件です。さらに10件は、評価したどの構成でも完全解決できませんでした。
Veroが示したのは、AIの弱点がコード生成や一問ずつの証明だけにあるのではない、ということです。難しいのは、リポジトリ全体で使い回せる論理を組み立て、最後まで整合した成果物として完成させることでした。
テスト合格と証明完了は、同じ「通った」ではない
一般的な開発では、コードの正しさをユニットテストやレビューで確かめます。これは現実的で重要な方法ですが、テストした入力と人間が気づいた観点しか直接は確認できません。
形式検証は、実装が仕様を満たすことを機械的に証明します。たとえば「口座が存在しない状態で口座を作ると、残高0の口座が得られる」という仕様を、具体的な数例ではなく、対象となる全入力について証明します。
もちろん万能ではありません。仕様に書かなかった要件は証明されません。間違った仕様を正しく証明してしまうこともあります。それでも、仕様が捉えた範囲では、テストより強い保証を得られます。
これまでの検証付きコード生成ベンチマークには、主に二つの限界がありました。
- 一つの関数だけを実装して証明する
- 実装は与えられ、AIは証明だけを書く
実際のリポジトリでは、一つの関数を直すと別のモジュールの証明が壊れます。下位の補助関数について定理を作り、それを上位のAPIで再利用し、全体をビルドできる状態に保つ必要があります。
Veroは、この依存関係を評価単位に入れました。
43件のリポジトリで「実装と証明」を同時に測る
Veroには、Python、Dafny、Verus、Coqの実在プロジェクトを基にした43件のLean 4リポジトリがあります。対象は暗号プロトコル、分散システム、パーサー、数学アルゴリズム、データ構造などです。
全体では743個の採点対象APIと2,705個の形式仕様があります。43問の小テストではなく、数千の証明義務を含むリポジトリ群です。
評価には二つのモードがあります。
証明だけを作るモード
参照実装は固定されます。AIは、その実装が全仕様を満たす証明を書きます。
コードと証明を作るモード
AIはAPIの実装も書き、その自作コードが全仕様を満たすことを証明します。証明しやすい実装へ変えられる一方、実装変更で複数の証明を壊す危険もあります。
採点は厳格です。編集を許された領域だけを新しいベンチマークへ移し、信頼されていない公理や、証明を形だけ成立させる仕掛けを拒否します。部分点ではなく、リポジトリ内の全仕様が機械検証を通ったときだけ完全解決です。
さらに、Veroはベンチマーク側の誤りも監査できます。仕様同士が矛盾している、または参照実装が仕様を満たせない場合、AIは無理に証明を捏造するのではなく、「この条件は同時に成立しない」と形式的に証明できます。
評価問題そのものをAIに疑わせ、反証も正解として扱う。これは、難しいベンチマークほど重要な設計です。
87.3%通っても、完成は27件だった
研究チームは、Codex 0.140.0とGPT-5.5の二つの推論設定、Claude Code 2.1.191とClaude Opus 4.8、Claude Sonnet 5を評価しました。各構成を二つのモードで走らせ、1回あたりの上限は90分です。
最も強かったGPT-5.5のxhigh設定は、コードと証明のモードで43件中27件、証明だけのモードで25件を完全解決しました。
ここで注目したいのは、個別仕様の通過率です。同じ構成は、コードと証明のモードで87.3%、証明だけのモードで85.8%の仕様を通しました。
局所的には大半を解けています。それでもリポジトリ単位では、コードと証明の16件が未完了でした。研究が確認した10件は、どの構成とモードの組み合わせでも完全解決できませんでした。
これは単純な採点の厳しさではありません。
形式検証では、未証明の仕様が一つ残っただけでも、その部分に対応する保証は成立しません。コードと証明のモードでは、証明できない理由が「証明文が足りない」だけでなく、「自分で書いた実装が仕様に違反している」可能性もあります。
小さな成功率を積み上げても、全体完成率にはならない。Veroは、エージェント評価で見落とされやすい集約の罠を可視化しました。
完成したリポジトリには、共有する補助定理があった
では、最後まで完成した実行は何が違ったのでしょうか。
82件の完全解決を調べると、AIが書いた補助定理は、コードと証明のモードで証明行の中央値73.6%、証明だけのモードで71.6%を占めました。
補助定理は、一つの問題だけを閉じる使い捨てではありません。82件中80件では、同じ補助定理が少なくとも二つの仕様で共有され、65件では少なくとも五つの仕様で共有されていました。
つまり、完成したAIは2,705個の仕様を独立した小問として処理したのではありません。下位の性質を定理としてまとめ、上位の証明から再利用できる「論理のライブラリ」を作っていました。
依存の深さも効きます。補助定理を必要としない仕様は、他の実行でも83.9%または80.1%通りました。ところが補助定理の連鎖が4段以上になると、通過率は50.6%または39.1%まで下がります。
AIが苦手だったのは、ファイルをまたぐこと自体ではありません。必要な不変条件を見つけ、段階的な補助定理へ分解し、後続の証明で再利用することでした。
実装を早く固定し、証明だけを増やし続ける
もう一つ興味深い行動があります。
各構成は、実行時間の前半で実装量をほぼ固定しました。その後も証明文は増え続けましたが、実装へ戻って構造を変える動きは少なかったのです。
証明が難しいとき、二つの方針があります。
- 現在の実装を固定し、より強い補助定理を探す
- 同じ仕様を満たしながら、証明しやすい実装へ組み替える
Veroでは、最も強い構成が一部のリポジトリで参照アルゴリズムを単純な実装へ置き換え、証明を完成させました。5組の事例では、自作実装に対して250個の仕様をすべて閉じましたが、固定された参照実装への証明では201個にとどまりました。
これは手抜きではありません。仕様を満たす別の実装を選び、効率と引き換えに証明可能性を上げた結果です。
一方、多くの未完了実行は実装を足場として固定し、期限まで証明を追加し続けました。残り時間を増やすだけではなく、証明対象のコード自体を見直す戦略が必要だったと考えられます。
実務では「局所合格」と「全体完成」を分けて測る
ここからは、論文結果を基にしたAICompanyの実務的な解釈です。
すべての開発でLeanを導入する必要はありません。Veroの教訓は、もっと一般化できます。
AIエージェントへ大きな変更を任せるとき、ファイル単位のテスト合格数や、個別タスクの成功率だけを完成指標にしないことです。
たとえば、次の二層で確認できます。
局所ゲート
- 変更した関数のテストが通る
- 型検査と静的解析が通る
- 個別の受入条件を満たす
リポジトリゲート
- 全体ビルドが再現できる
- 共有する前提と不変条件が一貫している
- 複数モジュールをまたぐ回帰テストが通る
- 未解決項目と暫定処理がゼロである
- 成果物が指定場所に揃い、別環境から検証できる
局所ゲートを90%通過しても、リポジトリゲートが落ちれば出荷可能な成果物ではありません。逆に、全体ゲートが落ちた理由を共有不変条件、実装構造、検証環境のどこに置くかで、次の修正方針が変わります。
証明やテストが行き詰まったら、同じ修正を繰り返すだけでなく、実装を証明しやすい形へ変える選択肢も残します。Veroの結果は、エージェントへ「テストを通せ」だけでなく、「必要なら設計へ戻れ」と指示する価値を示しています。
小さく試すなら、一つの仕様を二つの実装で証明する
Veroの全評価を再現するには、Leanの環境、複数モデル、344回のエージェント実行が必要です。個人が同じ規模で試すのは重い作業です。
ただし、中心的な考え方は小さく試せます。
たとえば、重複を除いた昇順リストを返す関数を考えます。仕様を次の三つに分けます。
- 出力は昇順である
- 出力に重複がない
- 入力に存在した要素は、出力にも存在する
次に、同じ仕様へ二つの実装を用意します。
- 状態を細かく更新する独自アルゴリズム
- 標準ライブラリの整列と重複除去を組み合わせた実装
コードの短さや実行速度だけでなく、必要な補助定理の数、依存の深さ、証明全体の再利用性を比べます。証明に詰まったら、証明文だけを足す前に、実装の構造を変えた方が全体が単純になるか確認します。
これはVeroの数値を再現する実験ではありません。論文が示した「実装選択と証明可能性の相互作用」を、自分の開発環境で観察するための思考実験です。
この研究だけでは分からないこと
Veroは強いベンチマークですが、結果の範囲は明確に区切る必要があります。
第一に、すべての評価対象はLean 4です。元のプロジェクトがPython、Dafny、Verus、Coqでも、評価用にはLeanへ翻訳されています。
第二に、ほどよい規模のLean構造へ移しやすいコードが中心です。並行処理や時間的性質を持つプロトコルは、ほとんど含まれません。
第三に、新しく完成させる形式の課題です。既存の巨大な本番リポジトリへ小さな変更を加え、古い保証を壊さず保守する能力は別の評価が必要です。
第四に、評価環境はCodex 0.140.0とGPT-5.5、Claude Code 2.1.191とClaude Opus 4.8またはClaude Sonnet 5です。別バージョン、別モデル、別の時間上限では結果が変わります。
第五に、費用データの多くは推定です。時間切れになった実行が最終利用量を出す前に停止したため、中央値の1分あたり費用から補完されています。
第六に、形式証明は仕様より強くなりません。仕様が安全上の条件を欠いていれば、その条件は証明されません。
公開リポジトリにはベンチマーク、評価ハーネス、テスト、上流コミットの固定情報があります。一方、公開直後の時点で見えるコミットは一つです。AICompanyは344回の評価を独立再実行していません。
最後の1件を閉じる能力が、完成度を決める
Veroの数字は、AIコーディングエージェントが弱いという単純な話ではありません。最も強い構成は、43件中27件でコードと証明を同時に完成させました。形式検証付きリポジトリをここまで自動で進められること自体、大きな前進です。
ただし、87.3%という局所通過率は、完成保証ではありませんでした。
実務で価値を持つのは、簡単な項目を大量に通す能力だけではありません。残った難所に共通する不変条件を見つけ、補助定理や共通テストへ変え、必要なら実装へ戻り、全体を一つの検証可能な成果物として閉じる能力です。
AIエージェントの評価は「何個できたか」から「全体を完成させたか」へ進む必要があります。
最後の1件を閉じられない95点と、依存関係を整理して完成した100点は、出荷の場面では別物です。Veroは、その差を機械検証で測るための基準を公開しました。
参考資料
※本記事は論文と公式リポジトリの一次情報を基に、AICompanyが実務への適用方法を独自に整理したものです。AICompanyは論文の全評価を独立再現していません。