AI 程式驗證
P³ Jointly Plans Programs and Proofs First, Improving Lean-Verified Solve Rates by 4.6 to 11.2 Percentage Points
P³ requires agents to agree on the implementation structure, helper lemmas, and proof decomposition before writing code, avoiding repeated proof patching after the program is complete. It outperformed comparison workflows across every model combination on three Lean 4 benchmarks, although the best solve rate on the hardest repository-level tasks was still only 22.2%.
P³ (Joint Program-and-Proof Planning) targets a common failure mode in formally verified program generation: an agent first decides on an implementation and then asks Lean to prove that it satisfies the specification. If the data structures, recursion strategy, or invariants are not proof-friendly, subsequent tool feedback merely triggers an expensive cycle of patching the program and tactic script. Instead, P³ first generates a shared plan that jointly determines the program decomposition, bridging predicates, and helper lemmas, and only begins producing Lean code after confirming that the implementation and proof structures are compatible.
The researchers also created Lean4Commit0, which converts core APIs from public repositories into library-level Lean tasks and adds specifications covering relationships across APIs. Problems must pass three filters: validation against a reference implementation, mutation rejection, and LLM review. Compared with verifying a single algorithmic function, this setup more closely reflects scenarios in which library interfaces must jointly preserve properties. The authors evaluated Codex-GPT-5.5, Gemini-3-Pro, Claude Sonnet 4.6, and Claude Opus 4.7 on Verina, AlgoVeri, and Lean4Commit0, comparing an unspecified-strategy workflow, a program-then-proof workflow, and P³.
P³ achieved the highest solve rate in all 12 benchmark–model combinations, outperforming the stronger baseline by 4.6 to 11.2 percentage points. On difficult problems, per-problem API costs fell by as much as 39.6%, while completion time decreased by as much as 37.2%. However, the best result on Lean4Commit0 was only 22.2%, indicating that repository-level relational proofs remain far from solved. Each experimental configuration was run only once, all backends were closed-source models, and the dataset was skewed toward Python APIs. Moreover, formal verification guarantees only that a program satisfies the specification as written; if the specification omits requirements, passing Lean may still create false confidence. From an engineering perspective, key questions are whether the method transfers to systems such as Verus and Dafny, and whether open models can reproduce the same gains.