P³: Joint Program-and-Proof Planning for Verified Code Generation 精读

论文链接： arXiv:2608.09277

代码与数据： 论文配套的完整 prompt、harness、脚本、锁定环境和运行元数据发布在 figshare。

发表时间： 2026 年 8 月

作者机构： Zenan Li、Ziran Yang、Peiyang Song、Zhaoyu Li、Kaiyu Yang。其中 Kaiyu Yang 是形式化验证与 AI 交叉领域的重要研究者，同时也是 Verina 基准的核心作者之一——这意味着 P³ 与 Verina 共享同一研究谱系，P³ 的实验设计与 Verina 的评测体系有深度对接。Zenan Li 等作者也参与过 AlgoVeri 基准的工作，作者团队对三大基准中的两个都有直接贡献。

领域标签： cs.SE（软件工程）、cs.AI（人工智能）、cs.LO（逻辑），属于「LLM + 形式化方法」的交叉方向。

一、论文背景

1.1 从"写一段能跑的代码"到"写一段被证明正确的代码"

在过去几年里，大语言模型（LLM）在代码生成上取得了惊艳的进展。给定一句自然语言需求，比如"写一个函数判断两个整数是否异号"，模型能瞬间吐出可执行的 Python、Rust 或 Lean 代码。但是，“能跑"不等于"正确”——一个能通过 10 个测试用例的函数，仍可能在第 11 个边界条件上悄悄出错。这种"测试通过 ≠ 无 bug"的鸿沟，是软件工程几十年来的一块心病。

要真正消灭这道鸿沟，学界有一个古老却始终未能大规模落地的梦想：形式化验证（Formal Verification）。它的野心不是"让代码跑通一批测试"，而是"用数学证明的方式论证代码必然满足规范"。换句话说，不是经验性地相信代码，而是逻辑上证明代码。一旦证明通过，就不再需要人工 review 兜底——因为数学证明不会"偶尔出错"。

这种"证明代码正确"的范式有一个迷人的口号：correct by construction——“构造时即正确”。它追求的不是"写完再查 bug"，而是"代码从诞生那一刻起就携带了正确性的数学保证"。

近年来，LLM 的崛起为这个梦想注入了新的可能。研究者提出了一个新范式：验证代码生成（Verified Code Generation）。它的目标非常激进——让 LLM 一次性产出三件东西：

1. 代码（Code）：实现开发者意图的可执行程序；
2. 规范（Specification）：用形式化语言描述"这段代码应该满足什么数学性质"（前置条件 + 后置条件）；
3. 证明（Proof）：一段机器可检查的数学证明，论证"这段代码确实满足这个规范"。

如果 LLM 能稳定地完成这三件事，我们就能自动化地生产出"被数学证明正确"的软件——这比任何测试覆盖率都更可靠。这就是论文开篇所讲的：promising software that is correct by construction。

1.2 一个类比：盖房子同时出具建筑安全证书

为了理解"验证代码生成"的独特之处，我们先打一个比方。

想象你要盖一栋大楼。传统软件开发就像"先盖楼，盖完再请质检员来验收"。质检员做完压力测试、抗震测试、消防测试，列出一张问题清单。你回去返工，修修补补，再请质检员来——如此反复。问题在于，有些结构性的缺陷（比如承重墙位置不对、地基深度不够）是后期修补救不了的：你必须推倒重建。

验证代码生成 则是另一种范式：你盖楼的同时，同步出具一份建筑安全证书，证书里用数学公式论证了"这栋楼在任何可能的风载、任何可能的地震条件下都不会倒塌"。证书不是事后写的，而是和图纸、钢筋、混凝土一起，在设计阶段就被规划好。

这里的关键区别在于：“质检"只能发现 bug，但"证明"能从源头消灭 bug。前者是"事后兜底”，后者是"构造时正确"。

但这件事非常难。让 LLM 写代码容易，让 LLM 写一段"机器可检查的数学证明"则难如登天——业界最好的模型（如 OpenAI o4-mini）在 Verina 基准上一次性写出正确证明的成功率只有 3.6%。证明，是横亘在"验证代码生成"面前的最大瓶颈。

1.3 Lean 定理证明器：一个自动化裁判

在理解为什么"证明"这么难之前，我们需要先认识一位特殊的角色：Lean 定理证明器。

Lean 是一门"既能写程序、又能写证明"的语言。你可以把它理解为一个极其严苛的自动化数学裁判：你在 Lean 里写出一段代码、一段规范、一段证明，然后按下运行键——Lean 会用一套严密的数学规则（依赖类型理论）逐一检查你的证明是否逻辑无误。只要 Lean 点头，你的代码就数学上必然满足规范，没有任何反驳的余地。

Lean 之所以重要，是因为它是当前机器可检查证明领域最被信任的平台之一。AWS 用它验证 Cedar 授权语言；以太坊基金会支持的项目用它验证密码学协议；数学家甚至用它形式化了费马大定理的证明。它的"最小可信内核"保证了只要内核没问题，所有被 Lean 接受的证明都是绝对正确的。

但 Lean 的代价是：写证明极其痛苦。它不像写 Python 那样"差不多就行"，每一个逻辑步骤都要用 Lean 能理解的 tactic（策略）显式写出来，一个未闭合的目标（goal）就让整个证明失败。即便是最强 LLM，也常常在 Lean 的 tactic 搜索空间里迷路。

1.4 当前的核心困境：程序与证明"分家"

有了 Lean 这个裁判，有了 LLM 这个选手，我们终于可以组织一场"验证代码生成"的比赛了。但目前的比赛流程，存在一个致命的设计缺陷——

当前主流做法（论文称之为 de facto workflow，即"事实上的标准流程"）是一个顺序流水线：

规范  →  先合成程序  →  再尝试证明程序正确

这就像盖房子时：先按自己的喜好把楼盖完，再请质检员来出安全证书。如果质检员发现"承重墙不能这样设计"，你只能回去拆楼重盖；如果你改了承重墙，之前的装修（=证明的前半段）也跟着作废。

这种"先程序、再证明"的解耦（decouple）会导致什么问题？论文观察到两类典型困境：

1. 程序本身结构上难以验证：LLM 写代码时只考虑"怎么实现功能"，没有考虑"这段代码将来怎么证明"。结果代码可能用了一个非常难证的数据结构（比如 List.foldl 累加器），或者用了一个看似合理但证明上极其脆弱的分支结构。等到写证明时才发现：这段代码在数学上根本无从下手。

2. 脆弱的修补循环（brittle repair loops）：一旦证明失败，Agent 会尝试"打补丁"。但补丁往往是治标不治本——改一处证明可能逼着代码也改，改代码又让另一处证明失效，于是陷入 “改代码 → 改证明 → 再改代码” 的拉锯。论文用了一个精准的描述：“alternate between patching the code and patching the proof”。

这种顺序流水线，本质上是让程序与证明两个本应紧密耦合的对象在时间上解耦。它的根本缺陷在于：程序若不考虑证明可验证性，就会在结构上埋下不可逾越的障碍。

1.5 一个 1976 年的洞察被遗忘了

有意思的是，这个问题的"解药"早在 1976 年就被图灵奖得主 Edsger Dijkstra（就是发明 Dijkstra 最短路径算法的那位）一语道破。在他的名著《A Discipline of Programming》中，他写道：

“Instead of first designing a program and then trying to prove its correctness, we develop correctness proof and program hand in hand.”

（与其先设计程序再试图证明它正确，不如让正确性证明与程序携手开发。）

Dijkstra 的意思是：程序的正确性论证不应该在程序写完之后才追加，而应该在写程序的同时——甚至在写程序之前——就规划好。证明应该"略先于程序"生长，程序应该"按证明的要求来塑造"。这就是 correct-by-construction 的原始哲学。

但近 50 年来，这条原则在工业界几乎从未被大规模实践——因为让人类程序员同时写程序和证明太痛苦了。直到 LLM 的出现：如果 LLM 能自动产出程序和证明，那 Dijkstra 的理想是不是终于可以落地？

P³ 这篇论文，正是要把 Dijkstra 这条 50 年前的洞察，注入到 LLM Agent 的工作流里。它的核心主张是：与其让 LLM 先写程序再证明，不如让 LLM 先规划一个"程序-证明共享计划"，再在这个计划下同步细化两者。

二、论文定位和关联工作

2.1 研究脉络：验证代码生成的三股力量

P³ 处在一个快速兴起的交叉领域——LLM 驱动的形式化验证。这个领域大致由三股力量推动：

力量一：评测基准的成熟

在 P³ 之前，要让 LLM 做"验证代码生成"，首先得有一套公认的评价标准。近两年涌现了几个关键基准：

这条谱系清晰地显示：从"测一段算法"到"测端到端代码+证明"再到"测真实仓库级 API"，评测在快速逼近真实软件工程。

力量二：Agent 工作流的演化

光有基准还不够。LLM 怎么"动手"做验证代码生成？经历了几个阶段：

1. 单次 prompt（One-shot）：直接让 LLM 一次吐出代码+证明，失败就放弃。这种做法在 Verina 上 proof 成功率只有 3.6%。
2. 迭代修复（Iterative Refinement）：让 LLM 看到 Lean 编译器的报错信息，反复修改证明。Verina 允许 64 轮修复，能把简单题的证明成功率提升到约 20%——但计算成本爆炸，且对复杂题"算再多也救不回来"。
3. 技能包（Skill-based Sequential Pipeline）：代表性工作是 Lean 4 Skills（论文 [14]）。它把"先写程序、再写证明"固化为一个 Agent 技能包，引导 LLM 沿着顺序流水线工作。这就是论文里基线 Seq 的来源。
4. 规划增强（Plan-then-Execute）：让 LLM 在动手前先"想一想"——先规划再执行。但现有规划只规划"怎么写程序"，不规划"怎么写证明"。

P³ 正是在这条谱系的最新节点上：它把规划的对象从"程序"扩展到"程序+证明"。

力量三：correct-by-construction 的现代化

Dijkstra 的思想一直活在形式化方法社区，但工业界从未大规模落地。近年来 Dafny 环境（Microsoft Research）等系统部分实现了"correct-by-construction"的开发体验。但把这条原则注入到 LLM Agent 工作流，P³ 是第一个系统性的尝试。

2.2 P³ 在谱系中的定位

把上述三股力量汇总成一张对比表：

2.3 关键定位结论

P³ 的独特定位可以概括为三个"第一次"：

1. 第一次 把 Dijkstra 的"程序-证明携手开发"原则系统化地注入 LLM Agent 工作流；
2. 第一次 用"共享计划"显式约束程序和证明的结构一致性，从源头避免"可执行但不可验证"的程序结构；
3. 第一次 提出从真实开源仓库提炼、包含跨 API 关系规范的库级验证代码生成基准（Lean4Commit0），把评测从"教科书题"推向"真实软件"。

三、问题定义

3.1 从具体场景出发：一个 listMax 的例子

要理解 P³ 解决的本质问题，先看一个具体场景。假设我们给 LLM 这样一个任务：

规范：给定一个非空的自然数列表 xs，写一个函数 listMax 返回列表中的最大元素，并证明它的正确性。

LLM 可能有两种典型的实现思路（论文里举的例子）：

实现 A（结构化递归）：

listMax [x] = x
listMax (x :: y :: t) = max x (listMax (y :: t))

直接对列表结构做模式匹配，递归到只剩一个元素。后置条件"返回值等于列表最大值"本身可以直接作为证明的"桥接谓词"（bridging predicate），证明非常自然。

实现 B（用 List.foldl）：

listMax xs = List.foldl max 0 xs

更简洁，看起来很"高级"。但问题来了：foldl 的累加器（accumulator）是被全称量化的，证明时必须把后置条件强化为一个关于累加器的辅助引理 foldl_max_gen，否则归纳法根本推不出来。

两种实现都"能跑"，但在证明可验证性上天差地别。实现 A 是证明友好的，实现 B 是证明敌对的。问题在于：如果 LLM 在写代码时只想着"实现功能"，它很可能选了 B，等到证明阶段才发现自己掉进了泥潭。

这就是 P³ 想要解决的核心场景：如何让 LLM 在写代码之前，就同时考虑"这个实现能不能被证明"？

3.2 抽象问题：什么是"程序-证明共享计划"

把上述场景抽象一下。验证代码生成的标准形式化定义是：

给定：一个形式化规范 σ = (P, Q)，其中 P 是前置条件（输入约束），Q 是后置条件（输入与输出的关系）。

求：一个二元组 (π, κ)，其中 π 是满足 σ 的可执行程序，κ 是证明 π 满足 σ 的 Lean 证明。

P³ 在这个标准定义之上，引入了一个新的中间对象——共享计划 ρ（shared plan）。它把问题重新表述为：

求：一个三元组 (ρ, π, κ)，其中 ρ 是一个同时约束 π 和 κ 结构的计划，π 和 κ 都在 ρ 下细化产生。

这里的关键创新是 ρ。它不是"先写程序"也不是"先写证明"，而是在两者之前先写的一个"统一蓝图"。ρ 必须同时承诺：

• 程序将怎么分解（递归结构、case 分支、辅助函数）；
• 证明将怎么组织（归纳策略、桥接谓词、辅助引理）；
• 两者必须结构一致——证明的归纳骨架必须对应程序的递归骨架。

这就像盖楼前先画一份图纸：图纸上同时标注了"承重墙在哪里"（程序结构）和"抗震论证基于什么模型"（证明结构）。两者必须互相契合，否则图纸不通过。

3.3 抽象的精妙之处

P³ 这个抽象的精妙之处在于：它不是简单地"先规划再编码"，而是把规划对象本身扩展为程序和证明的联合体。

可以打一个更精细的类比：

这个抽象的合理性在于：程序的可验证性，本质上是程序结构的一个属性。它不是"写完代码之后可以追加"的东西，而是"必须在设计阶段就考虑"的东西。一旦你在抽象层面接受了这一点，“程序-证明共享计划"就成了一个自然的必然选择。

3.4 问题的约束

当然，P³ 的问题并不是无约束的"随便规划”。它有几个硬性约束：

1. 计划必须可执行：ρ 里的程序草图必须能被细化为合法的 Lean 程序，证明草图必须能被细化为合法的 Lean 证明。
2. 结构必须一致：ρ 一旦冻结，π 和 κ 必须严格遵循它的分解——细化时不能再重新选择递归变量、case 分支等。
3. 质量必须可评估：ρ 必须能用某种方式预测"将来的证明负担有多重"，以排除那些"看起来合理但证明上不可行"的计划。
4. 成本必须受控：整个流程（规划 + 细化）的 API 成本和墙上时间，必须低于现有的顺序流水线。

这四条约束共同定义了 P³ 要解决的问题：如何在严格的结构一致性约束下，让 LLM 自动产出一个同时考虑程序和证明的计划，并在该计划下高效细化？

四、问题解法

P³ 的解法分为两大阶段：规划（Planning） 和 细化（Elaboration）。下面我们逐个拆解。

4.1 第一阶段：规划——产出程序-证明共享计划 ρ

这一阶段的目标是：从规范 σ 出发，产出一个同时约束程序和证明的结构蓝图 ρ。

共享计划 ρ 的四项承诺

ρ 不是一段自由文本，而是一个结构化的承诺集合，包含四项明确的"承诺"（commitments）：

这张表里最值得注意的是第 (iv) 项——证明义务在程序还没写时就显式列出了。这就是 Dijkstra 说的"证明略先于程序"。

规划的具体流程

规划不是一个简单的"让 LLM 写一份计划"。它是一个带质量门控的筛选过程：

1. 候选生成：从 σ 提出多个候选计划，每个都包含四项承诺。
2. 草图级验证：对每个候选，做"非正式但显式"的检查——
   • 程序草图是否满足算法指令？
   • 证明草图能否解释"分解保持桥接谓词"？
   • 证明草图能否解释"桥接谓词蕴含 Q"？
3. 拒绝坏候选：拒绝以下候选——
   • 程序草图违反算法指令；
   • 分解不保持桥接谓词；
   • 桥接谓词无法蕴含 Q。
4. 选择最优候选：在通过检查的候选中，选预期证明负担最小的那个。
5. 冻结 ρ：选定后，ρ 的结构承诺被"冻结"，后续细化必须严格遵循。

一个关键概念：桥接谓词

“桥接谓词”（bridging predicate）是 ρ 中最核心的发明之一。它是一个比后置条件 Q 更强的中间断言，作用是"桥接"程序分解和证明目标。

回到 listMax 的例子：

• 实现 A 里，后置条件 Q 本身就够当桥接谓词——证明自然流畅。
• 实现 B 里，Q 不够强（因为 foldl 的累加器是隐式的），必须把 Q 强化为一个关于累加器的辅助引理 foldl_max_gen——这就是"桥接谓词"。

P³ 的规划阶段会显式识别这种强化，并要求：任何 Q 的非平凡强化都必须被命名为辅助引理，不能隐含。这就避免了"写代码时糊弄过去，写证明时才发现坑"的情况。

计划存留率：规划质量的实证证据

一个自然的问题是：LLM 真的能在规划阶段就选出好计划吗？论文给了一组有力的证据：在 Verina 的 189 条 Claude-Opus-4.7 轨迹中——

• 131 / 141 成功（92.9%）保留了初始计划；
• 仅 4 / 48 失败（8.3%）归因于计划不当。

也就是说，一旦 P³ 在规划阶段选定 ρ，绝大多数情况下这个计划能一路走到最后。这证明了规划阶段的质量门控是有效的。

4.2 第二阶段：细化——在 ρ 下同步生成程序和证明

有了冻结的 ρ，接下来就是细化（Elaboration）。这一阶段的核心约束是：不能再重新选择结构——递归变量、case 分支、辅助函数、归纳策略都已经在 ρ 里定死了，细化只是"填充具体内容"。

程序细化 π

Agent 编写实现 π 时，必须严格遵循 ρ 固定的分解：

• 递归参数的形式不能改；
• case split 的边界不能改；
• 数据表示不能临时换；
• 辅助例程的接口不能变。

这就像盖楼时，图纸定了"承重墙在 X 位置"，施工队就不能临时把墙挪到 Y 位置——即使 Y 位置看起来更方便。

证明脚手架 κ

证明不是一次性写完的，而是先生成一个与程序同形状的"脚手架"（scaffold）：

• 目标定理（top-level theorem）；
• ρ 命名的所有辅助引理的陈述；
• 顶层证明结构（调用 ρ 指定的归纳/案例分析/引理应用）。

此时脚手架在 ρ 论证的"叶节点"可能仍有局部空隙，表示为 Lean 的占位符 sorry。关键点在于：这些空隙是局部的、结构已知的，不再是"无约束的证明搜索"。

证明完成：从全局搜索到局部填充

有了脚手架，证明的完成就从"无约束的全局证明搜索"变成了"在已知结构下填充局部空隙"。Agent 反复请求 Lean 检查文件 → 读取错误信息 → 填充剩余的证明叶节点或辅助引理，全程保持 ρ 固定的结构。

这是一个根本性的转变：

一个工程优化：子代理派遣

论文还提到一个工程层面的设计：细化步骤若足够受约束，可派遣给更便宜的子代理（cheaper subagents）。

这是 Agent 系统里"关注点分离"的典型应用：

• 主代理（强模型）：负责规划——这是高智力任务，需要强推理。
• 子代理（便宜模型）：负责局部细化——这是低智力任务，结构已定，按模板填空即可。

这种分工让 P³ 在保持高质量的同时控制了 API 成本，是后面"成本降低 40%“的重要来源之一。

4.3 失败处理：把二元反馈变成结构化指导

任何方法都会遇到失败。P³ 的精妙之处在于：它把 Lean 验证器的"通过/不通过"这种二元反馈，转化为结构化的失败分类与处理指导。

失败被分成两类：

这个分类机制是 P³ 区别于 Seq 的一个核心设计。Seq 的失败处理是"局部修不好就全量重启”——Agent 重写代码和证明两个产物，成本爆炸。P³ 则是"先判断失败层级，只在必要时才回到规划"，重启频率显著更低。

4.4 整体工作流全景

把规划、细化、失败处理串起来，P³ 的完整工作流如下：

            ┌─────────────────────────────────┐
            │      形式化规范 σ = (P, Q)        │
            └──────────────┬──────────────────┘
                           │
                  ┌────────▼────────┐
                  │   规划阶段       │
                  │  (Planning)      │
                  │  生成候选 ρ_i     │
                  │  草图级筛选       │
                  │  选最优 → 冻结 ρ  │
                  └────────┬────────┘
                           │
              ┌────────────▼─────────────┐
              │       细化阶段            │
              │  (Elaboration)            │
              │                           │
              │  ┌─────────┐ ┌──────────┐ │
              │  │ 程序 π  │ │ 证明脚手架│ │
              │  │         │ │   κ      │ │
              │  └────┬────┘ └────┬─────┘ │
              │       │           │       │
              │       └─────┬─────┘       │
              │             │             │
              │      Lean 编译器检查        │
              └─────────────┬─────────────┘
                            │
                ┌───────────▼───────────┐
                │    失败分类            │
                │  细化级？计划级？       │
                └───────────┬───────────┘
                            │
              ┌─────────────┴─────────────┐
              │                           │
       细化级失败                   计划级失败
       就地局部修复                 退回规划阶段
       保持 ρ 不变                  修订 ρ

这个流程最关键的洞见是：ρ 是一个结构性的"中介"。它不是被一次性消费掉就扔掉的中间产物，而是贯穿整个细化过程、决定失败如何处理的活的约束。这是 P³ 区别于所有"先规划再执行"的朴素方案的根本所在。

五、评估指标与实验证据

5.1 主指标：求解率（Solve Rate）

P³ 最核心的评估指标是求解率（Solve Rate）。它的定义非常严格：

一个任务计为"已解决"（solved），当且仅当产出的解决方案满足算法指令且通过 Lean 检查器。

这两个条件缺一不可：

• “通过 Lean 检查器”：证明 κ 在 Lean 里编译通过，且没有使用 sorry（占位符）作弊。
• “满足算法指令”：LLM 不能"钻空子"——比如实现一个满足弱后置条件的平凡算法（如返回常量），即便它能通过 Lean，也会被 LLM judge 判定为"算法退化"（spec gaming）。

这个指标衡量的是端到端的能力：不是"能不能写代码"，不是"能不能写证明"，而是"能不能同时写出被严格证明正确的非平凡代码"。

5.2 三个基准：从教科书题到真实仓库

P³ 在三个基准上做了评测，难度从低到高：

第三个基准 Lean4Commit0 是 P³ 自己提出的，也是这篇论文的重大贡献之一。我们稍后在 5.5 节单独展开。

5.3 基线方法：Plain 与 Seq

P³ 的实验对比了两个主要基线：

• Plain（Plain Lean-agent）：Agent 接收形式规约和 Lean 工具（Lean LSP MCP），不引导任何特定工作流。LLM 自由发挥。
• Seq（Program-then-Proof / Skill-based Sequential）：Agent 被引导"先产出实现，然后生成并修复证明"。基于 Lean 4 Skills 的技能包，代表现有的程序-然后-证明范式。

这两个基线覆盖了"无策略"和"顺序流水线"两种主流做法。此外还有一个消融基线：

• Plan-Seq：在 Seq 之前加一个"只规划实现"的步骤，用来对比"规划程序"和"联合规划"的差异。

所有方法共享相同的实验设置：每任务 API 预算 30.0 USD，墙上时间上限 180 分钟，同一 Docker 镜像，Lean 4.28.0，每个 (task, model, method) 配置运行一次。

5.4 核心实验结果：12/12 全胜

Table 2：求解率（%）跨后端模型、方法、基准

这张表最醒目的结论是：P³ 在全部 12 个（基准, 模型）单元中全部获得最高求解率，无一例外。绝对增益 Δ 在 +4.6 到 +11.2 个百分点之间。

几个值得注意的细节：

1. 增益在更难的基准上依然稳定：Lean4Commit0 的求解率整体很低（9%–22%），但 P³ 仍稳定提升 4.6–5.5 个点。这说明 P³ 不是"在简单题上刷分"，而是在"真实困难场景"中也有效。
2. 不同模型都受益：从 GPT-5.5 到 Gemini-3-Pro，从 Claude-Sonnet 到 Claude-Opus，P³ 的提升跨模型稳定。这说明 P³ 是一个模型无关的工作流改进，不是依赖某个特定模型的奇技淫巧。
3. 基线的相对强弱随基准变化：在教科书式的 Verina 上，Plain 反而比 Seq 略好（说明"不引导"比"顺序流水线"更好）；但在仓库级 Lean4Commit0 上，Seq 反超 Plain 1.8–3.7 个点（说明复杂任务需要某种引导）。P³ 在两种 regime 下都更强。

5.5 Lean4Commit0：填补仓库级评测的空白

前面提到，Lean4Commit0 是 P³ 自带的新基准，值得单独讲一讲。

为什么要造新基准？

在 P³ 之前，验证代码生成的基准（Verina、AlgoVeri）都是独立算法题——写一个排序函数、写一个查找函数、写一个红黑树节点。但真实软件工程不是这样的：真实软件是一组相互依赖的 API，它们之间的关系（比如"set 之后 get 返回什么"）是无法通过孤立推理任何一个 API 来证明的。现有基准无法评测这种"关系级"的验证能力。

Lean4Commit0 的构造流程

论文设计了一个精细的构造流程：

1. 源库范围：选取 108 个真实开源库，跨四大生态系统——
   • Python（65 个）
   • Rust（17 个）
   • C/C++（15 个）
   • Java（11 个）
2. 领域覆盖：密码学原语、数据结构、Web/网络框架、解析器、调度器、游戏模拟器。
3. API 提取：每个库选若干核心 API（库主要数据结构的用户面向入口点），每个 API 编码为三元组：
   • Lean 函数签名（body 为 sorry）
   • 后置条件谓词
   • 正确性定理（proof 为 sorry）
4. 规模：511 个实现占位符 + 519 个定理占位符 = 1030 个占位符。

跨 API 关系规范：Fabric 示例

最能体现 Lean4Commit0 价值的是跨 API 关系规范。以 Python SSH 部署库 Fabric 为例：

Fabric 的配置逻辑涉及 Config.set 和 Config.get 两个 API，配置条目携带优先级（从默认值到运行时覆盖）。Lean4Commit0 把这种关系显式编码为形式化规范：

• 性质 1：设置 key k 为 value v 后，后续查询 k 返回 some v；
• 性质 2：若同一 key 在较低层级 set 后又在较高层级 set，get 返回更高优先级的值。

这两个性质无法通过孤立推理 set 或 get 来消解——证明必须把"更新"和"查询"连接起来，并尊重优先级排序。这就是"关系规范"的本质：它要求 LLM 理解 API 之间的协同语义，而不仅是单个 API 的行为。

规约质量保证

从 GitHub 抓来的代码不能直接用——必须验证"翻译成 Lean 后的规范"真的等价于原始语义。论文设计了一个三重质量门控：

质量评分公式：质量评分 = 0.5 × Mutation(σ) + 0.5 × Review(σ)，准入门槛是"参考满足完整 + 质量评分 ≥ 80%"。最终 108 个库全部通过此阈值，全基准平均质量分 90.7%，10 个库达到 100%。这保证了 Lean4Commit0 的规范质量。

Table 1 展示了各语言的基准规模与质量指标：

这张表说明：Lean4Commit0 不仅规模可观（1030 个占位符），而且经过了严格的质量控制——突变检测的拒绝率高达 98.6%（意味着规范足够严格，能挡住绝大多数行为突变），LLM 审查分 82.7%（意味着规范非平凡、非空洞）。

5.6 消融实验：联合规划 vs 仅实现规划

P³ 的核心主张是"联合规划"——程序和证明必须一起规划。为了验证这一点，论文设计了一个关键消融：Plan-Seq。

Plan-Seq 的定义是：“允许规划实现侧的选择，但禁止在运行 program-then-proof 管道前预期不变式、证明分解、归纳策略、证明引理”。换句话说，Plan-Seq 是"只规划程序"的版本。

Table 3：实现规划消融（Claude-Opus-4.7，求解率 %）

这张表揭示了几个深刻的结论：

1. 联合规划比仅实现规划稳定提升 3.3–8.3 个点：这是 P³ 相对于 Plan-Seq 的纯增益，直接证明了"联合"这个词的必要性。
2. Plan-Seq 在 Lean4Commit0 上反而有害：13.9，低于 Seq 的 17.6。这是一个反直觉但极其重要的发现——只规划程序而不规划证明，在跨 API 关系任务上比不规划还差！原因是：独立合理的 API 实现可能难以在关系定理下连接，除非它们针对共享证明义务进行规划。
3. 越难的任务，联合规划的优势越大：在简单的 Verina 上 Δ=4.8，在复杂的 Lean4Commit0 上 Δ=8.3。这说明联合规划的价值随任务复杂度上升而放大。

5.7 效率指标：成本和时间双降

除了求解率，论文还在"困难子集"上比较了效率。困难子集定义为：按三种方法平均成本取 top 25% 的任务（Verina n=48，AlgoVeri n=20，Lean4Commit0 n=27）。

Table 5 摘要（困难子集）：

• 每任务 API 成本降低：3.0% – 39.6%
• 墙上时间降低：3.1% – 37.2%

更具体地说：

• P³ 在每一个（基准, 模型）单元上都是最便宜且最快的方法。
• 最大成本节省出现在 Verina 和 AlgoVeri（最高约 40% / 37%）。
• Lean4Commit0 的时间缩减空间较小——因为三种方法在仓库级任务上常接近 180 分钟上限，都比较吃力。

效率提升的根源：论文做了 trace 分析，发现 Seq 的成本主要来自"全量重启修复"（full-restart repair）——局部修复在已提交程序下失败后，Agent 会重写代码和证明两个产物。而 P³ 在细化前就检查结构一致性，重启频率显著更低。

一个值得注意的细节：在"已解决交集"（all-solved intersection）上，P³ 与基线大致可比，甚至在较简单的单元上能看到可见的规划开销（planning overhead）。这说明 P³ 的效率优势主要来自"避免无效的修复循环"，而不是"每次都更快"。

5.8 案例研究：两个典型任务

论文给了两个案例研究，直观展示 P³ 的优势。

案例 1：左倾红黑树删除（AlgoVeri）

这是一个经典但极难的算法。三种方法的表现：

P³ 的优势在于：它在规划阶段就比较了两条路线的证明负担，选了证明更简单的"重建路线"，避免了 Seq 那种"埋头干到一半才发现路走错"的浪费。

案例 2：Memchr（Lean4Commit0）

这是一个三 API 关系任务。在相同后端和预算下，仅 P³ 解决——Plain 和 Seq 都失败了。这直接印证了"跨 API 关系规范需要联合规划"的论点。

5.9 指标如何证明论文的核心主张

汇总一下，P³ 的实验设计如何支撑其核心主张：

整体看，这套实验设计是严谨的：不仅有主实验（Table 2），还有消融（Table 3）、效率分析（Table 5）、规划质量分析（存留率）、定性案例（红黑树、Memchr）。多角度证据交叉验证了 P³ 的有效性。

六、效果优势的根源解释

6.1 baseline（Seq）的根本局限：结构错配

要理解 P³ 为什么更优，先要精确定位 Seq 的根本局限。

Seq 是一个顺序流水线：先写程序，再写证明。它的根本问题不是"效率低"，而是结构性错配（structural mismatch）。具体而言：

Seq 在写程序时，优化目标是"实现功能"——LLM 会选择它认为最自然、最简洁、最高效的实现方式。但这个选择完全没有考虑"这段代码将来怎么证明"。

这就导致了一个不可逾越的障碍：一旦程序结构选定，证明的难度就被"锁死"了。如果程序用了一个证明敌对的结构（如 List.foldl 累加器、复杂的循环不变式、不可计算的辅助函数），那么无论后续用多少轮修复，都救不回来——因为问题不在证明本身，而在程序结构。

这就像盖楼时：施工队按"施工方便"把承重墙放在了 X 位置，等质检员来验收才发现"X 位置的承重墙无法满足抗震论证"。这时候你只能拆楼重建，而不是"修一修"。

Seq 的"全量重启修复"就是这个拆楼重建——Agent 重写代码和证明两个产物。这不是效率问题，是结构问题。

6.2 P³ 的根本改变：约束结构的"前置"

P³ 的根本性改变，不是"加了一个规划阶段"，而是把对证明可验证性的约束，从"事后修补"前置到了"结构设计阶段"。

具体追溯这个因果链：

1. 方法差异：Seq 在写程序时无证明约束；P³ 在写程序之前就通过 ρ 同时约束程序结构和证明结构。
2. 机制变化：ρ 强制要求"程序分解"和"证明义务"互相契合——证明的归纳骨架必须对应程序的递归骨架，桥接谓词必须能蕴含 Q。
3. 缓解的瓶颈：这从源头消除了"可执行但不可验证"的程序结构。LLM 不能再选一个"证明敌对"的实现，因为这样的实现会在规划阶段就被草图级验证拒绝。
4. 体现在指标上：
   • 求解率提升（Table 2）：因为避免了结构错配导致的失败。
   • 成本下降（Table 5）：因为重启频率降低。
   • 计划存留率 92.9%：因为规划阶段选出的 ρ 确实能走到最后。

6.3 反事实推理：如果去掉"联合"

消融实验（Table 3）就是一次完美的反事实推理：Plan-Seq 是"去掉联合"的版本——它允许规划程序，但禁止规划证明。

结果很有意思：

• 在简单题（Verina）上，Plan-Seq 比 Seq 略好（69.8 vs 68.3）——规划程序有点用。
• 在中等题（AlgoVeri）上，Plan-Seq 比 Seq 好不少（44.8 vs 40.3）——规划程序确实有用。
• 但在 Lean4Commit0 上，Plan-Seq 反而比 Seq 差（13.9 vs 17.6）！

为什么？因为 Lean4Commit0 是关系规范任务——单个 API 的实现再合理，如果它的结构和其它 API 的证明义务不匹配，关系定理就证不出来。Plan-Seq 允许你"独立规划每个 API 的实现"，但这种"独立合理的实现"可能无法在关系定理下连接。

这个反事实直接证明：“规划"本身不够，必须是"联合规划”。P³ 相对 Plan-Seq 的 +3.3 到 +8.3 个百分点，完全是"联合"这个词的贡献。

6.4 优势根源汇总

把上述分析汇总成一张因果链表：

核心一句话：P³ 的优势不是"更努力"，而是"结构上必然更好"。它把对证明可验证性的考虑，从"事后修补"前置到了"结构设计"，从源头消灭了 baseline 不可逾越的障碍。

七、必要知识反推

要做出 P³ 这篇论文，作者最少必须掌握哪些知识？我们逐层反推。

7.1 领域知识层

1. 形式化验证与 Lean 定理证明器

不掌握 Lean，就根本无法理解"为什么证明这么难"。Lean 的 tactic 搜索空间、sorry 占位符、LSP 协议、归纳策略——这些都是论文方法直接操作的对象。论文作者 Kaiyu Yang 是 Verina 的核心作者，对 Lean 有极深的工程理解。

为什么必须：不理解 Lean，就无法设计"在 Lean 反馈下迭代细化"的工作流，也无法判断"什么样的程序结构证明友好"。

2. 程序正确性证明的经典范式

论文直接引用了 Dijkstra 1976 年的《A Discipline of Programming》，并以"correct-by-construction"为方法命名。这要求作者熟悉 Floyd-Hoare 逻辑、最弱前置条件、循环不变式、桥接谓词等经典概念。

为什么必须：ρ 的四项承诺（合约、程序分解、库依赖、证明义务）每一项都对应着经典程序验证的一个核心要素。没有这套语言体系，根本无法描述"什么是程序-证明共享计划"。

3. 软件仓库结构与 API 协同

Lean4Commit0 不是凭空构造的——它需要作者理解真实软件仓库的结构：什么是核心 API、什么是配置/查询的优先级关系、什么是跨 API 的协同语义。

为什么必须：不理解真实软件的 API 协同，就无法构造出 Fabric 的 set/get 关系规范这种"非孤立的验证任务"。

7.2 方法论知识层

4. LLM Agent 工作流设计

P³ 是一个 Agent 工作流——它涉及规划、细化、失败分类、子代理派遣。这要求作者熟悉 Agent 系统的设计模式：主从代理分工、结构化反馈、迭代修复、技能包（skill package）等。

为什么必须：不掌握 Agent 工作流，就无法把 Dijkstra 的哲学落地为可执行的算法。

5. 现有验证代码生成基线

作者必须熟悉 Plain、Seq、Lean 4 Skills 等基线方法的细节，才能设计出合理的对比实验。论文里 Plan-Seq 这个消融的设计，尤其体现了对"现有规划方法为什么不 work"的深刻理解。

为什么必须：不做这个消融，就无法证明"联合"这个词的必要性。

6. 评测基准设计与质量门控

Lean4Commit0 的三重质量门控（不可满足、欠约束、空洞）体现了作者对基准设计方法论的掌握——突变测试、LLM-as-judge、规约充分性的形式化检查。

为什么必须：不做质量门控，从 GitHub 抓来的规范可能根本等价于原项目的语义，基准就失去了意义。

7.3 工程知识层

7. Lean LSP MCP 集成

P³ 的 Agent 通过 Lean LSP MCP 与 Lean 编译器交互。这要求作者知道如何把 Lean 嵌入到 Agent 的工具调用循环里。

为什么必须：没有这个工程基础，Agent 就无法实时获取 Lean 的错误反馈。

8. 跨语言代码翻译

Lean4Commit0 涉及 Python、Rust、C/C++、Java 到 Lean 的翻译。这要求作者理解不同语言的语义差异，以及如何把这些语义映射到 Lean 的依赖类型系统。

为什么必须：不掌握跨语言翻译，就无法构造一个跨四大生态系统的仓库级基准。

9. 大规模实验编排

论文跑了 4 个模型 × 3 个基准 × 3 个方法 = 36 个单元的实验，每任务预算 30 USD、180 分钟。这要求精细的 Docker 镜像管理、API 预算控制、并行编排。

为什么必须：实验规模一旦失控，结果不可复现。

7.4 知识融合的关键节点

这些知识不是简单叠加的。P³ 的创造性来自几个关键的融合节点：

融合节点 1：Dijkstra 哲学 × LLM Agent

Dijkstra 的"程序-证明携手开发"是一句哲学口号，50 年来未被工业落地。P³ 的创造性在于：把它翻译成了 LLM Agent 可以执行的具体算法（规划 → 细化 → 失败分类）。没有对 Dijkstra 的深刻理解，想不到这个起点；没有对 Agent 工作流的掌握，落不了地。

融合节点 2：桥接谓词 × 共享计划 ρ

桥接谓词是经典程序验证的概念，共享计划是 Agent 工作流的概念。P³ 把两者融合为"ρ 的证明义务承诺"——桥接谓词不再是写证明时才想到的技巧，而是在规划阶段就必须显式命名的结构承诺。这种融合让 Dijkstra 的"证明略先于程序"变得可操作。

融合节点 3：突变测试 × LLM-as-judge × 规约质量

Lean4Commit0 的质量门控是三种技术的融合：突变测试（来自软件工程）+ LLM 审查（来自 LLM 评测）+ 参考满足（来自形式化验证）。单独哪一个都不够——突变测试无法检测空洞，LLM 审查无法检测欠约束，参考满足无法检测非平凡性。三者融合才构成了一个可信的质量门。

融合节点 4：跨 API 关系规范 × Lean 形式化

Fabric 的 set/get 关系规范，要求作者同时理解"真实软件的配置优先级语义"和"Lean 的全称量化表达力"。这是软件工程实践与形式化方法的交叉点——单独任何一边都构造不出这种任务。

八、论文中可以提取的通用性灵感

P³ 这篇论文虽然是关于验证代码生成的，但它蕴含的几条原理有更强的普适性，可以推广到其它领域。

8.1 灵感一：把"事后约束"前置为"事前规划"

核心思想：当一个产物的可接受性（如可证明性、可测试性、可维护性）本质上依赖于它的结构时，不要试图在产物完成后再约束，而应该在结构设计阶段就把约束前置。

论文证据：P³ 把"证明可验证性"从"写完程序后修补"前置到"规划阶段同时约束程序和证明"。结果：求解率提升 4.6–11.2 个百分点，Plan-Seq（只规划程序）在 Lean4Commit0 上反而变差。

推广场景：

1. 代码可测试性：写代码时不考虑可测试性，写完再补测试会很痛苦。应该在架构阶段就把"模块可独立测试"作为约束。
2. API 可文档化：API 实现时不考虑文档化，发版后再写文档会漏掉设计意图。应该在 API 设计阶段同步产出文档契约。
3. 机器学习模型可解释性：训练完再追求可解释性（post-hoc explanation）常被批评为"自欺欺人"。应该在模型设计阶段就嵌入可解释结构（intrinsic interpretability）。
4. 产品可访问性（accessibility）：开发完再补无障碍支持，常需要重构 UI。应该在设计阶段就遵循无障碍规范。
5. 数据管道可监控性：上线后再加监控会发现关键埋点缺失。应该在系统设计阶段就规划监控点。

8.2 灵感二：联合规划优于顺序流水线（当产物耦合时）

核心思想：当两个产物（如程序和证明、前端和后端、产品定义和测试计划）存在结构性耦合时，把它们放在一个顺序流水线里（先 A 后 B）会导致结构错配；应该在共享计划下同步规划两者。

论文证据：P³ 的联合规划比 Seq（顺序流水线）提升 4.6–11.2 个点；比 Plan-Seq（只规划 A）提升 3.3–8.3 个点。尤其在 Lean4Commit0 的跨 API 关系任务上，“独立合理的实现"反而无法连接。

推广场景：

1. 前后端协同：先后端定义 API、再前端实现，常导致 API 与前端需求错配。应该在接口契约（如 OpenAPI）层联合规划。
2. 硬件-软件协同设计：先做硬件再做软件，常发现硬件不支持软件需要的关键操作。应该在 ISA 层联合规划。
3. 产品-测试协同：先写产品代码再写测试，常发现某些路径无法测试。应该在 TDD/BDD 层联合规划。
4. 法律合同-履行流程协同：先签合同再设计履行流程，常发现条款无法落地。应该在合同起草阶段联合规划。
5. 学术论文-实验协同：先写方法再跑实验，常发现实验无法区分方法优劣。应该在方法设计阶段联合规划实验对照组。

8.3 灵感三：失败的层级化分类（避免无效重启）

核心思想：当一个迭代系统遇到失败时，不要无差别地"全量重启”。应该先判定失败的层级（局部问题 vs 结构问题），只在该层修复；只有结构问题时才退回更高层重规划。

论文证据：P³ 把失败分为"细化级"（局部修复）和"计划级"（退回规划）。Seq 的全量重启成本爆炸，P³ 的层级化处理让成本最高降 40%。

推广场景：

1. 编译器错误修复：不要每次出错就重写整个函数。应该区分"语法错误"（局部修复）和"设计错误"（重构）。
2. 运维故障处理：不要每次告警就重启服务。应该区分"瞬时抖动"（局部缓解）和"架构瓶颈"（架构调整）。
3. 学生辅导：不要学生做错题就让他重学整章。应该区分"知识点遗漏"（补这一个点）和"前置知识缺失"（回到基础）。
4. 代码 review：不要每次发现问题就要求重写整个 PR。应该区分"风格问题"（局部修）和"架构问题"（重新设计）。
5. 科研实验调试：不要实验失败就推倒重来。应该区分"操作失误"（重做实验）和"假设错误"（修正假设）。

8.4 灵感四：基准设计要逼近真实复杂度（含关系规范）

核心思想：一个好的评测基准不应该只覆盖"孤立任务"，还应该覆盖关系任务——多个组件协同才能解决的任务。因为真实世界的复杂度，更多来自组件间的关系而非单个组件的难度。

论文证据：P³ 提出 Lean4Commit0，特意包含跨 API 关系规范（如 Fabric 的 set/get 优先级）。结果发现：Plan-Seq（在孤立任务上有效的"只规划程序"）在关系任务上反而有害，揭示了孤立评测会掩盖的失败模式。

推广场景：

1. 自动驾驶评测：不能只评测单辆车的行为，还要评测多车交互（如无保护左转、合流）。
2. 代码 review 工具评测：不能只评测单文件 review，还要评测跨文件、跨模块的语义一致性检查。
3. 多轮对话评测：不能只评测单轮回复质量，还要评测多轮一致性、记忆保持、话题切换。
4. 检索系统评测：不能只评测单 query 召回，还要评测 session 内的 query 序列、用户兴趣演化。
5. Agent 评测：不能只评测单步决策，还要评测长程任务中的子任务协同、错误恢复。

8.5 灵感五：经典哲学思想可以是创新的源泉

核心思想：在被工程化奉为圭臬的领域，回溯到该领域的经典哲学源头，常常能找到解决当代问题的钥匙。50 年前的智慧可能因为工具不够而未被落地，但今天的工具（如 LLM）可能让它起死回生。

论文证据：P³ 直接引用 Dijkstra 1976 年的洞察作为方法命名（“Joint Program-and-Proof Planning”），把一个 50 年前未能落地的哲学，用 LLM Agent 现代化为可执行的工作流。

推广场景：

1. MVC 模式：1970 年代的 Smalltalk 哲学，在前端框架时代重新焕发活力。
2. Lisp 的同像性（homoiconicity）：1950 年代的思想，在宏系统、可微分编程里重新被重视。
3. Actor 模型：1970 年代的并发模型，在 Erlang/Akka 等现代并发系统里落地。
4. 敏捷宣言：长期被"伪敏捷"掩盖，回溯原始价值观常能找回本质。
5. 教育学里的"建构主义"：Piaget/Vygotsky 的理论，在 AI 辅助学习时代有了新的工具支撑。

附录：关键术语速查

• 验证代码生成（Verified Code Generation）：让 LLM 同时生成代码、规范、证明，三者必须同时通过 Lean 检查。
• Lean：一门同时支持编程和证明的语言，其最小可信内核保证了被接受的证明绝对正确。
• 规范（Specification）：形式化描述代码应满足的数学性质，含前置条件 P（输入约束）和后置条件 Q（输入-输出关系）。
• 证明（Proof）：用 Lean 的 tactic 语言编写的数学论证，证明代码满足规范。
• 共享计划 ρ（Shared Plan）：P³ 的核心对象，同时约束程序结构和证明结构的四项承诺。
• 桥接谓词（Bridging Predicate）：比后置条件 Q 更强的中间断言，用于桥接程序分解和证明目标。
• 细化级失败 / 计划级失败：P³ 的失败分类。细化级可局部修复，计划级需退回规划。
• Lean4Commit0：P³ 提出的仓库级基准，108 库 1030 占位符，含跨 API 关系规范。
• Plan-Seq：消融变体，只规划程序不规划证明。在 Lean4Commit0 上反而比 Seq 差。
• Plain / Seq：两个主要基线。Plain 不引导工作流，Seq 是"先程序后证明"的顺序流水线。

精读总结：P³ 把 Dijkstra 50 年前的"程序-证明携手开发"哲学，落地为 LLM Agent 的"联合规划 + 计划下细化"工作流。它的核心创新不是"加了规划"，而是把规划的对象扩展为程序和证明的联合体——通过共享计划 ρ 同时约束两者的结构，从源头消除"可执行但不可验证"的程序结构。实验上，P³ 在 Verina/AlgoVeri/Lean4Commit0 三个基准的全部 12 个（基准, 模型）单元中均获最高求解率，绝对增益 4.6–11.2 个百分点，困难子集上成本最高降 40%、时间最高降 37%。消融实验进一步证明：去掉"联合"的 Plan-Seq 在关系规范任务上反而比 Seq 更差——这直接验证了"联合规划"而非"规划本身"才是关键。P³ 还贡献了 Lean4Commit0 这一从真实仓库提炼的库级基准，把验证代码生成的评测从"教科书题"推向了"真实软件"。更一般地，P³ 揭示了一条普适原理：当两个产物存在结构性耦合时，把它们放在顺序流水线里必然导致结构错配；正确的做法是在共享计划下同步规划两者。这条原理远超验证代码生成本身，可推广到前后端协同、软硬协同、产品测试协同等众多场景。