人工智能领域迎来重大突破——Google DeepMind开发的AlphaProof模型成为首个在国际数学奥林匹克竞赛（IMO）中达到银牌水平的AI系统，相关研究成果登上权威科学期刊《自然》。这一成果被学界视为AI在复杂推理领域迈出的关键一步，标志着自动化系统已具备攻克传统难题的潜力。
研究团队通过将数学定理证明转化为强化学习任务，构建了独特的训练框架。模型首先在包含3000亿token的数学与代码语料库中进行预训练，掌握符号逻辑与基础数学表达结构。随后，利用约30万条Lean证明器数据开展监督微调，使其理解形式化语法。为解决训练数据不足的问题，研究团队开发了基于Gemini模型的自动形式化系统，生成涵盖代数、数论等领域的8000万个形式化问题，为强化学习提供核心素材。
AlphaProof的核心创新在于"测试时强化学习"（TTRL）机制。当遇到新问题时，系统会生成数千个结构相似的变体进行短期自我训练，再将优化后的策略应用于原题求解。这种"临场学习"方式使模型在多项基准测试中的解题率提升10%-15%。主训练阶段累计消耗约8万TPU天计算资源，通过不断尝试证明、验证结果、更新策略的循环，逐步掌握复杂推理模式。
在2024年IMO模拟测试中，AlphaProof独立证明了三道非几何难题，包括全场最难题目P6。配合负责几何题的AlphaGeometry 2系统，两者合计获得28分（满分42分），达到人类参赛者的银牌水平。这是AI首次在国际数学奥林匹克竞赛中达到奖牌标准，相比此前仅能解决中学水平题目的系统，展现了基于经验学习的形式化系统在复杂推理领域的突破。
伊利诺伊大学厄巴纳-香槟分校助理教授Talia Ringer在同期发表的观点文章中指出，AlphaProof是她使用过的首款真正实用的AI工具。其证明质量高度可靠，每步推理都能通过证明辅助工具获得即时反馈，避免了自然语言模型常见的模糊与错误。尽管存在计算成本高、推理速度慢等局限，但这一成果为"可验证的机器推理"提供了可行路径。
研究团队强调，AlphaProof的核心价值在于将强化学习与形式化逻辑系统结合，实现了可验证的高水平数学推理。与自然语言模型不同，其每步逻辑均通过Lean验证器审查，为AI在科学推理中的应用奠定基础。未来工作将聚焦优化模型效率、降低算力需求，并探索形式化学习在数学及其他科学领域的应用，同时开发交互式工具促进人机协作。
论文链接：https://www.nature.com/articles/s41586-025-09833-y
新闻与观点文章链接：https://www.nature.com/articles/d41586-025-03585-5