---
title: "LEAP: Agentic Formal Theorem Proving with General LLMs"
created: 2026-07-03
updated: 2026-07-03
type: paper
tags: ["formal-mathematics", "theorem-proving", "lean", "agentic", "google"]
sources: ["arxiv:2606.03303"]
arxiv_id: "2606.03303"
authors: "Po-Nien Kung, Linfeng Song, Dawsen Hwang, Jinsung Yoon, Chun-Liang Li, Simone Severini, Mirek Olšák, Edward Lockhart, Quoc V Le, Burak Gokturk, Thang Luong, Tomas Pfister, Nanyun Peng"
venue: "arXiv 2026 (Google Cloud AI / DeepMind)"
code: "https://github.com/google-deepmind/superhuman/tree/main/leap"
---

# LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

> [原始存档](raw/papers/leap-agentic-atp.md) | 代码: [google-deepmind/superhuman/leap](https://github.com/google-deepmind/superhuman/tree/main/leap) | Benchmark: [imobench.github.io](https://imobench.github.io)

## 核心贡献

LEAP (LLM-in-Lean Environment Agentic Prover) 是一个 **仅使用通用 LLM**（无需专用证明器模型微调）的 agentic [[formal-theorem-proving|形式化定理证明]] 框架。它挑战了「通用 LLM 不适用于严格形式化任务」的既有假设——通过 agentic 框架设计，通用 LLM 可以在 ATP 上达到甚至超越专用系统。

同时引入 [[lean-imo-bench|Lean-IMO-Bench]]——将 IMO 级别问题形式化到 [[lean-proof-assistant|Lean]] 中的新基准。

## 架构：蓝图驱动的自动化定理证明

LEAP 的核心工作流（Figure 1）：

```
给定定理 → 注册为 OR 节点（根目标）
    ↓
直接形式化路径：
  非正式证明 → 翻译 Lean → 编译器验证
  → 失败 → LLM 驱动修正循环（重写 + 重试）
    ↓ 仍失败
分解路径：
  非正式蓝图生成 → 形式化证明草图（AND 节点）
  → 子目标（新 OR 节点）→ 递归处理
```

三个关键设计选择：

### 1. [[and-or-dag-memoization|AND-OR DAG 分层记忆化]]

- **OR 节点**：开放目标（可用任意有效策略解决）
- **AND 节点**：候选分解（需证明所有子目标才算成功）
- **单调精化**：分解后可在不破坏已有依赖结构的前提下修改/扩展/放弃
- **引理记忆化**：中间引理跨分支复用
- **预期引理规划**：可提前提出辅助引理——当前不需要但未来可能有用

### 2. [[interleaved-informal-formal-planning|非正式-形式化交错规划]]

LLM 的优势在非正式推理、策略生成和自修正；Lean 提供严格的机器可验证检查。LEAP 在两条路径中都经过非正式证明草图——这是规划空间，使证明构建比直接生成代码更稳健。

### 3. [[verification-guided-proof-search|验证引导的证明搜索]]

两层验证：
- **Lean 编译器**：形式化检查语法和类型正确性；sketch 中仅允许 `sorry` 占位符用于新声明的子目标
- **LLM Reviewer**：评估分解质量——子目标是否相关、是否简化问题、是否为合理路径。这是**搜索过滤器**：识别无前途的分解，触发回溯，鼓励探索替代策略

## 实验结果

### Putnam 2025（12 题，仅 2 rollouts）

| 方法 | 解决率 | 备注 |
|------|--------|------|
| Gemini-3.1-pro (Pass@128) | 0% | 单次生成不足 |
| Goedel-Prover-V2-32B | 0% | 专用 ATP 模型 |
| Hilbert (2 rollouts) | 33.3% | Agentic + 专用模型 |
| Aristotle (2 rollouts) | 75.0% | IMO Gold 专用系统 |
| **LEAP (2 rollouts)** | **100%** | **仅通用 LLM** |

### Lean-IMO-Bench（60 题）

| 方法 | 解决率 |
|------|--------|
| Gemini-3.1-pro (Pass@128) | <10% |
| Goedel-Prover-V2-32B | ~5% |
| Aristotle | 48% |
| **LEAP** | **70%** |

### Knuth 哈密顿分解

LEAP 自主形式化了 Knuth 偶数阶 Cayley 图哈密顿分解中一个关键子问题的验证证明——展示了研究级别的实用性。

## 关键洞察

- 瓶颈不在形式语言理解，而在于**缺乏与证明环境的结构化、迭代式交互**
- Agentic 分解 + 交错规划 + 验证引导搜索三者的组合，让通用 LLM 超越了专用系统
- LLM Reviewer 作为搜索启发式评估器的方向值得关注——当前只是简单的 DFS + 回溯

## 相关概念

- [[formal-theorem-proving|形式化定理证明]]
- [[lean-proof-assistant|Lean 证明助手]]
- [[autoformalization|自动形式化]]
- [[and-or-dag-memoization|AND-OR DAG 记忆化]]
- [[blueprint-driven-atp|蓝图驱动 ATP]]
- [[interleaved-informal-formal-planning|非正式-形式化交错规划]]
- [[verification-guided-proof-search|验证引导证明搜索]]
- [[lean-imo-bench|Lean-IMO-Bench]]
- [[anticipatory-lemma-planning|预期引理规划]]