arXiv cs.LGは2026年8月13日(現地時間)、AIエージェントが形式的に検証されたソフトウェアリポジトリを構築できるかを評価する初のベンチマーク「Vero (ベロ)」を導入したと発表した。Veroは、実世界のマルチモジュールコードベースにおける実装と証明の一貫した選択能力を問うもので、既存の評価手法の課題解決を目指す。本ベンチマークには、Python、Dafny (ダフニー)、Verus (ヴェルス)、Coq (コック) などの多様な言語で構成された43のマルチモジュールインスタンスが含まれる。最先端のAIエージェントでも、43インスタンス中27インスタンスしか完全に解決できなかったと報告されている。
AIエージェントはプログラミング用途での活用が進むものの、生成されたコードの正確性については保証を提供しない点が課題とされてきた。これに対し、エージェントが実装と同時にその仕様の機械検証済み証明を生成する「検証済みコード生成」は、信頼性の高いAI生成ソフトウェアへのより堅固な経路を提供する。しかし、既存のベンチマークは個別の関数に焦点を当てるか、提供された実装に対する証明生成のみを評価していたという。
Veroは、リポジトリレベルでの実装と証明の統合合成を評価する初のベンチマークである。本ベンチマークには、実世界のPython、Dafny、Verus、Coqなどのリポジトリから選定された43のマルチモジュールインスタンスが含まれており、暗号プロトコルから分散システムまで多様なドメインをカバーしている。各インスタンスは、事前に決定されたAPIインターフェース、手作業でキュレーションされた形式仕様、参照実装を持つマルチモジュールのLean 4リポジトリで構成され、「proof-only」と「code-and-proof」の両評価モードをサポートする。
ベンチマークの信頼性向上を目的として、Veroには監査メカニズムも搭載されている。これにより、エージェントが提供された仕様の充足不能性や参照コードの不正確さを形式的に証明でき、キュレーション中に潜在的なコードおよび仕様のエラーを発見・修正することが可能になる。著者らがLeanツールチェーンにアクセスできる最先端のコーディングエージェント構成を評価したところ、最も強力なエージェントでも43インスタンス中27インスタンスしか完全には解決できなかったと報告されている。さらに、最も困難なリポジトリでは、仕様を一つも完了できなかった。Veroは、リポジトリ規模の検証済みソフトウェア合成に向けた進捗を測定するための具体的なテストベッドを提供するもので、現行のエージェントはその目標にはまだ達していないという見方が示された。
参考: arXiv cs.LG (アーカイブ) — 2026年8月14日 02:41 (JST)
原文ハイライト"Vero: Can AI Agents Build Formally Verified Software Repositories?"