コードを書きながら正しさも証明せよと言われ、最強のエージェントは43問中27問——難問は0
ドーン・ソン氏らのチームは8月13日、arXivでVeroを公開した。リポジトリ規模の検証付きコード合成のための初のベンチマークだとされる。Veroはエージェントにテストを通る関数を求めるのではなく、複数モジュールにまたがるコードベース上で動く実装と、その実装が形式仕様に一致することを機械的に検査できる証明の両方を求める。実際のリポジトリから構築された43件の課題を含み、Lean 4、Dafny、Verus、Coqといった証明・プログラミング言語と、暗号プロトコルから分散システムまでの領域にわたる。著者らが試した最も強力なエージェント構成は43件中27件を完全に解いたが、最難関のリポジトリでは仕様を一つも閉じられなかった。
なぜ重要かエージェントがソフトウェアを書くという主張のほとんどは「テストが通ること」に依拠している。だがテストは、誰かが書こうと思いついた場合しか覆わない。機械検査による証明は、モデルがどれだけ賢そうに聞こえたかを一切問わない唯一の証拠だ——証明は通るか通らないかのどちらかである。リポジトリ全体という規模でこの基準に照らしてエージェントを測ったのは今回が初めてで、答えは「易しい三分の二は越えるが、難しい三分の一には手が届かない」だった。コーディングエージェントが次に「信頼できる」と紹介されたとき、覚えておくと役に立つ数字である。
アプリで読む——無料・9言語
関連ニュース
機械学習が病んだ脳細胞の形を読み、それを落ち着かせる既承認薬を九つ選び出した2026-08-21噂：コーディングのベンチマークを無料で制した匿名モデルは、智譜（Zhipu）の未発表フラッグシップだとされる
2026-08-21ディープシークの安価な主力モデルが「見る」ようになった——視覚を要するエージェント課題でアンソロピック最上位に迫ると主張
2026-08-21エヌビディアが競合の「モデル製造装置」に60億ドル、動かしていた109人も採用
2026-08-21AIの訓練方法を改善するために4時間とGPUを1枚与えたところ、最良のエージェントは1点満点で0.25。そして大半は試みすらしなかった
2026-08-21