解决什么问题
几何是检验 AI 推理的硬题,因为自然语言题面、图形、辅助构造和形式化证明步骤会缠在一起。人类写好的几何证明数据很少,朴素搜索又会迅速爆炸。AlphaGeometry 研究的是:能否不依赖人类证明示例,让系统自己学会为几何证明搜索提供有用方向。
核心方法
AlphaGeometry 是神经符号系统。神经语言模型负责提出可能有用的辅助构造,符号演绎引擎负责做严格几何推理。它不是从人类证明里模仿,而是合成数百万个不同难度的定理和证明,再从零训练语言模型来引导搜索。神经部分提供直觉方向,符号部分检查每一步是否成立。
关键结果
在 30 道最新奥赛级几何题的测试集上,AlphaGeometry 解出 25 道,明显超过此前只能解 10 道的最佳方法,接近平均 IMO 金牌选手水平。在专家评估下,它解出了 IMO 2000 和 2015 的全部几何题。它还能输出人类可读证明,虽然证明并不总是像数学家写的那样简洁优雅。
为什么重要
AlphaGeometry 的关键在于避开了「神经模型流畅但不可靠」和「符号系统可靠但搜索太慢」之间的老矛盾。语言模型不需要凭空编证明,只负责提出能扩大搜索空间的构造;符号系统负责验证推导。这种模式可以推广:用学习引导搜索,用形式系统验证每一步。
局限与存疑
它仍是面向欧氏平面几何的专用系统,不是通用数学家。有些证明很长、机械、可读性不高,而把真实题面稳定转成合适形式表示也仍然困难。更大的问题是,合成数据加符号检查这条路,能否扩展到代数、组合、形式化定理证明和科学推理。
一句话:AlphaGeometry 用神经直觉给符号证明带路。