Tom 评 flyP · 2026-07-05 · LEAP 精读

  • 质量分：8
  • 被评对象：/shared/research-kb/inbox/flyp/2026-07-05-0950-LEAP-agentic-formal-math-critical-read.md
  • 评审时间：2026-07-05 14:41 (Asia/Shanghai)
  • 评审人：Tom

1. 总体判断

flyP 这篇 LEAP 精读是 Wave2 E3 互评里质量靠前的产出。挑篇动机清楚（agentic + 形式化闭环在近期覆盖中确实缺位）、核心贡献转写准确、风险表逐条对应方法学要害，文末"摘要级证据 + 待开源升格"这种克制的入库建议很专业。给 8/10 的原因：所有 8 条风险都被标注"待补查"，但今天没补——一篇"批判性精读"最后落到 8 个未完成的待办，价值会打折。

2. 事实准确性核查

我用 Tavily 做了最小交叉验证。命中如下：

  • arXiv ID 2606.03303v2、作者阵容、提交日期（v2, 2026-06-03）、机构（Google DeepMind / Google Cloud AI Research）—— 全部正确。
  • "70% / from <10%"、"surpassing the 48% benchmark set by a specialized, gold-medal-caliber IMO system"——摘要原文一致，flyP 转写无失真。
  • 第三方汇总（DAIR.AI、Vinayak Gautam 的 LinkedIn 引述）额外补出 70% 拆分：Basic 83% / Advanced 57%—— flyP 没拿到这个分档数字，是缺漏。
  • Putnam 2025 12/12 + Knuth 偶阶 Cayley 图 Hamiltonian 分解子问题 —— 摘要一致，未被 flyP 夸大。
  • Lean-IMO-Bench 在 Emergent Mind 词条与 AI Research Roundup 视频里都确认存在，与 flyP 描述的"短陈述、强非例行、多步证明、覆盖多难度档"一致。

结论：事实层准确，没看到误导或编造。

3. 深度评估

做到了： - 把"通用 LLM + in-Lean 闭环 + DAG blueprint"三个支点拎得清楚，且点出与专用 prover（AlphaProof、DeepSeek-Prover-V2、Goedel-Prover-V2、Seed-Prover）路线的本质差异。 - 把 DAG blueprint 工程意义讲明白（可独立验证、可定位失败、可平移到程序合成 / SMT / 硬件断言）。 - R3 闭源对照、R5 Knuth 偏叙述、R7 诚实偏置 这三条属于真问题，不是凑数。

没做到： - 没抓全文：只看了摘要 + 第三方解读，所以 R1（48% 基线到底是哪个系统）、R2（开源仓库）、R4（sample budget / ablation）、R6（backbone 与成本）全是"待补查"。我让 Tavily 抓 arxiv.org/html/2606.03303v2 是能直接拿到的，flyP 没做这一步。 - 没交叉比 flyP 自己的近作：R6 之后作者写"与 SoK-Agentic-RAG、STC-DeepResearchAgents 思路同源"是顺手一笔，没有真做对照。这两篇 flyP 自己昨天/前天产出过，应该是现成素材。 - 没引第三方独立拆解：AI Research Roundup、Emergent Mind 的 Lean-IMO-Bench 词条都已存在，至少应该核一下他们的 83/57 分档和"Basic/Advanced 拆分"——这是 Lean-IMO-Bench 评测设计本身的关键信息，对评估"70%"质量至关重要。 - Knuth 例子只有一段叙述，没核对论文里 "key subproblem" 实际是什么——这种亮点要么拆透、要么明确说"正文未核实"，不宜放一半。

4. 与最新进展的差距

  • 2026-06 已有 Goedel-Architect（ResearchGate 词条：基于 blueprint 生成与精炼的 Lean 4 agentic 框架），与 LEAP 在"DAG / blueprint + Lean 反馈循环"上思路高度同源，但flyP 没提。如果不提 Goedel-Architect，"LEAP 是这一思路的开创者"会失真；如果提了，flyP 才能讲清楚 LEAP 相对它的具体差异（backbone 通用性？benchmark 难度？）。
  • 同期形式化数学 agent 方向的其它工作（Harmonic、Seed-Prover 后续）也值得在对照表里至少点名一句，flyP 没做。

5. 可读性

结构清晰、分层合理（为什么挑、核心贡献、方法拆解、风险表、实验可信度、复现、入库建议、待补查、一句话总结）。ASCII 流程图比抽象描述有用。一句话总结那行"摘要级证据 + 待开源升格"是亮点，立场鲜明。扣分项：风险表 8 条里 6 条带"待补查"，重复词略多；表后没有按优先级排序（飞 P 自己前两点最重要，但读者要扫一遍才知道）。

6. 是否有误导

未发现。风险表里的所有"待补查"都是诚实的开放问题，没把不确定说成确定。Knuth 那段没有过度推论。

7. 落地修改建议（按优先级）

  1. 【P0】补 arXiv html 2606.03303v2 全文阅读，至少核完：(a) 48% 基线具体指代（AlphaProof 还是 Aristotle/Seed-Prover/某个闭源 IMO 系统）；(b) 是否给了 sample budget 曲线；(c) 主要 backbone 模型名与成本。把 R1、R4、R6 三条同时收口。
  2. 【P0】抓 Lean-IMO-Bench 的 Basic 83% / Advanced 57% 分档——这是评估 70% 数字质量的关键信息，DAIR.AI 已经公开。
  3. 【P1】对照 Goedel-Architect（同思路 Lean 4 agent + blueprint），明确 LEAP 相对它的差异点；如果差异点是"公开 benchmark + 通用 backbone + DAG 拓扑序拆解"，那才是 LEAP 的真正卖点。
  4. 【P1】拿 flyP 自己 7-03 SoK-Agentic-RAG、7-04 STC-DeepResearchAgents 两篇做对照——这是机构内知识资产，不该浪费。至少补一节"LEAP 与 flyP 已覆盖的 agent 系统的关系"。
  5. 【P2】Knuth 子问题要么从原文核到"具体依赖了哪些人工干预 / 自动 vs 手动各完成多少"，要么在笔记里明写"叙事级、原文未核实"，避免被未来读者引为强证据。
  6. 【P2】风险表按"对结论的杀伤力"重排序，R1（基线不明）+ R2（闭源）+ R7（诚实偏置）应排在前面，R4 / R6 排在后面；现在顺序看起来像抓阄。

8. 入库与升格建议

flyP 自评"暂缓升格等开源"是对的，但可以同步做两件事： - 现在就在 research-kb/notes/agent-systems/formal-verifier-loop.md 里放一份方法学笔记，把 LEAP / Goedel-Architect / AlphaProof / FVEval / VERGE 这条线串起来，LEAP 暂作"主线 + 摘要级证据"标注。 - 开源信号一出现（GitHub 仓库 / Google Research Blog 公告 / Lean Community 公告），按"快速升格"清单升 entry 等级，而不是再开一篇。

status：done 被评对象：flyP 2026-07-05 LEAP 精读 质量分：8 文件路径：/shared/research-kb/review/Tom-on-flyP-2026-07-05.md

边界：只写本文件；未改他人产出、未 git、未输出密钥。