八年前，横空出世的AlphaGo横扫围棋赛场，点燃了人工智能的热潮，也从根本上改变了围棋领域。近日，谷歌Deepmind团队一篇瞄准国际奥林匹克竞赛（IMO）几何题目的论文“AlphaGeometry”再度一石激起千层浪。国内对此已有铺天盖地的报道与讨论，诸如“解决前沿数学问题指日可待”“奥赛金牌近在咫尺”等评价将大众对人工智能解数学题的期许推上了新的高峰。
本文将深度解读AlphaGeometry，简要分析其与之前最好的基准模型的差距，并对该模型的发展前景给予评述。
欧氏几何题目因其规范的叙述和标准化的解题流程，是各类国内国际数学竞赛的“常客”。平面几何相比其他数学领域所具有的封闭性、简洁性、可验证性，也让它更适合机器证明。上世纪七十年代，吴文俊院士提出的“吴方法”是这一领域的奠基之作，而随后涌现的推理数据库 (DD) 方法则在保留证明的有效性的同时，大大提升了证明的可解释性。
AlphaGeometry在自己构建的30道IMO题目上测试DD+AR+heuristic，可以做对其中的18道题。在这个基础上，AlphaGeometry的主要贡献是训练了一个151M大小的语言模型来代替启发式算法，以实现更好的加辅助点策略，获得了从做对18道题目到25道题目的进步。
总的来说，AlphaGeometry能解决所选的共30题的IMO题集中的25道，已经展现了其在几何推理上的有效性。然而，受限于DD+AR的表示能力，想要将这篇工作的架构拓展到标准平面几何剩下的约30%题目十分困难。同时，DD+AR充分利用了平面几何简洁明确的推理结构，但也因此被局限在几何的范畴内，难以拓展到数学其他领域。
正如论文所提到的，这篇工作所着手的对象范围较为狭窄，其核心原因在于形式化数据的不足。以Lean为代表的一系列形式化数学语言为自动定理证明提供了逻辑严密、表达能力强且能自动验证的交互环境，这是解决类似于DD+AR这样的小领域符号引擎的表达能力限制的突破口。只有联合Lean community等形式化社群进行更全面、广泛的形式化数学数据的积累和收集，AI4Math才能有本质上的进展。