核心观点 - 谷歌DeepMind公开了其数学奥林匹克竞赛金牌模型AlphaProof的完整技术细节，该模型通过将数学证明构建为强化学习游戏并采用创新的训练方法，在2024年IMO中取得突破性成绩[2][4][5] 技术架构与训练方法 - 核心思路是将数学证明过程构建为可训练的强化学习游戏，基于Lean定理证明器创建环境，每个数学命题是一个游戏关卡[7] - 模型采用30亿参数的编码器-解码器transformer架构作为核心证明网络，同时输出策略建议和完成证明的步数估计[8] - 搜索算法受AlphaZero启发但做了关键改进，引入AND-OR树结构处理多个独立子目标，并加入渐进采样机制[9] - 预训练使用了约3000亿个token的代码和数学文本，微调使用了Mathlib库中约30万个人工编写的证明[9] - 通过基于Gemini 1.5 Pro开发的翻译系统，将约100万道自然语言数学题转换成约8000万道形式化问题，极大扩充了训练数据[10] - 主训练阶段消耗了约8万TPU天的计算资源，通过主强化学习循环和测试时强化学习循环协同工作[10][13] 团队与开发过程 - 团队规模较小，大部分时间约10人，临近IMO比赛时才有更多人加入[4] - 核心突破来自IMO金牌得主Miklós Horváth提出的方法，即创建问题变体作为初始状态进行训练[4] - 团队在一年中探索了多种研究思路，失败的经验与成功的经验最终都被整合进AlphaProof系统[5] IMO表现与测试时强化学习 - 在2024年IMO上成功解决了代数和数论的三道题，包括最难的P6题，该题609名参赛选手中仅5人完全解出[15] - 关键机制是测试时强化学习，针对每道难题生成约40万个相关变体，专门训练“专家”模型来攻克原题[13][15] - 每道题的TTRL过程需要2-3天计算时间，最终成绩达到金牌水平[15][16] 能力评估与行业应用前景 - 系统已向科学界开放，数学家试用反馈显示其特别擅长找出反例，能帮助快速调整和修正数学陈述[20] - 在处理Mathlib已有概念的数学子领域表现出色，但在面对充满“定制化定义”的全新概念时存在瓶颈[20] - 面临的行业挑战包括对持续演进的Lean定理证明器的依赖，以及数学题数据的有限性，未来需拓展问题自动生成能力[20] - 该方法展示了AI在封闭数学系统中共享知识并生成训练数据的潜力，预示其在数学领域可能超越人类[20]