2026-08-11
DeepMind 在 Nature 发表 AlphaProof：一个 3B 参数证明网络在 Lean 里做强化学习，IMO 2024 解 4/6、28/42 分，达到银牌线，差一分金牌。
大模型在数学题上越来越能写，但自然语言写的证明没法机器核验，对不对只能靠人判断，没法当干净的训练信号。Lean 这类形式化语言能自动验证证明，强化学习又提供了在可验证环境里试错的机制。这篇（2025 年 11 月正式刊于 Nature）要回答的问题是：把 AlphaZero 那套「策略价值网络加自我对弈加搜索」的范式，能不能搬到形式化数学证明上做到奥赛级。对应的成绩单是 2024 年国际数学奥林匹克（IMO）：AlphaProof 解出非几何题里的三道，加上 AlphaGeometry 2 解的几何题，合计 4/6、28 分，落在银牌区，差一分到金牌。这是 AI 首次在 IMO 拿到奖牌级表现。
AlphaProof 把在 Lean 里证题建模成一个强化学习的序列决策问题，叫「Lean 环境」：状态是当前 Lean 的 tactic 状态（所有假设和待证目标），动作是一条 tactic，每走一步奖励负 1（鼓励最短证明），目标是累计回报最大。几个关键部件：
跨几个形式化基准都到 SOTA（miniF2F、formal-imo、PutnamBench-test），即便每题只给 2 个 TPU 分钟的搜索预算也有竞争力，在 PutnamBench-test 上尤其明显。formal-imo 是作者新整理的 258 道历史非几何 IMO 题（代数 107、组合 77、数论 74）。IMO 2024 的关键数字：
| 题目 | 解题方 | 结果 |
| P1、P2、P6 | AlphaProof | 全分（由 Timothy Gowers 与 Joseph Myers 按 IMO 规则判分） |
| P4（几何） | AlphaGeometry 2 | 解出 |
| P3、P5 | 未解 | 未解 |
合计 4/6、28/42 分，银牌区，距金牌线一分。要强调两点：一是这些证明是赛前冻结模型、赛后由独立专家按官方规则判的分，不是自评；二是 AlphaProof 每题的计算时间是「多日」级，远超人类选手的 4.5 小时。答案类题（「求所有满足条件的 n」）用 k=500 个候选答案去猜，全部猜中正确答案，再由 AlphaProof 在低算力反证模式下筛。
这是第一次有 AI 系统在 IMO 拿到奖牌级分数，也说明 AlphaZero 那套「从可验证的自我经验里学习」能从棋盘类游戏迁移到数学推理。对从业者，真正的信号是形式化语言给了强化学习一个 0/1 的真值奖励，绕开了自然语言证明没法自动判对错的老问题；TTRL 则是「用算力换单题深度」的一个具体范式，把通用模型攻不下的难题用变体加专门训练啃下来。开源方面，文章以 CC BY 4.0 开放获取，miniF2F 修正版和 formal-imo 基准也放了出来。
作者自己列得很坦白。算力门槛极高：主循环约 8 万 TPU·天、自动形式化约 10 万 TPU·天，这种规模基本把学术组挡在门外。TTRL 解难题要多日推理，实用性受制于速度。能力范围也有限：成绩集中在高中到本科竞赛数学，依赖一个固定的已知概念库，题材相对一致；要推广到研究前沿的开放数学是「相当大的一步」。几何因为当时 Mathlib 的高阶几何库（内切圆、全等等）缺位，根本没法在 Lean 里表述，只能交给单独的 AlphaGeometry 2。另外，自动形式化是整条链的前提，而它在组合题上只有 33.3% 的 pass@1，这部分误差会直接限制能证什么。