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