コードを書きながら正しさも証明せよと言われ、最強のエージェントは43問中27問——難問は0
ドーン・ソン氏らのチームは8月13日、arXivでVeroを公開した。リポジトリ規模の検証付きコード合成のための初のベンチマークだとされる。Veroはエージェントにテストを通る関数を求めるのではなく、複数モジュールにまたがるコードベース上で動く実装と、その実装が形式仕様に一致することを機械的に検査できる証明の両方を求める。実際のリポジトリから構築された43件の課題を含み、Lean 4、Dafny、Verus、Coqといった証明・プログラミング言語と、暗号プロトコルから分散システムまでの領域にわたる。著者らが試した最も強力なエージェント構成は43件中27件を完全に解いたが、最難関のリポジトリでは仕様を一つも閉じられなかった。
なぜ重要かエージェントがソフトウェアを書くという主張のほとんどは「テストが通ること」に依拠している。だがテストは、誰かが書こうと思いついた場合しか覆わない。機械検査による証明は、モデルがどれだけ賢そうに聞こえたかを一切問わない唯一の証拠だ——証明は通るか通らないかのどちらかである。リポジトリ全体という規模でこの基準に照らしてエージェントを測ったのは今回が初めてで、答えは「易しい三分の二は越えるが、難しい三分の一には手が届かない」だった。コーディングエージェントが次に「信頼できる」と紹介されたとき、覚えておくと役に立つ数字である。
アプリで読む——無料・9言語
関連ニュース
すべてのAIを訓練する方法を使わずに、モデルが学びました。2026-10-06TikTokが見ている動画の中に買い物ボットを入れました。
2026-10-06Reflectionが5010億パラメータのモデルを無料で配ります。
2026-10-06ウィキメディアがOpenAIのエージェントを5月の障害で疑っています。
2026-10-06メタの助手はあなたの周りの全員を一時間ごとに記録しています。
2026-10-05