智能体的形式数学证明框架

Prover Agent：基于智能体的形式数学证明框架

PROVER AGENT: AN AGENT-BASED FRAMEWORK FOR FORMAL MATHEMATICAL PROOFS

https://arxiv.org/pdf/2506.19923

摘要：

我们提出了 Prover Agent——一种用于自动定理证明的新颖人工智能智能体，它将大语言模型（LLMs）与形式化证明助手 Lean 相结合。Prover Agent 协调一个非形式化推理 LLM、一个形式化证明模型以及来自 Lean 的反馈，同时还能生成辅助引理。这些辅助引理不仅限于形式化证明中的子目标，还可包括特殊情形或从假设中推导出的潜在有用事实，有助于发现可行的证明策略。它在 MiniF2F 基准上达到了 88.1% 的成功率，在使用小型语言模型（SLMs）的方法中创下新纪录，且所需的样本预算远低于以往方法。我们还提供了理论分析和案例研究，阐明这些生成的引理如何助力解决具有挑战性的问题。代码已公开发布：https://github.com/kAIto47802/Prover-Agent。

1 引言

近年来，大语言模型（LLMs）在推理能力方面的进步推动了人工智能多个领域的显著进展，包括数学定理证明与问题求解（OpenAI, 2024；DeepSeek-AI, 2025；Yang 等, 2025a；Lewkowycz 等, 2022）。然而，LLMs 容易产生错误和幻觉，从而削弱其可靠性（Ji 等, 2023；Huang 等, 2025；Xu 等, 2025）。推理时扩展技术（如思维链，chain-of-thought）通过让模型反思并修正错误的推理步骤，大幅提升了其推理性能（Wei 等, 2022）。尽管如此，彻底消除错误仍然极具挑战性，尤其对于更困难的问题（Wei 等, 2022；Zeng 等, 2025）。

形式化证明助手（如 Lean（Moura & Ullrich, 2021）、The Rocq Prover（原 Coq）（Barras 等, 1999）和 Isabelle（Paulson, 1994））基于 Curry–Howard 对应关系，通过计算机严格验证用其语言书写的数学证明中每一步推理的正确性。这帮助数学家确保证明的严谨性——在此过程中，不允许任何错误、细节遗漏、隐含假设或歧义。然而，使用形式化证明助手通常需要耗费大量人工精力并关注极致细节。因此，自动定理证明长期以来一直是人工智能与形式化方法领域的一项重大挑战（Newell & Simon, 1956；Irving 等, 2016；Polu & Sutskever, 2020；Jiang 等, 2023；Lu 等, 2023）。

近年来，将 LLM 用于形式化定理证明变得日益重要，催生了大量相关研究（Wang 等, 2024b；Wu 等, 2024a；Xin 等, 2025b；Li 等, 2025；Xin 等, 2025a；Dong & Ma, 2025；Lin 等, 2025b；Zhang 等, 2025；Wang 等, 2025；Ren 等, 2025；Ji 等, 2025；Lin 等, 2025c；Cao 等, 2025；Zhou 等, 2025；Chen 等, 2025）。这不仅为保证 LLM 数学推理的正确性提供了途径，也标志着自动定理证明的重大突破。关键在于 LLM 与形式化证明助手的互补优势：LLM 擅长推理与生成，但可能出错且缺乏正确性保证；而 Lean 等形式化证明助手则具备基于数理逻辑的完美验证能力，却不具备生成性。

然而，在非形式化推理与形式化证明之间仍存在显著鸿沟（Yang 等, 2025b）。例如，即使 o3-mini（OpenAI, 2025）在自然语言数学竞赛题上表现优异，若直接提示其为一道竞赛级问题生成完整 Lean 证明，单次尝试的成功率仅为 6.0%（Yousefzadeh & Cao, 2025）。即便在数学数据上微调、使用强化学习或引入思维链，纯神经方法仍难以生成正确的形式化证明，其形式化证明能力远落后于其自然语言中的非形式化推理能力。

为弥合这一差距，我们提出一种新颖的智能体框架（Prover Agent），协调非形式化推理 LLM、形式化证明模型与 Lean 验证系统。针对无法直接求解的难题，该智能体生成辅助引理以协助发现可行的证明策略。这些引理不仅限于可直接插入形式化证明的子目标，还可包括特殊情形或从假设中推导出的潜在有用事实。当整体证明策略初始不明确时，这类引理尤其有效，有助于构建可行的证明计划。在 MiniF2F 基准（Zheng 等, 2022）上，该方法达到 88.1% 的成功率，在使用小型语言模型（SLMs）的方法中创下新纪录。值得注意的是，它仅使用 SLMs，且样本预算远低于以往高性能方法，推理成本显著更低。此外，我们还提供了理论分析与案例研究，展示智能体生成辅助引理的有效性。

我们的贡献总结如下：

• 结合非形式化与形式化推理，并利用 Lean 反馈：我们的智能体在 Lean 验证下协同非形式化 LLM 与形式化证明器。LLM 生成自然语言推理与引理，证明器将其形式化，Lean 进行验证。Lean 检测到的错误立即反馈，支持对构造的证明进行迭代优化。
• 通过辅助引理生成实现策略发现：对于难以直接求解的问题，智能体生成辅助引理（如特殊情形、潜在有用事实或假设驱动的猜想），并对其进行形式化证明。通过结合已验证引理重新审视整体证明，系统即使在初始路径不明的情况下也能发现可行策略。
• 当前最优的定理证明性能：在 MiniF2F 基准（Zheng 等, 2022）——一个包含 488 道来自数学奥林匹克与高等数学的标准形式化定理证明基准——上，我们的智能体达到 88.1% 的通过率，在使用 SLMs 的方法中树立了新标杆。
• 推理成本高效：88.1% 的成功率仅使用 SLMs 实现，且样本预算远低于以往高性能方法，凸显了本方法在推理成本上的高效性。

2 相关工作

本节简要概述自动形式化定理证明的近期进展，代表性系统的详细信息见附录 A。

基于树搜索的形式化证明：树搜索方法逐策略（tactic-by-tactic）构建 Lean 证明，通过显式搜索（如最佳优先搜索或蒙特卡洛树搜索 MCTS）导航证明空间（Lample 等, 2022；Wang 等, 2023；Wu 等, 2024a；Zhou 等, 2024；Li 等, 2025；Xin 等, 2025a,b）。该方向始于由目标状态引导的逐步策略预测，现已发展为优化策略模型、搜索启发函数和数据筛选以处理更长证明的成熟系统。

整体证明生成：与树搜索互补的是整体证明生成（First 等, 2023），即模型一次性输出完整 Lean 脚本，常伴随长思维链推理轨迹。该方法通过专家迭代流程（将已验证证明回流至训练）（Polu 等, 2023；Wu 等, 2021, 2024a；Lin 等, 2025a,b,c；Dong & Ma, 2025）以及利用形式化验证器反馈的强化学习（Kaliszyk 等, 2018；Xin 等, 2025a；Zhang 等, 2025；Wang 等, 2025；Ren 等, 2025；Gloeckle 等, 2024；Ji 等, 2025；Lin 等, 2025c）不断进步。

结合检索增强生成（RAG）的形式化定理证明：另一新兴方向是将基于 LLM 的证明器与检索增强生成结合，在推理时查询外部知识源或证明库以补充模型推理（Yang 等, 2023；Shen 等, 2025）。

证明精炼与子目标分解：部分工作探索了证明精炼——根据证明助手的反馈改进初始证明尝试（Thakur 等, 2024；Zhou 等, 2025；Chen 等, 2025；Lin 等, 2025c）。另一方向涉及子目标分解——将复杂定理拆解为更易证明的简单子目标（Dong 等, 2025；Wang 等, 2024a；Ren 等, 2025；Zhou 等, 2025），常由自然语言草图引导（Jiang 等, 2023；Cao 等, 2025）。

子目标分解方法与我们的工作有一定相似之处，但我们的方法采用了更全面的策略，将其纳入更广框架。在前述工作中，必须预先正确构想完整的证明草图，而这往往很难做到。相比之下，我们的方法并不要求从一开始就完全看清整体证明策略。我们不仅限于与预定义证明计划直接对齐的子目标分解，还考虑特殊情形或潜在有用事实等辅助引理，以自底向上的方式逐步构建证明策略。

3 方法

整体工作流程如图 2 所示，对应的伪代码见算法 1。给定一个形式化数学问题，我们的智能体首先尝试直接证明——这对较简单的问题通常已足够。对于无法直接求解的更难问题，它会生成辅助引理以揭示可行的证明策略。这些引理随后被分别形式化并逐一证明，最终利用已证引理合成原问题的完整证明。在整个过程中，Lean 的反馈被用于对构造的证明进行迭代优化。下文将分阶段描述该过程，重点说明非形式化 LLM、形式化证明模型与 Lean 如何协同构建形式化证明。

3.1 基于非形式化推理与迭代反馈的形式化证明构建

智能体首先尝试在不进行分解的情况下直接证明给定问题或所生成的引理。为利用非形式化 LLM 相较于形式化证明模型更强的数学推理能力，我们首先使用非形式化 LLM 为该问题或引理生成一段自然语言的非形式化证明。随后，形式化证明模型以此非形式化证明作为上下文引导，生成形式化证明，并交由 Lean 验证。若验证成功，则此步骤完成；若失败，则重复上述过程，直至找到成功证明或达到最大尝试次数 N init
。该过程有助于为后续的迭代精炼阶段建立更优的初始证明草稿。

若证明仍失败，智能体进入迭代精炼阶段。从此前所有尝试中选取 Lean 验证错误最少的证明作为初始草稿。随后，基于 Lean 的反馈对该草稿进行迭代修正：在每次迭代中，将上一次的证明尝试、错误位置及对应的错误信息一并提供给证明模型，由其修改并生成修正后的证明版本。该过程持续进行，直到证明被 Lean 成功验证，或达到最大精炼尝试次数 N refine
。

这一迭代精炼过程利用 Lean 的验证能力识别并修正错误，本质上是一种通过上下文学习实现的自纠错机制，类似于人类如何从反馈中改进理解。这有效弥补了推理时扩展（如思维链）的一个关键局限：单纯增加推理步数并不能保证更好结果，因为模型的自纠错能力有限（Zeng 等, 2025；Song 等, 2025；Stechly 等, 2025；Huang 等, 2024）。

此外，若某个生成的引理无法被证明，系统可放弃该引理——这模拟了人类数学家的典型做法：当整体策略尚不清晰时，常会探索多个方向，其中一些最终被证明无效而被舍弃，转而聚焦更有希望的路径。或者，若引理本身仍过于困难，系统还可递归地引入更小的辅助引理，最多递归至深度上限 D 。

3.2 通过非形式化推理生成引理

当直接证明方法失败时，智能体会生成若干辅助引理。这些引理不仅限于可直接插入最终证明的子目标，还可包括特殊情形或从假设中推导出的潜在有用事实，以帮助构建证明策略。这是与先前工作的关键区别：以往方法通常依赖于根据预定义的证明草图将问题分解为子目标（Jiang 等, 2023；Wang 等, 2024a；Ren 等, 2025；Cao 等, 2025；Zhou 等, 2025）。这类方法要求事先构想出正确的整体证明策略，而这往往极具挑战性。事实上，这些方法通常依赖 DeepSeek-V3（DeepSeek-AI, 2024）和 DeepSeek-R1（DeepSeek-AI, 2025）等更大、更强的模型，以期从一开始就准确预测整个证明计划。

相比之下，我们的方法不要求从一开始就看清整体证明策略。通过生成辅助引理，智能体能够以自底向上的方式逐步构建有效的证明策略，即使初始时完整结构并不明确。

这种方法模仿了人类数学家通常的工作方式：当整体策略在初始阶段不清晰时，他们往往会探索特例或思考从假设中能推导出什么内容。通过这种试错过程，他们逐步发现整体证明策略。

系统首先以自然语言生成引理，以利用非形式化大语言模型更强的数学推理能力。随后，这些引理由一个形式化模型转换为形式化语句——该模型仅形式化其前提和结论，而不尝试构造证明。Lean 也在此用于验证这些形式化语句的语法正确性，直至它们被重新生成为有效语句为止。这些经形式化后的引理随后使用第 3.1 节所述的证明构建流程进行证明。

3.3 基于已验证引理与迭代反馈的最终证明合成

4 理论分析

我们提出理论分析，以论证第 3 节所述方法的有效性。
引理的使用具有两个关键作用：(i) 在给定策略下对证明步骤进行分解，使其更易处理；(ii) 在初始阶段尚不明确合适证明策略时，辅助发现该策略（例如通过检验特殊情形）。以往工作主要聚焦于 (i)，通常依赖更大的模型来直接构思整体策略（Wang 等, 2024a；Jiang 等, 2023；Ren 等, 2025；Cao 等, 2025；Zhou 等, 2025），而我们的方法同时利用 (i) 和 (ii)，从而更有效地解决困难问题。第 4.1 节和第 4.2 节分别简要呈现了针对情形 (i) 和 (ii) 中引理使用的理论分析结果。详见附录 C。

4.1 引理在结构化证明分解中的优势

证明详见附录 C.1。定理 4.4 表明，基于引理的分解能在所需尝试次数的数量级上带来指数级提升；而定理 4.5 指出，对于较小的 p p （即困难问题），使用引理可减少所需的尝试次数。这为我们的方法提供了理论支持：对难题生成引理，而对简单题直接求解。此外，定理 4.6 表明，最优引理是那些能将原问题划分为难度大致相等子问题的引理。

4.2 引理在发现证明策略（例如特殊情形）中的优势

此外，该结果还意味着：不仅引理，任何与最终正确证明共享互信息的上下文信息，同样可以提升成功概率，从而为我们使用自然语言证明和 Lean 反馈的做法提供了理论依据。

5 实验

5.1 实验设置

存在若干可能导致无效 Lean 证明被错误接受的漏洞，例如与 apply? 策略相关的用户界面缺陷（Ren 等，2025），以及 REPL² 中的一个 bug。为避免这些问题、防止无效证明被误判为正确，我们改用 lake build 而非 REPL 来验证证明，并额外确认未使用 apply? 策略。此外，为规避该漏洞并获得可靠的基线结果，我们重新运行了针对 Goedel-Prover-V2-8B 的实验。

我们使用 GitHub³ 和 Hugging Face⁶ 上提供的官方提示词，同时保持其他所有实验设置与我们方法中的完全一致，从而确保公平比较。对于 DeepSeek-Prover-V2，我们依赖 Ren 等人（2025）报告的结果——其中该漏洞已被修复。更多细节请参见附录 D。

5.2 主要结果：与先前最先进方法的比较

结果如表 1 和图 1 所示。我们的智能体达到了 88.1% 的成功率，在使用小型语言模型（SLMs）的方法中创下新的当前最优纪录。值得注意的是，我们的智能体仅使用 260 的样本预算就取得了这一结果，远低于以往工作，凸显了其在推理成本方面的高效性。

5.3 模块化与可扩展设计

为验证我们方法的鲁棒性，我们在多个模型上进行了实验，包括 DeepSeek-Prover-V2 和 Goedel-Prover-V2。如表 1 所示，在两种设置下，我们的方法均以更小的样本预算取得了比原始模型更高的成功率。此外，我们的方法还能对这些模型进行集成：在样本预算平均分配给两个模型的实验中，智能体取得了更高的成功率，表明模型之间能互补解决单个模型无法攻克的问题。
与端到端训练单一大型模型的单体方法不同，我们的方法采用正交策略——无需任何训练，直接组合现有的 LLM 与证明器模型。这种模块化设计具有实际优势：系统可通过简单替换组件，立即受益于 LLM 和证明器模型的最新进展，并能轻松随未来技术进步而扩展。

5.4 非形式化、形式化与 Lean 协同的有效性

表 1 显示，在两种模型设置下，即使在迭代精炼之前，我们的方法已优于对应的原始基线，凸显了与非形式化 LLM 协作带来的收益。此外，在引入迭代精炼后，性能进一步提升。

5.5 消融研究：分析各阶段的贡献

5.6 案例研究：引理引导证明的成功实例

接下来，我们通过一个案例研究来展示引入辅助引理的方法在实践中确实有效。该问题的详细讨论及相关输出（包括生成的引理、最终形式化证明及对应的推理过程）见附录 E。我们分析了一个直接证明尝试失败、但借助辅助引理最终成功证明的问题。

在此案例中，我们的智能体生成了一个对应于将 n = 3 代入原问题的特殊情形引理，同时还生成了其他可能与求解相关的辅助引理。如在使用该引理时的思维链过程所见（参见附录 E.5），智能体立即关注 n = 3 的情形，并迅速提出数学归纳法作为证明策略。这使其能够快速转入在清晰证明计划下的细节填充阶段，并最终完成证明。此外，在辅助引理中考虑的策略与证明技巧也重新出现在后续推理过程和最终证明中：即使某个引理本身未被直接使用，其生成过程中探索的技巧仍为整体证明构建提供了宝贵线索。

作为对比，我们进一步考察了不使用引理时的推理过程，聚焦于最终错误最少的轨迹（见附录 E.6）。与成功使用引理的情形相比，此处的证明策略远不够清晰，模型在缺乏连贯计划的情况下徘徊不定。结果，即便它最终想到了使用数学归纳法，也无法展开具体细节，导致证明失败。这一对比凸显了我们辅助引理方法的有效性——它超越了以往工作中简单的子目标分解，真正助力发现并执行可行的证明策略。

5.7 在奥林匹克级别问题上的表现

表 2 展示了 MiniF2F 测试集上各子类别的结果。这些结果表明，在 DeepSeek-Prover-V2 设置下，我们的方法在奥林匹克级别问题上表现尤为出色，甚至超越了 Ren 等人（2025）提出的 DeepSeek-Prover-V2——后者使用了规模大得多的 671B 模型，并且样本预算高达 8192。值得注意的是，即使我们仅使用无迭代精炼的直接证明方法，且样本预算仅为 100，其性能已超过 DeepSeek-Prover-V2。这表明，与基于自然语言的非形式化推理协同工作可能是关键所在。

奥林匹克级别问题对数学推理能力要求极高，而非形式化 LLM 强大的推理能力很可能在此发挥了决定性作用。另一方面，在 MATH 和 Custom 类别中，我们的智能体并未超越 DeepSeek-Prover-V2。这些类别中持续存在的性能差距表明，模型规模和样本预算在此可能更为重要。由于 DeepSeek-Prover-V2 本身已具备一定的数学推理能力，因此能独立处理这些相对数学难度较低的问题。相比之下，在 Goedel-Prover-V2 设置下，各类别之间未观察到显著差异。这很可能是因为 Goedel-Prover-V2 已经具备处理所有这些类别所需的基本数学能力，因此类别间的差异并不明显。

5.8 更广泛的适用性与未来潜力

我们的流程中没有任何部分是专为数学竞赛问题设计的。只要 LLM 具备相关领域知识或被提供适当的知识库，该方法同样可应用于其他领域的形式化证明，例如学习理论或物理学。这为实现无幻觉、无逻辑错误的人工智能驱动的数学理论构建提供了潜在路径。

6 结论

我们提出了 Prover Agent——一种模块化框架，协调非形式化推理大语言模型（LLM）、形式化证明模型与 Lean 验证系统。通过生成辅助引理并结合反馈驱动的精炼机制，我们的方法在 MiniF2F 基准上取得了使用小型语言模型（SLMs）方法中的当前最优性能。未来工作包括开发针对不同类型问题生成更有效引理的机制，并将本框架拓展至数学以外、但同样需要形式化验证的领域，例如软件验证。

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