バークレーのVero基準、完答は43件中27件

バークレーのRDI研究所が、Veroと名付けた新しいベンチマークを公開した。これはAIエージェントに対し、コードベース全体という規模で二つのことを同時にこなすよう要求する。必要なAPIをすべて実装すること、そして与えられた仕様のそれぞれが成立することを証明すること。しかもコード・証明・ビルドの三者が終始一貫している必要がある。これまでの形式検証ベンチマークは単一の定理や単一の関数にとどまるものがほとんどで、リポジトリ規模のものはVeroが初めてとなる。

課題はPython、Dafny、Verus、Coqの既存コードから移植された43件のマルチモジュールLean 4プロジェクトで、合計で743個のAPIと2,705件の形式仕様をカバーする。評価は二つのモードで行われる。証明のみモードでは参照実装が与えられ、エージェントは証明だけを担当する。実装と証明モードでは、エージェント自身が実装を書いたうえで、それが仕様を満たすことを証明する必要がある。

スコアボード

90分の予算内での完全解決数(満点43):

1行目と3行目の間の落差に注目すべきだ。同じGPT-5.5、同じCodexを使いながら、推論の設定をmediumからxhighに引き上げただけで、実装と証明モードのスコアは2から27へと跳ね上がった。この種のタスクでは、推論予算を増やすことの限界的な効果はまだ全く飽和していない。

難しいのは個々の証明ではない

首位の行にはもう一組の数字が隠れている。GPT-5.5(xhigh)は実装と証明モードで個々の仕様の87.3%を、証明のみモードでは85.8%を通過する。しかし「インスタンス全体を完全にやり遂げる」という基準に切り替えた途端、その数字は27/43、25/43まで落ち込む。研究者たちの見立てははっきりしている。個々の仕様を証明すること自体はもはや難所ではなく、証明リポジトリ全体の一貫性を保つことこそが難所だというのだ。

この二つの数字の落差には、エンジニアリング上の重い意味がある。個々の仕様で87%という通過率は、数十件の仕様を持つプロジェクトでは、ほぼすべてのプロジェクトでいくつかの仕様が解けずに残ることを意味する。そして形式検証はオール・オア・ナッシングの世界だ。たった一件でも証明できない仕様が残れば、リポジトリ全体がビルドを通らず、それまで正しく証明できていた部分にも部分点は一切与えられない。これは単体テストが87%通ればリリースできるソフトウェア開発とは、まったく別の話だ。

もう一つ注目すべき細部が、証明コードの中身だ。完全に解決できた実行結果を見ると、補助定理が証明コードの中央値で73.6%を占めていた。つまりエージェントが書いたものの4分の3は、主定理を支えるためだけの足場に過ぎないということだ。この比率は、今のモデルが簡潔な証明構造を見つけ出すのではなく、補題を積み上げて力任せに押し切る幅優先的なアプローチを取っていることを示唆している。

アルゴリズムを自分で選ぶと、助かるのは5回、こじれるのは17回

実装と証明モードは、エージェントにもう一つの自由度を与える。実装を自分で書けるということは、証明しやすいアルゴリズムを自分で選べるということでもある。研究者はこの自由度が実際にもたらす純効果をペア比較で調べた。その結果、アルゴリズムを変えたことで成功に至ったケースは5件、逆に失敗の原因になったケースは17件だった。

この5対17という数字は多くを物語っている。理屈のうえでは、自分で実装を選べる自由は損にはならないはずだ。最悪でも参照実装をそのままコピーすればいい。ところが実際には、モデルはしばしば「賢い」と自分で判断した実装を選び、それが結局はるかに証明しにくいものだったために、90分間そこから抜け出せなくなっていた。コードを書けることと、どのコードなら証明しやすいかを見抜けることは別の能力であり、今のエージェントは前者しか持ち合わせていない。

ランキングにはもう一点、書き添えるべきことがある。43件のインスタンスのうち10件は、すべての構成・両モードを通じて一度も解決されなかった。これらは現行手法の硬い天井を示しており、次の研究が最も注視すべき対象でもある。

AIコーディングツールを作る人にとって、Veroの価値は順位そのものではなく、これまで経験則でしか語れなかった「リポジトリ規模の一貫性」を計測可能な指標に落とし込んだ点にある。SWE-benchのようなベンチマークが測るのは一つのバグを正しく直せるかどうかだが、Veroが測るのは一つのエンジニアリングプロジェクトの制約全体に耐えられるかどうかだ。両者の難易度は同じ土俵にない。

参考資料:バークレーRDI研究所の公式ブログ、CocoLoop。ベンチマークの規模、両モードの完全解決数、仕様単位の通過率、補助定理の比率、ペア比較の統計はいずれも公開レポートの記載に基づき確認済み。