上一篇
DeepMind AlphaProof：IMO金牌数学证明AI技术全解析与创新突破
谷歌DeepMind近日在国际数学奥林匹克竞赛（IMO）中斩获金牌的人工智能模型AlphaProof，其完整技术架构已全面公开，引发学术圈广泛关注。
秉承DeepMind的经典命名风格，这一全新系统被正式定名为AlphaProof。
研究成果以论文形式发表于顶级期刊《自然》，首次深度剖析了AlphaProof的技术细节与训练方法论。特别值得注意的是，论文中多次引用了此前无师自通的围棋AI AlphaZero的核心思想。
论文作者Tom Zahavy借此机会透露了开发过程中的幕后故事：
AlphaProof研发团队的规模相对精简。在多数时间仅有10人左右的核心小组，直到临近IMO赛事时才有更多成员加入支持。
实现关键突破的核心人物是IMO金牌得主Miklós Horváth。
他提出了一种创新方法，能够生成AI所处理数学问题的多种变体，并将这些变体作为初始训练状态，使智能体在多样化场景中进行强化学习。
将数学证明转化为可训练的游戏环境
AlphaProof的核心理念颇为直观：将复杂的数学证明过程重塑为一个可反复演练的游戏。
该系统基于Lean定理证明器构建了一个强化学习环境。在此环境中，每个数学命题都相当于一个新的游戏关卡，AI需要通过选择恰当的策略（tactics）来逐步推进证明。
若某个策略应用成功，系统将生成新的子目标；一旦所有目标均被完成，即标志着证明成功结束。
论文披露，AlphaProof采用了一个拥有30亿参数的编码器-解码器transformer模型作为其“智能中枢”。
该证明网络不仅需理解当前的证明状态，还需同步输出两项关键信息：
一是推荐后续尝试的策略列表，二是预估完成证明所需的剩余步数。
这种双输出设计使得系统能更高效地分配计算资源，优先探索最具潜力的证明路径。
在搜索算法层面，AlphaProof借鉴了AlphaZero的树搜索思想，但进行了重要优化。
例如引入AND-OR树结构以处理证明中的多个独立子目标，当证明需同时满足多个条件时，系统会将其分解为独立子问题各个击破。此外还融入了渐进采样机制，使系统在关键路径上能探索更多样化的证明策略。
训练AlphaProof所面临的主要挑战在于数学题源的稀缺性。
团队首先使用约3000亿token的代码与数学文本对模型进行预训练，使其掌握基本逻辑结构与数学语言。随后利用Mathlib库中约30万个人工编写的证明进行微调，让模型熟悉Lean语法与证明技巧。
真正的突破性进展源自自动形式化过程。团队基于Gemini 1.5 Pro开发了一套专用翻译系统，能将自然语言数学问题转换为Lean可理解的形式语言。经过反复迭代优化，该系统最终从约100万道自然语言数学题中衍生出约8000万道形式化问题，规模远超现有所有数据集。
主强化学习循环是训练过程的核心引擎。系统持续尝试证明或反驳这些自动生成的命题，成功的证明则用于更新神经网络参数。
即使自动形式化的结果并非完全精确，只要其构成有效的形式命题，AlphaProof都能从尝试证明的过程中汲取经验。
整个主训练阶段消耗了约8万TPU天的巨大计算资源。
论文中的核心架构图阐释了AlphaProof双学习循环的协同工作机制。
在主强化学习循环中，约100万道非正式数学问题先经形式化系统处理，转化为约8000万道Lean可理解的形式化问题。证明网络结合树搜索算法在Lean环境中不断尝试，无论成功找到证明、发现反证或超时失败，每次尝试都会生成经验数据反馈至学习系统。
测试时强化学习循环则展现了一种更精细的自适应机制。
当面对一道特别困难的目标问题时，变体生成器会围绕该题产生约40万个相关变体，相当于为单题构建了一个专属数据集。
这些变体囊括了多种数学直觉：如简化特殊情况、推广至一般形式、探索类似结构等。
系统会启动一个独立的AlphaZero式学习进程，专门在这些变体上训练，逐步积累解决原问题所需的洞察力。此机制可并行处理多个目标问题，每个问题都有其独特的变体课程与专属学习进程。
IMO赛场上的临场突破与表现
AlphaProof在2024年IMO中的表现令人瞩目，如今更多开发细节得以披露。
面对IMO级别的高难度题目，单纯增加搜索时间往往收效甚微。此时，前述测试时强化学习（TTRL）便发挥关键作用，即生成大量相关变体问题（如简化版、推广版、类比版等），并专门训练一个“专家”模型来攻克原题。
以2024年IMO第一题为例，该题要求找出所有满足特定整除性质的实数α。AlphaProof生成的变体包括：仅考虑有理数情况、假设α满足更强性质、证明α须接近某整数等。通过在这些变体上训练，系统逐渐掌握解决原题的关键。
实际比赛中，AlphaProof成功解决了代数与数论领域的三道题（P1、P2、P6），其中P6是赛事最难题目，609名参赛者中仅5人完全解答。
每道题的TTRL过程需2-3天计算时间，虽远超人类选手的9小时限制，但考虑到此前最先进AI系统连最简单IMO题都难以应对，此成就已堪称里程碑。
Tom Zahavy回忆称，比赛期间通过部分证明系统初步评估的成绩仅达铜牌水平，但TTRL仍在后台运行。
三日后，当三个完整证明相继呈现时，团队才确认金牌在手，激动地敲锣打鼓庆祝胜利。
数学AI的未来发展方向与挑战
AlphaProof夺金后，谷歌DeepMind已向科研界开放其使用权限，多位数学家在《自然》上分享了试用体验。
罗格斯大学数学家Alex Kontorovich发现，AlphaProof尤其擅长定位反例：
每当系统指出我的陈述存在问题时，我都能迅速找出遗漏假设，调整后重新尝试。这种迭代交互对获得正确形式化陈述至关重要。
伊利诺伊大学Talia Ringer教授让两名博士生各提供一个棘手引理。AlphaProof在一分钟内证明了其中一个，而另一个则被反证，原因是定义存在漏洞。
她评价道：“AlphaProof倾向于寻找反证的特性可能是其最令人惊喜的实用功能”。
当然，数学家们也测试出AlphaProof的局限性。
伦敦帝国理工学院Kevin Buzzard尝试用它翻译费马大定理证明时遇到困难。他发现当证明充满“定制化定义”时，AlphaProof便难以奏效。
这也印证了AlphaProof团队在论文中的发现：系统在处理Mathlib已有概念时表现卓越，但面对全新定义时则会遭遇瓶颈。
Tom Zahavy也分享了对AI在数学界应用的思考：
AlphaProof面临的一大挑战在于其对Lean定理证明器的依赖。Lean虽功能强大且社区活跃，但其持续演进为AlphaProof创造了不稳定环境。这意味着在Lean高级策略更成熟的数学子领域，AlphaProof性能通常更优。
另一关键问题是“数据有限性”。独特数学题的数量本质有限。为使强化学习智能体真正通用化，它需能自主生成问题。尽管目前在创建IMO级别问题变体方面取得一定成功，此方向仍需进一步拓展。
Hinton在今年6月访谈中指出，AI未来在数学领域很可能远超人类，因为它能在封闭数学系统中即时共享知识并生成自有训练数据。
AlphaProof的方法，正是这一预言的前瞻性演练。
论文地址：https://www.nature.com/articles/s41586-025-09833-y
参考链接：
[1]https://www.tomzahavy.com/post/how-we-achieved-an-imo-medal-one-year-before-everyone-else
[2]https://www.nature.com/articles/d41586-025-03585-5
本文由主机测评网于2026-01-23发表在主机测评网_免费VPS_免费云服务器_免费独立服务器，如有疑问，请联系我们。
本文链接：https://www.vpshk.cn/20260119906.html
