Vero、コーディングエージェントをLean 4リポジトリ全体へ拡張—最強構成でも完全解決は27/43問

Veroは「検証付きコード生成」を単一関数からリポジトリ全体へ拡張した。43件のLean 4プロジェクトはPython、Dafny、Verus、Coqのライブラリを基にしており、合計743個の未実装APIと2,705件の形式仕様を含む。対象分野は暗号プロトコル、コンセンサスシステム、パーサー、データ構造にまたがる。各課題ではデータ型、APIインターフェース、仕様が固定されている。エージェントは実装を補完し、さらにすべての仕様についてLeanカーネルで検査可能な証明を生成しなければならない。

評価はproof-onlyとcode-and-proofに分かれる。前者では参照実装が提供される一方、後者ではエージェントによるアルゴリズムの書き換えが認められる。そのため、帰納法を適用しやすい実装を選べる可能性がある一方で、モジュール横断の証明を壊す可能性もある。公理の追加や課題の改変による抜け道を防ぐため、採点システムは指定領域の変更のみを抽出し、クリーンなコピー上でプロジェクトを再ビルドしたうえで、証明が依存する公理を検査する。このベンチマークでは、「仕様が充足不能」または「参照実装が誤っている」ことを示す形式的な反証も受け入れ、データの欠陥がモデルの失敗として数えられないようにしている。

著者らはCodexとClaude Codeを4つの最先端モデル構成と組み合わせて評価した。最良だったGPT-5.5 xhighは、code-and-proofモードで43問中27問を完全に解決したが、10問は両モードのいずれでも、どの構成も解決できなかった。失敗は、モジュール横断の不変条件、プロトコルの整合性、独自の数学理論に集中していた。エージェントは再利用可能な補題ライブラリを先に構築せず、個々の局所的な証明を順番に試す傾向があった。

この点でVeroは、一般的な「テストに合格するか」という評価よりも、安全性が重要なソフトウェアの検証作業に近い。ただし、日常的なソフトウェア開発能力を直接示すものではない。データセットは人手で移植された43件のプロジェクトに限られ、結果はエージェント用ツール、推論予算、Leanの習熟度にも左右される。今後は、異なるチームがランキングを再現できるか、またエージェントが探索時間を延ばすだけでなく、ファイル横断の補題を主体的に計画できるかを検証する必要がある。