获得数学奥赛银牌AlphaProof的《自然》论文介绍11月12日谷歌DeepMind的AlphaProof论文在《自然》在线发表。这个AlphaProof和大模型做数学题最大不同是，它的解题过程是严谨的，做出来肯定是对的；而大模型会一个词一个词地生成，最后给出个答案声称做出来了，但实际中间某些步骤可能是错的，或者没有严格证明。需要注意的是，AlphaProof是得了2024年IMO的银牌，6题解出4题，现在发表的是这个成果。而2025年IMO在7月已经办了，谷歌的DeepMind开发Gemini Deep Think，用大模型路线得了金牌，6题做出5题，自然语言解题，得到IMO官方确认；OpenAI也声称大模型得了金牌，也是只有最难一题没做出来，但IMO官方没认。但是，美国大公司的先进大模型选择闭源，这些成果细节不公布，怎么让大模型做数学题的，不是太清楚。《自然》上发表的先进大模型代表是DeepSeek，因为细节愿意公布。AlphaProof的细节也在论文中公布了。可以看出AlphaProof的思想与架构和下棋的AlphaZero很象。类似之处在于，下棋系统的每一步都有严格规则，最终下完一盘数子，结果可以绝对确认；AlphaProof的证明解体系统依赖于数学界之前的形式化系统Lean，这个系统是严格的，每一步都有根据。现在来看，只要有海量算力，AlphaZero可以说是一个“容易”的学术问题。构建一个能下棋的初始神经网络（评估局势的价值网络、给出行动的策略网络）以及搜索“博弈树”的算法，然后self-play自对弈至终局，根据结果就有“奖励”，用这个奖励来调整神经网络。整个过程是一个“强化学习”RL过程，在环境中互动学习，形成一个个版本，越来越强。它容易，因为不需要准备样本，对弈本身就能生成海量样本。但是对于要做数学题的AlphaProof，如何构造学习过程要困难多。数学题不像下棋可以自然进行，需要海量的样本，样本生成构成了核心难度。研究团队开发了一套自动形式化系统，基于Gemini的大模型，通过在海量的自然语言数学文本（如教科书、竞赛题、论文等）和Lean代码语料上进行微调，使其具备了将非形式化的数学问题自动翻译成形式化的Lean定理陈述的能力。等于做了个数学形式化翻译器。这套系统自动形式化了大约100万个自然语言数学问题。然后就构建下棋self-play一样的证明系统，即AlphaProof证明网络和树搜索算法，在Lean环境中探索可能的证明路径。这就和AI下棋很像了。数学问题证明也构成一个“树”，按不同选择，一步步往下推，有的路不通，有的路能发现有意义的中间结果，有的导向最终成功的证明。类似AlphaZero的还有，AlphaProof在尝试证明过程中，即使是超时失败的，也能生成有意义的样本，相当于做数学题的“经验”，失败了可以当负样本。这样，最终生成了8000万个样本。这对于数学证明体系来说，是海量的。类似于围棋AI自对弈的盘数，远远超过人类下过的高质量围棋对局。AlphaProof在这么多样本教育下，终于学会了数学概念到证明所需的技术。这里有个细节，IMO分为代数、数论、组合、几何四类问题。几何是指欧几里德几何，有自己的特色，AlphaProof实际做的是代数、数论、组合三个部分。几何题由DeepMind之前开发的AlphaGeometry2来做，开发原理不同。AlphaGeometry2有做proof的神经网络，还有一个负责“猜想”网络，相当于划辅助线、提出猜想，然后让proof网络来验证，最终也是靠谱的。这个论文让人信服地相信，AI是可以做出IMO数学题的。而且不是针对IMO特训或者瞎猜的，是通过海量题的严格训练，掌握了数学题的内在规律。技术细节都足够扎实。但是要指出，IMO数学题都只能算是“容易”的题。我看人类学者有重大贡献的数学论文，经常是30-50页甚至更长，过程复杂、漫长。而IMO“难题”，最终答案往往不是太长，一页纸差不多了。以前觉得围棋是对AI很困难的问题，后来认为奥赛数学题对AI很难。AI的破解过程，揭示了这些问题的内在规律，只是人类很难学会。人类智慧的最后堡垒是困难的论文级数学发现，这方面AI还没什么重大突破。
