Certified Program Synthesis with a Multi-Modal Verifier

1. 研究背景与问题 (Problem)

认证程序合成 (Certified Program Synthesis / Vericoding) 是指从自然语言描述的任务中，自动生成程序、形式化规范（Formal Specification）以及机器可验证的正确性证明的过程。尽管大语言模型（LLM）在代码生成方面取得了进展，但实现端到端的认证合成仍面临两大核心挑战：

1. 规范质量难以保证 (Specification Quality):
   • 从自然语言生成的规范往往要么太弱（允许错误的实现通过），要么太强（排除了所有正确的实现）。
   • 现有方法缺乏系统性的手段来检测并修正这些缺陷。作者发现，在现有的基准测试（如 VERINA 和 CLEVER）中，约 10% 的参考规范本身存在缺陷。
2. 验证器生态碎片化 (Fragmented Verifier Landscape):
   • 现有的程序验证工具主要分为两类：
     • 自动激活式 (Auto-active): 如 Dafny, Verus。依赖 SMT 求解器，自动化程度高但表达能力有限，难以处理复杂证明。
     • 交互式 (Interactive): 如 Lean, Rocq。表达能力极强，但需要大量人工编写证明脚本，自动化程度低。
   • 现有的合成方法通常针对单一验证范式构建，导致工作流、提示策略和反馈循环被工具细节深度绑定，难以跨工具迁移，且无法灵活应对不同难度的子任务。

2. 方法论 (Methodology)

为了解决上述问题，作者提出了 LeetProof，这是一个基于多模态验证器 (Multi-Modal Verifier) 的代理流水线（Agentic Pipeline）。其核心思想是将认证合成分解为多个阶段，每个阶段匹配最合适的验证模式（测试、SMT 自动化、交互式证明）。

2.1 核心架构：LeetProof 流水线

LeetProof 构建在 Velvet 之上，Velvet 是一个嵌入在 Lean 定理证明器中的多模态程序验证库。流水线分为三个主要阶段：

1. 规范合成 (Specification Synthesis):

   • LLM 根据自然语言描述生成形式化规范（前置/后置条件）及测试用例。
   • 关键创新： 引入随机化规范测试 (Randomized Specification Testing)。在生成代码前，利用基于属性的测试（PBT, Property-Based Testing）验证规范。
     • 检查前置条件是否被满足。
     • 检查生成的输入/输出对是否满足后置条件。
     • 唯一性检查 (Uniqueness Check): 确保规范没有过于宽松（即不存在其他非预期的输出也能满足规范）。
   • 如果 PBT 发现反例，LLM 会修正规范。这比纯符号化验证（SMT）在 Lean 中成本更低且更有效。

2. 程序与不变量合成 (Program & Invariant Synthesis):

   • LLM 生成 Velvet 代码（命令式程序）并推断循环不变量（Loop Invariants）。
   • 多模态验证：
     • 首先尝试 SMT 自动化（SMT-based tactics）验证生成的不变量。
     • 对于 SMT 无法处理的验证条件 (VCs)，使用 PBT 在运行时寻找反例。
     • 如果 PBT 发现不变量不成立（如图 5 所示的错误案例），反馈给 LLM 进行修正。
   • 此阶段的目标是生成“高置信度”的不变量，而非完全证明。

3. 证明合成与剩余义务处理 (Proof Synthesis & Residual Obligations):

   • 生成最终的机器可验证证明。
   • 首先尝试完全自动化（SMT + Lean 内置策略如 grind, aesop）。
   • 对于自动化无法关闭的“剩余义务”（Residual Obligations），利用 LLM 代理进行分解，或委托给前沿 AI 证明器（如 Aristotle）进行交互式证明。
   • 设计原则： 将昂贵的交互式证明保留在最后阶段，前期利用廉价的测试和 SMT 进行过滤。

2.2 技术基础设施

• Velvet: 基于 Hoare 逻辑的命令式程序验证器，嵌入 Lean。
• Plausible: Lean 的 PBT 框架，用于生成随机输入并寻找反例。
• 元编程 (Meta-programming): 作者开发了 Lean 元编程工具，将 Velvet 方法转换为包含运行时断言的测试程序，实现了在编译期插入 PBT 检查。
• 存在量词处理: 针对验证条件中的存在量词，提出了一种基于边界枚举的启发式方法，使 PBT 能够有效处理此类逻辑。

3. 主要贡献 (Key Contributions)

1. LeetProof 流水线: 首个基于基础多模态验证器的端到端认证合成代理流水线，统一了测试、SMT 自动化和 AI 辅助交互式证明。
2. Lean 测试基础设施: 提出了针对 Lean 的测试新方法，包括基于类型类的输出变异（用于检查规范完备性）、有界枚举处理存在量词，以及用于随机测试合成程序和不变量的元编程框架。
3. 规范质量评估: 证明了基于 PBT 的规范生成器在 VERINA 基准上达到了 97.4% 的语义准确率。更重要的是，随机化测试发现了现有基准（VERINA 和 CLEVER）中约 10% 的规范缺陷。
4. 实证评估: 构建了一个包含 50 个命令式 LeetCode 问题的新基准，并展示了 LeetProof 在相同成本预算下，比单模式（Single-mode）Lean 基线产生更多完全认证解的能力。

4. 实验结果 (Results)

作者在 50 个 LeetCode 命令式算法问题（涉及双指针、滑动窗口等）上进行了评估，对比了 LeetProof (多模态) 与 单模式 Lean 基线（直接让 LLM 生成 Lean 代码和证明）。

• 完全认证解的数量 (Fully Certified Solutions):
  • 在 50 个问题中，LeetProof 成功完全证明了 28 个，而单模式基线仅证明了 17 个。
  • 在评估集（35 个问题）中，LeetProof 证明了 23 个，基线为 16 个（提升 44%）。
  • 在开发集（15 个问题）中，LeetProof 证明了 5 个，基线为 1 个。
• 部分证明与可修复性:
  • LeetProof 生成的 18 个“部分证明”案例（即代码正确但证明未完成），全部可以通过更强的 AI 证明器（Aristotle）完成剩余证明。
  • 相比之下，单模式基线有 7 个部分证明案例即使使用 Aristotle 也无法完成。这表明多模态分解产生的证明义务在结构上更容易处理。
• 鲁棒性:
  • 实验使用了 GPT-5.2 和 Claude Opus 4.6 两种不同的 LLM 后端。结果一致表明，多模态流水线在两种模型下均优于单模式基线。
• 成本效益:
  • 通过 PBT 和 SMT 在早期过滤掉错误，减少了昂贵交互式证明的调用次数。在固定预算（每问题 5 美元）下，多模态方法显著提高了成功率。

5. 意义与结论 (Significance)

• 范式转变: 论文证明了在认证合成中，多模态验证（结合测试、SMT 和交互式证明）比单一验证模式更有效。它打破了工具碎片化的限制，允许流水线根据任务难度动态选择最合适的验证模式。
• 成本与正确性的平衡: 将昂贵的交互式证明保留在“最后一公里”，利用廉价的 PBT 和 SMT 进行早期过滤，极大地降低了合成成本，同时保证了最终结果的正确性。
• 基准测试的改进: 揭示了现有基准测试中广泛存在的规范缺陷，强调了自动化规范质量检查（如 PBT）在合成流水线中的必要性。
• 未来方向: 为构建更强大的 AI 辅助编程系统提供了架构蓝图，即利用基础验证框架（如 Lean）和多种推理模式的组合，而非依赖单一的黑盒生成器。

总结: LeetProof 通过巧妙地将随机化测试、SMT 自动化和交互式证明整合到一个统一的流水线中，成功解决了认证程序合成中的规范质量差和验证工具单一的问题，显著提高了自动生成正确且可验证代码的成功率。