首次击败人类数学天才 让高中生头疼的数学考试被DeepMind AI攻克了
让人类高中生头疼的最难数学考试—— 国际数学奥林匹克竞赛(IMO)——被人工智能(AI)攻克了。在一项近期公布的研究中, Google DeepMind 团队称他们的 几何解题系统 AlphaGeometry 解决了 84%(42/50)的几何难题,其表现 首次超过了 IMO 平均金牌得主 (40.9/50)的水平。
此外,去年 7 月,AlphaGeometry 也“联手”AlphaProof(一个基于强化学习的形式数学推理新系统),在当年 IMO 中首次达到了银牌获得者的水平。
AlphaGeometry2 是 AlphaGeometry 的显著改进版本。它是一个 神经符号混合系统,其语言模型基于 Gemini, 并在比其前身多一个数量级的合成数据上从头开始训练。这帮助模型解决更具有挑战性的几何问题, 包括关于物体运动和角度、比例或距离的方程问题。
AlphaGeometry2 使用的符号引擎比其前身快两个数量级。 面对新问题时,一种 新颖的知识共享机制 被用来实现不同搜索树的先进组合,以解决更复杂的问题。
对此,伦敦帝国理工学院数学家 Kevin Buzzard 评价道:“我想,不久之后,计算机就能在 IMO 竞赛中拿满分了”。
相关研究论文以“Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2”为题,已发布在预印本网站 arXiv 上。
01 更强的数学推理,速度提升 300 倍
AlphaGeometry2(AG2)是 Google DeepMind 开发的一款神经-符号混合 AI 系统,用于解决国际数学奥林匹克(IMO)的几何问题。
AG2 结合了语言模型(Neural)和符号推理引擎(Symbolic),采用一种混合推理方法(neuro-symbolic approach)来解决几何问题。 相比其前代 AlphaGeometry(AG1),AG2 在解题率、搜索算法、语言模型和符号推理方面都有重大改进,首次超越了 IMO 平均金牌得主的表现。
据论文描述, AG2 在原始 AlphaGeometry(AG1)语言的基础上进行了扩展 ,使其能够处理更复杂的几何问题,包括:
物体移动(Locus-type Problems):AG2 新增了轨迹(locus)相关谓词,使 AI 能够推理点、直线、圆等几何对象的移动;
线性方程问题(Linear Equations):AG2 现在可以解析涉及角度、比例和距离的线性方程;
新的几何谓词(Predicates):AG2 语言新增了多个谓词,以支持更复杂的几何推理。
这些扩展将 AG2 语言的覆盖率(coverage rate)从 66% 提高到了 88% ,使其能够处理更多 IMO 几何题目。
图|AG2 与 AG1 的训练数据分布对比(a-c): a.与 AG1 相比,AG2 包含更复杂/更长的问题; b.AG2 在每种问题类型的示例分布上更加均衡; c.G2 在包含辅助点的证明与不包含辅助点的证明之间具有更均衡的比例)
此外, AG2 还采用了 Gemini 语言模型,相比 AG1 具有更强的数学推理能力。 该语言模型用于预测几何构造(如辅助线、角度计算等),并帮助生成解题步骤,其训练数据包含 3 亿条自动生成的定理和证明,大幅扩展了 AI 的数学知识库。
同时, AG2 采用了一种新型搜索算法(Shared Knowledge Search Trees, SKEST),引入知识共享机制,将多个搜索树(multiple search trees)结合在一起, 相比 AG1 仅用单一搜索策略,AG2 允许不同搜索路径可以共享已验证的数学推理,显著提升了 IMO 竞赛的求解能力。
图| 搜索算法概览: 将多个搜索树结合在一起并通过一种特殊的知识共享机制,在它们之间共享已证明的推理
不仅如此, 相比 AG1 的符号引擎,AG2 在求解速度上提升 300 倍 ,并且新增处理“双点”能力,能够解决一些需要构造多个相交点的问题。
02 探索可泛化 AI
尽管 AG2 已经取得突破性进展,但仍存在一定局限性。 在 AG2 未能解决的题目中,有 6 道 IMO 题目因涉及变量点个数、不等式、非线性方程而未能求解,因 AG2 语言尚不支持这些类型;2 道题目涉及更高级的几何技术(如反演、投影几何、根轴法),目前也未在 AG2 的符号引擎中实现。
DeepMind 团队表示,未来 AlphaGeometry 的改进方向将包括处理涉及不等式和非线性方程的数学问题,这些能力对于 “完全解决几何问题” 至关重要;此外,进一步改进自动数学公式化(Auto-Formalization)技术,使 AI 能更准确地 从自然语言解析数学问题 也在团队的计划当中。
另外,研究表明, AG2 不仅能够生成辅助构造(auxiliary constructions), 还能推导出完整的证明(full proofs),这表明 当前的语言模型有潜力在无需外部工具(如符号推理引擎)的情况下独立运行。 如果他们的设想正确,这些解题能力可能会成为未来 通用人工智能(AGI) 的一个重要组成部分。
AlphaGeometry2 或许表明, 符号操作和神经网络这两种方法的结合 ,是探索可泛化 AI 的一条有希望的道路。 事实上,根据 DeepMind 的论文,同样具有神经网络架构的 o1 无法解决 AlphaGeometry2 能够解答的任何 IMO 问题。