谷歌DeepMind推出的AI系统AlphaProof首次公开技术细节，其在2024年国际数学奥林匹克竞赛（IMO）中斩获银牌，成为首个在该赛事中达到奖牌水平的人工智能系统。该成果于11月12日发表在《自然》杂志，标志着机器数学推理能力的重要突破。 AlphaProof与AlphaGeometry 2协作，完成IMO六道题中的四道，获得28分，相当于当年609名参赛者中的银牌水平。尤其值得一提的是，它成功解答了当年最难的第六题，仅五名人类选手完成该题，彰显其解决复杂数学问题的能力。 系统核心在于将形式化数学语言与强化学习深度融合。为避免大语言模型常见的“幻觉”问题，研究团队采用Lean这一可自动验证证明正确性的定理证明系统。通过微调Gemini模型，将百万级自然语言数学题自动转化为Lean可处理的形式化语句，生成八千万条训练数据，突破了形式化数据稀缺的瓶颈。 AlphaProof架构借鉴AlphaZero，采用拥有三十亿参数的编码器-解码器变换器网络，输出策略与价值函数，指导树搜索算法在证明空间中高效探索。其创新点在于“乘积节点”设计，能有效分解目标、追踪子任务完成状态，提升搜索效率。 最引人注目的是“测试时强化学习”（Test-Time RL, TTRL）机制：面对难题，系统会自动生成难度递增的变体问题，通过解决简单变体积累经验，逐步攻克原始难题。这一策略在破解IMO第六题中起到关键作用。 训练过程采用渐进式策略：从简单问题起步，避免资源浪费，随能力提升逐步扩大搜索规模。尽管推理时间差异大——有的问题几分钟，有的需三天，但研究团队强调，重点在于推理能力而非速度。 菲尔兹奖得主Timothy Gowers评价其成果“令人印象深刻”，剑桥大学专家Katie Collins认为形式化验证能增强数学成果可信度，推动合作。 值得注意的是，DeepMind同期推出的Gemini Deep Think已实现端到端自然语言推理，在4.5小时内获35分金牌，标志着AI正从形式化路径向自然语言路径演进。未来，形式化验证与自然语言理解或有望融合，催生更强大、通用的数学AI工具。 目前系统仍需人工将题目转化为形式语言，自动转换仍是挑战。此外，AlphaProof在组合数学上表现较弱，团队正深入分析原因。论文作者Julian Schrittwieser表示，当前限制主要在于TPU算力，未来可扩展性极强。