AIがコードの「正しさ」まで証明する時代へ

AIがコードを書けるようになって久しいが、「生成されたコードが本当に正しいか」という問いに対して、これまでの評価は実質的に「テストを通過するか」に依存していた。テストは書いた人間の想像力の範囲でしか動かない。想定外のケースに対して正しく動くかどうかは、テストだけでは保証できない。

Microsoftが発表したAxDafnyが取り組んでいるのは、その先の問いだ。Dafnyは、コードの正しさを数学的に検証できるプログラミング言語で、「このコードはあらゆるケースで仕様を満たす」という証明を形式的に生成することができる。AxDafnyは、AIがそのコードと証明の両方を自動生成するフレームワークとして設計されている。

発表内容によると、検証失敗が起きたときにAIが反復的に修正を繰り返す「検証誘導型の修復ループ」が核になっている。不変条件、アサーション、終了引数（無限ループにならないことの証明）まで含めて自動生成し、検証器のフィードバックをもとにAIが自律的に修正を重ねる仕組みだ。

AxDafnyがDafnyBenchというベンチマークで達成した検証成功率は92.7%。従来の最高水準を6.5ポイント上回る。また、研究チームが新たに作成した「LCB-Pro-Dafny」という250問のベンチマーク（競技プログラミングの問題を形式仕様付きでDafnyに変換したもの）でも、ベースラインのGPT-4.5を大きく超えた。

注目したいのは、論文が「検証成功と実行時テスト通過は、異なる側面を測定している」と明確に主張している点だ。これは見逃せない視点の転換で、AIコード生成の評価が今後「テストを通るか」と「正しいことが証明されるか」の2軸で語られるようになる転換点として、記録しておく価値がある。

AIエージェントの信頼性という文脈でいえば、AIエージェント同士の「信頼」は今まだ幻想だったでも触れたように、AIが生成した成果物をどう信頼するかは業界全体の課題になりつつある。コード生成はその最前線にある。

実務の観点では「自分のプロジェクトに今すぐ使えるか」という問いより先に、「AIが書いたコードの信頼性をどういう基準で判断するか」という問いを持っておくことの方が今は重要だ。

形式検証という概念自体は新しくない。航空・宇宙・金融インフラなど、バグが人命や大規模損失に直結する領域では以前から使われてきた技術だ。ただし、専門的な訓練と多大な工数が必要だったため、一般的なソフトウェア開発の現場には広がりにくかった。

AxDafnyのアプローチが意味を持つとすれば、その「書くのが難しい証明」をAIに任せられる可能性が出てきた点にある。形式仕様さえ定義できれば、証明の自動生成・修復を繰り返してくれる。

一方で、現実的な制約もある。Dafnyは普及度の低い言語であり、形式仕様を正しく書けること自体が一定の専門性を要する。LCB-Pro-Dafnyのベンチマーク問題は競技プログラミング由来のため、仕様が明確に定義しやすい問題に限られている。業務システムのような「仕様そのものが曖昧」な状況での適用はまだ遠い。

短期の実務インパクトは限定的だが、「AIが生成したコードの正しさをどう担保するか」という問題設定が、これから数年で主要なテーマになる可能性は高い。複数AIを束ねても限界がある、その理由が判明でも見えてきたように、AIを組み合わせる複雑なシステムほど、個々の部品の信頼性が問われるようになる。