LEAP：利用代理框架增强LLMs在形式数学中的能力

# LEAP：利用智能体框架极大提升大语言模型在形式化数学中的能力
来源：https://arxiv.org/html/2606.03303
\\uselogo\\correspondingauthor

ponienkung@google\.com\\reportnumber

Linfeng SongGoogle CloudDawsen HwangGoogle DeepMindJinsung YoonGoogle Cloud AI ResearchChun\-Liang LiGoogle Cloud AI ResearchSimone SeveriniGoogle CloudMirek OlšákGoogle DeepMindEdward LockhartGoogle DeepMindQuoc V LeGoogle DeepMindBurak GokturkGoogle Cloud AI ResearchThang LuongGoogle DeepMindTomas PfisterGoogle Cloud AI ResearchNanyun PengGoogle Cloud AI Research

###### 摘要

大型语言模型（LLMs）在非正式数学推理方面表现强劲，但在生成Lean等语言中可机械验证的证明方面却困难重重。我们提出LEAP（LLM-in-Lean环境智能体证明器），这是一个智能体框架，能使通用基础模型在自动化形式定理证明上达到最先进性能。LEAP利用了基础模型的能力，如非正式推理、指令遵循和迭代自我改进。通过将复杂问题分解为更小的单元，该系统通过与Lean编译器持续交互，在形式证明构建与非正式蓝图之间架起桥梁。为了在日益饱和的基准测试之外提供严格的评估，我们引入了Lean-IMO-Bench，这是一个在Lean中形式化的IMO风格问题基准，其特点是陈述简短但证明过程高度非常规、多步骤且难度范围广泛。实验表明，在最新的2025年普特南数学竞赛（北美本科生年度数学竞赛）中，LEAP解决了全部12个问题，与前沿形式化数学模型的近期突破持平；在Lean-IMO-Bench上，LEAP将通用大语言模型的单次形式化解题率从低于10%提升至70%，显著超过了专门IM O金牌级系统设定的48%基准。此外，我们通过自主形式化解决开放组合学挑战的复杂证明，包括验证了Knuth偶数阶Cayley图哈密顿分解中一个关键子问题的证明，展示了LEAP的研究级实用性。

## 1 引言

大型语言模型（LLMs）在使用自然语言进行数学推理方面取得了令人瞩目的进展，这通常被称为“非正式数学推理”，它在数学竞赛和研究级数学中展现出强大的复杂推理和问题解决能力[huang2025winning, luong2025geminiimo, feng2026towards, feng2026aletheia, feng2026semi]。然而，正如Hilbert[hilbert]和Goedel-Prover-V2[goedel_prover_v2]等近期工作所讨论的，自然语言的解决方案常常存在逻辑谬误和幻觉，并且难以自动验证。这种验证困难不仅是自动化系统的局限；即便是对人类数学家而言，验证复杂的证明也是一个出了名的耗时过程，需要稀缺的专家劳动力[greiffenhagen2024checking]。一个著名的例子是开普勒猜想的证明[hales2005proof]，它花费了四年的同行评审，最终审稿人只能声称对其正确性有“99%的把握”，111https://en.wikipedia.org/wiki/Kepler_conjecture 最终还需要长达十年的形式化验证努力[hales2017formal]。这个验证瓶颈突显了在自然语言中评估正确性是一项艰巨的任务，从而激发了对形式化数学的探索。在形式化数学中，证明用机器可检查的语言编写，并由严格的验证内核（如Lean[moura2021lean]、Isabelle[nipkow2002isabelle]、Coq[huet1997coq]、HOL Light[harrison2009hol]）进行验证，提供了有保证准确性的自动化验证。然而，弥合与形式定理证明的差距仍然是一个重大挑战，自动化形式证明器的性能目前远落后于使用自然语言的通用大语言模型。

为了弥合这一差距，研究界的近期努力主要集中在专门的形式化证明器模型（例如，AlphaProof[alphaproof]、DeepSeek Prover V2[deepseek_prover_v2]、Seed Prover[seed_prover]、Goedel Prover V2[goedel_prover_v2]）在形式化语料库上进行微调，其假设是通用大语言模型在没有专门化的情况下对严格的形式化任务效果不佳。事实上，根据FormalProofBench[formalproofbench]222该论文附带一个私有数据集和一个公开排行榜 https://www.vals.ai/benchmarks/proof_bench。我们多次联系他们希望参与排行榜，但未收到回复。和TaoBench[taobench]的结果，通用大语言模型的性能通常不如专门的证明器模型。

虽然一些近期工作探索了智能体或推理时搜索，但它们仍然依赖于专门的模型。例如，Hilbert[hilbert]、AlphaProofNexus[sketchprover]、Aristotle[aristotle]和Seed Prover V1.5[seed_prover_v1_5]使用通用大语言模型进行非正式推理，但依赖专门模型进行Lean证明步骤。Axiom333https://github.com/AxiomMath/putnam2025 和Numina444https://github.com/project-numina/Numina-Putnam2025 声称在2025年普特南竞赛上取得了强劲结果，但仍是闭源的，无法公开访问，使其在科学上无法验证。

在本文中，我们表明，虽然通用大语言模型在单次定理证明中仍然受限，但瓶颈并非语言理解，而是在一次尝试中生成冗长、复杂且正确的证明。通用大语言模型为专门模型提供了互补的技能：强大的非正式推理、指令遵循、工具使用和自我改进。这些使其成为智能体自动化定理证明（ATP）框架的理想选择，在该框架中，证明构建被分解并迭代改进。为此，我们引入了**LEAP**（LLM-in-Lean Environment Agentic Prover），一个**仅**使用通用大语言模型进行形式化数学的智能体框架。受人类工作流程启发，LEAP首先生成一个高层蓝图，形成有向无环图（DAG），然后生成Lean证明，并通过编译器反馈迭代修正错误。

为了评估在MiniF2F[zheng2022minif2f]和PutnamBench[putnambench]等日益饱和的基准测试之外的进展，我们引入了Lean-IMO-Bench，将具有挑战性的非正式数学基准IMO-Bench[imo-bench]的问题陈述形式化为Lean。与现有基准测试（要么侧重于较短问题，要么强调广泛的本科覆盖面）相比，Lean-IMO-Bench针对一个互补领域：那些解决方案通常依赖于高度非常规洞察力，并通过冗长、多步骤且结构复杂的证明展开的基本陈述，为形式定理证明提供了更严格的测试。

实验上，在最新的2025年普特南数学竞赛（一项具有挑战性的北美年度本科生数学竞赛，2025年最高分是110分（满分120），中位数仅为2分）中，LEAP在Lean中解决了全部12个问题，取得了完美表现。这与此前前沿形式化数学推理模型（如Axiom3 (https://arxiv.org/html/2606.03303#footnote3) 和Numina4 (https://arxiv.org/html/2606.03303#footnote4)）的突破性成果相匹配。在Lean-IMO-Bench上，LEAP将通用大语言模型的解题率从低于10%大幅提升至70%，超过了专门的ATP模型（5%）和Aristotle（48%）。Aristotle是一个包含专门ATP组件的强大系统，在2025年IMO中获得了金牌成绩。本文的贡献有三点：

- **受工作流程启发的智能体设计**：我们引入了LEAP，一个智能体框架，它将人类数学工作流程编码化——结合高层蓝图草拟与底层形式证明生成及迭代编译器反馈。关键在于，LEAP证明了仅使用通用大语言模型即可实现最先进的形式定理证明，挑战了“专用微调不可或缺”的信念。
- **Lean-IMO-Bench数据集**：为了评估在MiniF2F和PutnamBench等饱和基准之外的进展，我们引入了Lean-IMO-Bench，这是一个新的挑战性数据集，将IMO-Bench中的非正式问题陈述翻译成形式化的Lean陈述。资源可在 https://imobench.github.io/ 获取。
- **强大的实证结果与洞察**：LEAP解决了2025年普特南竞赛的全部12个问题，并在Lean-IMO-Bench上相比先前基线取得了巨大改进。我们的分析表明，通用大语言模型在形式化数学中的主要瓶颈并非仅仅是形式语言理解，而是缺乏与证明环境的结构化、迭代式交互。LEAP生成的Lean解决方案可在 https://github.com/google-deepmind/superhuman/leap/ 获取。

## 2 LEAP：蓝图驱动的自动化定理证明

### 2.1 使用蓝图形式化证明

形式化数学证明很少是一次性完成的任务：它需要一个结构化的计划，逐步将高层论证转化为Lean。为了管理这种复杂性，近期的形式化工作通常使用Lean Blueprint工具555https://github.com/PatrickMassot/leanblueprint，它允许数学家编写一个人类可读的证明路线图，该路线图与Lean代码链接，并可视化为有向无环图（DAG），其中每个节点代表一个证明义务。这个工作流程在协调大型项目中发挥了关键作用，例如费马大定理的形式化路线图666https://leanprover-community.github.io/blog/posts/FLT-announcement/，其中一项多年的证明工作通过显式的依赖图进行组织。

受此工作流程启发，我们引入了LEAP，一个用于自动化定理证明的智能体，具有层次化分解和规划能力。LEAP不是一次性合成完整的证明，而是逐步起草蓝图，将Lean目标分解为支撑引理，并将演进中的证明计划维护为一个与或DAG。

参见标题图1：LEAP工作流程。LEAP首先尝试直接形式化，并配合编译器反馈修订和LeanSearch[leansearch]检索。如果失败，则生成非正式蓝图和形式证明草图，仅在依赖关系保持无环时将已验证的子目标添加回DAG。

### 2.2 概述

图1 (https://arxiv.org/html/2606.03303#S2.F1) 展示了LEAP的工作流程。给定一个输入定理，LEAP将其Lean陈述注册为**根目标**，777**目标**是任何需要证明的定理或引理陈述；分解引入**子目标**。参见附录C (https://arxiv.org/html/2606.03303#A3)。在AND-OR DAG中表示为一个OR节点。为了处理一个开放目标，**状态读取器**会获取其陈述、依赖关系和相关引理。LEAP随后首先尝试**直接证明**：生成一个非正式证明，将其翻译成Lean代码，并用Lean编译器检查候选证明。

如果直接证明失败，LEAP转为**分解**。它首先起草一个非正式蓝图，提出中间引理，然后将蓝图翻译成Lean证明草图。该草图假定仅使用所提出的引理来证明当前目标：主定理主体是**无sorry**的，而`sorry`占位符仅允许出现在新提出的引理陈述中。如果草图被Lean编译器接受，则将其作为AND节点添加，而提出的引理则作为子OR节点添加。这确保了所有子子目标一旦被证明，父目标也就被证明。然后，验证过的草图被传递给**状态写入器**，它在将更新提交到DAG之前检查更新是否保持无环性。然后，智能体递归处理新创建的子目标。

这个工作流程依赖于三个紧密耦合的设计选择：**基于DAG的层次化记忆化**，它保留进度并跨分支重用引理；**交织的非正式-形式化规划**，它将自然语言策略与可执行的Lean代码连接起来；以及**验证引导的证明搜索**，它使用编译器反馈和基于LLM的评审来接受、修订、分解或放弃候选分支。

### 2.3 通过DAG进行层次化记忆化

LEAP使用AND-OR DAG不仅是为了记录证明进度，也是为了结构化层次化记忆化。OR节点代表开放目标或引理陈述，每个都可以通过任何有效的证明策略来解决；而AND节点代表候选分解，其成功取决于证明所有组成子目标。图2 (https://arxiv.org/html/2606.03303#S2.F2) 展示了这种结构。

DAG提供了两个核心优势。首先，**单调细化**：一旦一个目标被分解为支持性子目标，后续搜索可以专注于扩展和解决这些后代，而无需重构已建立的依赖顺序。这将局部证明探索与全局证明组织分离开来：单个证明尝试可以修订、扩展或放弃，而DAG则保留整体证明计划的稳定依赖结构。其次，**引理记忆化**：中间引理陈述被存储为共享的证明节点，并且可以在不同分支中出现相同子问题时重用。这也支持**预期引理规划**：在蓝图生成期间，LEAP可能提出当前草图不立即需要但可能支持后续证明步骤的辅助引理陈述。这些预期的引理在图形内存中保持可用，而不需要成为解决当前AND节点的必要条件。总之，这些特性允许独立的证明计划汇聚在共同的依赖关系上，同时减少冗余推导。

由此产生的依赖结构也提高了透明度：它揭示了哪些目标仍然开放，哪些引理已被解决，以及哪些节点阻碍了后续进展。这有助于LEAP确定何处可能需要额外的引理、修订的分解或更强的假设，同时为人类-AI协作提供了一个可解释的蓝图式工作空间。

### 2.4 交织的非正式-形式化规划

如图1 (https://arxiv.org/html/2606.03303#S2.F1)所示，LEAP中的直接证明路径和蓝图分解路径都经过一个非正式证明草图。这反映了LLMs和Lean互补的优势：LLMs擅长非正式推理、策略生成和改进，而Lean提供严格的机器可检查验证。

在直接证明中，LEAP首先为当前目标生成一个非正式论证，然后再将其翻译成候选的Lean证明。在分解中，它起草一个非正式蓝图，解释目标如何被简化为支持性子目标，然后将该计划转换为记录所提议依赖关系的Lean草图。在这两种情况下，非正式草图在形式化之前提供了一个规划空间，使证明构建比单独的直接代码生成更不脆弱（参见附录C (https://arxiv.org/html/2606.03303#A3) 中的非正式证明和蓝图示例）。

这种交织也使得证明进度更具可解释性：每个形式化尝试都与一个非正式理由配对，允许用户检查为什么提出某个证明步骤或分解，而不仅仅是阅读Lean代码或编译器反馈。

### 2.5 验证引导的证明搜索

如图1 (https://arxiv.org/html/2606.03303#S2.F1)所示，LEAP在两个层面使用验证。首先，Lean编译器正式检查候选证明和草图，确保接受的代码在语法上有效且类型正确。对于证明草图，LEAP仅允许在所提议的子目标（引理）处使用`sorry`占位符。这保留了证明DAG的AND-OR语义：一旦所有被引用的子目标都得到证明，父目标也就被证明。其次，在蓝图提出新的子目标后，一个LLM评审器会评估它们的可证明性和有用性——如果子目标太过强大或难以实现，则拒绝该分解，转而触发修订或回溯。