AlphaGeometry：DeepMind 大算力再造奇迹，但「算力代替智力」或许并非最优解
作者：李宝珠
编辑：三羊
封面图来源：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
我信奉的信条是物理学家路德维希·波兹曼的名言：没有什么比一个好的理论更实用的了。我现在想招数学能力强（但这并不意味着你必须来自数学系）、对理论分析非常感兴趣的博士研究生，以便与我一起享受如何优雅地使用数学解决实际问题。欢迎发送简历给我。
——林宙辰