AlphaGeometry：DeepMind 大算力再造奇迹，但「算力代替智力」或许并非最优解
内容提要
AlphaGeometry是谷歌DeepMind的一种AI系统，结合了神经语言模型和符号推演引擎，能够解决复杂的几何问题。在国际奥林匹克数学竞赛中，AlphaGeometry表现出色，解决了25道题，超过了之前的方法和人类平均水平。虽然算力优势带来了强大的模型性能，但实际应用价值更重要。AlphaGeometry在教学和科研方面有潜力，但AI工具的特异性和统一性仍是挑战。AI for Science需要降低使用门槛和提升科研人员的能力。
延伸解读
算力优势与智力替代的边界
AlphaGeometry 在 IMO-AG-30 测试集上解决了 25 道题，接近人类金牌得主平均 25.9 道的水平，这背后是 DeepMind 强大的算力支撑。然而，林宙辰教授指出，算力替代智力在 AI 领域虽多次被验证有效，但迈向行业专家最后 1% 的突破仍难靠 AI 实现。这提醒我们，算力可以堆出高性能模型，但实际应用价值才是关键，AI 工具目前仍是“亦师亦友”的存在。
合成数据破解训练难题
AlphaGeometry 面临几何定理证明数据库匮乏的问题，研究人员通过符号引擎在随机定理前提上运行 10 万个 CPU 72 小时，生成了约 5 亿个合成证明示例，去重后得到 1 亿个训练数据。这种合成数据方法不仅解决了数据来源，还使模型无需人类演示即可自主应对复杂几何挑战，为 AI 在数学领域的训练提供了可借鉴的路径。
AI 工具的特异性与统一性挑战
当前 AI 工具缺乏统一性，即使在同一数学学科内，面向数论和几何的工具也差别很大，更不用说跨学科通用。林宙辰教授对比计算机语言的通用性指出，AI 工具尚未成为可方便取用的基础底座。未来需要降低使用门槛、提升统一性，使科研人员能像编程一样组合 AI 组件，同时科研人员也需提升使用 AI 的能力，才能充分发挥 AI 的威力。
Q&A
AlphaGeometry 在 IMO 几何题测试中的表现如何？
在 30 道 IMO 几何题的基准测试中，AlphaGeometry 在给定时间内解决了 25 道题，而之前 SOTA 的「吴方法」解决了 10 道，人类 IMO 金牌得主平均可以解决 25.9 个问题。
AlphaGeometry 是如何工作的？
AlphaGeometry 结合了神经语言模型和符号推演引擎。符号推演引擎从定理前提中穷尽地推演出新陈述，直到定理得到证明或陈述用尽；如果未能找到证明，语言模型会构建辅助点，增加可证明条件，然后重新开始符号引擎搜索，如此循环直到找到解决方案。解决方案会被自动解析为人类可阅读的语言。
AI 在数学定理证明中面临哪些主要挑战？
林宙辰教授表示，AI 进行数学定理证明的两大挑战是「表达」和「计算量」。表达是指将数学定理表达为计算机可以计算的方式；计算量是指传统方法在面对高难度问题时操作空间呈指数级增长，难以处理。
AlphaGeometry 如何解决训练数据匮乏的问题？
AlphaGeometry 使用合成数据进行训练。研究人员通过在各种随机定理前提上使用现有的符号引擎，利用 10 万个 CPU 运行了 72 小时，获得了大约 5 亿个合成的定理证明示例，进行形式规范化及去重后，最终得到了 1 亿个定理证明示例，其中有 900 万个示例涉及至少一个辅助构造。
AlphaGeometry 在实际应用中有哪些潜力？
林宙辰教授认为，AlphaGeometry 能够像 AlphaGo 一样成为「老师」，在教学方面起到更大的辅助作用。此外，它在模型性能方面的突破展示了算力优势，为崇尚算力的研究人员和企业增添了信心。
当前 AI 工具在科研应用中存在什么局限性？
林宙辰教授指出，目前的 AI 工具缺乏统一性，特异性强。即使只针对数学学科，面向数论和面向几何学所开发的 AI 工具就已经存在很大差别，更不用提跨学科的 AI 工具了。AI 工具还没有像计算机一样成为基础底座，可以方便取用。
未来如何推动 AI for Science 的发展？
林宙辰教授认为，未来一方面需要将 AI 工具的使用门槛降低，达到一定的统一性，使得 Science 人员也能够针对不同的问题自行组合使用 AI 工具的组件，就像计算机编程一样；另一方面，Science 人员也需要逐步提升使用 AI 工具的能力，才能充分发挥 AI 的威力。
