102 lines
4.5 KiB
Markdown
102 lines
4.5 KiB
Markdown
---
|
||
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|预期引理规划]]
|