Google LEAP用可迭代证明蓝图，让通用大模型在形式化数学证明中大幅提效。
原文标题：破解率从低于10%直升70%，Google团队凭「可迭代的数学证明」斩获Putnam竞赛满分
原文作者：数据派THU
冷月清谈：
怜星夜思：
2、如果通用大模型加智能体框架已经能做到这么高，通过专用证明模型还有必要吗？
3、形式化数学证明如果继续突破，会最先影响数学研究、软件验证，还是AI训练本身？
4、Putnam 12题全对听起来很震撼，但这种竞赛成绩能代表真实数学能力吗？
原文内容
来源：ScienceAI本文约1500字，建议阅读5分钟用大模型把数字证明拆成一张可迭代的施工图。
在通用人工智能（AGI）的发展之路上，形式化数学证明（Formal Theorem Proving）一直被公认为是最难啃的硬骨头之一。
在 Lean 这种严苛的机械验证语言面前，哪怕是人类最顶尖的非正式数学推理模型，一旦被要求「一次性写出完美的完整证明」，其通过率往往惨不忍睹，甚至不足 10%。这种尝试的失败，过去常被归咎于通用模型的数学底层能力不足，迫使整个学术界走向了高成本、重度依赖微调的专用证明模型（Specialized Provers）路线。
2026 年 6 月 3 日，Google Cloud AI Research 与 Google DeepMind 团队发表的一篇论文彻底打破了这一迷思：「LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks」文内表示，这种弱点不仅仅是模型的数学能力问题，而是使用方式的问题——缺少与验证器的结构化交互。
论文链接：https://arxiv.org/abs/2606.03303
LEAP
前文已提出当下研究界的主流路线：很多工作依赖专门的 prover model，并默认通用 LLM 不够适合严谨的 formal theorem proving。
针对此，研究团队推出了 LEAP（意为跃迁） 智能体框架。在不进行任何专用微调的前提下，LEAP 直接让通用 foundation 模型在极其硬核的 Lean-IMO-Bench 上将形式化求解率直接拉升至 70%，并在极其艰难的 2025 年普特南数学竞赛（Putnam 2025）中斩获了 12 题全对（100% 胜率） 的绝佳成绩。
LEAP 不是一次性综合完整证明，而是逐步绘制蓝图，将精益目标分解为支持引理，并以 AND-OR DAG 形式维护不断演变的证明计划。
图 1：LEAP工作流程。
它先尝试直接形式化内容；如果失败，就生成一个 informal blueprint，把大问题拆成一串支持性引理，并把这些依赖组织成一个 AND-OR DAG。这个 DAG 不只是记录进度，还承担交错非正式-形式规划与预见引理规划职能。
Lean-IMO-Bench
为了避免在已经饱和的基准上做表面文章，作者新建了 Lean-IMO-Bench，把 IMO-Bench 里的挑战题正式化到 Lean 中。这个基准保留了题目短、但证明很长、很绕、很非套路的特征，专门测试模型是否真的能把一串复杂推理落到机械可验证的证明上。
这个基准测试包含 60 个问题，涵盖了代数、数学、数论、几何等方面，并由专家手工形式化再复核一次。团队对其的期望是成为对形式化定理证明更尖锐的测量尺，而不是简单换个题库。
在最新的 2025 Putnam Competition 这场惨烈的比拼中，传统的单发生成模型全军覆没，得分为 0。而 LEAP 凭借精妙的 DAG 蓝图设计，直接斩获 100% 满分。论文把这和近期一些前沿形式推理系统并列看待，说明它已经进入了形式化数学的最前沿区间。
表 1：Putnam 2025 的竞赛成绩。
更有代表性的，是 LEAP 在 Lean-IMO-Bench 上的提升：通用 LLM 的原生单发胜率从 10% 以下 提升到 70%，这个成绩将之前号称达到 IMO 金牌标准的专用系统 Aristotle 远远甩在了身后。
表 2：基础与高级题集中的分类求解率。
从空白到直白
LEAP 的成功带来了需要思考的问题：我们真的需要倾注所有资源去无限微调那些极度偏科、缺乏泛化能力的专用小模型吗？
答案是否定的。通用的 FM 本身就蕴含着一片未被完全开发的浩瀚汪洋。它们海量的常识、出色的宏观规划能力和长文本逻辑留存，搭配恰当的学术支架，完全可以在专业壁垒极高的领域上演从无到有的逆袭。
未来团队的主要目标是突出通用大型语言模型在代理式工作流中的独立强大性，但他们也给出了超出现有文本之外的期待：结合基础模型的高层结构推理与精细调优的专业模型中专注、形式化的步骤生成相结合的混合架构，将会成为一种极为高效的设计。
相关链接：https://x.com/rohanpaul_ai/status/2062658115603218493
编辑：文婧
