arXiv cs.LG、AIエージェント向け検証済みSW構築の新ベンチマーク「Vero」発表
arXiv cs.LGは2026年8月13日(現地時間)、AIエージェントが形式的に検証されたソフトウェアリポジトリを構築できるかを評価する初のベンチマーク「Vero (ベロ)」を導入したと発表した。Veroは、実世界のマルチモジュールコードベースにおける実装と証明の一貫した選択能力を問うもので、既存の評価手法の課題解決を目指す。本ベンチマークには、Python、Dafny (ダフニー)、Verus (ヴェルス)、Coq (コック) などの多様な言語で構成された43のマルチモジュールインスタンスが含まれる。最先端のAIエージェントでも、43インスタンス中27インスタンスしか完全に解決できなかったと報告されている。