核心观点 - 谷歌DeepMind在Nature上完整公开了其数学证明AI系统AlphaProof的技术细节，该系统在2024年国际数学奥林匹克竞赛（IMO）中取得金牌级表现，其核心创新在于将数学证明构建为强化学习游戏，并利用大规模自动生成的问题进行训练[1][8][26] 技术架构与训练方法 - 系统基于Lean定理证明器构建强化学习环境，将数学命题视为游戏关卡，AI通过选择策略推进证明[8][9] - 采用30亿参数的编码器-解码器transformer模型作为证明网络，同时输出策略建议和完成证明的步数估计[12][13] - 搜索算法采用受AlphaZero启发的树搜索，并引入AND-OR树结构处理多个独立子目标，以及渐进采样机制[15] - 预训练使用约3000亿个token的代码和数学文本，微调使用Mathlib库中约30万个人工编写的证明[16] - 通过基于Gemini 1.5 Pro的翻译系统，将约100万道自然语言数学题自动生成为约8000万道形式化问题，极大扩充了训练数据集[16][21] - 主训练阶段消耗约8万TPU天的计算资源[19] 关键创新：测试时强化学习 - 面对IMO级别难题时，系统会为每道题生成约40万个相关变体（如简化版、推广版），并启动独立的AlphaZero式学习过程进行专门训练[23][24][26] - 此TTRL机制使系统能针对特定难题积累洞察，是解决IMO最难题P6的关键，每道题训练需2-3天计算时间[24][26] - 比赛期间，团队最初仅凭部分证明系统判断为铜牌水平，但后台运行的TTRL在三天后陆续完成三个完整证明，最终达到金牌成绩[27][28] 团队与开发过程 - AlphaProof核心团队规模较小，大部分时间仅有约10人，临近IMO比赛时人员增加[3] - 关键突破来自IMO金牌得主Miklós Horváth提出的方法，即创建问题变体作为初始状态供智能体训练[4][5] - 团队在一年内探索多种研究思路，成功部分被整合进最终系统[7] 应用前景与局限性 - 系统已向科学界开放，数学家试用反馈显示其特别擅长找出反例，能在一分钟内证明或反证棘手的引理，有助于迭代修正数学陈述[30][31][32] - 局限性在于处理充满“定制化定义”的全新概念时遇到瓶颈，在Lean证明器策略成熟的数学子领域表现更佳[33][34] - 未来发展面临“数据有限性”挑战，需使AI能自主生成问题以实现通用性，其即时共享知识并生成训练数据的能力预示在数学领域可能远超人类[35][36][37]