发表机构
Apodex; Princeton University; Caltech; University of Toronto（Apodex; 普林斯顿大学; 加州理工学院; 多伦多大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
P³是一种用于验证代码生成的程序与证明联合规划的LLM智能体工作流，在三个基准上的求解率优于基线，还降低了API成本与运行时间。
AI 中文摘要
验证代码生成要求大语言模型（LLM）同时生成可执行程序和机器可验证的证明，以证明程序符合形式化规范，有望构建构造即正确的软件。当前主流工作流将问题拆分为两部分：先合成程序，再尝试证明其正确性。我们发现这种顺序流水线在实践中既低效又效果不佳：未考虑证明的程序可能存在细微错误，或结构难以验证，迫使LLM陷入脆弱的修复循环，交替修补代码和证明。受Dijkstra提出的“程序及其正确性论证应协同开发”的观点启发，我们提出P³，一种基于LLM的智能体工作流，该工作流先从规范中推导统一的程序与证明规划，再在该共享规划下细化实现和证明框架。为在现实场景中评估验证代码生成，我们进一步引入Lean4Commit0，一个源自代码仓库的库级基准，通过从真实软件仓库中提取核心API，并将其需求（包括API间的关系规范）转换为Lean任务构建而成。我们使用四个前沿LLM后端，在Verina、AlgoVeri及我们的Lean4Commit0基准上评估P³，结果显示其在每个基准-模型设置中均达到最高求解率。与更强的基线相比，在每个基准的困难子集上，它将求解率提升了4.6至11.2个百分点，每个任务的API成本降低了约40%， wall-clock时间缩短了约37%。针对性的消融实验进一步显示，与仅实现规划相比，联合规划程序与证明的收益为3.3至8.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.
