谷歌AlphaProof破解IMO难题秘诀：4人团队如何实现数学突破

谷歌DeepMind在国际数学奥赛（IMO）中再次实现重大突破，其研发的AlphaProof模型成功斩获竞赛金牌。这项突破性研究成果以完整论文形式发表于《自然》期刊，首度系统性地揭示了该人工智能系统的技术架构与训练方法。值得关注的是，曾创造"无师自通"下棋奇迹的AlphaZero相关技术，在本研究中被多次借鉴并实现创新性改进。

该项目研发团队规模精干，长期维持在十余人左右，仅在临近赛事时适当扩充人手。突破性进展源于团队成员、前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