2.7 KiB
2.7 KiB
title, created, updated, type, tags
| title | created | updated | type | tags | ||||
|---|---|---|---|---|---|---|---|---|
| LEAP Review | 2026-07-03 | 2026-07-03 | review |
|
LEAP: Agentic Formal Theorem Proving — Review
📌 基本信息
- 论文：LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
- 作者：Po-Nien Kung et al. (Google Cloud AI / DeepMind)
- arXiv：2606.03303 | 领域：cs.AI | 日期：2026-06-02
- 代码：google-deepmind/superhuman/leap
🎯 核心概念
- AND-OR DAG 分层记忆化 — 证明树组织为有向无环图：OR 节点=开放目标，AND 节点=候选分解。支持单调精化、跨分支引理复用、预期引理规划
- 蓝图驱动 ATP — 仿效人类数学家工作流：非正式蓝图 → 形式化证明草图 → 子目标递归。直接形式化失败后的回退策略
- 非正式-形式化交错规划 — LLM 管策略推理（自然语言），Lean 管严格验证（代码）。在形式化之前先用非正式草图规划
- 验证引导证明搜索 — 双层：Lean 编译器（硬约束）+ LLM Reviewer（软约束/搜索过滤器）。消融实验证明 Reviewer 不可省略
- Lean-IMO-Bench — 60 题 IMO 级新基准，专为测试非平凡洞察和长链多步证明设计
🔗 概念网络
- 核心三角：blueprint-driven-atp ↔ and-or-dag-memoization ↔ verification-guided-proof-search
- 伞概念连接：formal-theorem-proving → lean-proof-assistant → autoformalization
- 跨域关联：LEAP 的 agentic 设计与 workspace-first-architecture 共享「分解+隔离」的设计范式
- 新增 10 概念 + 1 论文 = 11 页
📚 Wiki 集成
| 组件 | 状态 |
|---|---|
papers/leap-agentic-formal-math-2026.md |
✅ |
raw/papers/leap-agentic-formal-math-2026.md |
✅ |
| 伞概念 ×3 | ✅ |
| 专属概念 ×7 | ✅ |
| Review | ✅ |
💡 关键洞察
- 通用 LLM 可以超越专用 ATP 模型 — 前提是有正确的 agentic 框架。LEAP 证明瓶颈不在语言理解而在缺乏结构化迭代交互。Putnam 2025 12/12，Lean-IMO-Bench 70%（vs 专用 Aristotle 的 48%），仅 2 次 rollout
- 「非正式蓝图 → 形式化代码」的双层规划是通用范式 — 这不仅是 ATP 的设计模式，也是任何需要 LLM 在严格约束下生成代码的通用策略：先规划、再翻译、验证反馈迭代
- LLM Reviewer 作为搜索启发式 — 当前只是过滤弱分解，但方向是 LLM 作为启发式评估器引导搜索（不只在 ATP，在 Agent 规划中也是通用方向）