あなたは、超高性能なロボットに物語の書き方を教えていると想像してください。あなたはプロンプトを与え、ロボットは物語を吐き出します。しかし、ここには一つ仕掛けがあります。あなたが欲しいのは単なる物語ではありません。数学的に「真実であること」が保証され、プロットの穴がなく、物理法則を破る魔法が存在せず、キャラクターが説明なしに消えたりしない物語です。これは**検証可能なコード生成（verified code generation）**の世界です。これは、人工知能に対して、単にソフトウェアを書かせるだけでなく、そのソフトウェアに独自の「正当性の証明」——つまり、「あらゆる状況において、私が言った通りに正確に動作することを約束します」という数学的な証明書を添えさせることを求める分野です。

長い間、この標準的な方法は、二段階のダンスのようなものでした。まずロボットがコード（物語）を書き、次に別のロボット校閲チームがその物語が筋が通っているかをチェックします。もし校閲者がプロットの穴を見つけたら、物語を書き手に送り返して修正させます。書き手は物語をパッチ修正して送り戻し、このサイクルが繰り返されます。しかし、この論文は、この「書いてからチェックする」というダンスがしばん不器用で非効率であることを示唆しています。それは、橋を完成させた後に、支持梁を入れ忘れたことに気づいて、橋を解体して作り直すようなものです。著者は、コードと証明を別々に書くのではなく、ロボットが最初から両方が完璧に適合するように、橋の「道路」と「支持構造」の両方を同時に計画すべきだと提案しています。

問題点：「書いてからチェックする」という罠

**「Joint Program-and-Proof Planning for Verified Code Generation（検証可能なコード生成のためのプログラムと証明の結合計画）」**と題されたこの論文は、AIが検証可能なソフトウェアを書く際の、もどかしいボトルネックに取り組んでいます。現在、ほとんどのシステムは「プログラム・ディール・プルーフ（プログラムを書いてから証明する）」というワークフローに従っています。これは、シェフに複雑な料理を作らせた後、料理がテーブルに並んでから、食材が新鮮であったか、調理方法が安全であったかをフードクリティック（批評家）に証明させるようなものです。もし批評家が問題（例えば、鶏肉の生焼けなど）を見つけた場合、シェフは料理を作り直し、今度は批評家に気に入ってもらえることを祈りながら、再び調理しなければなりません。

著者らは、この逐次的なアプローチには欠陥があると主張しています。AIが先にコードを書くことを決定すると、表面上は問題なさそうに見えても、証明するのが悪夢のように困難な構造を選んでしまう可能性があるからです。例えば、リストの中から最大値を見つけるプログラムを書くとしましょう。AIは、書くには短くて簡潔な手法を選ぶかもしれませんが、それが機能することを証明するためには、非常に複雑で隠れた数学的ルールが必要になるかもしれません。一度コードが書かれてしまうと、AIは行き詰まります。その特定のコードに合う超難解な証明を編み出すか、あるいはコードを破棄して最初からやり直すかのどちらかを選ばなければなりません。これは、膨大な時間の浪費、コスト、そしてAIがコードと証明を何度もパッチ修正しながら、結局うまく噛み合わないという「修復ループ」を引き起こします。

解決策：P3（「手を取り合う」プランナー）

これを解決するために、研究者たちはP3という新しいワークフローを導入しました。ここでは、AIは建築家のように、レンガを一つ積む前に、建物とその安全検査の両方の設計図を描きます。

P3は、いきなりコードを書き始めるのではなく、まず**統合された計画（unified plan）**を作成します。この計画は、以下の2つの問いに同時に答えるハイレベルなスケッチです。

1. コードはどう機能するか？（「プログラム・スケッチ」）
2. どのようにしてそれが機能することを証明するか？（「証明スケッチ」）

この計画は、解決策の構造を決定します。コードの「形」（例えば、再帰ループを使うか、フォールドを使うかなど）を選択すると同時に、その形が安全であることを証明するために必要な数学的ルール（不変量）を同時に選びます。それは、「私たちは吊り橋を作るので、私たちの証明計画には吊りケーブルの張力をチェックすることを含める必要がある」と決めるようなものです。

この共有された計画が確定したら、AIは詳細を「具体化（elaborate）」していきます。AIは実際のコードと実際の証明を書き込みますが、それはあらかじめ合意された設計図の空欄を埋める作業に過ぎません。もし証明が失敗しても、構造はすでに決定されているため、AIはどこに問題があるのかを正確に把握できます。もし計画自体が悪い場合（例：橋のデザインが不可能である場合）、AIは必死に完成した建物をパッチ修正するのではなく、設計図を書き直すために計画段階へと戻ります。

新しいテスト場：Lean4Commit0

著者らは、従来のAIシステムのテストは、ロボットに教科書の数学パズルを解かせるような、簡単すぎるものだと気づきました。現実世界のソフトウェアはもっと複雑です。彼らの新しい手法を適切にテストするために、彼らはLean4Commit0という新しいベンチマークを構築しました。

彼らは108個の実世界のオープンソース・ソフトウェア・ライブラリ（Python、Rust、C/C++、Javaで記述）をスクレイピングし、それらのコア機能を「検証可能なコード」の課題へと変換しました。単純な「2つの数字を足す」といったタスクではなく、これらの課題はプログラムの異なる部分間の複雑な関係を扱います。例えば、設定システムにおいて、「設定を『高』に設定した後、後に『低』に設定した場合、システムが正しく『低』の設定を記憶していること」を証明させるようなものです。これらのタスクは、AIが異なる関数がどのように相互作用するかを理解することを要求するため、教科書の問題よりもはるかに難易度が高くなります。

分かったこと：賢い計画が勝つ

チームは、P3を、Codex、Gemini、Claudeのバージョンを含む4つの強力なAIモデルを用いて、Verina、AlgoVeri、そして彼らの新しいLean4Commit0という3つのベンチマークでテストしました。

結果は明白でした。**「一緒に計画する方が、別々に書くよりも優れている」**ということです。

• 成功率： P3は、あらゆるテストにおいて他のどの手法よりも多くのタスクを解決しました。最も困難なタスクにおいて、既存の最高の手法と比較して、成功率を4.6〜11.2パーセントポイント向上させました。
• 効率性： 単に多くの問題を解くだけでなく、より速く、より安価に解決しました。困難なタスクにおいて、P3はAPIコールのコストを最大**40%削減し、費やした時間を最大37%**短縮しました。これは、AIが不可能なことを証明しようとしたり、構造的に間違っているコードを書き直したりして時間を無駄にすることがなかったためです。
• 「結合」の優位性： 「結合計画」こそが秘訣であることを証明するために、彼らはAIがコードを計画したが、事前に証明を計画しなかった「コードのみの計画」を行うテストを実施しました。この手法はP3よりも成績が悪く、証明について事前に考えることが差を生む鍵であることを裏付けました。

実世界の例：赤黒木（Red-Black Tree）

この手法が実際にどのように機能するかを示すために、著者らは計算機科学の古典的な問題である「赤黒木（データの効率的な整理に使用される複雑なデータ構造）からのノード削除」を取り上げました。

• 旧来の方法（プログラム・ディール・プルーフ）： AIはノードを削除するための特定の方法を決定しました。しかし、その方法は構造的に非常に乱雑であったため、穴を埋めるためだけに6,300行以上のコードが必要になったか、あるいは完全に失敗しました。
• P3の方法： AIはまず削除の計画を立てました。AIは、別の構造的なアプローチの方が証明しやすいことに気づきました。その計画に従った結果、わずか1,105行で問題を解決しました。

なぜこれが重要なのか

この論文は、AIが真に信頼できるソフトウェアを書くためには、「コード」と「証明」を別々の仕事として扱うのをやめる必要があることを示唆しています。AIがコードを設計している最中に、そのコードの数学的な安全性についても考えさせることで、構築段階から正しい（correct by construction）だけでなく、より安価で迅速に生産できるソフトウェアが得られます。これは「後で直す」から「最初から正しく作る」への転換であり、ソフトウェアがそれを証明する数学と同じくらい堅牢であることを保証するものなのです。