LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

原始存档 | 代码: google-deepmind/superhuman/leap | Benchmark: imobench.github.io

核心贡献

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

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

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

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

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

三个关键设计选择：

1. and-or-dag-memoization

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 + 回溯

4.5 KiB Raw Permalink Blame History Unescape Escape