P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation
作者: Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li, Kaiyu Yang
分类: cs.AI, cs.PL
发布日期: 2026-08-10
💡 一句话要点
提出P$^{3}$以解决验证代码生成中的效率与有效性问题
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 验证代码生成 大型语言模型 程序合成 形式化验证 软件工程 自动化开发
📋 核心要点
- 现有的验证代码生成方法将程序合成与证明过程分开，导致生成的程序可能难以验证或存在隐性错误。
- 本文提出P$^{3}$，通过统一的程序与证明计划，协同生成程序和证明，从而提高生成效率和有效性。
- 在多个基准测试中，P$^{3}$的求解率较强基线提升4.6至11.2个百分点，且每任务API成本降低约40%。
📝 摘要（中文）
验证代码生成要求大型语言模型（LLM）生成可执行程序及其符合形式规范的机器可验证证明，旨在构建正确的软件。现有方法将程序合成与证明过程分开，导致效率低下和有效性不足。本文提出P$^{3}$，通过从规范中推导统一的程序与证明计划，协同生成程序和证明，显著提高了求解率并降低了每任务的API成本和时间。实验表明，P$^{3}$在多个基准测试中均表现优异，解决率提升4.6至11.2个百分点。
🔬 方法详解
问题定义：本文旨在解决验证代码生成中程序合成与证明过程分离导致的效率低下和有效性不足的问题。现有方法常常在生成程序时未考虑其证明，导致生成的程序难以验证或存在错误。
核心思路：P$^{3}$的核心思路是从规范中推导出统一的程序与证明计划，确保程序和证明的协同生成，避免了反复修补的低效过程。
技术框架：P$^{3}$的整体架构包括两个主要阶段：首先是从规范生成程序与证明的统一计划，其次是在该计划下详细实现程序和证明的框架。
关键创新：P$^{3}$的创新在于将程序合成与证明过程结合为一个统一的计划，而非传统的分开处理，这一设计显著提高了生成的有效性和效率。
关键设计：在实现过程中，P$^{3}$使用了先进的LLM后端，并通过针对性消融实验验证了联合规划的优势，具体参数设置和损失函数设计未在摘要中详细说明，需参考完整论文。
🖼️ 关键图片
📊 实验亮点
在实验中，P$^{3}$在Verina、AlgoVeri和Lean4Commit0基准测试中均实现了最高的求解率，相较于更强的基线，求解率提升了4.6至11.2个百分点，且在困难子集上每任务API成本降低约40%，时间减少约37%。
🎯 应用场景
该研究的潜在应用领域包括自动化软件开发、形式化验证和安全关键系统的代码生成。通过提高代码生成的正确性和效率，P$^{3}$能够在软件工程中减少人工干预，提升开发效率，降低错误率，具有重要的实际价值和未来影响。
📄 摘要（原文）
Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification, promising software that is correct by construction. The de facto workflow decouples the two halves of the problem: first synthesize a program, then attempt to prove it correct. We observe that this sequential pipeline can be both ineffective and inefficient in practice. A program generated without anticipating its proof can be subtly incorrect or structurally difficult to verify, forcing the LLM into brittle repair loops that alternate between patching the code and patching the proof. Inspired by Dijkstra's view that a program and its correctness argument should be developed hand in hand, we propose $P^3$, an LLM-based agentic workflow that first derives a unified program-and-proof plan from the specification, then elaborates the implementation and proof scaffold under this shared plan. To evaluate verified code generation in realistic settings, we further introduce Lean4Commit0, a repository-derived, library-level benchmark built by extracting core APIs from real-world software repositories and translating their requirements, including relational specifications across APIs, into Lean tasks. Using four frontier LLM backends, we evaluate $P^3$ on Verina, AlgoVeri, and our Lean4Commit0 benchmark, where it achieves the highest solve rate in every benchmark--model setting. Compared with the stronger baseline, it improves solve rates by 4.6--11.2 percentage points and reduces per-task API cost by up to roughly 40\% and wall-clock time by up to roughly 37\% on the difficult subset of each benchmark. A targeted ablation further shows gains of 3.3--8.3 points over implementation-only planning, isolating the benefit of planning the program and proof jointly.