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

会议: NeurIPS 2026
arXiv: 2608.09277
OpenReview: https://openreview.net/forum?id=hIC9ua4c4q
代码: https://figshare.com/s/2ab7020cacaffcf0d258
领域: 代码智能
关键词: 形式化验证, 代码生成, 联合规划, Lean 4, 证明引导

一句话总结

针对传统“先写程序后补证明”导致代码与归纳结构脱节的瓶颈，提出程序与证明联合规划框架 \(P^3\)，先共谋计算分解与桥接谓词再执行精化，并在新提出的真实软件库级基准 Lean4Commit0 上取得显著超越 baseline 的求解率与效率。

研究背景与动机

随着大语言模型在代码生成领域的飞速发展，生成目标已从自动补全代码片段演进到完整函数乃至仓库级开发。与此同时，以 Lean 4 为代表的交互式定理证明系统逐步走向实用，为构建兼具可执行实现与机器可检查正确性证明的软件提供了底层环境。形式化验证代码生成（Verified Code Generation）在此背景下应运而生：模型被要求在给定形式化规范下，同时合成可执行程序及其机器可检查证明，从而在逻辑内核层面对所有合法输入提供严格正确性保证，避免有限测试用例覆盖不足所带来的安全与可信隐患。

然而，现有形式化代码生成框架大体遵循解耦的“先程序后证明”（program-then-proof）流水线，即 LLM 先固化具体代码实现，再调用自动化求解器或证明智能体搜索验证证书。这种单向串行时序面临严重的结构性矛盾：一个在语义外延上满足规范的程序，其控制流或数据结构若未预先考虑证明需求，往往欠缺自然的循环不变式或归纳结构；验证失败时模型被困在脆弱的局部修补回环中，在代码补丁与证明补丁间反复震荡。甚至在探索大量候选修补后，由于最初固化的代码结构本质上难以证明，导致海量 token 与时间预算被彻底浪费。

本文回归 Dijkstra 提出的经典程序设计思想——程序的结构与正确性论证应当“携手并进”（hand in hand）协同设计。若能在生成具体代码和证明之前，先在高级抽象层对两者的结构进行联合规划，就能从根源上规避结构失配与事后无效修补。核心 idea：构建程序与证明联合规划框架 \(P^3\)，首先从形式化规范推导出包含计算分解与桥接归纳谓词的共享结构规划，进而在该共享规划引导下协同精化实现代码与证明骨架，实现“由构造保证一致性”。

方法详解

整体框架

\(P^3\) 是一个基于 Lean 4 环境的智能体工作流。系统输入为目标函数或 API 集合的形式化规范 \(\sigma = (P, Q)\)（包含前置条件 \(P\) 与后置条件 \(Q\)），输出为可执行程序 \(\pi\) 以及可被 Lean 4 内核检查的证明证书 \(\kappa\)。整个流程分为两大阶段：联合规划（Joint Planning）与引导精化（Plan-Guided Elaboration）。在规划阶段，模型生成并筛选出同时具备代码分解结构与桥接证明草图的共享规划 \(\rho\)；在精化阶段，模型根据 \(\rho\) 生成具体实现代码与证明骨架，随后基于 Lean LSP/MCP 反馈闭合证明叶节点，并根据验证反馈在精化级修补与规划级重构之间精准路由。

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}, 'subGraphTitleMargin': {'top': 8, 'bottom': 16}}}%%
flowchart TD
    A["输入规范 σ=(P, Q)<br/>前置条件 P 与后置条件 Q"] --> B["联合规划阶段<br/>提出候选计划并验证承诺"]
    B --> C["共享结构规划 ρ<br/>冻结分解/桥接谓词/辅助引理"]
    C --> D["规划引导精化阶段<br/>生成代码 π 与证明骨架 κ"]
    D --> E["Lean 4 内核反馈验证<br/>检查目标定理与证明叶节点"]
    E -->|局部报错/叶节点未闭合| F["精化级局部修补<br/>保持规划结构不变"]
    F --> E
    E -->|桥接谓词过弱/规划失效| G["规划级横向重构<br/>回退至规划阶段重新推导"]
    G --> B
    E -->|内核完全接受| H["输出已验证软件 (π, κ)<br/>实现与机器证明双闭合"]

关键设计

1. 联合规划：预先绑定四项结构性承诺 传统流水线在编写代码时不感知证明负担，极易选出虽然代码紧凑但证明极难的实现模式（如以 List.foldl 实现最大值检索，会迫使后续证明必须凭空发现并强化针对任意累加器的通用不变式）。联合规划通过在高级规划 \(\rho\) 中显式冻结四项跨代码与证明的结构性承诺来消除这一盲区：一是形式化契约与渐近复杂度指令；二是程序的具体分解策略（如递归变量、分支解构方式、终止性度量 termination_by）；三是依赖的 Lean 标准库与 Mathlib 现有引理；四是核心证明义务，包括连接前后置条件的桥接谓词（bridging predicate）、归纳策略以及显式命名的辅助引理声明。规划智能体在草图层面上评估候选方案，主动剔除违反复杂度约束或桥接谓词推导负担过重的解法，选择证明负担最小的结构作为冻结规划 \(\rho\)。

2. 规划引导精化：代码与证明骨架的协同展开 在冻结规划 \(\rho\) 指引下，精化阶段不再是盲目的端到端搜索，而是结构严格受约束的代码与证明实例化过程。对于程序实现，智能体严格沿用 \(\rho\) 所规定的控制流分解（如结构递归而非折叠算子），禁止在实现阶段临时切换算法；对于证明证书，智能体同步构建匹配该结构的证明脚手架，包括顶层定理框架、计划中声明的辅助引理签名以及顶层归纳步骤，而将各归纳分支的具体战术填充留为 sorry 叶节点。此时的证明补全被降维为局部目标闭合问题，智能体借助 Lean 4 LSP/MCP 提供的精确目标上下文与类型错误信息，逐个消解叶节点，避免因证明结构方向错误导致全盘推翻。

3. 双层故障诊断与受控回退路由 将生成拆分为规划与精化两层后，编译与证明器的二元报错得以转化为结构化的故障定位信号。系统将验证失败精准解耦为两类：精化级失败（Elaboration-level failure）指在当前规划下某一分支缺失具体战术、桥接步骤存在微小推导缝隙或实现语法微调，智能体限定在固定轮次和候选预算内进行原地修补；规划级失败（Plan-level failure）则在局部修补连续陷入死循环、或 Lean 反馈暴露当前桥接谓词本质过弱（必须引入未规划的全新算法或不变量）时触发。一旦判定为规划级失败，智能体坚决放弃当前代码与证明，执行横向回退（horizontal pivot），重新生成并评审新的规划 \(\rho\)。这种明确的回退切入点从机制上终结了“在死胡同代码上盲目修补证明”的高耗能抖动。

一个完整示例

以非空整数列表最大值函数 listMax 为例：若采用“先代码后证明”，模型通常写出紧凑的 xs.foldl max xs.head!（Version B）。但在后续证明中，后置条件 \(\forall z \in xs, z \le \text{listMax}(xs)\) 无法直接由归纳法推出，必须凭空强化出对任意累加器初始值 \(init\) 均成立的通用引理： $\(ys.\text{foldl}\ \max\ init \in init :: ys \ \land\ \forall z \in init :: ys,\ z \le ys.\text{foldl}\ \max\ init\)$ 在缺乏预先规划时，LLM 极难自行泛化出这一脱离原规范的引理，常在主定理证明中陷入无尽死循环，最终被迫整体推翻重写。 而在 \(P^3\) 的规划阶段，模型同时评估 Version B 与基于列表结构模式匹配的递归方案 Version A（即 | [x], _ => x 与 | x::y::t, _ => max x (listMax (y::t) ...)）。规划器发现 Version A 的控制流直接天然镜像后置条件，后置条件本身即可充当桥接谓词，归纳假设可直接作用于尾列表，完全无需额外的不变量强化引理。因此 \(P^3\) 在规划阶段直接冻结 Version A，精化阶段仅需顺次闭合单元素与双元素归纳分支，以极低的代码行数和零回退成本一次性通过 Lean 4 内核检查。

实验关键数据

主实验

评估在经典算法函数级基准 Verina（189 题）、AlgoVeri（77 题）以及本文构建的真实软件库级基准 Lean4Commit0（108 个库、1030 个占位符）上开展，对比无策略 prompt 的 Plain 基线、顺序执行的 Seq 基线（program-then-proof）与 \(P^3\)。各模型在 30 美元 API 预算与 180 分钟超时限制下单次运行，求解率统计如下（要求通过 Lean 内核检验且符合算法指令）：

基准数据集	底座模型	Plain 基线 (%)	Seq 基线 (%)	本文 \(P^3\) (%)	绝对提升 \(\Delta\) (%)
Verina	Codex-GPT-5.5	72.0	67.7	77.2	+5.2
Verina	Gemini-3-Pro	59.3	60.8	72.0	+11.2
Verina	Claude-Sonnet-4.6	64.0	61.9	73.0	+9.0
Verina	Claude-Opus-4.7	68.8	68.3	74.6	+5.8
AlgoVeri	Codex-GPT-5.5	36.4	33.8	44.2	+7.8
AlgoVeri	Gemini-3-Pro	33.8	31.2	39.0	+5.2
AlgoVeri	Claude-Sonnet-4.6	35.1	32.5	40.3	+5.2
AlgoVeri	Claude-Opus-4.7	39.0	40.3	48.1	+7.8
Lean4Commit0	Codex-GPT-5.5	11.1	13.0	18.5	+5.5
Lean4Commit0	Gemini-3-Pro	09.3	11.1	15.7	+4.6
Lean4Commit0	Claude-Sonnet-4.6	10.2	13.0	17.6	+4.6
Lean4Commit0	Claude-Opus-4.7	13.9	17.6	22.2	+4.6

消融实验

为确认增益来自于“程序与证明的联合规划”而非单纯的“增加了规划步骤”，论文设计了 Plan-Seq 变体——该变体仅对程序实现的算法与分解进行规划，但严禁在写代码前预测不变量、证明解构或辅助引理，随后运行标准的程序后证明流程。使用 Claude-Opus-4.7 的求解率对比表明，联合规划具有不可替代的价值：

配置	Verina (%)	AlgoVeri (%)	Lean4Commit0 (%)	说明
Plain 基线	68.8	39.0	13.9	朴素智能体交互
Seq 基线	68.3	40.3	17.6	标准先程序后证明
Plan-Seq（仅规划实现）	69.8	44.8	13.9	缺乏证明预测，跨 API 关联显著退化
本文 \(P^3\)（联合规划）	74.6	48.1	22.2	联合规划全面最优，比 Plan-Seq 高 3.3-8.3%

关键发现

• 联合规划相比单纯实现规划的决定性收益：在 Lean4Commit0 上，Plan-Seq 求解率（13.9%）甚至显著低于没有实现规划的 Seq（17.6%）。这是因为在多 API 关系规约下，脱离共享证明义务而仅凭“直觉”做出的独立实现决策，往往导致多 API 之间的关联定理在数学上变得极难闭合；唯有 \(P^3\) 联合推导才能使跨 API 的关系规约成立。
• 高难度子集上的消耗与耗时大幅缩减：对三大基准中平均成本前 25% 的高难度题目分析显示，\(P^3\) 在所有模型和基准组合中均实现最低调用成本与最短耗时，单个任务成本相比强基线降低 3.0% 至 39.6%，耗时缩减 3.1% 至 37.2%。这归功于 \(P^3\) 避免了 Seq 频繁发生的“整套推翻重写（full restart）”——在 Verina 与 AlgoVeri 上，\(P^3\) 的完全重写率较 Seq 降低了 2 到 4 倍。
• 规划的极高保留率：在 Verina 上使用 Claude-Opus-4.7 的全部 141 个成功案例中，有 92.9%（131 例）从始至终保留了初始联合规划，仅有 7.1% 在中途更换规划，验证了预先规划的高可用性与决策准确性。

亮点与洞察

• 将 Dijkstra 程序正确性共谋理论落地为 LLM Agent 规范：首次在神经定理证明与代码生成中，把经典形式化方法中“规范与证明共同决定程序形态”的思想具象化为四项冻结承诺与双层回退机制，为 Verified Code Generation 确立了新的工作流范式。
• 库级关系规约基准 Lean4Commit0：突破了传统单函数小算法的玩具评测局限，涵盖 108 个真实开源库，首次引入多 API 联动的关系规范，并通过“参考实现满足性、代码变异拒绝率、LLM 空洞审查”三道自动化质量门禁确保了规约的高严谨性。
• 从无序局部修补转变为分层故障诊断：将 Lean 编译器的报错信息显式解耦为“精化层局部调优”与“规划层架构重构”，并设立了严格的横向回退触发条件，为长程复杂证明搜索提供了极为高效的探索策略。

局限与展望

• 当前受限于单形式化后端与闭源模型：目前 \(P^3\) 机制仅在 Lean 4 及前沿闭源底座（Codex-GPT-5.5、Gemini-3-Pro、Claude 系列）上验证，尚未拓展至 SMT 体系（Dafny、Verus）或开源小模型/专用形式化模型上。
• 库级规范提取尚偏向 Python 核心 entrypoint：Lean4Commit0 的提取主要关注核心 API，难以全面覆盖具有深层长程系统依赖、动态复杂构建或重度并发的现实工程。
• 未来方向：探索将 \(P^3\) 思想泛化到 Dafny、Rust Verus 等 SMT 自动化验证系统，将循环不变式与 Ghost 代码同样纳入联合规划，并结合强化学习在规划空间进行偏好对齐。

相关工作与启发

• vs Seq 类形式化代码生成框架（如 WybeCoder、Goedel-Code-Prover、AutoVerus）：现有方法均在固定实现的前提下搜索证明或修补注解，极易因实现结构不亲和证明而引发长期无意义修补；\(P^3\) 在编写代码前完成结构共谋，将一致性提前至构造阶段。
• vs 纯证明分解框架（如 Planning to Hammer、DeepSeek-Prover-V2）：已有基于规划的定理证明研究仅在固定目标定理后对证明目标（subgoals）进行分解，不涉及可执行程序的协同设计；\(P^3\) 则处理双目标约束，在满足可执行算法复杂度的同时最小化证明义务。

评分

• 新颖性: ⭐⭐⭐⭐⭐ 首次提出程序与证明联合规划范式，突破了解耦的串行生成瓶颈。
• 实验充分度: ⭐⭐⭐⭐⭐ 覆盖三大基准、四大前沿大模型，消融实验与高难度子集分析极其扎实。
• 写作质量: ⭐⭐⭐⭐⭐ 逻辑结构严谨连贯，运行示例（listMax）与理论动机呼应极为清晰。
• 价值: ⭐⭐⭐⭐⭐ 为大模型走向高可靠、高确定性的形式化软件工程提供了极具启发性的系统架构。

相关论文

• [NeurIPS 2026] Property-Guided LLM Program Synthesis for Planning
• [ICML 2026] AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms
• [ACL 2026] PaT: Planning-after-Trial for Efficient Test-Time Code Generation
• [NeurIPS 2026] DCVD: Dual-Channel Cross-Modal Fusion for Joint Vulnerability Detection and Localization
• [NeurIPS 2026] Constrained Code Generation with Discrete Diffusion