AlphaProof：人工智能在国际数学奥林匹克竞赛中获银牌

今日，首个达到国际数学奥林匹克竞赛（IMO）银牌水平的人工智能（AI）模型——AlphaProof，在权威科学期刊 Nature 上发表重要成果。

论文链接：https://www.nature.com/articles/s41586-025-09833-y

去年，Google DeepMind 凭借 AlphaProof 这一奥赛级人工智能模型，引发了学界轰动，被业内视为“登月”时刻。

据论文描述，AlphaProof 展示了自动化系统攻克传统认为无法解决的数学难题的能力，不仅是技术层面的里程碑，也为“可验证的机器推理”提供了可行路径。

新闻与观点文章链接：https://www.nature.com/articles/d41586-025-03585-5

在同期发表的新闻与观点文章中，伊利诺伊大学厄巴纳-香槟分校助理教授 Talia Ringer 表示：

AlphaProof 是她所用过的首款“真正实用的 AI 工具”，拥有“高度可靠”的证明质量，每一步推理都能获得来自证明辅助工具的即时反馈，避免了自然语言推理中的模糊与错误。

“尽管存在局限性……但可以肯定的是，这个领域正在发生深刻变革，AlphaProof 或许正是未来趋势的先行者。”

AlphaProof：实现奥数级形式化推理

训练能够在复杂、开放环境中进行有效推理并找到解决方案的智能体（Agent），是人工智能研究的关键挑战之一。

数学，尤其是奥数题目，要求创造性思维和多步推理能力，因此被视为衡量高级智能体能力的标准化评估场景。

研究团队延续了在 AlphaZero 等系统中的思路，通过强化学习让智能体在规则明确的环境中进行自我博弈与改进，这次以数学定理为“棋盘”。

在具体实现上，AlphaProof 将数学定理证明过程转化为一个强化学习任务。在 Lean 定理证明器环境中，每一次证明过程都被定义为状态、动作与奖励，通过不断尝试与反馈，学习如何将假设转化为结论。

AlphaProof 的训练过程分为多个阶段。首先，模型在约 3000 亿 token 的数学与代码语料上进行预训练，学习符号逻辑、语法和基础的数学语言表达结构。随后，研究者利用约 30 万条 Lean tactic 证明数据对模型进行监督微调。为了构建大规模训练数据，他们开发了基于 Gemini 模型的自动形式化系统，生成了约 8000 万个形式化数学问题。

在主训练阶段，AlphaProof 系统在生成的问题上进行自我博弈式学习：不断尝试证明、验证结果、更新策略，并通过 Lean 核心验证结果的正确性。研究团队称，这一过程累计消耗了约 8 万 TPU 天的计算资源。

在推理阶段，研究团队提出了“测试时强化学习”（TTRL）机制。当 AlphaProof 遇到难度较高或未见过的题目时，会围绕目标问题生成数千个结构相似的变体进行短期自我强化学习。

这种“临场学习”的方法显著增强了模型的泛化与解决新题的能力：实验结果显示，TTRL 让系统的解题率在多项基准上提升了约 10%–15%。

从结果上看，AlphaProof 在多个数学推理基准测试上展现出了领先的性能。在 miniF2F、PutnamBench、formal-IMO 等形式化数学基准测试上均达到了 SOTA 水平。

在 2024 年的国际数学奥林匹克 IMO 模拟测试中，AlphaProof 表现尤为突出——成功独立证明三道非几何题。与此同时，Google DeepMind 的另一个系统 AlphaGeometry 2 则负责解决几何题。两者合计得到 28 分（满分 42），相当于人类参赛者的银牌水平。

迈向可验证科学智能

研究团队强调，AlphaProof 的核心贡献在于证明了强化学习可以与形式化逻辑系统结合，实现高水平的可验证数学推理。

与基于自然语言模型的推理不同，AlphaProof 的每一步逻辑均通过 Lean 的验证器审查。这种“形式化可验证”的方法为人工智能在科学推理和理论研究中的应用奠定了重要基础。

尽管 AlphaProof 也存在一些局限——包括训练与推理的计算成本高、推理速度慢等——研究团队认为这一成果展示了人工智能系统向更高层次推理能力迈进的可行路径。

在未来工作中，他们将优化模型效率、降低算力需求，并探索形式化学习在数学与其他科学领域的应用。此外，他们还计划开发交互式工具，使研究人员能够直接与系统协作。