作者：李宝珠

编辑：三羊

封面图来源：Google DeepMind

DeepMind 用算力堆出奇迹？被夸上天的 AlphaGeometry 含金量有多高

近日，谷歌 DeepMind 的 Alpha 系列再添新成员——AlphaGeometry，依旧声势浩大，「里程碑」、「史诗级」、「逼近人类」等赞美之词溢出屏幕。那么，这个号称奥数能力金牌级的 AI 系统到底有多少含金量呢？

AlphaGeometry 由谷歌 DeepMind 团队和纽约大学的研究人员共同研发，**将神经语言模型 (neural language model) 与符号引擎 (symbolic deduction engine) 相结合，**能够解决复杂的几何问题，并且水平接近人类。

在对 30 道国际奥林匹克数学竞赛 (IMO) 几何题的基准测试中，在给定时间内 AlphaGeometry 解决了其中的 25 道题，之前 SOTA 的「吴方法」解决了 10 道，而人类 IMO 金牌得主平均可以解决 25.9 个问题。

诚然，自 AlphaGo 面世以来，伴随着多次面向不同学科的革新性突破，「DeepMind 出品，必属精品」的定位逐渐在人们心中扎根。但同时，业内也不乏理性、辩证的声音——算力替代智力固然可喜，但实际应用价值更加重要。所以，借着 AlphaGeometry 的发布，我们想浅谈一下，这到底是算力优势下的狂欢，还是 AI for Science 的探路。

值得一提的是，**我们采访到了北京大学智能学院教授林宙辰，针对相关学术问题进行了探讨与学习。**林宙辰教授曾先后在南开大学、北京大学、香港理工大学攻读数学和应用数学专业，而后又回到了北京大学数学学院攻读博士学位，开始进入人工智能领域。（点击查看林宙辰教授专访）

表达与计算量：AI for Math 的两大挑战

林宙辰教授表示：“过去，数学定理的「表达」与大规模的计算量是 AI 进行数学定理证明的两大挑战。”

“首先，作为十分抽象化、且高度依赖逻辑推理的学科，数学拥抱 AI 的第一步就是要解决「表达」问题，将数学定理表达为计算机可以计算的方式是后续 AI 应用的基础。”

“AlphaGeometry 所针对的几何问题，「表达」的难度属于数学中较低的一种，解析几何、代数几何的出现，其实已经实现了通过数值来表示几何形状和几何对象间的关系，加之吴文俊院士在 20 世纪 70 年代所提出的「数学机械化」，也在一定程度上为平面几何定理与机器语言之间构建了连接桥梁。”

“其次，吴文俊院士提出的「吴方法」以及传统的Gröbner基等方法，已经从理论上解决了平面几何定理证明的问题，但是却囿于算力，换言之，由于存储量、计算量大，尤其是在面对比较难的平面几何问题时，操作空间会呈指数级增长，所以过往的很多方法都难以处理高难度问题。”

“计算量大的问题对于「财大气粗」的 DeepMind 而言显然不是主要障碍，主要困难在于如何避免操作空间指数级增长，此时机器学习方法可以帮上忙。”

具体而言，AlphaGeometry 基于 1 亿个合成数据进行训练，无需人类演示即可自主应对复杂的几何学挑战，并生成人类可阅读的证明。

如下图所示，以我国中小学生最熟悉的「等腰定理」为例，想要证明 ∠ABC=∠BCA，需要先手动将问题转化为计算机语言，进而将其输入到 AlphaGeometry。

AlphaGeometry 通过运行符号推演引擎启动证明搜索，该引擎从定理前提中「穷尽」地推演出新的陈述，直到定理得到证明或新的陈述被用尽。如果符号推演引擎未能找到证明，语言模型就会构建一个辅助点，增加可证明的条件，进而重新开始通过符号引擎搜索证明。如此循环，直到找到解决方案。

解决方案将会被自动解析为人类可阅读的语言，所以还能够进行验证、评估。

值得一提的是，AlphaGeometry 使用了合成数据进行模型训练，解决了相关数据库匮乏的问题。

研究人员通过在各种随机定理前提上使用现有的符号引擎，利用 10 万个 CPU 运行了 72 小时后，获得了大约 5 亿个合成的定理证明示例，进行形式规范化及去重后，最终得到了 1 亿个定理证明示例，其中有 900 万个示例涉及至少一个辅助构造，许多证明步骤超过 200 步，是国际奥林匹克数学竞赛几何题平均证明长度的 4 倍。

合成数据生成过程

为了对比测试 AlphaGeometry 解决实际问题的能力，研究人员尝试将自 2000 年以来的 IMO 竞赛中的几何问题转化为符号引擎可读的机器语言，并发现其中只有 75% 可以成功表达，进而形成了一个由 30 道经典几何问题组成的测试集 IMO-AG-30。

每个问题都有不同的运行时间，这是因为其推导闭包大小各不相同。研究人员发现，运行时间与问题的难度并不相关。例如，IMO 2019 P6 比 IMO 2008 P1a 难得多，但要在 IMO 时限内求解，所需的并行化时间却要少得多。

由于语言模型解码过程会返回 k 个不同的序列，描述 k 个可供选择的辅助结构，研究人员在 k 个选项上进行集束搜索 (beam search)，使用每个集束的得分作为其值函数。这种方法具有很强的并行性，在有并行计算资源的情况下，可以大幅提高搜索速度。

研究人员发现，在 GPU V100 加速语言模型有四个并行副本的情况下，解决所有 25 个问题并保持在规定时间内的最少并行 CPU 数量如下图所示：

10 个不同的模型/方法，在 IMO-AG-30 测试集中的表现如下图所示。有意思的是，GPT-4 在测试中竟一道题都没有做对。

算力替代智力的背后，应用价值才是重点

最近两天，网络上铺天盖地的各类报道已经将 AlphaGeometry 的成果剖白得淋漓尽致，其影响力无需赘述，所以我们更希望能够探究，喧闹过后，AlphaGeometry 能为科研、为 AI 应用发展带来哪些实际价值？

对此，林宙辰教授表示：“**目前来看，AlphaGeometry 能够像 AlphaGo 一样成为「老师」，在教学方面起到更大的辅助作用。**此外，AlphaGeometry 在模型性能方面的突破不可否认，其更是进一步展示了「大力出奇迹」——强大的算力优势造就了强悍的模型性能，这也在某种程度上进一步为「崇尚」算力的研究人员、企业增添了信心。”

不过，正如林宙辰教授所言，在 AI 领域，尽管我们已经无数次见证了「算力替代智力」的有效性，但最终迈向行业专家的最后1% 的突破还是很难靠 AI 来实现的。

所以，就目前而言，无论是 AlphaGeometry，亦或 GPT 模型等其他 AI 工具，在人们的日常生活以及科研工作中，仍是「亦师亦友」的存在，灵活使用 AI 工具已是大势所趋，如何将算力造就的「奇迹」应用于实际问题才是人类难以被取代的价值所在。

借古鉴今，AI 工具的快速崛起与计算机的普及有着很多相似之处，例如革命性的工作方式转变，正势如破竹地替代传统方法，逐渐成为职场能力的考核标准……但对比之下，AI 工具的局限性也更加凸显，那就是特异性。

林宙辰教授认为：“目前的 AI 工具缺乏统一性，即使只针对数学学科，面向数论和面向几何学所开发的 AI 工具就已经存在很大差别，更不用提跨学科的AI工具了。AI 工具还没有像当今的计算机一样，成为基础底座，可以方便取用。目前的计算机语言有 C 语言、Java、Python等，完全可以基于其中一种语言解决数学、物理、化学等多学科的问题，这体现了其通用性，但是 AI 工具则不然，光看 Alpha 系列便可知一二。”

所以，林宙辰教授认为：“未来，当 AI 工具可以抽象出来可以重用时，AI for Science 才能够「大行其道」。”

这也是 HyperAI超神经在持续追踪 AI for Science 发展进程时所观察到的现象，部分课题组或研究团队会在本学科成员之外，专门招聘一位主攻 AI 的成员，负责开发研究中需要的 AI工具，而Science 部分则还是交由传统的科研人员来完成。

毫无疑问，AI 对科研进程的帮助与提升已经日益明显，正在成为新趋势，但这种 AI+Science 的团队模式又是否是长久之计呢？

林宙辰教授认为：“未来，一方面需要将 AI 工具的使用门槛降低，达到一定的统一性，使得 Science 人员也能够针对不同的问题自行组合使用 AI 工具的组件，就像计算机编程一样；另一方面，Science 人员也需要逐步提升使用 AI工具的能力，才能充分发挥AI的威力。”

道阻且长，行之将至。AI for Science 由DeepMind 等大厂引发，加之国家政策推进，已经开始了漫漫征程，其中的荆棘需要科研与产业界共同肃清，才能够真正在落地中为人类发展创造价值。

最后，感谢北京大学智能学院林宙辰教授对笔者撰文提供的帮助与支持。目前林宙辰教授的课题组正在招聘博士研究生，欢迎符合要求的学生将简历发送至：zlin@pku.edu.cn

我信奉的信条是物理学家路德维希·波兹曼的名言：没有什么比一个好的理论更实用的了。我现在想招数学能力强（但这并不意味着你必须来自数学系）、对理论分析非常感兴趣的博士研究生，以便与我一起享受如何优雅地使用数学解决实际问题。欢迎发送简历给我。

——林宙辰

来源: HyperAI超神经