Ax-Prover：用于数学与量子物理定理证明的深度推理智能体框架

Ax-Prover：用于数学与量子物理定理证明的深度推理智能体框架

Ax-Prover: A Deep Reasoning Agentic Framework for Theore Proving in Mathematics and Quantum Physics

https://arxiv.org/pdf/2510.12787

摘 要

我们提出 Ax-Prover——一个用于 Lean 中自动定理证明的多智能体系统，能够解决跨学科科学领域的问题，并可自主运行或与人类专家协作。为实现这一目标，Ax-Prover 通过形式化证明生成来处理科学问题求解，该过程既需要创造性推理，也要求严格的语法严谨性。Ax-Prover 通过为大型语言模型（LLMs）配备定制的 Lean 工具来应对这一挑战：LLMs 提供知识与推理能力，而 Lean 工具确保形式正确性。

为评估其作为自主证明器的性能，我们在两个公开数学基准以及我们新引入的两个 Lean 基准（分别来自抽象代数和量子理论）上对 Ax-Prover 进行了评测。在公开数据集上，Ax-Prover 是所有不依赖领域特定训练的证明器中表现最佳的；在新基准上，它显著优于所有基线模型。这表明，与难以泛化的专用系统不同，我们基于工具的智能体定理证明方法提供了一种可在多样化科学领域中通用的形式验证范式。

此外，我们通过两个经典与量子密码学中的实际案例研究，展示了 Ax-Prover 作为研究者友好型助手的能力。在这两个安全通信的基石领域中，Ax-Prover 与领域专家合作，利用标准的人机交互方式，形式化并验证了具有挑战性的安全保证，使不具备 Lean 专业知识的研究者也能参与这一新兴领域。

1 引言

开发能在跨学科科学领域中可靠推理的大型语言模型（LLMs），仍是学术界和工业界人工智能的核心挑战。目前，基于 LLM 的形式化推理系统主要聚焦于数学领域，并已取得卓越成果 [19, 16]。近期，大量工作致力于训练用于 Lean 形式定理证明的推理 LLM。Lean 是一种开源编程语言兼交互式证明助手，配合其社区驱动的 Mathlib 库 [36]，为 AI 系统提供了严谨环境：在此环境中，AI 必须进行符号推理与结构化形式化，并建立在不断演进的数学知识体系之上。

DeepSeek-Prover 系列 [68, 69, 55]、Kimina-Prover-72B [66]、Goedel-Prover [38, 39] 和 Seed-Prover [16] 等 LLM 证明器表明，可从前沿 LLM 中蒸馏出专用证明模型，并在 Lean 中训练以实现定理证明，在 MiniF2F [73] 和 PutnamBench [63] 等数学基准上达到最先进水平。

然而，这些模型仍存在关键局限：第一，它们主要在数学领域训练和测试，其跨领域泛化能力尚不明确；且通常基于固定版本的 Mathlib 训练，面对新版本中定义的增删或重命名等变更时表现脆弱。保持其更新需频繁重训练并系统性“遗忘”过时知识，成本高昂。第二，尽管训练提升了其生成 Lean 证明的能力，却使其能力相对于通用 LLM 变窄——无法使用外部工具，也无法与人类协作。第三，部署和使用这些模型需要高性能计算资源和专业技能。

这些问题共同表明，不断扩大专用证明器的规模可能在灵活性和可用性方面收益递减。

相比之下，Claude [5] 和 GPT [51] 等通用 LLM 在数学、物理、计算机科学等多个领域编码了丰富知识，具备强大的自然语言理解、问题解决和交互能力，并可通过 API 轻松集成到任意工作流中。但它们并未专门训练用于 Lean 中的形式化陈述或证明构造，也无法原生与 Lean 环境交互。

这造成了一种尖锐的割裂：专用证明器深度集成 Lean，但领域狭窄、使用困难；通用 LLM 领域宽广、易于访问，却缺乏与形式化推理基础设施对接的能力。

为弥合这一鸿沟，我们提出Ax-Prover，一种基于模型上下文协议（MCP）[46] 的新型定理证明智能体工作流，通过 lean-lsp-mcp 仓库 [25] 为通用 LLM 赋予 Lean 工具。Ax-Prover 将 LLM 的推理能力与 Lean 的形式验证能力相结合：LLM 分析未证明定理、提出证明草图、生成逐步 Lean 代码；Lean 工具则使 LLM 能检查目标、搜索相关结果、定位错误并验证证明——这些能力对严格的形式化定理证明至关重要。

Ax-Prover 克服了当前最先进证明器的主要局限：第一，使用前沿 LLM 避免了领域过度专业化，而 MCP 接口使其能兼容任意新版 Mathlib 及项目相关的自定义库，无需重训练；第二，保留了工具使用与对话能力，支持人机交互协作；第三，直接利用现有前沿模型，无需部署专用系统。

我们在两个公开数学竞赛数据集（NuminaMath-LEAN [50] 和 PutnamBench [63]）上评估 Ax-Prover，并引入两个新数据集以支持新领域的评测：

• AbstractAlgebra：聚焦群、环、域等代数结构，测试证明器在更抽象、研究导向环境中的推理能力，区别于现有竞赛风格数据集；
• QuantumTheorems：迈出自动化定理证明向纯数学之外科学领域拓展的第一步，评估模型在量子力学中的形式推理能力。

结果显示，Ax-Prover 在 PutnamBench 上表现优异——在完全开源的智能体中准确率最高；在其他数据集上，显著优于未配备 Lean 工具的通用 LLM 和当前最先进的专用证明器，尤其在我们提出的新数据集上优势明显。

除作为自主求解器外，Ax-Prover 亦被设计为研究者助手。我们在第 6.1 与 6.2 节展示了密码学领域的两个面向研究者的用例。密码学是 Lean 的理想试验场：其安全性依赖精确数学推理，但常缺乏标准化假设和显式逻辑结构。机器验证证明可彻底改变此类安全保证的构建与信任方式——确保每一步、每个假设和归约都显式且可验证。

在第一个用例中，Ax-Prover 与密码学研究者合作，形式化并验证了矩阵分支数（branch number）的一个替代定义 [45]，揭示了非形式化论证中的一个细微漏洞，并在研究者自己的笔记本电脑上于两天内生成了可复用的 Lean 证书。在第二个用例中，它协助量子信息研究者将量子密钥分发（QKD）中的一个熵界 [41] 从物理风格推导转化为机器可验证组件。

这些案例表明，Ax-Prover 不仅提升基准准确率，更降低了研究者在实际工作中使用 Lean 的门槛，为复杂推理带来清晰性与严谨性，并在安全关键领域实现可解释、由研究者主导的验证。

我们的贡献有三方面：(i) 设计了 Ax-Prover——一种轻量级智能体工作流，通过 MCP 将通用 LLM 与 Lean 工具连接，并证明其在多个科学领域中性能媲美甚至超越通用 LLM 与专用证明器；(ii) 引入覆盖抽象代数与量子物理的新形式化 Lean 数据集，补充现有基准；(iii) 通过与领域专家合作的用例，展示 Ax-Prover 作为助手的能力：成功形式化验证了近期密码学成果 [45] 以及量子密钥分发 Lo-Chau 安全框架中的熵界 [41]。

2 相关工作

Lean 中的自动定理证明源于经典方法，例如决策过程（decision procedures）[21, 11] 和启发式引导的证明搜索（heuristic-guided proof search）[33, 57]。然而，这些方法面临特定挑战：前者无法处理一般数学领域（如超越函数和复数），后者在分布外（out-of-distribution）场景下表现不佳。

近期工作将机器学习引入该领域：从启发式调优 [64]，到前提选择（premise selection）与战术预测（tactic prediction）[31, 30]，最终发展出能够生成 Lean 证明的基于 Transformer 的语言模型 [54, 35, 53, 70]。更近期的大规模系统通过蒸馏、监督微调和强化学习，在形式化证明任务上训练 LLM，进一步推动了这一趋势。当前专用模型的代表包括 Kimina-Prover [66]、DeepSeek-Prover 系列 [68, 69, 55]、Goedel-Prover 1 和 2 [38, 39]、Prover Agent [10]、Apollo [52] 以及 Seed-Prover [16]。这些均为高度专用的证明器，以 Lean 定理为输入，自主生成证明。

非常近期的一类研究开始探索包含前沿 LLM 与形式验证器的智能体工作流（agentic flows），例如 Hilbert [65] 和 Aristotle [2]。尽管我们也采用类似思路，但存在若干关键差异：
(i) 我们通过 MCP（Model Context Protocol）让 LLM 直接访问 Lean 工具；
(ii) 我们的框架既无需训练也无需微调 [2]，且不依赖任何专用证明器 [65]；
(iii) 我们在数学之外的领域（如量子物理）验证了方法的有效性；
(iv) 我们展示了系统作为人类研究者交互式助手的能力。

此外，另一条并行的研究路线探索了经典机器学习在支持 Lean 定理证明专家方面的应用，例如前提选择与战术预测 [28, 13]，以及近期通过外部接口连接 Lean 的 LLM [8, 9, 60]。这些方法展示了 AI 辅助证明的潜力，但仍存在资源消耗大、难以跨科学领域迁移的问题。近期工作如 [34] 试图通过增强在 Lean 内部的适应性来缓解此问题。

与此同时，人机协作日益受到关注：对话式助手 [20] 和“副驾驶”（copilot）式集成 [17] 表明，形式化工具可增强而非取代人类推理。我们的工作延续这一方向，弥合了重量级专用证明器与轻量级、研究者友好型系统之间的鸿沟，后者能更灵活地适应不断演进的 Lean 生态系统。

3系统架构

我们以多智能体架构实现 Ax-Prover，包含三个智能体，每个均由配备特定提示（prompt）的大型语言模型（LLM）实现：协调器（Orchestrator）、证明器（Prover）和验证器（Verifier）。借鉴近期面向复杂任务（如科学发现 [29, 71]）的智能体设计，我们避免采用单体式（monolithic）结构，而是为每个专用智能体分配明确角色。这种分离实现了专业化与模块化：各智能体可独立优化、替换或扩展，使研究者能根据自身需求调整 Ax-Prover，而不会破坏系统稳定性。

图1（左）展示了我们的工作流：协调器接收一个未证明的 Lean 语句，并将其转发给证明器；证明器通过推理、调用 MCP Lean 工具并生成 Lean 代码（图1右），迭代地推进证明过程。随后，验证器检查该证明并将结果反馈给协调器。若证明完整且无错误，协调器终止任务；否则，它向证明器提供反馈，后者继续证明过程。通过这一闭环流程，系统逐步将未证明定理转化为形式化验证的 Lean 证明。接下来，我们将详细介绍各智能体及其工具。

3.1 专用智能体

3.1.1 协调器（Orchestrator）

协调器的角色类似于分布式系统中的调度器：它本身不执行计算，而是确保计算在各智能体之间顺畅流转。其主要承担三项职责：
第一，任务分发——接收用户输入，并据此向证明器发出指令；
第二，反馈路由管理——接收验证器的诊断输出，并在发现错误时向证明器提供结构化反馈；这种分离确保了证明生成与验证评估保持独立，同时仍支持迭代精调；
第三，决定何时终止精调循环——当验证器确认证明完整且无错误时，或当尝试次数超过可配置阈值时，循环终止。

3.1.2 证明器（Prover）

证明器（Prover）是系统中的构造性核心，其任务是将未证明的 Lean 定理转化为完整的证明。定理证明既需要创造性——例如找到合适的引理或使用恰当的战术，也需要严谨性——确保结构和 Lean 代码在语法上正确。为实现这一目标，证明器在基于 LLM 的启发式探索与借助 lean-lsp-mcp 提供的 MCP Lean 工具所支持的严格形式化之间取得平衡（参见第 3.2 节）。

我们指示证明器采用增量式、逐步推进的方法执行任务，并将每次对定理证明的更新写入一个.lean文件。这样做有两个原因：
第一，满足 MCP Lean 工具的要求——其中部分工具需要通过.lean文件路径来检查其中的代码；
第二，允许用户实时观察证明过程。

图2展示了证明器流程的主要阶段：

• 初始阶段：证明器通过扫描输入的 Lean 文件，识别以sorry（表示证明未完成的占位符战术）标记的未完成证明，从而确定目标定理（左上）；
• 证明草图：随后，它撰写一份证明草图——即用自然语言粗略勾勒证明的逻辑流程，将复杂证明分解为更易管理的步骤（右上）；
• 形式化阶段：接着，将草图中的每一步形式化为以have开头、以sorry结尾的 Lean 语句（左下），使证明器能在 Lean 上下文中清晰看到原始定理如何被拆解为当前步骤与后续步骤；
• 逐步求解：然后，证明器依次处理每个步骤，提出 Lean 战术以替换每个sorry。每完成一步，就调用特定的 Lean 工具——lean diagnostic messages（参见第 3.2 节）——评估所生成步骤是否正确。若检测到严重错误或仍有sorry存在，证明器会尝试修正错误或调整推理。当所有步骤均被正确解决后，证明器结束任务（右下）。

工具使用对证明器至关重要。这一点在图1（右）中清晰体现——该图摘自一次实验运行中的 LLM 日志，展示了证明器如何通过工具增强的推理实现探索与形式化：

• 使用 MCP 工具读写 Lean 文件（read fileedit file
• 在证明的不同位置识别目标（lean goal
• 在 Mathlib 中搜索相关定理（lean search
• 验证证明的正确性（lean diagnostic messages）。

这种方法使证明器表现得像一位谨慎的数学家：先拟定计划，再借助相关工具逐步探索并实现想法，在 Lean 中验证其正确性，并仅在每一步都通过验证后才继续推进。

3.1.3 验证器（Verifier）

验证器在我们的工作流中充当正确性的最终守门人。它既不生成也不修改证明，仅评估证明器所生成证明的正确性。验证器可访问文件系统工具（用于读取证明器生成的文件）以及一个 Lean 工具——lean diagnostic messages——用于评估证明的正确性。

验证器的操作分为两步：

1. 使用lean diagnostic messages工具编译证明器生成的 Lean 文件，解析返回的诊断信息，并生成错误报告；
2. 给出最终裁决：仅当文件中不存在一级错误（level-1 error，见第 3.2 节）时，该证明才被视为已验证。

乍看之下，验证器似乎冗余，因为它与证明器使用相同的lean diagnostic messages工具。然而，其存在出于两个关键原因：
(i) 证明器可能因步数耗尽（见第 5.1 节）而返回不完整或错误的证明；
(ii) 有时即使仍存在错误，证明器也会提前终止。

因此，一个独立的验证器对确保系统鲁棒性至关重要——这类似于软件开发流水线中，激进的测试始终需由保守的编译器进行最终校验。

3.2 MCP 工具

如上所述，工具的使用在我们的方法中至关重要。我们通过MCP（Model Context Protocol）为 LLM 提供对工具的访问权限。MCP 是一种标准接口，允许 LLM 智能体以统一且受控的方式调用外部服务 [46]。我们实现了两类工具：文件系统工具（Filesystem tools）和Lean 工具（Lean tools）。

文件系统工具处理文件操作，例如read file（读取文件）、write file（写入文件）和list directory（列出目录内容）（参见附录 A.1）。

Lean 工具使 Ax-Prover 能够执行多种对定理证明至关重要的操作。我们通过lean-lsp-mcp 项目[25] 为 Ax-Prover 提供这些工具的访问权限，该项目为 Lean 环境提供了标准化接口。借助这些工具，Ax-Prover 能够：

• 在本地库中搜索；
• 在错误或警告出现时进行诊断；
• 在证明的任意位置观察当前的 Lean 上下文；
• 查询外部搜索引擎。

值得注意的是，外部搜索引擎为 Ax-Prover 提供了比 LLM 参数化知识中更最新的 Mathlib 信息：

• Loogle可在 Mathlib 的最新版本中搜索声明；
• Leansearch则基于 Mathlib 的一个较近但非最新的版本。

由于 Mathlib 是一个快速演进的库，Ax-Prover 的这一能力确保了其在导入、定理引用和证明构造方面与当前环境兼容，而无需依赖 LLM 在训练时所学到的特定（或多个）Mathlib 版本的知识。

我们使用的 Lean 工具可分为四大类，如表1所示。

需特别说明的是，lean diagnostic messages工具返回一个数字代码：

• 0：表示证明成功编译，无错误或警告；
• 1：表示证明中存在明确的编译错误；
• 2：表示证明成功编译但包含警告信息，例如证明未完成（含有sorry），或代码风格未通过 linter 检查。

只有当返回代码为0，或返回代码为2 但不包含sorry时，该证明才被视为正确且完整。

4 数据集

尽管 LLM 在 Lean 中用于数学验证的应用正在迅速发展，但全面、高质量的数据集仍然稀缺。目前仅有少数开源数据集可用，其中较为著名的包括 MiniF2F [73]、PutnamBench [63] 和 NuminaMath-LEAN [50]。这些基准包含来自国际数学奥林匹克（IMO）或普特南竞赛（Putnam exam）等赛事的高难度、高层次数学问题。

其他数据集虽存在，但有明显局限。例如，Deepseek-Prover-V1 Train [23] 包含 2.7 万条由 LLM 生成的定理陈述与证明，但其中大多数问题非常简单，平均仅需 2–3 行代码即可解决。Lean Workbook [72]（5.7 万条）收集了由 LLM 生成的数学问题形式化版本。尽管在过滤后报告了 93.5% 的陈述级准确率，但后续分析指出，其中仍有相当一部分样本存在语义错误和幻觉（hallucinations）[42, 67]，这限制了其可靠性。

值得注意的是，当前有价值的基准数据集几乎全部聚焦于数学领域，且即使在该领域内，也主要局限于高中至本科水平的竞赛类问题。为丰富生态系统并拓展 Lean 数据集的覆盖范围，我们构建了两个新数据集：

• AbstractAlgebra(AA)：一个基于标准抽象代数教材的 Lean 4 数据集。与现有聚焦于本科竞赛风格谜题的数学基准不同，AA 面向研究生或研究级数学，强调更深层的抽象概念，而非冗长的逐步代数操作。
• QuantumTheorems(QT)：涵盖基础量子力学核心主题的数据集，问题范围从密度矩阵到量子中继网络的标度律（scaling laws）。通过将理论物理与形式化验证方法相结合，QT 不仅为在量子力学定理上测试证明智能体提供了前所未有的机会，也标志着向评估任何以数学为基础的科学学科中的科学推理模型迈出的关键一步。

在下文中，我们将详细介绍这两个新数据集，以及我们在实验中使用的其他数据集。

4.1 抽象代数

AbstractAlgebra 是一个经过整理的数据集，包含 100 道从 Dummit & Foote 的抽象代数教材 [26] 练习题中提取并形式化为 Lean 的问题。这些问题通过自动化流程提取和形式化（详见附录 B.1）。该数据集包含两个子集：50 道来自第 1.1 章的简单问题，以及 50 道来自第 1.2–2.5 章的中等难度问题。这两个类别反映了书中章节难度的逐步提升。

如上所述，现有数据集主要聚焦于高中至本科水平的竞赛数学，通常涉及以谜题形式呈现的基础概念，需要多步推理。例如，一道竞赛题可能要求确定所有满足 (a² + b²)/(ab + 1) ∈ ℤ 的正整数 a, b —— 这个问题在概念上是基础的，但需要一系列巧妙的数论变换才能解决。

相比之下，AA 数据集面向研究级数学，涉及更深层次的概念，每道题所需的推理步骤较少。例如，一道 AA 问题可能要求：“证明二面体群 Dₙ 中每个元素 x = srⁱ 的阶为 2。” 通过提出这类问题，AA 填补了以 AI 为中心的形式化工作（主要针对初等数学）与研究数学家所研究的高级主题之间的空白。

最后，我们强调：抽象代数是许多数学领域的基础，为数论、几何、拓扑等研究提供了关键工具——事实上，在 arXiv 上列出的 32 个主要数学分类中，有 22 个建立在抽象代数之上 [1]。它也支撑着数学之外的重要领域，如密码学、物理学和化学。抽象代数广泛的基石性质凸显了开发能在该领域问题上表现优异的 AI 证明系统的重要性，因为这有望加速多个科学领域的进展。

4.2 量子定理

QuantumTheorems 包含 134 道涵盖量子理论核心领域的题目。这些问题引入了独特挑战，因为它们要求将有限维线性代数、复分析、矩阵理论与量子原理（如幺正性、厄米性和测量公设）相结合。这种领域特定的知识在现有的 Lean 数据集中缺失，使 QT 成为测试和推进物理学中形式化推理的宝贵基准。QT 通过迭代式“人在环中”过程生成，结合了自动化证明合成与专家人工筛选（更多细节和示例参见附录 B.2）。

我们生成的问题分为两个难度层级：

• 基础问题：较短（证明仅需 1–10 行 Lean 代码），通常可用标准自动化战术（如simplinarith）解决，例如证明某个测量后态是测量算符的本征态。
• 中级问题：证明需 10–50 行 Lean 代码，可通过系统性案例分析和重写规则协调解决，例如证明对易可观测量的同时对角化。

QT 代表迈向计算机验证量子力学的第一步，旨在应对确保量子信息协议与算法正确性的挑战。该数据集除科研外还具有实际意义：随着量子技术日益复杂，证明中的错误或隐藏假设可能带来严重后果。例如，最近发现的一处声称可攻破基于格的密码学的证明漏洞——数周后才被专家识别——说明了在高风险领域中未经检验的推理所带来的风险 [56, 18]。QT 提供了一种前所未有的资源，可用于开发能更早发现此类错误的工具。

4.3 NuminaMath-LEAN

NuminaMath-LEAN [50] 是一个非常近期（2025 年 8 月）发布的大型数据集，包含约 104,000 道以 Lean 形式化的竞赛级数学问题。该数据集由开发 Kimina-Prover [66] 的同一研究团队创建，源自 NuminaMath 1.5 [37]，问题选自国际数学奥林匹克（IMO）、美国数学奥林匹克（USAMO）等著名竞赛。

每个问题均包含一个 Lean 形式化陈述，其中 19.3% 由人工标注者编写，80.7% 由自动形式化模型生成 [50]。在全部问题中，25% 在 Kimina-Prover 的强化学习（RL）训练阶段被成功证明（记为 Solved-K），11% 由人类证明（Solved-H），其余 64% 尚无任何证明（Unsolved）[66, 37, 50]。我们对这三类问题进行了分析，发现明显的难度梯度：Solved-K < Solved-H < Unsolved。这一排序符合事实——Solved-H 和 Unsolved 问题均未被 Kimina-Prover 解决，从而提供了隐式的难度度量。此外，Solved-H 的证明平均长度（155 行）明显长于 Solved-K（98 行），这也从定量角度支持了我们的定性判断。

在实验中，我们从这三类中各随机抽取 100 道问题，共 300 道，构建了一个平衡、具代表性且更节省计算资源的基准。

4.4 PutnamBench

PutnamBench [63] 是一个多语言基准，旨在评估神经定理证明器求解本科水平竞赛数学问题的能力。它包含了 William Lowell Putnam 数学竞赛（1962–2024 年）问题在三大主流证明助手（Lean、Isabelle 和 Rocq）中的形式化版本。本文聚焦于其中的 Lean 子集，共包含 660 道形式化问题。

这些问题要求巧妙运用广泛的本科数学主题，包括抽象代数⁴、分析、数论、几何、线性代数、组合数学、概率论和集合论。每年 Putnam 竞赛包含两场考试，每场六题，分别标记为 A1–A6 和 B1–B6。通常认为，在每场考试中，题目难度从第 1 题到第 6 题递增。

与目前已趋于饱和的 MiniF2F 基准（参见，例如 [55]）不同，PutnamBench 对大多数证明器而言仍具挑战性。此外，由于该基准被众多模型广泛采用，它成为评估我们方法与当前最先进定理证明模型性能对比的高价值测试平台。

5 实验

本节详细介绍我们所采用的实验设置（第 5.1 节）和实验结果（第 5.2 节），随后分析工具使用情况（第 5.3 节）以及模型部署所面临的挑战与成本（第 5.4 节）。

5.1 实验设置

我们将第 4 节介绍的基准数据集分为两组：新基准（New Benchmarks，包括 AbstractAlgebra、QuantumTheorems 和 NuminaMath-LEAN）和PutnamBench，分别对应两个不同的评估目标。

在新基准测试中，我们评估了 Ax-Prover 相对于三个强基线模型的性能：

• **Claude Sonnet 4 **(Sonnet)：该基线用于评估——若将驱动我们框架的同一 LLM（见下文）置于智能体流程之外且不提供 MCP 工具访问权限时，其表现如何。
• **DeepSeek-Prover-V2-671B **(DS-Prover) 和 **Kimina-Prover-72B **(Kimina)：两个专用的 Lean 证明器。

我们对所有模型均采用pass@1进行评估。尽管这与以往研究中使用极高 pass@k 值（如 [55]）的做法形成鲜明对比，但我们认为这更贴近真实应用场景：研究人员受时间和预算限制，无法多次独立运行证明器以期其中某次成功。

为保证透明性与可复现性，我们特别说明：对所有基线模型而言，pass@1 意味着单次尝试完整形式化整个证明；而对 Ax-Prover 而言，pass@1 指的是在一次连贯的尝试中执行一系列步骤（即 API 调用），其间推理与工具调用交错进行，不进行多次独立尝试（参见第 3.1.2 节）。

在这些实验中，我们使用Claude Sonnet 4[4] 驱动 Ax-Prover。此外，为控制成本，我们将 Ax-Prover 的 API 调用上限设为 200 次，并设置 25 分钟超时限制。对所有模型，我们通过外部 Lean 编译器编译生成的文件来计算最终结果，并将能成功编译且不含sorry的证明视为正确。

第二组基准仅包含PutnamBench，旨在评估 Ax-Prover 在最具挑战性的公开基准之一上的表现，并与现有最先进证明器进行比较。因此，我们未运行基线模型，而是直接将我们的结果与官方排行榜 [62] 上报告的结果进行对比。在此测试中，我们使用Sonnet 4.5驱动 Ax-Prover，取消了 25 分钟超时限制，并将最大 API 调用次数提高至 400 次，但仍保持上述定义的 pass@1 设置。

5.2 结果

新基准：我们在表 2 中报告该组结果。

在NuminaMath-LEAN数据集上，Ax-Prover 取得51%的准确率，显著优于 DS-Prover（28%）和 Kimina（31%），而 Sonnet 仅达到 5%。尤其值得注意的是，Ax-Prover 在Solved-H子集上解决了近一半的问题，在Unsolved子集上也达到了 26% 的解决率。此外，由于自动形式化错误（见第 4.3 节），部分定理本身存在问题；在测试过程中，Ax-Prover 成功识别出这些问题并报告了错误（见附录 C）。

在AbstractAlgebra(AA) 上，性能差距尤为显著：Ax-Prover 达到64%，比 DS-Prover（24%）高出 40 个百分点，而 Kimina（13%）和 Sonnet（8%）表现极差。我们认为，这是因为 AA 数据集对 DS-Prover 和 Kimina 而言严重偏离其训练分布。事实上，这些模型主要在 Mathlib 上训练，而 Mathlib 仅涵盖抽象代数的一个极小子集；或者它们在本科竞赛级数学问题上训练，而这类问题在性质上与 AA 中的问题截然不同（见第 4.1 节）。

在QT（QuantumTheorems）数据集上，Ax-Prover 在简单子集上达到完美性能（100%），在中等难度子集上达到92%的准确率，整体准确率为96%。这与 DS-Prover（61%）和 Kimina（57%）形成显著差距，而 Sonnet 的表现更差，仅为 40%。

为展示各模型之间的差异，我们以“量子可观测量是厄米矩阵”这一证明为例（完整证明见附录 D.1）：

• DS-Prover错误地将厄米性字段（Hermitian field）用于一个自定义的量子可观测量定义，误解了其类型；
• Sonnet虽然做出了更复杂的尝试，但遭遇了重写模式不匹配的问题，凸显其在管理 Lean 环境方面的困难；
• 相比之下，Ax-Prover通过系统性方法成功完成证明：显式应用厄米性质于对角元素，使用共轭转置的定义，并将其与“一个复数若等于其共轭则为实数”这一事实联系起来。

此例表明，成功的形式化定理证明需要：谨慎的逐步推理、扎实的类型论理解，以及对库中定理的熟悉程度。

在此案例中，性能差距源于我们方法在跨科学领域适应性上的灵活性，而专用模型则因过度专业化而受限。我们认为，DS-Prover 和 Kimina 无法泛化到 QT 的一个关键原因是：QT 中的物理概念（如狄拉克符号 bra/ket、可观测量、密度矩阵）均以自定义定义的形式实现在各个.lean文件中——因为这些物理术语并未包含在 Mathlib 中，因此也未出现在 DS-Prover 和 Kimina 的训练数据中（其训练数据主要来自本科数学竞赛问题）。这一局限并非量子力学独有：任何引入 Mathlib 之外新形式化术语或定义的领域，都可能对 DS-Prover 和 Kimina 构成类似挑战，而 Ax-Prover 则能灵活整合此类领域特定定义并对其进行推理。

PutnamBench：表 3 报告了 PutnamBench 上排名前十的模型结果。由于前十名均为专用证明模型，我们还额外列出了排名前三的非专用模型。

在“计算资源”（Compute）一栏中，pass@表示求解单个证明所进行的独立尝试次数。Hilbert 使用的是avg. pass@，这是一个智能体框架，可在不同层级并行执行推理与验证 [65]。该指标的确切定义尚不明确；我们推测它反映了对 Hilbert 子智能体的平均调用次数。类似地，“medium” 是 Seed-Prover 的一种特定测试设置，指在并行化精调过程中进行评估 [16]。

在此基准上，Ax-Prover 达到 14% 的准确率，成为表现最佳的开源模型，并在所有模型中排名第三。Ax-Prover 超越了 Goedel-Prover-V2 等其他开源模型，并将近翻倍了 DeepSeek 解决的问题数量，且所用计算资源远低于后者。

尽管 Ax-Prover 未达到榜首，但必须强调的是：其运行成本仅为 Hilbert 和 Seed-Prover 的一小部分（见“Compute”列）。我们的分析显示，Ax-Prover 在其解决的 92 道题目中，平均每道题生成 182 行证明代码。此外，它成功解决了所有难度级别的问题（见第 4.4 节），且解出问题的分布符合预期难度曲线：

• 第 1 级：39%
• 第 2 级：25%
• 第 3 级：16%
• 第 4 级：9%
• 第 5 级：7%
• 第 6 级：3%

总体而言，本节结果表明，Ax-Prover 在各项任务中均表现出色：在数学领域跻身顶尖模型之列，在物理领域则显著超越其他方法。同时，这些结果也凸显了当前方法的两大关键局限：

• 专用证明器无法泛化到其训练领域之外；
• 通用大语言模型（LLM）虽具创造性，却无法生成严谨的 Lean 证明。

值得注意的是，Ax-Prover 在所有数据集上使用同一基础模型（Sonnet），其性能超过独立使用的 Sonnet 两倍以上；即使在 PutnamBench 上，当 Deepseek 和 Kimina 被允许进行高 pass@n 次尝试时，Ax-Prover 仍能超越它们。这表明，将智能体推理与 Lean 工具集成相结合，对于实现跨领域的鲁棒定理证明至关重要。我们将在下一节更详细地探讨这一方面。

5.3 工具使用分析

为衡量工具使用对我们方法的影响，我们分析了证明器（Prover）在 NuminaMath-LEAN 数据集中最具挑战性的Unsolved 子集（100 道问题）上所执行的工具调用情况。我们发现，证明器每次运行平均调用工具 100.76 次。工具使用具有极高的可靠性，成功率超过 99%。

表 4 列出了使用频率最高的 10 个工具。位居首位的是edit file，因为证明器在每一步都会更新 Lean 文件；紧随其后的是lean diagnostic messages，这反映了系统明确要求对每个证明步骤进行验证（见第 3.1.2 节）。lean goal用于暴露当前的证明状态，而lean loogle和lean search（原文为 lean leansearch，应为笔误）则使证明器能够在库中搜索相关定理。

重要的是，这些工具均由证明器自主调用，无需任何显式指导。总体而言，这些统计数据清晰地展示了 Ax-Prover 如何通过一个紧密的反馈循环——编辑、目标检查、搜索与诊断——来实现高效的形式化推理。

5.4 部署分析

除了性能之外，部署复杂性在现实世界中使用 AI 模型时同样至关重要。在此方面，我们对各类证明系统进行了比较。

DS-Prover 和 Kimina 需要配备 GPU 的高性能机器，且无法通过模型即服务（MaaS）。我们在 Google Cloud 上托管了这两个模型：

• DS-Prover 部署在配备 8 块 H200（141GB 显存）GPU 的 A3 Ultra 虚拟机上；
• Kimina 部署在配备 8 块 A100（40GB 显存）GPU 的 A2 High GPU 虚拟机上。

这种部署方式负担沉重，且需要专业的 MLOps 技能：用户必须匹配硬件规格、配置分布式运行环境、调试服务问题，并应对 GPU 资源稀缺的现实——云服务商对 H100/H200 等高端 GPU 实施严格的配额限制和漫长的排队等待。即便对于资源充足的团队，这也严重阻碍了实验的可复现性。

相比之下，Ax-Prover 仅依赖 API 调用，除基本的客户端访问外无需任何基础设施，既可在本地客户端机器上运行，也可在轻量级容器中远程执行。

在经济成本方面：在 1000 个数据点上运行，DS-Prover 约花费300 美元，Kimina 约2000 美元，而 Ax-Prover 约4000 美元。乍看之下，我们的方法似乎更昂贵，但这仅是因为我们对专用模型采用了pass@1的评估设置。若采用该领域常见的高 pass@n 设置（例如 PutnamBench 上使用的配置），则成本将急剧上升：

• DS-Prover（pass@1024）成本约为30.7 万美元
• Kimina（pass@192）成本约为38.4 万美元

此外值得注意的是，尽管消耗了远更多的计算资源，DS-Prover（pass@1024）在 PutnamBench 上仅解决了47 个定理，而 Ax-Prover（pass@1）却解决了92 个。

更广泛地看，通用大语言模型正快速迭代升级。例如，Claude Haiku-4.5 [7] 据称在推理与编程能力上已达到 Claude Sonnet 4 的水平，但成本仅为后者的三分之一。这表明，每一代新 LLM 都将以更低的成本提供更强的推理能力，从而使 Ax-Prover 的相对效率随时间不断提升。

专用模型的部署与成本壁垒，也解释了为何它们至今未能在 IMO 风格数学竞赛等基准场景之外实现广泛应用。对大多数研究者而言，管理专用硬件、应对 GPU 配额限制以及承担高昂费用，使得这些系统在实践中几乎不可用。

而 Ax-Prover 对研究者更为友好，不仅因为它消除了上述障碍，更因为它被明确设计为一名支持性助手——这一点将在下一节中进一步展示。

6 用例：密码学中面向研究者的友好型验证

Lean 中的自动定理证明为密码学及相关安全科学领域提供了一条标准化定义、假设和证明义务的可靠路径。当前，许多安全声明往往基于异构的假设和代数框架提出，这使得比较、复用和独立验证变得困难。学术界已多次呼吁采用更清晰、更统一的方法论与语义规范 [59, 14, 12, 32]。这一需求至关重要：细微的建模漏洞可能在系统部署后仍会破坏看似强大的安全保证。

例如，在隐私保护领域，Netflix Prize 数据集的去匿名化事件 [47] 以及马萨诸塞州团体保险委员会数据发布中的重识别攻击 [61] 都表明，对保护机制的非形式化推理在实践中可能失效。因此，对严格、机器可验证的证明的需求，不仅是一种学术偏好，更是构建可信数字系统的紧迫且具有社会意义的要求。

然而，Lean 中的完整形式化证明极其困难。除了需要掌握有限域、线性与多线性代数、概率论和信息论等领域的知识外，还要求具备依赖类型理论、战术设计和库导航等方面的证明工程技能[22, 36]。近期量子信息领域的专门工作也报告了类似挑战：将物理风格的推理与证明助手的语义对齐十分困难 [44]。

以下两个案例研究表明，Ax-Prover 有助于弥合这一鸿沟：通过将前沿推理能力与 Lean 工具结合，它能够在无需专用基础设施的情况下，实现研究级的形式化与验证，并提供交互式、编译器检查的反馈。在实践中，Ax-Prover 与研究人员协作——由人类专家提供领域洞察、问题分解和证明策略，而 Ax-Prover 则负责处理战术工程、库搜索、错误诊断和代码重构，从而弥补研究人员在 Lean 技能和形式方法知识上的不足。

6.1 用例一：经典密码学

现代密码学保护着日常数字系统。设计背后数学中的微小错误就可能引入漏洞，因此拥有可解释且可验证的证明至关重要。Lean 提供了一种统一且可审计的方式：定义共享、假设显式、证明可重运行和复用 [59, 14]。

我们考察了论文《一种计算有限域上非奇异矩阵分支数的新算法》[45]。简言之，该工作提出了一种更优的分支数（branch number）测试方法——分支数用于衡量密码强度，使设计者能快速筛选大量候选矩阵。

一位密码学研究者与 Ax-Prover 合作，在 Lean 中形式化了所需定义，并验证了论文的核心主张。Ax-Prover 负责处理 Lean 的技术细节、战术选择和错误诊断，补充了研究者的领域知识。在验证过程中，系统揭示了原非形式化论证中的一个漏洞：某些最小值是在特定参数下可能为空的集合上取的。我们最终的 Lean 形式化明确加入了必要的前提条件，从而避免了该问题。结果是一个机器验证的定理证书——约 2000 行 Lean 代码，在两天工作时间内于普通笔记本电脑上完成，并附带可用于未来分析的可复用引理（见附录 F）。该案例表明，工具增强、面向研究者的工作流能使有意义的密码学验证变得切实可行。

从时间与资源角度看，该密码学案例研究在一台笔记本电脑上用两个工作日完成了约2000 行 Lean 代码。作为对比，Math Inc. 近期对素数定理的 Lean 形式化 [43] 产生了超过25,000 行代码，耗时数周。但该工作依赖于大规模智能体基础设施 [43]、陶哲轩与 Alex Kontorovich 提供的部分 Lean 证明，以及研究人员为 Gauss 自动形式化智能体精心编写的详细蓝图。相比之下，Ax-Prover完全在单台笔记本上运行，从零开始（无任何现有 Lean 代码），无需蓝图设计，而是作为交互式助手，支持快速、可验证的进展。这凸显了面向研究者、工具辅助的形式化推理工作流在实践中的显著优势。

6.2 用例二：量子密码学

量子密码学追求基于物理原理的统计性、信息论安全，而非依赖计算能力受限的假设。量子密钥分发（QKD）是典型代表：双方通过检验量子关联来认证密钥的保密性，再应用信息论后处理。由于这些安全保证建立在算子理论、线性代数和概率论之上，它们天然适合自动定理证明。此前量子信息领域的 Lean 形式化工作已指出，将物理风格推导转化为机器可验证数学存在显著挑战 [44]。

我们聚焦于Lo-Chau 框架[41]，该框架影响了后续如 Shor-Preskill 对 BB84 协议的分析 [58]。其中关键一步是将一个物理测试（与 EPR 对的高保真度）转化为一个熵界（entropy bound），用以量化窃听者所能获取的信息上限。

借助 Ax-Prover，我们在 Lean 中形式化并证明了该熵界——即 Lo-Chau 引理 1（“高保真度蕴含低熵”），并将其导出为一个可复用的库引理（见附录 G）。具体而言，我们编码了保真度所隐含的谱约束，调用了冯·诺依曼熵的 Schur 凹性，并推导出所述熵界。所得引理成为形式化 QKD 分析的一个模块化组件，既加强了物理风格推理与机器可验证数学之间的接口，也回应了社区对标准化、可复用证明组件的广泛需求 [59, 14, 12]。

7 结论

我们提出了Ax-Prover——一种新颖的智能体工作流，将通用大语言模型（LLM）的广泛推理能力与 Lean 证明环境的形式化严谨性相结合。我们的系统解决了当前专用证明器存在的三大主要局限：(i) 难以泛化到数学以外的科学领域，且随着 Mathlib 等库的快速演进而迅速过时；(ii) 无法有效与人类专家协作，也无法利用外部工具；(iii) 工程实现与维护成本高昂。

评估结果表明：

• PutnamBench上，Ax-Prover 是表现最佳的开源模型，在所有模型中排名第三，且所用计算资源远低于顶尖模型；
• 在公开数据集NuminaMath-LEAN上，其性能优于基线模型；
• 在我们新引入的两个数据集——AbstractAlgebra（研究级抽象代数）和QuantumTheorems（量子物理定理）上，Ax-Prover 同样显著超越现有方法。

这些基准不仅为未来智能体的跨领域推理提供了新的测试平台，也标志着在任何以数学为基础的科学学科中评估推理模型的一个关键里程碑。

这些结果凸显了 Ax-Prover卓越的领域泛化能力，与难以适应训练数据之外新领域的专用模型形成鲜明对比。更重要的是，它们表明 Ax-Prover 有潜力成为需要长链严谨推理的科学人工智能系统中的深度形式化推理助手。通过将多学科推理与严格的形式验证相结合，该系统可在任何要求可验证、无错误推理的场景中支持 AI 驱动的科学发现。

我们将这一性能归功于其多智能体架构以及通过MCP（Model Context Protocol）与 Lean 工具的紧密集成。Ax-Prover 通过迭代编辑证明、检查目标、诊断错误，表现得如同一位谨慎的数学家，系统性地探索并验证每一步。实验中工具调用的高频次与高有效性证实了它们在提升证明质量、实现类人调试中的关键作用。

此外，我们的案例研究进一步表明：Ax-Prover 不仅能自主证明定理，还能与研究人员开展富有成效的协作。研究者将其作为合作伙伴，用于构建论证结构、验证引理、诊断证明失败原因。这种交互展示了 Ax-Prover 如何响应专家指导、加速验证流程，甚至能发现非形式化推理中的错误。

展望未来，我们计划通过引入并行化智能体来增强 Ax-Prover，使其能够同时探索多条证明路径，从而提升在复杂证明形式化中的创造力与成功率。我们还计划集成一个长期记忆模块，用于存储过往证明与人机交互中的信息。这一能力将使 Ax-Prover 不仅能处理孤立问题，还能参与长期、协作式的科研项目。

这些发展将推动我们迈向更宏大的目标：可验证的科学人工智能——即 AI 系统通过形式化验证的推理，真正参与到科学发现之中。

原文链接： https://arxiv.org/pdf/2510.12787