技术摘要：BRIDGE——在领域引导的验证程序合成中构建表示

1. 问题陈述

大型语言模型（LLMs）生成代码的能力日益增强，但在形式化验证的背景下，生成的程序往往看似正确，却隐藏着细微的缺陷、缺失的边界情况或不匹配的假设。在像 Lean 这样的证明助手环境中，程序验证并非单次生成任务，而是一个多工件预测问题。成功的验证需要四个耦合工件的相互一致性：

1. 可执行代码：实现部分。
2. 形式化规范：行为约束（前置条件、后置条件、不变式）。
3. 定理陈述：将代码与规范联系起来的断言。
4. 证明尝试：由内核检查以验证断言的脚本。

当前的 LLM 系统在此设定下表现挣扎，因为独立处理这些工件会导致语义漂移。模型可能会生成通过测试但无法通过 Lean 终止性检查的代码，生成能通过类型检查但空洞无物的规范，或者生成可证明但与原始任务无关的定理。核心挑战在于将非正式意图转化为一系列工件，其中语法、类型、递归结构、契约和证明义务保持对齐。

2. 方法论：BRIDGE 框架

作者提出了 BRIDGE，这是一个结构化提示框架，将可验证的编码过程分解为三个相互关联的领域：代码、规范和定理/证明。BRIDGE 不要求模型直接从自然语言跳跃到最终证明，而是强制执行一种结构化推理流，使工件相互约束和检查。

2.1 领域分解

• 代码领域：生成最终的 Lean 实现。BRIDGE 将直接的 Lean 生成与中间推理脚手架进行比较。
  • 功能脚手架：受 OCaml 和 Haskell 启发，这些脚手架鼓励不可变数据、模式匹配、结构递归和组合式定义。这与 Lean 的依赖类型理论和终止性纪律自然契合。
  • 命令式脚手架：受 Python 和 C++ 启发，这些脚手架鼓励循环和可变性。
  • 关键洞察：中间程序是一个推理脚手架，而非经过认证的信源工件。它无需在其源语言中编译；其目的是引导模型偏向于 Lean 可验证的结构。
• 规范领域：描述预期的保证。BRIDGE 利用各种推理风格（契约式设计、基于属性的测试、测试驱动开发、防御性编程）来明确假设、边界情况和保证。规范不仅评估其类型检查能力，还评估其非空洞性以及区分正确实现与看似合理但错误实现的能力。
• 定理/证明领域：明确正确性断言。提示模型提出属性（界限、不变式、单调性）并尝试证明。该领域作为下游验证的诊断工具，检查生成的定理是否可以被展开，以及证明是否能在不使用 sorry（未证明目标的占位符）的情况下完成。

2.2 推理假设

核心假设是：验证的成功取决于中间推理的结构。直接生成迫使模型同时恢复算法、用 Lean 表达它、满足类型/终止约束并推断规范。BRIDGE 将这些压力分离开来。具体而言，作者发现以功能代码生成开始的顺序特别有效：模型首先使用功能脚手架生成与 Lean 兼容的代码，然后利用该实现作为规范和定理陈述的语义锚点。

3. 主要贡献

1. 多工件框架：BRIDGE 引入了一种可验证编码的结构化方法，将任务分解为相互关联的代码、规范和定理/证明领域，利用跨工件推理来减少语义漂移。
2. 功能推理改善合成：在包含 178 个问题的 Lean 基准测试中，与直接提示相比，功能对齐的中间推理将Lean 可执行正确性提高了高达 1.5 倍。它实现了相当的成功率，但所需的 Lean 评估次数减少了约 2 倍，表明样本效率更高。
3. 改进的下游工件：BRIDGE 风格的提示产生了更有用的形式化工件。它生成了更多能在 Lean 中成功展开的定理陈述，以及更多与实现对齐的已完成证明尝试。规范引导的提示也改善了常规代码生成（在 Python 中最高提升了 17.5 个百分点）。
4. 可学习的归纳偏置：在 BRIDGE 风格的功能轨迹上进行监督微调（SFT），其表现优于匹配的直接轨迹微调（例如，在 VERINA 基准测试上提升了 9.1 个百分点）。这表明该框架捕捉到了一种可学习的归纳偏置，而不仅仅是一次性的提示效应。

4. 实验结果

作者在自定义的 178 个问题 Lean 基准测试以及包括 VERINA、CLEVER 和基于求解器的 DAFNYBENCH 试点在内的公共基准测试上评估了 BRIDGE。

• 可执行正确性：在最小核心设置中，使用功能脚手架，178 项任务的通过率从直接生成的 44/178 提高到功能生成的 59/178。经过修复轮次后，差距仍然为正（83/178 对比 77/178）。
• 样本效率：与直接提示相比，功能脚手架以大约一半的 Lean 评估次数达到了相当的成功率，降低了候选项检查的成本。
• 可迁移性：这些优势转移到了公共基准测试上。在 VERINA 上，功能提示将通过率提高了高达 6.3 个百分点。在 DAFNYBENCH 上，它将验证通过的 pass@5 提高了 7.3 个百分点。
• 证明诊断：在完整的证明实验中，功能代码产生了更多不含 sorry 的已完成证明（34/178 对比功能 SFT 证明器的 20/178），并生成了更短、更清晰的实现，使证明模型更容易完成证明。
• SFT 增益：在功能轨迹上进行微调将 VERINA 上的性能从 20.3% 提升至 29.4%，证明了推理结构可以被模型内化。

5. 意义与局限性

该论文声称推理表示至关重要。通过将生成过程结构化以与目标验证系统（Lean）对齐，BRIDGE 减少了语法、类型和终止性失败。该框架提供了一种面向验证的归纳偏置，连接了代码、规范、定理陈述和证明尝试，使得流程更易于检查，也更适应下游证明搜索。

适度声明与局限性：

• 非完整验证：BRIDGE 研究的是验证合成的“前端”。它不声称能在大规模上解决完整的语义验证。生成的规范和定理陈述可能仍然薄弱、空洞或过度受实现影响。
• 范围：评估侧重于局部的、算法性的任务。作者尚未在大型形式化库、丰富的状态化程序或长视野证明上测试 BRIDGE。
• 模型依赖性：结果因模型、提示和搜索预算而异。BRIDGE 被呈现为一种有用的归纳偏置，而非独立于底层模型的通用改进。
• 未来工作：作者指出，下一步是关闭 BRIDGE 工件与更强证明搜索之间的循环，可能整合使用工具的定理证明器、形式化库检索以及来自可验证奖励的强化学习。

总之，BRIDGE 证明了将验证编码分解为结构化的、领域对齐的推理步骤，显著提高了生成工件的质量和可验证性，为在不需完全自动化证明过程的情况下实现更可靠的形式化合成提供了一条途径。