AI 程式驗證
P³ 先共同規劃程式與證明，Lean 驗證解題率提高 4.6 至 11.2 個百分點
P³ 要求代理在寫程式前先統一規劃實作結構、輔助引理與證明分解，避免完成程式後才反覆修補證明。它在三套 Lean 4 基準的全部模型組合均勝過比較流程，但最難的儲存庫任務最高仍只解出 22.2%。
P³（Joint Program-and-Proof Planning）針對形式驗證程式生成的一個常見失敗模式：代理先決定實作，再要求 Lean 證明其符合規格。若資料結構、遞迴方式或不變量不利於證明，後續工具回饋只會觸發程式與 tactic script 之間的昂貴修補循環。P³ 改為先產生共享計畫，同時決定程式分解、橋接述詞與輔助引理，確認實作和證明結構相容後才展開 Lean 程式碼。
研究亦建立 Lean4Commit0，把公開儲存庫的核心 API 轉為函式庫層級 Lean 任務，並加入跨 API 關係規格。題目需通過參考實作、突變拒絕及 LLM 審查三道篩選；相較只驗證單一演算法函式，這更接近函式庫介面必須共同維持性質的情境。作者以 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 個百分點；困難題的單題 API 成本最多降低 39.6%，時間最多減少 37.2%。然而 Lean4Commit0 最佳結果只有 22.2%，顯示儲存庫級關係證明仍遠未解決。實驗每個設定只跑一次，後端皆為閉源模型，資料偏向 Python API，而且形式驗證只保證程式符合「寫下來的規格」；規格若遺漏需求，Lean 通過仍可能產生錯誤信心。工程上值得追蹤的是該方法能否轉移至 Verus、Dafny 等系統，以及公開模型能否重現相同增益。