2024年7月，Google DeepMind宣布其AI系统AlphaProof在国际数学奥林匹克竞赛（IMO）中斩获银牌，成为首个在该赛事中获得奖牌的人工智能系统。这一成就在11月12日通过发表于《自然》杂志的完整论文得以全面披露。AlphaProof与AlphaGeometry 2协同作战，成功解答了六道题目中的四道，总分28分，达到当年参赛者前10%的水平，尤其攻克了被誉为当年最难的第六题——仅五名人类选手完全解决此题。这一突破标志着AI在高级数学推理领域迈出了关键一步。 AlphaProof的核心创新在于将形式化数学语言与强化学习深度融合。为克服大语言模型常见的“幻觉”问题（即生成看似合理实则错误的推理），研究团队采用Lean这一交互式定理证明系统作为底层环境。Lean能自动验证每一步推理的逻辑正确性，确保输出无误。然而，Lean的数学库mathlib仅有约二十万个定理，远不足以支撑大规模训练。为此，团队利用微调后的Gemini模型，将一百万个自然语言数学命题自动转化为八千万条Lean形式化语句，构建了庞大的合成训练数据集。 系统架构借鉴AlphaZero思想，采用一个拥有三十亿参数的编码器-解码器变换器网络，输出策略（建议下一步行动）与价值函数（评估路径前景），配合一种名为“乘积节点”的树搜索机制。该机制要求所有子目标同时被证明，有效追踪进度并聚焦难点，显著提升搜索效率。最具突破性的技术是“测试时强化学习”（Test-Time RL, TTRL）：面对难题时，系统自动生成一系列难度递增的变体问题，通过逐步攻克简单情形积累经验，最终解决原始难题。这一策略在破解第六题中发挥了决定性作用。 训练过程采用渐进式策略：初期限制搜索规模以避免资源浪费，随着能力提升逐步扩展深度与广度。尽管AlphaProof解决某些问题仅需几分钟，个别难题耗时长达三天，但研究团队强调，目标并非速度竞赛，而是验证推理能力是否达到人类奥赛水平。菲尔兹奖得主Timothy Gowers评价其为“显著进步”，剑桥大学专家Katie Collins则指出，自动化形式化将极大增强数学成果的可信度与协作效率。 值得注意的是，同年IMO中DeepMind推出的Gemini Deep Think系统已实现端到端自然语言推理，在4.5小时内取得35分金牌，无需形式化语言中介。这表明AI数学推理正从“形式化路径”向“自然语言路径”快速演进。未来两者或将融合，催生更强大、通用的数学AI工具。 尽管AlphaProof表现优异，仍面临挑战：目前需人工将IMO题目转化为形式语言；其在组合数学领域表现较弱，团队正探究原因。论文作者Julian Schrittwieser强调，TTRL的可扩展性受限于TPU算力，暗示未来可通过更大规模计算实现更强推理能力。总体而言，AlphaProof不仅验证了强化学习与搜索对大模型的有效性，也为构建可验证、可信赖的通用AI系统提供了全新范式。