程序验证的智能体证明

# 面向程序验证的智能体证明（Agentic Proving）  
来源：https://arxiv.org/html/2605.23772  

**Alessandro Sosso**  
奥胡斯大学 计算机科学系  
丹麦奥胡斯  
sosso@cs\.au\.dk  

**Akhil Arora**  
奥胡斯大学 计算机科学系  
丹麦奥胡斯  
akhil\.arora@cs\.au\.dk  

**Bas Spitters**  
奥胡斯大学 计算机科学系  
丹麦奥胡斯  
spitters@cs\.au\.dk  

###### 摘要  
近年来，智能体系统已成为形式化数学自动定理证明的最先进方法。为了评估这些能力在**程序验证**中能延伸多远，我们在智能体证明框架下，对 Claude Code 在 Clever（一个用于可验证代码生成的 Lean 4 基准测试）上的表现进行了评估。结果表明，Claude 能为 98.8% 的问题生成看似有效的规范（其中 81.3% 也通过了 Clever 基于同构的评分，在基准测试中未发现真实规范存在问题的部分），能针对正确的真实规范为 87.5% 的问题证明实现正确，并在端到端程序生成与验证流水线上（针对前提自洽的条目）达到了 98.1% 的成功率。在所有阶段中，Claude 还对其自身的尝试提供了高质量的反馈（经人工审查确认），准确识别了失败的根本原因以及数据集中残留的缺陷。这些发现凸显了现有程序验证基准的难度与现代智能体证明器能力之间日益增长的错配，并指出了对更严谨、更具缺陷鲁棒性的评估方法的需求，特别是需要替代基于同构的生成规范评分方法。更广泛而言，我们的结果提供了经验证据，表明紧密的编译器参与循环的智能体范式目前是基础程序验证的最有效方法。

## 1 引言  
大型语言模型（LLM）已知会产生幻觉，即便是最近的“推理”模型也可能生成看似连贯但逻辑无效的论证。相比之下，形式逻辑提供了一种历史悠久且严谨的替代方案：数学论证可以用形式语言表达，并通过机械检查确保其正确性。这一方法体现于基于类型论（如 Rocq[28 (https://arxiv.org/html/2605.23772#bib.bib35)]、Lean[21 (https://arxiv.org/html/2605.23772#bib.bib16)]、Agda[23 (https://arxiv.org/html/2605.23772#bib.bib36)]）、高阶逻辑（如 Isabelle[22 (https://arxiv.org/html/2605.23772#bib.bib37)]、HOL4[29 (https://arxiv.org/html/2605.23772#bib.bib38)]、HOL-Light[12 (https://arxiv.org/html/2605.23772#bib.bib39)]）以及集合论（如 Mizar[3 (https://arxiv.org/html/2605.23772#bib.bib40)]、MetaMath[5 (https://arxiv.org/html/2605.23772#bib.bib41)]）的交互式证明助手中。本文聚焦第一类，特别是 Lean 4 定理证明器。

近年来，将 LLM 应用于类型论设定下的自动构造证明取得了显著进展。知名系统在 Lean 4 的形式化数学基准测试中表现强劲[14 (https://arxiv.org/html/2605.23772#bib.bib42),1 (https://arxiv.org/html/2605.23772#bib.bib1),7 (https://arxiv.org/html/2605.23772#bib.bib43)]，在 Isabelle[18 (https://arxiv.org/html/2605.23772#bib.bib33),35 (https://arxiv.org/html/2605.23772#bib.bib34)] 和 Rocq[4 (https://arxiv.org/html/2605.23772#bib.bib31),33 (https://arxiv.org/html/2605.23772#bib.bib32)] 上也是如此。这些系统采用多种架构策略，包括整体证明生成、证明状态搜索，以及越来越多地采用集成规划、工具使用和迭代精炼的智能体设计。

本文研究这些进展如何转化为**程序验证**——一个既具有实际相关性又结构上具有挑战性的场景。与非形式化数学不同，程序验证需要对可执行工件、显式规范和微妙的边界条件进行推理，且受到严格的语法和语义约束。为此，我们在 Clever[30 (https://arxiv.org/html/2605.23772#bib.bib12)]（一个最新的 Lean 4 可验证代码生成基准测试）上评估了最先进的智能体范式。图1 (https://arxiv.org/html/2605.23772#S1.F1) 提供了我们实验管道的概览示意图。

#### 初步实验  
作者之前的测试评估了领先的智能体和非智能体证明器在 Clever 和 Verina[36 (https://arxiv.org/html/2605.23772#bib.bib11)] 这两个 Lean 4 可验证代码生成基准测试的证明生成任务上的表现。这些实验表明，基于 Claude Code 的智能体系统在基准测试的已验证正确部分达到了接近饱和的性能，Aristotle[1 (https://arxiv.org/html/2605.23772#bib.bib1)] 紧随其后，而专门的整体证明生成模型和符号策略则远远落后。最强的智能体还持续识别出基准测试本身规范和实现中的错误，在多个案例中提出修复方案并成功证明了修正后的陈述。这些发现表明，编译器参与循环的智能体系统是基础程序验证最有效的脚手架，而现有的程序验证基准测试已不再像其设计初衷那样对现代智能体证明器构成挑战。本文对上述两个观察结果进行跟进，在完整的 Clever 流水线上评估了一个智能体系统，使用其原生评估基础设施而非初步研究中使用的自定义蒸馏；详情请参见附录A (https://arxiv.org/html/2605.23772#A1)。

#### 贡献  
我们的智能体 Claude Code 设置在整个 Clever 流水线上达到了新的最先进水平。具体来说：
- - •规范认证：Claude 为 98.8% 的问题生成了看似有效的规范，其中 81.3% 也通过了 Clever 基于同构的评分（在基准测试中未发现真实规范存在问题的部分）。
- - •实现认证：Claude 针对正确的真实规范，为 87.5% 的问题成功生成并认证了实现。
- - •端到端流水线：在前提自洽的条目上，Claude 在完整的“规范+实现+证明”流水线上达到了惊人的 98.1% 成功率。
- - •自诊断反馈：除了原始性能，Claude 还持续对其自身输出产生论述充分的分析，识别并分类了失败的根本原因以及 Clever 基准测试中残留的缺陷。
- - •方法论洞见：我们的发现揭示了“针对真实规范的同构性”作为自动形式化评估方法的结构性局限，并提出了替代评估策略的具体建议。

参照图注  
图 1：实验管道概览示意图。四个生成和证明任务以黄色标识：Clever 的原生预期设置在顶部行以红色横向跨越，其他路径代表我们对设置的自定义变体。右上角的虚线部分为附录A (https://arxiv.org/html/2605.23772#A1) 的初步实验设置。

## 2 方法论

### 2.1 数据集
Clever 基准测试[30 (https://arxiv.org/html/2605.23772#bib.bib12)]是从 HumanEval[6 (https://arxiv.org/html/2605.23772#bib.bib13)] 改编而来的精心策划数据集，包含 161 个问题，用于测试在 Lean 中端到端的自动代码生成和验证。每个问题以带注释的 Lean 文件形式提供，包含多个部分：(1) 函数的自然语言（NL）规范（格式化为注释中的 Python 风格文档字符串），包括函数签名和示例用法；(2) 形式规范 `generated_spec` 的 Lean 4 签名，带有待替换的 `sorry` 占位符；(3) 人工编写的真实规范 `problem_spec`，签名相同；(4) 说明 `generated_spec` 与 `problem_spec` 之间语义等价的同构定理，带有占位符 `sorry`；(5) 实现的 Lean 4 签名，带有占位符 `sorry`；(6) 说明实现满足 `problem_spec` 的正确性定理，带有占位符 `sorry`。对于需要辅助定义的问题，还会提供辅助定义以及一些实现的形式化测试用例。

为了评估模型，基准测试采用分阶段流水线，定义了分属两阶段的 4 个不同任务：**规范认证**包括生成 `generated_spec` 规范（spec_gen），然后证明它与真实规范 `problem_spec` 同构（spec_iso）；**实现认证**包括实现函数（impl_gen），然后证明它满足 `problem_spec` 规范（proof_gen）。基准测试提供的测试框架允许选择性检索与每个任务相关的部分，然后可以合并回单个 Lean 脚本。基准测试通过格式化新的 Lean 脚本（包含生成的元素），并测试其能否成功编译且不含 `sorry` 关键字来评估解决方案。

#### 基准测试修订  
我们使用了原始基准仓库的一个自定义分支，以便跟踪基准测试的修复实施以及自定义设置所需的评估脚本的微小修改。随着实验的推进以及发现格式化错误、拼写错误和错误测试用例等问题，我们对基准测试条目进行了修订以修复这些问题。所有其他元素，如真实规范、辅助函数和定理签名，均保持不变。

#### 先前工作  
原始论文[30 (https://arxiv.org/html/2605.23772#bib.bib12)]报告了在 pass@600s 协议下严格的端到端上限为 1/161（≈0.62%），由 o4-mini、Claude-3.7 和 DeepSeek-R1 在 few-shot 配置下实现，以及由 GPT-4o 和 Claude-3.7 搭配 COPRA 证明代理[31 (https://arxiv.org/html/2605.23772#bib.bib49)]实现。最佳分阶段数字是实现认证上的 14/161（8.7%）（Claude-3.7+COPRA）和规范认证上的 3/161（1.86%）（GPT-4o+COPRA）。最强的部分流水线后续工作[16 (https://arxiv.org/html/2605.23772#bib.bib50)]报告了 Clever 上 54.0% 的结果，但该指标仅衡量了在单独提供的由 GPT-5.2 生成的实现上的正确性证明阶段；同一设置下前沿推理模型最多达到约 23.6%。独立的后续工作也揭示了 Clever 中的规范质量问题。规范级基于属性的测试[10 (https://arxiv.org/html/2605.23772#bib.bib51)]识别出 18 个有缺陷的条目（11.2%），包括 16 个后条件不充分、1 个实现错误和 1 个错误规范；顶层正确性定理上的集成 quickcheck[16 (https://arxiv.org/html/2605.23772#bib.bib50)]额外证伪了 10 个条目。

### 2.2 实验设置
我们的实验设置基于 Claude Agent SDK[2 (https://arxiv.org/html/2605.23772#bib.bib26)]，运行 Claude Opus 4.6，每个智能体实例配置了 *lean-lsp-mcp*[9 (https://arxiv.org/html/2605.23772#bib.bib21)]（一个与 Lean LSP 交互并提供搜索工具以在项目上下文和 Mathlib 中找到相关引理的专用 MCP 服务器）和 *lean4-skills*[11 (https://arxiv.org/html/2605.23772#bib.bib17)]（一个将 Lean 特定指令和命令、策略最佳实践及工作流模式注入模型上下文的包）。对于每次尝试，系统从模板初始化临时目录作为 Lean 项目，然后创建使用基准条目相关组件格式化的 Lean 文件，并提示新的智能体实例根据当前任务编辑文件。完成后或超时（设定为 3600 秒）时，检索结果文件以及智能体对话轨迹、工具调用和运行元数据。每个新的 Claude 实例都会获得作为系统提示的任务描述，概述细节和目标、输入文件和期望输出的格式、行为规则以及智能体应遵循的指导原则。然后，只需向智能体提供简短的 NL 提示，要求其按照先前提供的指令填充目标 Lean 文件的相应部分（spec_gen, impl_gen），或者，如果任务需要证明给定定理（spec_iso, proof_gen），则提供来自技能包的 `/lean4:autoprove` 命令，该命令启动多周期定理证明例程。然后要求 Claude 使用标志报告任务结果，可以在终止后的同一会话中作为后续提示，或者通过对 Lean 输出和智能体回复的连续分析进行报告。智能体可以将其分类为成功（ok）、失败（fail），或由于输入错误或不正确假设而严格按照论证为不可能（issue）（参见附录 B.1 (https://arxiv.org/html/2605.23772#A2.SS1)）。对于定理证明任务（spec_iso, proof_gen），“不可能”情况进一步细分为 `mismatch`（当定理不可证明，但输入元素是源 NL 描述和测试用例的不同但有效解释时）和 `issue`（当证明因至少一个元素（规范/实现/固定的基准组件如签名）出错而失败，即与 NL 描述矛盾时）（同样，两种情况下都必须提供严谨的支持论证或反例）。为了提取更深入的诊断见解，对 `issue` 类别中的结果进行了进一步分析，以粒度识别错误的来源：对于 spec_iso，是真实 `problem_spec`、生成的 `generated_spec` 或两者；对于 proof_gen，是规范、实现或基准结构组件。`mismatch` 类别中的条目仅在 spec_iso 的解决方案中发现。对此类情况进行了进一步分析，以识别同构定理的哪个方向是可证明的（即生成的规范是否严格强于或弱于真实规范），或者两者是否都不成立。对 Claude 报告的标志与通过基准测试框架的评估进行的交叉检查显示，除了两个实例外，所有且仅有的 `ok` 解决方案通过了评估：一个实例是由于测试用例中的错误导致编译失败，但解决方案在其他方面是正确的；另一个实例是尽管成功通过了评估，但被报告为 `fail`，因为 Claude 在终止前超时。

## 3 结果  
我们对所有四个流水线任务进行了实验，使用了多种提示，其详细程度和指导性递增。在所有情况下，只进行一次尝试（pass@1），因为事实证明这足以让 Claude 生成始终高质量（经人工检查确认）的规范、实现和证明。然而，基准测试框架报告的通关率并不总是反映这一点：在几种配置中，成功率远低于人工审查输出所建议的水平。因此，我们设计了下面描述的提示序列，以逐步解决这一差异。更多结果细节可在附录 C (https://arxiv.org/html/2605.23772#A3) 中找到。

### 3.1 规范认证

#### 简单提示  
第一次运行使用了最小提示