LEAP：当通用大模型遇见形式化数学——脚手架如何击败盲目微调

> 论文标题: LEAP: LLM-in-Lean Environment Agentic Prover > 作者: Po-Nien Kung, Linfeng Song, Dawsen Hwang, et al. (Google DeepMind) > 论文链接: https://arxiv.org/abs/2606.03303 > 项目资源: 开源框架，基于通用LLM（Gemini 3.1 Pro）

---

一、引言：形式化数学的"最后一公里"难题

形式化数学——使用Lean、Isabelle、Coq等严格语言编写机器可验证的证明——是数学推理的"圣杯"。它消除了人类证明中常见的逻辑漏洞和直觉跳跃，将数学真理建立在不可动摇的计算基础之上。

然而，这道门槛高得惊人。即使是顶级数学家，要将一个复杂的非形式化证明转化为形式化代码，也可能需要数年时间。2014年，Georges Gonthier团队完成开普勒猜想的形式化验证，耗费了10年时间和海量人力。

大语言模型（LLM）的出现带来了希望。它们在非形式化数学推理上表现出色，能生成看似合理的证明思路。但当被要求直接输出Lean代码时，即使是Gemini、GPT这样的 frontier 模型，成功率也接近零。

为什么？因为形式化证明不是"翻译"问题，而是结构化工程问题：

需要将高层次论证分解为可管理的引理
需要理解Lean的类型系统和tactic库
需要处理编译器反馈，迭代修正代码
需要在数百行代码中维护全局一致性

传统解决方案是专门化微调——训练专用证明器模型（AlphaProof、DeepSeek Prover V2等）。这些模型在大量形式化数据上微调，学习Lean的语法和证明模式。但代价是巨大的计算资源投入，以及模型泛化能力的受限。

LEAP提出了一个激进的问题：如果我们不微调，而是给通用LLM一个足够好的脚手架，会怎样？

---

二、核心洞察：瓶颈不在语言，而在结构

LEAP的核心假设颠覆了领域惯例：

> 通用LLM的失败，不是因为它们不懂数学或不懂Lean，而是因为一次性生成长、复杂、正确的证明超出了任何模型的单跳能力。

这个洞察来自对失败模式的观察：

通用LLM能写出正确的非形式化证明思路
通用LLM能理解Lean编译器的错误信息
通用LLM能根据反馈修订代码
但让它们一次性输出2000行零错误的Lean代码？几乎不可能

LEAP的策略是：不要试图让LLM一次性做对所有事情，而是设计一个智能体架构，让LLM在结构化环境中逐步构建证明。

这类似于人类数学家如何工作：先画蓝图，再填细节；遇到障碍时分解问题；验证每一步的正确性。

---

三、LEAP框架深度拆解

3.1 架构概览：蓝图驱动的证明工厂

LEAP是一个智能体框架，而非单一模型。它将定理证明视为一个规划-执行-验证的循环过程，核心组件包括：

┌─────────────────────────────────────────────────────────────┐
│                     LEAP 核心循环                            │
├─────────────────────────────────────────────────────────────┤
│  输入: 目标定理 T                                             │
│                                                              │
│  1. State Reader (状态读取器)                                │
│     └── 检索定理陈述、已有引理、相关上下文                     │
│                                                              │
│  2. NL Prover (非形式化证明器)                               │
│     └── 生成自然语言的证明思路或分解蓝图                       │
│                                                              │
│  3. Formal Prover (形式化证明器)                             │
│     └── 将非形式化内容翻译为Lean代码                         │
│                                                              │
│  4. Verifier (验证器) ──→ Lean编译器                         │
│     └── 检查语法、类型、逻辑正确性                           │
│         ├─ 通过 → 更新DAG，标记目标为解决                     │
│         └─ 失败 → Reviser基于错误信息重写                     │
│                                                              │
│  5. Reviewer (审查器)                                        │
│     └── LLM评估分解质量，过滤无前景的子目标                   │
│                                                              │
│  6. State Writer (状态写入器)                                │
│     └── 将新引理/分解提交到DAG，检查无环性                   │
└─────────────────────────────────────────────────────────────┘

3.2 关键创新一：AND-OR DAG 层次记忆化

LEAP最重要的数据结构是一个有向无环图（DAG），其中节点分为两类：

节点类型	含义	逻辑
OR节点	开放目标（待证明的定理/引理）	可被任意有效证明策略解决
AND节点	候选分解（一个证明计划）	成功当且仅当所有子目标被证明

为什么DAG比树更重要？

传统的递归搜索（如Hilbert）使用树结构，存在致命缺陷：

指数级冗余：不同分支可能独立发现相同的中间引理
无法共享：一个分支证明的引理，另一个分支无法复用
重复劳动：相同子问题被反复求解

LEAP的DAG解决了这些问题：

1. 引理记忆化（Lemma Memoization）：已证明的引理成为共享节点，任何需要它的分支直接引用，无需重新证明

2. 预期引理规划（Anticipatory Lemma Planning）：高层节点可以提出当前不需要但下游可能有用的辅助引理，提前布局

3. 单调细化（Monotonic Refinement）：一旦目标分解为子目标，后续搜索只扩展这些后代，不重构已建立的依赖顺序

实际效果：在消融实验中，移除DAG退化到朴素树结构，Lean-IMO-Bench Advanced集上的求解率从56.7%降至40.0%——证明DAG的共享机制对复杂问题至关重要。

3.3 关键创新二：交织的非形式化-形式化规划

LEAP的一个反直觉设计是：所有证明尝试都先经过自然语言阶段。

路径	流程
直接证明	生成非形式化论证 → 翻译为Lean代码 → 编译器验证
分解	起草非形式化蓝图（中间引理） → 翻译为Lean草图 → 编译器验证结构

为什么这样做？

1. 利用LLM的优势：通用LLM在非形式化推理上远强于形式化代码生成。让LLM先在"舒适区"规划，再翻译到Lean，比直接生成代码更可靠。

2. 可解释性：每个形式化步骤都配对自然语言原理，用户可以检查为什么采取某个证明步骤。

3. 错误隔离：非形式化阶段的错误更容易被发现和修正，避免在Lean的语法细节中迷失。

4. 渐进式形式化：蓝图可以包含sorry占位符，允许逐步细化——先确认分解结构正确，再填充子证明。

3.4 关键创新三：验证引导的证明搜索

LEAP使用两级验证来指导搜索：

第一级：Lean编译器（硬验证）

检查语法、类型正确性
确保引理调用与声明匹配
在证明草图中，只允许对新提出的子目标使用sorry

第二级：LLM审查器（软启发式）

评估分解质量：子目标是否更简单？是否与父目标相关？
过滤无前景的分解，避免在死胡同上浪费计算
触发回溯，鼓励探索替代策略

关键消融实验：在Putnam 2025 A5问题上，完整LEAP（含LLM审查器）在2次rollout内成功；移除LLM审查器后，8次rollout仍失败。审查器的作用是识别那些"形式上可接受但数学上无进展"的分解。

例如，一个糟糕的分解可能提出一个与祖父目标句法相同的子目标——Lean编译器会接受它（因为类型匹配），但证明实际上没有推进。LLM审查器能识别这种循环依赖。

---

四、实验结果：从0%到100%的跨越

4.1 Putnam 2025：全歼12题

William Lowell Putnam数学竞赛是北美本科生的顶级赛事，2025年最高分110/120，平均分仅约10分。

方法	类型	解决题目	求解率
Gemini-3.1-pro (Pass@128)	通用LLM直接形式化	0/12	0%
Goedel-Prover-V2-32B (Pass@128)	专用证明器	0/12	0%
Hilbert (开源框架)	混合系统	4/12	33.3%
Aristotle (专有，IMO金牌级)	专有系统	9/12	75.0%
LEAP	通用LLM + 智能体	12/12	100%

关键洞察：

直接形式化（即使是专门证明器）完全失败，证明"单次生成"策略的局限性
Hilbert作为开源框架，受限于指数级搜索复杂度，7天内只能解决4题
Aristotle作为专有IMO金牌级系统，仍遗漏3题
LEAP用通用LLM + 智能体架构，实现了100%求解

效率数据：

最简单题（b2）：46次LLM调用，300行证明
最难题（a5）：3000次LLM调用，2000行证明，170个活跃DAG节点

4.2 Lean-IMO-Bench：从<10%到70%

LEAP团队构建了一个新基准Lean-IMO-Bench，包含60道IMO风格问题（30基础/30高级），特点是：简短陈述但高度非常规、多步骤、结构复杂。

方法	基础集 (%)	高级集 (%)
Gemini-3.1-Pro (Pass@128)	20.0	3.3
Goedel-V2-32B (Pass@128)	10.0	0
Hilbert	36.6	6.6
Aristotle	76.7	20.0
LEAP	83.3	56.7

领域细分：

代数：LEAP 100%（基础/高级），完美表现
数论：LEAP 100%（基础/高级），完美表现
组合：LEAP 100%（基础）/ 25%（高级）
几何：所有方法接近0%——形式化奥林匹克几何在Lean中仍需要领域特定框架

关键发现：通用LLM的一次性形式化求解率低于10%，但LEAP将其提升到70%。这表明差距不在模型能力，而在架构设计。

4.3 研究级应用：Knuth的开放问题

LEAP不仅处理竞赛题，还展示了研究级能力：

Donald Knuth的Hamilton分解问题：

问题：有向Cayley图的边能否划分为三个Hamilton圈
挑战：20页密集的非形式化证明，涉及3D路由动态
LEAP成果：自主分解为结构化证明图，合成>5000行Lean代码，完整验证

Erdős问题457：

自主从第一原理推导已知证明
无需人工干预，将复杂文献转化为高保证形式证明

---

五、与现有方法的深度对比

5.1 专门证明器模型 vs. LEAP

维度	专门证明器 (AlphaProof, DeepSeek Prover V2)	LEAP
核心假设	通用LLM不经专门化对形式化任务无效	通用LLM在适当脚手架下可实现竞争性能
训练成本	大量计算资源，高度特定	零微调，仅使用通用API
泛化能力	受限于训练数据分布	继承通用LLM的广泛知识
迭代能力	通常一次性生成	利用编译器反馈循环改进
可解释性	黑盒生成	每步配对自然语言原理

关键证据：Goedel-Prover-V2-32B在迭代形式化中表现更差（10.0% → 6.6%），证明它缺乏解释错误、维护上下文、多步修订的能力——而这些正是通用LLM的强项。

5.2 混合系统 (Hilbert) vs. LEAP

Hilbert是LEAP最直接的比较对象，两者都使用通用LLM + 搜索。但架构差异导致性能鸿沟：

特性	Hilbert	LEAP
搜索结构	树，指数复杂度 O((n·b)^d)	DAG，共享引理，多项式复杂度
记忆化	无	引理记忆化 + 预期规划
Putnam求解	4/12 (33.3%)	12/12 (100%)
Lean-IMO基础	36.6%	83.3%

Hilbert的递归搜索设计导致指数级冗余LLM调用。LEAP的DAG架构从根本上解决了这一瓶颈。

5.3 专有系统 (Aristotle) vs. LEAP

Aristotle是IMO 2025金牌级系统，闭源， presumably 使用了专门化组件。

指标	Aristotle	LEAP
Putnam 2025	75%	100%
Lean-IMO基础	76.7%	83.3%
Lean-IMO高级	20.0%	56.7%
可验证性	闭源，不可科学验证	开源，可复现

LEAP全面超越，且仅使用通用LLM，无需专门训练。

---

六、设计哲学：脚手架胜过微调

LEAP的成功揭示了一个更广泛的原理：

> 对于需要深度推理和严格验证的任务，精心设计的智能体脚手架可能比昂贵的专门化微调更有效。

这一原理与TDV论文（本期另一篇解读）形成有趣呼应：两者都质疑"更强假设/更多专门化"的传统路径，探索"更弱假设/更通用架构"的可能性。

LEAP的脚手架设计体现了几个关键原则：

1. 分解优于端到端：将复杂问题分解为可管理的子目标，降低每步的认知负荷 2. 验证引导搜索：使用硬验证（编译器）确保正确性，软启发式（LLM审查器）引导搜索方向 3. 记忆化避免重复：DAG结构确保已证明的引理被复用，而非重复发现 4. 人机协作界面：自然语言蓝图使人类可理解和干预

---

七、局限性与未来方向

7.1 当前局限

局限	说明
几何领域	所有方法在Lean-IMO-Bench几何类别上接近0%，需要领域特定框架（如GeoCoq）
计算成本	复杂问题需要大量LLM调用（Putnam A5: 3000次），成本较高
搜索效率	当前使用简单DFS，未充分利用LLM作为启发式评估器进行智能剪枝
数据质量依赖	在视频数据集（Ego4D、FineVideo）上的扩展实验显示，运动一致性对TDV很重要

7.2 未来方向

1. 混合架构：将通用LLM的结构推理与专门证明器的局部步骤生成结合，可能是效率最优解 2. 智能搜索：用LLM作为价值函数评估分解质量，实现更高效的MCTS或A*搜索 3. 几何集成：整合GeoCoq等几何专用框架，攻克IMO几何题 4. 成本优化：开发更轻量的审查器和更高效的分解策略，降低LLM调用次数

---

八、结论：形式化数学的新范式

LEAP的意义远超一个竞赛成绩。它证明了：

1. 通用LLM的潜力被低估：它们不仅是"聊天机器人"，在适当架构下可执行严格的、可验证的推理任务 2. 脚手架设计是关键：智能体架构可以弥补单跳生成的局限性，释放模型的累积能力 3. 开源可复现：与闭源专有系统不同，LEAP的方法完全透明，可被科学社区验证和改进

正如论文所言：

> "现代通用LLM在配备适当结构支架时，对严格的领域特定任务具有实质性的推理能力。"

LEAP不仅为形式化数学开辟了道路，也为其他需要严格验证的领域（如程序验证、硬件设计、协议分析）提供了可借鉴的范式：不要急于专门化，先尝试更好的脚手架。

---

参考论文

Kung, P. N., Song, L., Hwang, D., et al. (2026). *LEAP: LLM-in-Lean Environment Agentic Prover*. arXiv:2606.03303.
相关对比方法：AlphaProof, DeepSeek Prover V2, Goedel Prover V2, Hilbert, Aristotle

#论文解读 #形式化数学 #自动定理证明 #智能体框架 #LLM #Lean #GoogleDeepMind #数学推理 #AIforMath #小凯