一年前，由谷歌 DeepMind 创建的 AI 数学模型 AlphaGeometry 在国际数学奥林匹克竞赛（IMO，International Mathematical Olympiad）中展现出比肩真人银牌得主的水平。
近日，DeepMind 正式推出 AlphaGeometry2，它在 IMO 中达到真人金牌得主的水平，并能解决 21 世纪以来 25 届 IMO 全部几何问题的 84%。
而 AlphaGeometry1 仅能解决 54% 的问题，这意味着 AlphaGeometry2 可以像顶尖人类选手一样解决棘手的数学问题。
（来源：https://deepmind.google/discover/blog/alphageometry）
对于过去 25 届 IMO 几何问题的覆盖率，此前 AlphaGeometry1 的几何问题覆盖率为 66%，AlphaGeometry2 则将几何问题覆盖率提高到 88%。
英国伦敦帝国理工学院的数学家凯文·布扎德（Kevin Buzzard）告诉媒体：“我认为不久之后，计算机就会在 IMO 上获得满分。”
（来源：arXiv）
用合成技术为 AlphaGeometry 寻找解题思路
IMO 赛题以其高难度而闻名，解决这些赛题需要对数学概念有着深入的理解，并且能够创造性地应用这些数学概念。几何赛题是 IMO 四个赛题类别之一，非常适合基础推理研究。但是，几何赛题会对 AI 提出特定的技能要求，比如 AI 必须针对平面上几何物体的陈述提供严格的证明。
自动解决几何问题有两种主要方法。一种是用代数的方法尝试；另一种方法依赖于合成技术。DeepMind 的研究人员专注于后者，因为它是一种更像人类的方法，适合将研究知识转移到其他领域。
尽管 AlphaGeometry1 取得了成功，但它在几个关键领域表现出局限性。而且，它的性能受到其领域特定语言范围、符号引擎效率和初始语言模型容量的限制。
为了解决上述局限性并提高性能，在打造 AlphaGeometry2 时，研究人员扩展了原始的 AlphaGeometry 语言，以便解决涉及到物体运动的几何赛题，以及解决包含角度、比率和距离的线性方程赛题。
同时，研究人员通过使用 Gemini 架构进行了更好的语言建模，并结合多个搜索树的新型知识共享机制让 AlphaGeometry2 的搜索过程得到极大改进。此外，研究人员还进一步增强了符号引擎和合成数据的生成能力。
AlphaGeometry2，更强更快的符号引擎
符号引擎是 AlphaGeometry 的核心组件。DeepMind 将其称之为演绎数据库算术推理（DDAR，Deductive Database Arithmetic Reasoning）。它是一种计算演绎闭包的算法，即给定一组核心初始事实，计算所有可推论事实的集合。
DDAR 通过遵循一组固定的推理规则来构建这个推理闭包，然后不断将新的事实添加到推理闭包中，直到无法再添加为止。DDAR 既能驱动语言模型的训练数据生成，又驱动推理步骤的搜索。在这两种情况之下，速度都至关重要。
更快的数据生成，将能产生更多以及更有力的数据过滤。而更快的证明搜索，则能带来更加广泛的搜索。这样一来，就能增加 AlphaGeometry2 在给定时间内找到解决方案的可能性。
为了提高速度，研究人员通过在 C++ 中实现其核心计算（高斯消元法）来进一步提高速度。新的 C++ 库通过 Pybind11 导出到 Python，通过此所打造的 DDAR2 比 DDAR1 快了 300 多倍。
为了针对速度提升进行基准测试，研究人员找出 25 个 DDAR 无法解决的 IMO 问题，并在配备 AMD EPYC 7B13 64 核 CPU 上运行 50 次测试。
结果显示，DDAR1 平均需要 1179.57±8.055 秒才能完成计算，而 DDAR2 的速度要快得多仅需 3.44711±0.05476 秒即可完成。
（来源：arXiv）
AlphaGeometry2，利用多个搜索树进行知识共享
在 AlphaGeometry1 中，研究人员使用了比较简单的集束搜索。在 AlphaGeometry2 中，研究人员设计了一种新的搜索算法，其能并行执行几个不同配置的集束搜索，并允许通过知识共享机制相互帮助。（注：集束搜索，是一种启发式图搜索算法，主要用于解决解空间较大的问题，并能减少搜索所需的时间和空间消耗。）
（来源：arXiv）
为了提高系统的鲁棒性，研究人员为每个搜索树配置使用了多种不同的语言模型，并将这种搜索算法称为搜索树共享知识集成（SKEST，Shared Knowledge Ensemble of Search Trees）。
其工作原理如下：在每个搜索树中，一个节点对应于一次辅助构造尝试，随后是一次符号引擎运行尝试。如果尝试成功，则所有搜索树终止。如果尝试失败，节点将把符号引擎设法证明的事实写入共享事实数据库。
这些共享事实经过过滤之后，便不再是特定于节点本身的辅助点，而仅仅与原始问题相关。这样一来，这些事实对于同一搜索树中的其他节点以及不同搜索树中的节点也可以起到作用。
对于证明搜索，研究人员使用谷歌的 AI 芯片 TPUv4 来为每个模型提供多个副本，并让同一模型内的不同搜索树根据自己的搜索策略查询同一服务器。（注：证明搜索，指的是机器在产生正确策略的过程中，会通过回溯来探索新的替代方案。）
除了异步运行这些搜索树外，研究人员还使用 DDAR workers 异步运行 LM workers。LM workers 将研究人员所探索的节点内容写到数据库中，然后 DDAR workers 异步地拾取这些节点并进行尝试。
研究人员表示，DDAR workers 通过相互协调来确保它们能够平等地分配工作。如果是一次解决多个问题，单个 DDAR 工作池会在不同问题之间共享，这样一来先前已被解决的问题就会释放自己的 DDAR 计算资源，从而用于其余正在解决中的问题。
AlphaGeometry2，利用 Gemini 架构进行训练
研究人员表示，AlphaGeometry1 的语言模型是一个自定义转换器，它采取无监督的方式，并分为两个阶段进行训练。它先是针对拥有辅助结构和没有辅助结构的问题进行培训，然后再只针对包含辅助结构的题进行培训。
而对于 AlphaGeometry2，研究人员利用 Gemini 训练流程并将训练过程简化为一个阶段：即对所有数据进行无监督学习。
与此同时，研究人员本次使用的新语言模型是一个基于稀疏混合专家 Transformer 的模型，该模型以 Gemini 为基础，并在 AlphaGeometry2 数据上进行训练。
在打造 AlphaGeometry2 的时候，研究人员使用三种训练设置来训练多个大小不同的模型。除了创建大约 3 亿条定理的大型综合训练集外，其还创建了三个评估集。所有这些评估集都包含完整的证明，同时在训练期间研究人员会计算它们的困惑度损失。
需要指出的是，和 AlphaGeometry1 一样的是，研究人员在推理过程中只使用语言模型建议的辅助点，并在整个证明上计算困惑度。同样与 AlphaGeometry1 一样的是，研究人员的主要下游指标是达成 IMO 赛题的解决率，而语言模型可以生成辅助点，然后通过集束搜索运行 DDAR。
研究中，研究人员使用 TPUv4 以硬件允许的最大 batch 大小来训练模型。在下图中，研究人员展示了不同大小的 Gemini 模型在参数计数方面的学习曲线。
（来源：arXiv）
通过以上努力，研究人员让 AI 学会了解答几何题。数学对 AI 模型来说真的很难，解答几何题需要复杂的推理技能，许多 AI 研究人员认为解决数学问题的能力可能预示着更强大、更智能的系统。
像 AlphaGeometry 这样的创新表明，人类正在开发具有人类一样推理技能的机器。这可以让人类构建更强大的 AI 工具，用于帮助数学家求解方程，也许还可以成为更好的辅导工具。
AlphaGeometry2 将在第 66 届 IMO 再“秀肌肉”
尽管 AlphaGeometry2 初步结果不错，但是研究人员认为仍然可以通过更多的形式化示例和监督微调，该进一步提高 AlphaGeometry2 的解题能力。
目前，受限于研究人员的领域语言（domain language），AlphaGeometry2 还不能解决可变点数、非线性方程和不等式等问题，而只有解决这些问题 AlphaGeometry2 才能实现 100% 地解决几何问题。
另外，AlphaGeometry2 并没有解决 IMO 和 IMO 短名单（IMOSL，International Mathematical Olympiad Shortlisted Problems）的所有赛题。研究人员认为，未来将这些赛题分解为子问题，并使用强化学习方法或许可以缩小这一差距。
另据悉，第一个在 IMO 测试中获得金牌的 AI 系统将赢得 AI Mathematical Olympiad Prize，并将获得 500 万美元的奖金。不过该奖励要求算法必须是开源的，因此 AlphaGeometry2 并不符合这一要求。
值得注意的是，2025 年 7 月研究人员将带着 AlphaGeometry2 参加第 66 届 IMO，届时或许会带来新的成绩。
参考资料：
https://www.nature.com/articles/d41586-025-00406-7
https://arxiv.org/pdf/2502.03544
运营/排版：何晨龙
