LEAP：用 Agentic 框架让通用大模型在形式化数学上达到 SOTA

瓶颈不在数学推理，而在形式化

Table 1 的数据很能说明问题。在 Lean-IMO-Bench 上，Gemini 2.5 Pro 用自然语言解题的基础集通过率 55.2%——说明数学推理能力是够的。但同一套模型换成 Lean 形式化证明，Gemini 3.1 Pro 的 Pass@128 直接掉到 20%（基础集）和 3.3%（高级集）。给你正确的自然语言证明再翻译成 Lean，Pass@128 没变，Avg.@128 只涨了 0.6%。

结论很清楚：数学推理不是瓶颈，可靠生成有效 Lean 代码才是瓶颈。

AND-OR DAG：证明不是树，是图

LEAP 围绕一个 AND-OR DAG 构建。OR 节点表示开放目标或待证引理——任何一种有效的证明策略都能解决它。AND 节点表示候选分解——所有组成子目标都必须被证明才算成功。这个 DAG 同时承担两个功能：

单调细化：一旦目标被分解为子目标，后续搜索只需要扩展和解决后代，不需要重构已建立的依赖关系。局部证明探索和全局证明组织被彻底分离。

引理记忆化：中间引理存储为共享证明节点，不同分支遇到同一子问题时直接复用。更聪明的是前瞻性引理规划——LEAP 可以在蓝图生成阶段提出当前不需要但可能支撑后续步骤的辅助引理，这些引理留在图记忆中随时待命。

Figure 2: LEAP 的 AND-OR DAG 示例（Putnam 2025 A6）。实线边是已建立依赖，虚线边是前瞻性引理。绿色节点已证明。

非形式-形式交织规划

LEAP 不直接从目标生成 Lean 代码。无论走直接证明路径还是蓝图分解路径，都先经过一个非形式证明草图——LLM 先写一段自然语言论证，再翻译成 Lean 候选证明。这个"缓冲区"让证明构建比直接代码生成脆弱性低得多。

两层验证并行工作：Lean 编译器检查形式正确性（语法、类型），LLM Reviewer 评估分解质量（子目标是否相关、是否真正降低了难度）。这个 LLM Reviewer 本质上是搜索过滤器——识别无望的分解、触发回溯。

Figure 1: LEAP 框架总览。直接证明路径和蓝图分解路径都经过非形式草图，再进入 Lean 验证循环。

实验结果：碾压级

Putnam 2025：12 道题，Gemini 3.1 Pro 直接形式化 0/12，Hilbert 4/12（33.3%），Aristotle 9/12（75%），LEAP 12/12（100%）。Hilbert 的递归搜索导致指数级复杂度，每个 rollout 需要 7 天时限。LEAP 最难的 A6 题需要 3000 次 LLM 调用，但简单题只需 46 次。

Lean-IMO-Bench：LEAP 基础集 83.3%、高级集 56.7%，代数和数论在两个难度级别都是 100%。Aristotle 基础集 76.7%、高级集 20.0%。所有方法在几何类别接近零分。

消融实验的三个关键发现

迭代能力是通用的：Gemini 3.1 Pro 迭代 Pass@1（36.6%）超过单次 Pass@128（20%）。但 Goedel-Prover-V2 从 10% 降到 6.6%——专用证明器不具备迭代修正能力。LEAP 选通用大模型作 reasoning backbone 是对的。

DAG 记忆化是核心：去掉全局引理共享的树结构变体，基础集解决率从 83.3% 降到 63.3%。

LLM Reviewer 是安全阀：去掉它，解决率从 70% 降到 40%。Agent 会反复扩展弱蓝图，浪费搜索预算。

研究级能力验证

LEAP 自主对 Knuth 偶数阶 Cayley 图 Hamilton 分解的关键子问题完成了形式化验证——约 20 页密集组合论证的非形式证明被分解为结构化 Lean 证明图。这是真实的研究级形式化，不是 benchmark 刷分。

工程启示

LEAP 的成功提出一个通用框架设计原则：不要训练专用模型适配形式化系统——构建让 LLM 通用能力（推理、规划、迭代修正、工具使用）能被结构化利用的 Agent 框架。AND-OR DAG 不限于定理证明，任何需要将复杂目标分解为可验证子任务、维护中间结果、支持前瞻性规划的领域都可以借鉴。