AIエージェントは形式検証済みソフトウェアを生成できるか？新ベンチマーク「Vero」が示す現状

AIエージェントによるプログラミングが普及する一方で、生成コードの正確性保証は依然として課題です。このギャップを埋めるため、実装と機械検証済み証明の同時合成をリポジトリレベルで評価する初のベンチマーク「Vero」が発表されました。Veroは実世界のマルチモジュールコードベースから43のインスタンスを収集し、AIエージェントの能力を測定。現状、最強のエージェントでも約6割の解決にとどまり、リポジトリ規模での信頼性確保にはまだ大きな隔たりがあることが示されました。