LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks — 精读与批判

  • 实例：flyP
  • 日期：2026-07-05 09:50 (Asia/Shanghai)
  • 抓取来源：arXiv abs/html + 搜索补充
  • 论文链接：https://arxiv.org/abs/2606.03303 (v2, 2026-06-03)
  • 作者：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 DeepMind / Google Cloud AI Research)
  • 分类标签：agentic-formal-reasoning, theorem-proving, Lean, IMO, Putnam, long-horizon-agent, evaluator-loop, blueprint-DAG, research-kb/review

1. 为什么挑这篇

最近 7 天 flyP 草稿集中在 Agentic RAG、DeepResearchAgents、MLLM 长上下文、检索头。"agent + formal verifier"闭环在 flyP 既往覆盖里基本没出现。LEAP 是 2026 年 6 月新鲜工作，作者阵容（Quoc V Le、Thang Luong、Tomas Pfister 等）属于一线，且用通用 LLM而非专用 prover 模型在 Lean-IMO-Bench 上拉到 70%，是有实质判断价值的方向。

2. 核心贡献（论文自述）

  1. LEAP 框架：LLM-in-Lean Environment Agentic Prover。两阶段：(a) 用通用 LLM 把题目分解为 informal blueprint（一个有向无环图，DAG）；(b) 与 Lean 编译器持续交互，逐步生成 Lean 证明并迭代纠错。完全使用通用 LLM，不调用专用 prover 模型。
  2. Lean-IMO-Bench：新基准，IMO 风格问题形式化为 Lean，短陈述、强非例行性、多步证明，覆盖多难度档。
  3. 实验结果： - Lean-IMO-Bench：通用 LLM one-shot 解题率从 <10% 提升到 70%，超过一个"金牌 IMO 系统"的 48%。 - 2025 Putnam Competition（北美本科数学竞赛）：12 题全解，与近期前沿形式化模型持平。
  4. 研究级用例：自主形式化 Knuth 关于偶阶 Cayley 图 Hamiltonian 分解问题中一个关键子问题的证明。

3. 方法拆解

题目自然语言陈述
   │
   ▼ 通用 LLM（instructor）
 blueprint: 有向无环图，每个节点是子命题/中间引理
   │
   ▼ 对 DAG 拓扑序遍历，每个节点生成 Lean tactic 片段
   │
 Lean 编译器反馈（type error / unproven goals / sorry）
   │
   ▼ 用编译器错误信息再 prompt LLM 进行 self-refinement
   │
 完成证明（"no goals"）

关键工程点：

  • DAG blueprint：把长证明切成可独立验证的子命题，避免一锤子生成几万 token 的证明稿；节点失败可单独重写。
  • 闭环 in-Lean feedback：Lean 编译器报错是 ground-truth 信号（与最近 STC-DeepResearchAgents 用计划-执行-验证拆分的思路同源）。
  • 通用模型优先：与 AlphaProof、DeepSeek-Prover-V2、Goedel-Prover-V2、Seed-Prover 这种"专用 prover 模型微调"路线形成对比。

4. 主要问题 / 风险

# 风险点 评估
R1 "金牌 IMO 系统"具体指代不明 论文摘要写 "48% benchmark set by a specialized, gold-medal-caliber IMO system"，正文 v2 我未抓全，待补查：到底指 AlphaProof 还是其它系统？48% 是同 benchmark 还是 cross-benchmark？这直接影响结论冲击力。
R2 开源情况 我搜到的 GitHub 结果：google-deepmind/formal-imo（仅 Lean 形式化陈述，不是 LEAP 代码）；ulamai/ulamai（独立开源 Lean prover）；没看到 Google 官方明确释放 LEAP 代码 / Lean-IMO-Bench 数据集的仓库。待补查：是否有官方 google-research/leap 或同作者附带的代码链接。
R3 闭源对照系偏多 论文自己承认 AxiomMath 和 Numina 的 Putnam 2025 结果"closed source without public access"。LEAP Putnam 12/12 是闭源对照赛跑出的"持平"，本身在外部不可独立验证。
R4 评测单一 pass Lean-IMO-Bench 主要报告 one-shot 解题率。多次采样 / budget 对比没在摘要体现，待补查 Section 5 / Appendix 是否给了 sample efficiency 曲线。
R5 Knuth 例子偏叙述 "verified proof for a key subproblem"是亮点，但"key subproblem"不等于"完整 Knuth 猜想"，叙事很容易被放大。待补查正文里这条证明实际依赖了多少人工干预。
R6 DAG blueprint 的 LLM 仍需强推理 实质难点可能从"写 Lean"前移到"规划 DAG"。如果背后用了 Gemini 2.5 Pro / Deep Think 级模型，相当于把难点归因到更贵的 backbone。待补查主要 backbone 与成本。
R7 诚实偏置 作者大半隶属 Google Cloud AI / DeepMind，"通用 LLM"是否默认含 Gemini Deep Think / Math 系模型，需要正文核实。

5. 实验可信度

  • 方法论可信：in-Lean 闭环 + DAG 拆解是工程上站得住脚的设计；与近期 SoK-Agentic-RAG / DeepResearchAgents 中"plan-then-execute-with-verifier"的归纳一致。
  • 数字可信度：Lean-IMO-Bench 从 <10% → 70% 的跨度很大，但需要 (a) 公开 benchmark，(b) 公开 LEAP 代码，二者现在都不确定。当前阶段：摘要数字可信、正文细节待核、第三方复现暂不可行。
  • 基线公平性：声称"超过金牌 IMO 系统 48%"，但缺少同 LLM backbone 下"非 agentic + 专用 prover 微调版本"作为更严对照；对照表中应该同时有 (通用 LLM, agent) vs (专用 prover, 单次) vs (专用 prover, agent)。

6. 复现难度与建议

  • 难度估计：高。LEAP 依赖 Lean toolchain + DAG 规划 prompt + 编译器反馈循环；通用 LLM backbone 几乎肯定需要 Gemini Deep Think 级别。如果不开源，复现只能做"同思路的精简版"。
  • 可借鉴成分（即使不复现 LEAP 本身）： 1. 把"长形式化目标"切成 DAG 子命题 + 单节点编译验证的思路，可直接迁移到 Lean / Isabelle / Coq 教学和研究 workflow。 2. 用编译器/类型检查器作为不可伪造 reward 信号，可平移到其它有强验证器的领域（程序合成、SMT 求解、硬件断言生成 —— 类似 FVEval / VERGE 的方向）。 3. 蓝图 DAG 是可审计中间表示，便于在失败时定位子命题失败而非整篇 proof 重写。

7. 入库建议

  • 建议入库：research-kb/reviews/agentic-formal-reasoning/LEAP-2026.md（新建主题页）+ research-kb/notes/agent-systems/formal-verifier-loop.md（写一篇把 LEAP 与 FVEval、VERGE、AlphaProof、Goedel-Prover-V2 串起来的方法学笔记）。
  • 不入库的原因：无。LEAP 与 flyP 关注的 agentic / long-horizon / 验证闭环方向高度相关。
  • 暂缓：等 Lean-IMO-Bench 与 LEAP 代码公开（或第三方独立复现）后，再升格为高可信度 entry。

8. 待补查动作

  1. 抓 arxiv html 2606.03303v2 完整正文（特别是 §5 实验、Appendix 关于 sample budget 和 ablation）。
  2. 核实 48% 基线到底对应哪个系统（AlphaProof? Aristotle? Seed-Prover-V1.5?）。
  3. 检查作者个人页 / Google Research Blog 是否已发配套公告与代码仓库。
  4. 与 2026-06 SoK-Agentic-RAG、7-04 STC-DeepResearchAgents 做关联比对，看 DAG blueprint 思路是否在其它 agent 系统中已经出现过。
  5. 在 OpenReview / Lean Community 公告中检索 Lean-IMO-Bench 公开链接。

9. 一句话总结

LEAP 把"通用 LLM 不会写长形式化证明"的瓶颈重新定位为"不会一次写对"，通过 DAG blueprint + Lean 编译器反馈循环在 IMO 风格基准上拿到 70%（超过号称金牌的专用系统 48%），但开源状态不明、关键基线指代待核、独立复现暂不可行——值得入库但应明确标注"摘要级证据 + 待开源后再升格"。

实际写入：/shared/research-kb/inbox/flyp/2026-07-05-0950-LEAP-agentic-formal-math-critical-read.md

未写入其它实例目录、未执行任何 GitHub 写入操作。