P³、プログラムと証明を事前に共同設計し、Leanの問題解決率を4.6～11.2ポイント向上

P³（Joint Program-and-Proof Planning）は、形式検証を伴うプログラム生成でよく見られる失敗パターンに対処する。従来、エージェントはまず実装を決定し、その後でLeanに仕様への適合を証明させる。データ構造、再帰方式、不変条件が証明に適していなければ、その後のツールからのフィードバックは、プログラムとタクティックスクリプトの間でコストの高い修正ループを引き起こすだけだ。P³では代わりに、まず共有計画を生成し、プログラムの分解、橋渡しとなる述語、補助補題を同時に決定する。実装と証明の構造に互換性があることを確認してから、Leanコードの作成に進む。

研究チームはさらに、公開リポジトリのコアAPIをライブラリレベルのLeanタスクへ変換し、API間の関係を表す仕様を追加したLean4Commit0を構築した。問題は、参照実装による検証、ミューテーションの排除、LLMによるレビューという3段階の選別を通過する必要がある。単一のアルゴリズム関数だけを検証する場合と比べ、これはライブラリのインターフェース群が性質を共同で維持しなければならない状況により近い。著者らはCodex-GPT-5.5、Gemini-3-Pro、Claude Sonnet 4.6、Claude Opus 4.7を使用し、Verina、AlgoVeri、Lean4Commit0において、特定の戦略を用いない方式、プログラムを先に作成してから証明する方式、P³を比較した。

P³は、ベンチマークとモデルの全12組み合わせで最高の問題解決率を達成し、より強力なベースラインを4.6～11.2ポイント上回った。難問では、1問を解決するためのAPIコストを最大39.6%、所要時間を最大37.2%削減した。しかし、Lean4Commit0での最高成績は22.2%にとどまり、リポジトリレベルの関係性の証明が依然として未解決であることを示している。実験は各設定につき1回しか実施されておらず、バックエンドはいずれもクローズドソースモデルで、データはPython APIに偏っている。また、形式検証が保証するのは、プログラムが「記述された仕様」に適合することだけだ。仕様に要件の抜けがあれば、Leanの検証に合格しても誤った安心感を生む可能性がある。エンジニアリング上、今後注目すべき点は、この手法をVerusやDafnyなどのシステムにも転用できるか、そして公開モデルで同様の改善を再現できるかどうかだ。