去年7月，Google DeepMind宣布其AI系统AlphaProof在国际数学奥林匹克竞赛（IMO）中斩获银牌，成为首个在该赛事中取得奖牌的人工智能系统。如今，这一里程碑式成果的技术细节已在《自然》杂志发表，全面揭示了其背后的创新机制。在2024年IMO中，AlphaProof与AlphaGeometry 2协同作战，成功解决四道题目，总分28分，达到人类参赛者中前10%的水平，尤其攻克了当年最难的第六题——该题仅有五名人类选手完全解答。 AlphaProof的核心突破在于将形式化数学语言与强化学习深度融合。传统大语言模型虽能生成看似合理的推理过程，却常因“幻觉”而出现逻辑错误。为确保严谨性，研究团队采用Lean这一交互式定理证明系统作为工作环境，其自动验证机制可即时检测每一步推理的正确性，杜绝错误传播。然而，Lean的数学库mathlib仅有约二十万个定理，数据稀缺成为瓶颈。 为此，团队利用微调后的Gemini模型，将一百万个自然语言数学命题自动转化为Lean可识别的形式化表达，生成八千万条合成数据，极大扩充了训练资源。AlphaProof的架构借鉴AlphaZero，采用一个拥有三十亿参数的编码器-解码器变换器网络，输出策略（建议下一步行动）与价值函数（评估路径潜力），结合专为数学证明优化的树搜索算法，在庞大证明空间中高效导航。 其创新点之一是“乘积节点”设计：当证明需拆解为多个子目标（如数学归纳法的基例与递推）时，系统要求所有子节点均被完成，从而精准追踪进展并集中资源于难点。更关键的是“测试时强化学习”（Test-Time RL），在面对难题时，系统会自动生成一系列难度递增的变体问题，通过解决简单情形逐步积累策略，最终攻克原始难题。这一机制在破解IMO第六题中发挥了决定性作用。 训练过程采用渐进式策略：初期聚焦小规模搜索，避免资源浪费；随着能力提升，逐步扩大搜索深度。系统还会主动识别错误命题并终止无效尝试，同时对已成功证明的命题反复优化，寻求更简洁优雅的解法。 尽管AlphaProof在代数与数论领域表现优异，但在组合数学上仍有短板，团队正深入分析原因。此外，目前系统仍需依赖人工将IMO题目转化为形式语言，尚未实现完全自主。不过，今年DeepMind推出的Gemini Deep Think系统已实现端到端自然语言推理，在4.5小时内获得35分金牌，标志着AI正从形式化路径向自然语言直接推理演进。 专家评价认为，AlphaProof不仅验证了AI在高阶数学推理上的潜力，更推动了数学证明的可验证性与可信度。未来，形式化验证与自然语言理解或将融合，催生更强大、通用的数学AI工具。正如研究者所言：“限制我们的，只是可用的TPU算力。”这一突破，正为人工智能迈向真正智能的数学思维铺平道路。