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

AIエージェントによるコード生成の現状と課題

AIエージェントがプログラミングに活用される機会は急速に増えています。しかし、生成されるコードの正確性については、いまだに保証がありません。この問題は、AIが生成するソフトウェアの信頼性を確保する上で、極めて重要な課題として認識されています。実装と同時に、その仕様の機械検証済み証明も生成する「形式検証済みコード生成」は、信頼性の高いAI生成ソフトウェアを実現するための強力なアプローチです。

これまでのベンチマークは、個々の関数に焦点を当てるか、または実装が提供された上での証明生成のみを評価するものが主流でした。実際のマルチモジュールコードベースにおいて、AIエージェントが実装と証明の選択を一貫して行えるか、という点は未解決の疑問として残されていたのです。

新ベンチマーク「Vero」の登場

このギャップを埋めるため、私たちは「Vero」を導入しました。Veroは、リポジトリレベルでの実装と証明の同時合成を評価する初のベンチマークです。Python、Dafny、Verus、Coqなど、実世界の多様なリポジトリから抽出された43のマルチモジュールインスタンスが含まれています。暗号プロトコルから分散システムまで、幅広いドメインをカバーしています。

各インスタンスは、所定のAPIインターフェース、手動で厳選された形式仕様、および参照実装を持つマルチモジュールのLean 4リポジトリで構成されています。これにより、証明のみの評価モードと、コードと証明の両方を評価するモードの両方をサポートしています。さらに、ベンチマークの信頼性を向上させるため、Veroには監査メカニズムも組み込まれています。エージェントは、提供された仕様の不満足性や参照コードの誤りを形式的に証明することが許されており、これによりキュレーション中に潜在的なコードや仕様のエラーが表面化し、修正されます。

現状のAIエージェントの能力と限界

私たちは、Leanツールチェーンにアクセスできる最先端のコーディングエージェント構成を評価しました。その結果、最も強力なエージェントでも、43インスタンス中27インスタンスしか完全に解決できませんでした。特に難易度の高いリポジトリでは、仕様を一つも閉じることができていません。これは、現在のAIエージェントが、リポジトリ規模での検証済みソフトウェア合成という目標に対して、まだ大きく及ばないことを具体的に示しています。

Veroは、リポジトリ規模での検証済みソフトウェア合成に向けた進捗を測定するための具体的なテストベッドを提供します。現在のエージェントはまだその目標に到達していませんが、このベンチマークを通じて、今後の研究開発が加速されることを期待しています。

私の見方：形式検証がAI生成コードの信頼性を高める

AIがコードを生成する時代において、形式検証はソフトウェアの信頼性を確保する上で不可欠だと私は考えます。単に「動く」だけでなく、そのコードが意図した通りに動作することを数学的に証明するプロセスは、バグや脆弱性を未然に防ぎ、開発コストを大幅に削減します。Veroのようなベンチマークの登場は、この分野の研究開発を加速させる重要な一歩です。現在のエージェントの限界が明確になったことで、私たちは次に何をすべきか、具体的な方向性を見出すことができます。この一次情報をもとに、私自身もAI生成コードの形式検証への取り組みをさらに強化していきます。