谷歌DeepMind在国际数学奥林匹克竞赛（IMO）中再获突破，其研发的AlphaProof模型成功斩获金牌。这一成果以完整论文形式发表于《自然》期刊，首次详细披露了该系统的技术架构与训练方法。值得注意的是，曾实现“无师自通”下棋的AlphaZero相关技术，在此次研究中被多次借鉴与改进。
项目核心团队规模精简，长期保持约十名成员，仅在IMO赛事临近时扩充人手。突破性进展源于团队成员、IMO金牌得主米克洛什·霍瓦特提出的创新方法：通过生成数学问题的多样化变体，构建智能体的训练环境。这些变体涵盖简化版本、推广形式及结构类似的问题，使系统能在更广泛的场景中积累解题经验。
AlphaProof将数学证明转化为强化学习任务，基于Lean定理证明器搭建训练环境。每个数学命题被视为独立关卡，系统需选择策略推进证明进程。成功策略将生成新子目标，直至所有目标完成即证明成功。其核心采用30亿参数的编码器-解码器Transformer模型，该模型需同时输出策略建议与剩余步骤预估，优化计算资源分配效率。
搜索算法层面，系统在AlphaZero树搜索基础上引入AND-OR树结构，可分解证明中的多重独立条件为子问题逐个攻克。渐进采样机制则允许在关键路径探索更多策略。训练数据构建分为三阶段：首先用3000亿token的代码与数学文本预训练模型；随后通过Mathlib库的30万个人工证明微调；最终利用基于Gemini 1.5 Pro开发的翻译系统，将约100万道自然语言数学题转化为8000万道形式化问题，数据规模远超现有集合。
主训练阶段消耗约8万TPU日计算资源，系统通过持续尝试证明或反证自动生成命题，成功案例用于更新神经网络。即便形式化结果存在误差，只要命题有效，系统仍能从中学习。测试阶段采用双循环机制：主循环处理大规模自动生成问题；测试时强化学习循环针对特定难题生成约40万个变体，启动独立训练进程积累解题洞察。
在2024年IMO赛事中，AlphaProof展现强大实力，成功解决代数与数论领域三道题目，其中包括仅5名选手完全攻克的最高难度试题P6。面对难题时，系统通过生成特殊变体（如限定有理数范围、强化条件假设）进行专项训练，每题需2-3日计算时间。团队透露，赛事期间部分证明系统仅能确保铜牌成绩，直至后台运行的测试时强化学习完成三道完整证明，才最终锁定金牌。
目前DeepMind已向科研界开放AlphaProof使用权限，多位数学家分享了试用体验。罗格斯大学学者发现系统擅长发现反例，助力修正理论假设；伊利诺伊大学团队用其验证棘手引理，一分钟内完成证明或找出定义漏洞；伦敦帝国理工学院测试费马大定理证明时则遇到挑战，显示系统在处理全新数学概念时仍存在局限。
研究团队指出，系统对Lean定理证明器的依赖构成双重影响：活跃的社区支持推动其在成熟数学子领域表现优异，但证明器的持续演进也带来环境不稳定性。数据局限性同样突出，尽管变体生成技术取得进展，但创建真正原创的数学问题仍需突破。该成果为AI数学研究提供了新范式，其技术路径印证了专家关于AI在封闭系统中超越人类潜力的预测。
论文全文链接：https://www.nature.com/articles/s41586-025-09833-y
相关技术讨论：https://www.nature.com/articles/d41586-025-03585-5
