45 lines
2.3 KiB
Markdown
45 lines
2.3 KiB
Markdown
# LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
|
||
|
||
- **arXiv ID**: 2606.03303
|
||
- **标题**: LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
|
||
- **作者**: 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
|
||
- **机构**: Google Cloud AI Research, Google Cloud, Google DeepMind
|
||
- **领域**: cs.AI
|
||
- **发表**: 2026-06-02
|
||
- **代码**: https://github.com/google-deepmind/superhuman/tree/main/leap
|
||
- **Benchmark**: https://imobench.github.io
|
||
|
||
## 摘要
|
||
|
||
LEAP (LLM-in-Lean Environment Agentic Prover) 是一个仅使用通用 LLM（无需专用证明器模型微调）的 agentic 形式化定理证明框架。核心设计：(1) 非正式蓝图 + 形式化证明的双层规划；(2) AND-OR DAG 分层记忆化；(3) 验证引导的证明搜索。
|
||
|
||
## 核心架构
|
||
|
||
**工作流**：给定定理 → 注册为根目标（OR 节点）→ 直接形式化尝试 → 失败则进入分解路径：
|
||
1. **直接形式化路径**：生成非正式证明 → 翻译为 Lean 代码 → 编译器验证 → 失败则进入 LLM 驱动的修订循环
|
||
2. **分解路径**：生成非正式蓝图（DAG 子目标）→ 翻译为 Lean 证明草图 → 添加为 AND 节点 → 子目标变为新 OR 节点 → 递归处理
|
||
|
||
**三个关键设计选择**：
|
||
- DAG 分层记忆化：保留进展、跨分支复用引理、支持预期引理规划
|
||
- 非正式-形式化交错规划：LLM 负责推理策略，Lean 负责严格验证
|
||
- 验证引导搜索：编译器形式检查 + LLM reviewer 质量评估（过滤弱分解）
|
||
|
||
## 关键结果
|
||
|
||
| Benchmark | LEAP | Aristotle (IMO Gold) | Baseline |
|
||
|-----------|------|---------------------|----------|
|
||
| Putnam 2025 (12 题) | **12/12 (100%)** | 9/12 (75%) | 0/12 (0%) |
|
||
| Lean-IMO-Bench Basic | **70%** | - | <10% |
|
||
| Lean-IMO-Bench Advanced | 显著提升 | 48% (总体) | ~3% |
|
||
|
||
- 仅 2 次 rollout（vs baselines 的 128 次）
|
||
- 自主形式化 Knuth 哈密顿分解的开放组合挑战的子问题验证证明
|
||
|
||
## 核心概念
|
||
|
||
- AND-OR DAG 分层记忆化
|
||
- 非正式蓝图 → 形式化证明交错规划
|
||
- 验证引导证明搜索（编译器 + LLM reviewer）
|
||
- 预期引理规划（anticipatory lemma planning）
|
||
- Lean-IMO-Bench 基准
|