myWiki/raw/papers/leap-agentic-atp.md

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 基准