AIが書いたアプリのミスを数学的に証明、マイクロソフトが新技術発表

米Microsoft Researchは2026年11月5日、AIエージェントが作成したソフトウェアの正しさを数学的に証明する開発手法「プルーフ・ドリブン・ディベロップメント（PDD）」と、その支援ツール「PDD Kit」を発表した。AIが一度に数万行から数十万行ものコードを生成するなか、人間がすべての行を目視で確認する従来の手法は限界を迎えている。PDD Kitは、開発者の意図を厳密な仕様へ変換し、AIが生成したコードがあらゆる入力に対してその仕様を満たすかどうかを自動で検証する。

AIによるコード生成の急増とテストの限界

開発現場では、AIエージェントに設計方針を伝えて実装を任せる手法が広がっている。しかし実際には、AIが指示と微妙に異なるコードを書き、その誤った実装に合わせて通ってしまう独自のテストを大量に作成する問題が起きていた。テストの合格数が多く一見正常に見えても、テストで実行される動作はプログラム全体のごく一部にすぎず、稼働後に予期せぬ不具合が露呈するリスクを抱えていた。

こうした課題に対し、PDD Kitは数学的な証明を用いる。かつて形式検証などの証明手法は専門知識や特殊な言語、膨大な時間を要するため一般的なソフトウェア開発には導入が困難だった。だが、近年のAI技術の進展によって厳密な仕様の記述や証明の生成が実用レベルに達したことを受け、日常的なアプリ開発への適用を目指して開発された。

意図の聞き取りから数学的証明までを自動化

PDD Kitは、米GitHub Nextが手掛ける共同計画環境「Chopin」上で動作する。開発者が自然言語で要望を入力すると、PDD Kitが解釈の曖昧な箇所について質問を投げかけ、開発者の意図を整理した文書を作成する。この内容をもとに、検証可能な部分は「Verus」向けの厳密な仕様へ変換され、仕様を満たす証明が自動生成される。Verusは、Microsoft Researchやカーネギーメロン大学などの複数研究機関が共同開発したRust言語向けの検証器である。

一方で、暗号処理ライブラリやユーザー画面など、証明が及ばない外部要素については従来の自動テストで補完する。安全性を仮定して証明の土台とする「信頼できる計算基盤（TCB）」の境界を明確にし、開発者に個別の承認を求める仕組みを備えている。

5,000行のWebアプリで不具合ゼロを実証

研究チームは本手法の実用性を確かめるため、Rustで記述された約5,000行のフルスタックWebアプリ「Pet Store」を構築し、ログイン処理の検証実験を実施した。開発者がChopin上で「正しいパスワードのときだけトークンを発行する」という趣旨の2文の指示を与えたところ、PDD Kitが「正しいパスワードなら必ず入れるか」といった論理的な漏れを質問形式で指摘し、意図を確定させた。

さらに、外部の認証関数や時刻取得など6つの境界要素について仕様を定め、開発者の承認を経て検証を実行した。その結果、既存の不具合を発見してコードを堅牢化し、定義された仕様に対してログインの不具合が一切存在しないことを数学的に証明した。担当した開発者は意図の確認のみを行い、AIが生成したコードを1行も直接確認することなく開発を完了したという。