🤖 AI

P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation

该论文介绍了 $P^3$ ，这是一种基于大语言模型（LLM）的智能体工作流，通过共同规划程序及其形式化证明来克服顺序生成的低效问题，在包括一个名为 Lean4Commit0 的新仓库衍生数据集在内的验证代码生成基准测试中，实现了最先进的性能并显著降低了成本。

原作者： Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li, Kaiyu Yang

发布于 2026-08-11

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li, Kaiyu Yang

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在教一个超级聪明的机器人写故事。你给机器人一个提示词，它便吐出一个故事。但这里有个限制：你不仅仅想要一个故事；你想要一个在数学上保证正确、没有剧情漏洞、没有违反物理定律的魔法、也没有角色在没有任何解释的情况下凭空消失的故事。这就是**验证式代码生成（Verified Code Generation）**的世界。在这个计算机科学的领域里，我们不仅要求人工智能编写软件，还要求它编写自带“正确性证明”的软件——即一份数学证书，声明：“我承诺这段代码会完全按照我的要求执行，且适用于每一种可能的情况。”

长期以来，实现这一目标的标准方法就像是一场两步走的舞蹈：首先，机器人编写代码（故事），然后，由另一组专门负责“机器人校对”的团队来检查故事是否合理。如果校对员发现了剧情漏洞，他们会将故事退回给作者进行修复。作者修补故事，再次发送，如此循环往复。但本文指出，这种“先写后查”的舞蹈通常既笨拙又低效。这就像是试图建造一座桥梁，但在桥建好之后才发现忘了放支撑梁，于是不得不拆掉重建。本文的作者提出了一种新方法：与其将代码和证明分开编写，不如让机器人同时规划整座桥——既规划道路，也规划支撑——确保它们从第一张草图开始就完美契合。

问题所在：“先写后查”的陷阱

这篇题为**《面向验证式代码生成的程序与证明联合规划》（Joint Program-and-Proof Planning for Verified Code Generation）**的论文，解决了一个困扰着 AI 编写验证式软件的瓶颈问题。目前，大多数系统遵循“先程序后证明”的工作流。这就像是要求一位厨师烹饪一道复杂的菜肴，然后在菜上桌后，再请一位美食评论家来证明食材是否新鲜以及烹饪方法是否安全。如果评论家发现了问题（比如鸡肉没熟），厨师必须回去重新烹饪，并祈祷这次能符合评论家的要求。

作者认为这种顺序方法存在缺陷。当 AI 首先致力于编写代码时，它可能会选择一种在表面上看没问题、但在证明起来却极其痛苦的结构。例如，假设 AI 编写一个寻找列表中最大数字的程序。它可能会选择一种编写起来简洁明快的方法，但这种方法需要一个极其复杂且隐藏的数学规则才能证明其正确性。一旦代码写完，AI 就陷入了困境：它要么必须发明一个难度极高的证明来匹配那段特定的代码，要么就得撕毁代码重新开始。这导致了大量的资源浪费和“修复循环”——AI 不断地修补代码和证明，但两者始终无法完美契合。

解决方案：P3（“手拉手”规划器）

为了解决这个问题，研究人员引入了 P3，一种全新的工作流。在 P3 中，AI 扮演的是一位大师级建筑师的角色，在铺设第一块砖之前，就已经绘制好了建筑本身及其安全检查的蓝图。

P3 不会直接跳到编写代码的阶段，而是首先创建一个统一规划（Unified Plan）。这个规划是一个高层级的草图，同时回答两个问题：

代码将如何运作？（“程序草图”）
我们将如何证明它的正确性？（“证明草图”）

该规划决定了解决方案的结构。它选择了代码的正确“形状”（例如，是在递归循环和折叠操作之间做选择），并同时选择了证明该形状安全所需的匹配数学规则（不变式）。这就像是决定：“我们将使用悬索来建造这座桥，因此我们的证明计划必须包括检查这些悬索的张力。”

一旦这个共享规划被锁定，AI 随后就会进行“细化（Elaboration）”。它编写实际的代码和实际的证明，但这仅仅是在预先商定的蓝图基础上填充细节。如果证明失败，AI 能够准确知道问题出在哪里，因为结构早已确定。如果规划本身有问题（例如，桥的设计根本无法实现），AI 会回到规划阶段重新绘制蓝图，而不是在完成后的建筑上进行徒劳的修补。

新的试验场：Lean4Commit0

作者意识到，以往测试这些 AI 系统的题目太简单了，就像是让机器人解教科书上的数学谜题。现实世界的软件要复杂得多。为了妥善测试这种新方法，他们构建了一个新的基准测试集 Lean4Commit0。

他们抓取了 108 个真实的开源软件库（使用 Python、Rust、C/C++ 和 Java 编写），并将它们的核心功能转化为“验证式代码”挑战。这些挑战不再是简单的“将两个数字相加”，而是涉及程序不同部分之间复杂的相互关系。例如，在一个配置系统中，任务可能是要求 AI 证明：“如果你将设置设为‘高’，随后将其设为‘低’，系统能否正确记住‘低’这一设置。”这些任务要求 AI 理解不同函数之间是如何交互的，这使得它们比教科书问题难得多。

研究发现：智能规划更胜一筹

团队针对四种最强大的 AI 模型（包括 Codex、Gemini 和 Claude 的版本）在三个不同的基准测试（Verina、AlgoVeri 以及他们的新基准 Lean4Commit0）上进行了测试。

结果非常明确：共同规划比分开编写效果更好。

成功率： 在所有测试中，P3 解决的任务数量都高于其他任何方法。在处理最难的任务时，与现有最佳方法相比，P3 将成功率提升了 4.6 到 11.2 个百分点。
效率： 它不仅解决了更多问题，而且解决得更快、成本更低。在困难任务中，P3 将 API 调用成本降低了高达 40%，并将耗时减少了高达 37%。这是因为 AI 不再浪费时间去尝试证明不可能成立的事物，或者重写结构错误的程序。
“联合”优势： 为了证明“联合规划”确实是成功的关键，他们进行了一项对比实验：让 AI 先规划代码，但不提前规划证明。这种“仅代码规划”的方法表现不如 P3，这证实了在规划代码的同时思考证明才是脱颖而出的秘诀。

现实案例：红黑树

为了展示这套方法的实际应用，作者研究了一个经典的计算机科学问题：从“红黑树”（一种用于高效组织数据的复杂数据结构）中删除节点。

旧方法（先程序后证明）： AI 确定了一种特定的删除节点方式。事实证明，这种方式在结构上非常混乱，以至于为了填补漏洞，证明过程需要超过 6,300 行 代码，否则就会彻底失败。
P3 方法： AI 首先规划了删除过程。它意识到采用另一种结构性的方法会更容易证明。它坚持了这一计划，并仅用 1,105 行 代码就解决了问题。

为什么这很重要

这篇论文表明，对于 AI 编写真正可靠的软件而言，我们需要停止将“代码”和“证明”视为两项独立的工作。通过强制要求 AI 在设计代码的同时思考代码的数学安全性，我们得到的软件不仅在构建过程中就是正确的，而且生产过程也更加廉价、快速。这是一种从“事后修补”向“一次到位”的转变，确保我们所依赖的软件像证明其正确性的数学逻辑一样坚如磐石。

技术摘要：P3 —— 用于验证代码生成的程序与证明联合规划

1. 问题陈述

本文探讨了验证代码生成（verified code generation）任务，即大语言模型（LLM）必须同时合成一个可执行程序 ( $\pi$ ) 以及一个能够证明该程序满足形式化规范 ( $\sigma = (P, Q)$ ) 的机器可检查证明 ( $\kappa$ )。与基于测试的生成不同，其正确性必须对所有容许的输入都成立，而不仅仅是针对有限的示例集。

作者指出当前事实上的工作流中存在一个关键瓶 much 瓶颈，该工作流遵循一种顺序性的“先程序后证明”模式：

LLM 提交一个具体的实现方案。
一个独立的证明阶段尝试完成证明义务（proof obligations）。
如果验证失败，系统会进入一种脆弱的“修补并重试”循环，在修复代码和修复证明之间交替进行。

这种顺序方法存在两个主要问题：

有效性（Effectiveness）： 在没有预见其证明的情况下生成的程序，可能缺乏必要的结构属性（例如特定的归纳不变式或分解策略）。局部修复往往无法恢复那些从未经过规划的、对证明友好的结构。
效率（Efficiency）： 大量的计算资源（Token 和时间）被浪费在探索那些在结构上与规范的证明要求不兼容的实现方案上。

本文借鉴了 Dijkstra 的原则，即程序及其正确性论证应当“手拉手”地共同开发，并据此认为实现过程与证明结构是相互约束的。

2. 方法论：P3 框架

作者提出了 P3，一种将规划与细化（elaboration）解耦的智能体工作流，以确保在程序和证明完全实现之前，两者之间的结构一致性。

2.1 联合程序与证明规划

在第一阶段，LLM 智能体根据规范 $\sigma$ 生成一个统一计划 ( $\rho$ )。该计划不仅仅是代码，而是一个包含四个特定承诺的高层草图：

形式契约（Formal Contract）： 算法指令和渐近约束。
程序分解（Program Decomposition）： 递归变量、分支结构、数据表示以及终止度量（termination measures）。
库依赖（Library Dependencies）： 将要使用的具体函数和现有的引理。
证明义务（Proof Obligations）： 桥接谓词（bridging predicate）、归纳/分类结构以及必要辅助引理的陈述。

智能体在草图层面验证这些候选计划。如果程序草图违反了指令、分解未能保持桥接谓词，或者谓词无法推导出后置条件，则该计划会被拒绝。智能体选择能使预期证明负担最小化的计划。

2.2 计划引导的细化

一旦选定计划 $\rho$ ，智能体进入细化阶段：

实现（Implementation）： 智能体严格遵循 $\rho$ 中固定的分解和结构来编写代码 ( $\pi$ )。
证明骨架（Proof Scaffold）： 智能体编写一个镜像计划结构的证明骨架 ( $\kappa$ )（例如特定的归纳原理或情况拆分），并留下局部空白（用 sorry 表示）供详细的策略（tactics）填充。
细化（Refinement）： 智能体利用 Lean 4 的反馈（通过 LSP/MCP）来填充这些空白。至关重要的是，如果局部修复反复失败，或者桥接谓词被证明过于微弱，智能体会将其识别为计划级失败。与其在代码和证明的编辑之间进行无效循环，智能体会退回到规划阶段以修订 $\rho$ 。

这种分离使得智能体能够区分细化级错误（可在局部修复）和计划级错误（需要结构性重构），从而显著缩小了搜索空间。

3. 基准测试：Lean4Commit0

为了在超越教科书算法的现实场景中评估验证代码生成，作者引入了 Lean4Commit0。

来源： 衍生自 108 个真实的开源库，涵盖 Python、Rust、C/C++ 和 Java。
范围： 它提取核心 API 并将其行为编码为 Lean 任务，包括约束多个函数间联合行为的关系型规范（例如 set 操作与 get 操作之间的一致性）。
质量控制： 通过三阶段流水线确保规范质量：
1. 参考满足度（Reference Satisfaction）： 验证原始库实现是否满足 Lean 规范。
2. 突变拒绝（Mutation Rejection）： 确保规范能拒绝改变行为的突变（防止规范约束不足）。
3. LLM 评审（LLM Review）： 标记平凡或无关的规范。
规模： 最终的基准测试包含 511 个实现占位符和 519 个定理占位符。

4. 实验结果

作者使用四个前沿 LLM 后端（Codex-GPT-5.5, Gemini-3-Pro, Claude-Sonnet-4.6, Claude-Opus-4.7）在三个基准测试（Verina, AlgoVeri, Lean4Commit0）上，将 P3 与两个基线——PLAIN 智能体（无特定策略）和 SEQ（先程序后证明）智能体进行了对比评估。

求解率（Solve Rates）： P3 在每种（基准测试, 模型）配置下均取得了最高的求解率。
- 与更强的基线相比，P3 将求解率提高了 4.6–11.2 个百分点。
- 在困难的子集基准测试中，P3 将每个任务的 API 成本降低了高达 ~40%，并将墙钟时间（wall-clock time）缩短了高达 ~37%。
消融实验（Ablation Study）： 与 PLAN-SEQ（仅规划实现选择而非证明结构）的对比表明，联合规划本身贡献了额外的 3.3–8.3 个百分点 的增益。这隔离出了在规划阶段预见证明结构所带来的具体收益。
案例研究： 在一个左偏红黑树删除任务中，程序后证明的基线要么在生成 6,344 行代码后失败，要么仅通过冗余的重建不变式（1,176 行）获得成功。而 P3 通过在提交前比较计划，仅用 1,105 行 代码便解决了该任务。

5. 意义与主张

本文声称，P3 证明了通过将程序和证明视为协同设计的产物而非顺序输出，可以使验证代码生成变得更加高效且有效。

结构一致性（Structural Consistency）： 通过建立共享的结构计划，P3 确保了实现与证明是“按构造”一致的，避免了事后协调的需求。
向现实代码的可扩展性（Scalability to Real-World Code）： Lean4Commit0 的引入弥合了学术基准（教科书算法）与生产软件（关系型 API 约束）之间的鸿沟，表明联合规划在处理复杂的库级任务时特别有益。
效率（Efficiency）： 该框架减少了迭代修复循环中常见的“震荡”行为，从而显著节省了计算资源和时间。

作者总结道，虽然验证器（Lean 4）仍然是最终权威，但智能体对程序和证明进行联合规划的能力，显著提高了在实际资源限制内产生验证解的可能性。