P³：面向可验证代码生成的程序-证明联合规划

可验证代码生成要求大语言模型（LLM）同时生成可执行程序和证明程序满足形式化规范的机器可检查证明，有望实现构造即正确的软件。事实上的标准工作流将问题的两半解耦：先合成程序，再尝试证明其正确。我们观察到这种顺序流水线在实践中既低效又无效。未预见其证明而生成的程序可能有微妙错误或在结构上难以验证，迫使 LLM 陷入在修补代码与修补证明之间交替的脆弱修复循环。受 Dijkstra 关于程序与其正确性论证应同步开发的观点启发，我们提出 $P^3$，一个基于 LLM 的 agentic 工作流：先从规范推导出统一的程序-证明计划，再在该共享计划下细化实现与证明骨架。为了在现实场景中评估可验证代码生成，我们进一步提出 Lean4Commit0，一个源自仓库的库级基准，通过从真实软件仓库提取核心 API 并将其需求（包括跨 API 的关系规范）翻译为 Lean 任务而构建。使用四个前沿 LLM 后端，我们在 Verina、AlgoVeri 和我们的 Lean4Commit0 基准上评估 $P^3$，它在每个基准-模型设置中都取得最高求解率。与更强的基线相比，它将求解率提升 4.6-11.2 个百分点，并在每个基准的困难子集上将每任务 API 成本最多降低约 40%、墙钟时间最多降低约 37%。一项针对性消融进一步显示相较仅规划实现的方案提升 3.3-8.3 个百分点，分离出联合规划程序与证明的收益。