上海
2024 年 7 月，国际数学奥林匹克竞赛（IMO）传来爆炸性消息。
Google DeepMind 的 AlphaProof 系统，首次在这项全球顶尖数学赛事中拿下银牌，这是 AI 历史上第一次达到 IMO 奖牌级别。
时隔一年多，2025 年 11 月 12 日，相关技术论文正式发表在《自然》杂志上，所有核心细节全部公开，让整个数学界和 AI 圈都为之震动。
这个能跟全球数学天才同台竞技的 AI，到底藏着什么秘密？它的出现又会带来哪些改变？
一、IMO 有多难？全球仅 1% 能拿满分的终极试炼
国际数学奥林匹克竞赛，可不是普通的数学考试。
它面向 16-19 岁的青少年，聚集了全球最顶尖的数学人才，每届都有上百个国家参赛。
比赛分两天进行，每天 4.5 小时，总共就 6 道题，满分 42 分，但难度却高到让人望而生畏。
2024 年的比赛中，全球只有不到 1% 的参赛者能拿到满分，金牌分数线更是高达 29 分。
更值得一提的是，这赛事堪称 “数学大师摇篮”，陶哲轩、Timothy Gowers 等多位菲尔兹奖得主，都曾是 IMO 的参赛选手。
AlphaProof 在这次比赛中拿到 28 分，刚好卡在银牌区间，排名能进全球前 10%，直接超越了 609 名人类参赛者中的大多数。
更让人意外的是，他还攻克了当年最难的第 6 题，这道题全球只有 5 名人类选手完全解答出来。
二、打破 “幻觉”：AlphaProof 的三大核心技术
传统 AI 解题最大的问题，就是容易 “瞎编”，也就是所谓的 “幻觉”。
明明推理过程错了，却能说出看似合理的结论，这在要求绝对严谨的数学证明中完全行不通。
为了解决这个问题，DeepMind 团队给 AlphaProof 装了三套 “杀手锏”。
首先是用对了工具 ——Lean 形式化语言。
这东西就像个严格的 “安检仪”，每一步推理都要符合逻辑规则，只要有一点错误就会被立刻检测出来，从根源上杜绝了 “幻觉”。
但 Lean 的问题是训练数据太少，标准数学库只有 20 万个定理，根本不够 AI 学习。
团队的第二个妙招，就是 “自动形式化”。
他们用微调后的 Gemini 语言模型，把 100 万个自然语言数学命题，转换成了 8000 万个 Lean 能理解的形式化语句，一下子解决了数据短缺的难题。
最关键的是第三招 —— 测试时强化学习（TTRL）。
遇到特别难的题，AlphaProof 不会硬冲，而是先生成一堆难度各异的题目变体，从简单的开始练手。
通过解决这些 “练习题” 积累经验，最后再回头攻克原题，这也是它能拿下第 6 题的关键。
除此之外，系统还借鉴了 AlphaZero 的架构，用 30 亿参数的网络搭配 “乘积节点” 搜索，能高效分解难题、集中资源突破关键点。
三、比人快还是慢？AI 解题的独特逻辑
AlphaProof 的解题节奏，跟人类选手完全不一样。
人类选手要在两天共 9 小时内完成所有题目，而 AlphaProof 处理简单题只要几分钟，碰到难题却可能要花三天时间。
对此 DeepMind 团队说得很实在，重点不是比谁快，而是验证 AI 能不能达到奥赛级别的推理能力。
毕竟现在的时间差距，随着技术进步迟早会缩小。
从解题风格来看，AlphaProof 也有明显的偏向性。
它在代数和数论领域表现突出，但在组合数学上相对较弱，目前团队还在研究背后的原因。
还有个小遗憾，现在 AlphaProof 还不能直接看懂自然语言的题目，需要人工翻译成形式语言才能工作。
不过团队已经在试验基于 Gemini 的自然语言推理系统，未来有望实现完全自主解题。
菲尔兹奖得主 Timothy Gowers 看完他的解答后，直言 “这很令人印象深刻，是显著的进步”。
剑桥大学的 AI 专家也认为，这种形式化证明能让数学成果更可信，还能促进学术合作。
四、从银牌到金牌，AI 要改写数学史？
AlphaProof 的突破，只是 AI 数学推理的一个起点。
就在今年的 IMO 竞赛中，DeepMind 又推出了全新的 Gemini Deep Think 系统，直接实现了端到端的自然语言推理。
它不用形式化语言当中介，4.5 小时内就拿到 35 分，直接达到了金牌水平，进步速度让人惊叹。
这意味着 AI 数学推理，正在从 “形式化验证” 和 “自然语言理解” 两个方向快速推进。
未来这两条路径很可能会融合，诞生出更强大的通用数学 AI 工具。
论文作者 Julian Schrittwieser 透露，目前限制 AlphaProof 的主要是 TPU 算力。
这种在推理时投入大量计算资源的模式，或许会成为 AI 优化的新方向。
更重要的是，它证明了强化学习与搜索的组合，对大语言模型同样有效，为构建更可靠的 AI 系统提供了思路。
长远来看，AI 不仅能辅助人类解决难题、验证证明，还可能发现人类没注意到的数学规律。
或许用不了多久，我们就能看到 AI 和人类数学家携手，攻克那些困扰多年的数学难题，彻底改变数学研究的范式。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
