前言

最近我在做 AI for Math 相关的产品，不是那种让大模型讲题的工具，而是更偏结构化的几何表达、约束关系、图形结构、推理能力这些。

做着做着会发现一个问题：让 AI 聊数学不难，让 AI 真正做数学，很难。

尤其是几何。

我可以让模型解释“为什么内错角相等”，但让它在一张复杂图里自己找到关键辅助线，它就开始胡说八道。

这时候再回头看 Google 的路线，会发现他们其实很早就开始系统性地做这件事。

AlphaGeometry（AG1）是第一代。

AlphaGeometry2（AG2）是升级版。

如果把两代系统连起来看，它倒是一份非常清晰的数学 AI 系统踩坑记录。

我写这篇文章，就是想站在 Google 的肩膀上，看一看：

• 他们卡在哪
• 怎么解决
• 哪些地方是工程问题
• 哪些地方是认知误区

一、第一代 AlphaGeometry：它到底解决了什么？

AG1 的核心思路其实蛮务实的：不要指望大模型自己证明几何题，而是让大模型负责“猜”，符号系统负责“算”，搜索负责“找”。

具体来说：

• LLM 提出辅助构造
• DDAR 符号引擎做角度和比例推理
• 搜索系统遍历可能路径

这个架构本身是非常理性的，它承认语言模型不擅长严谨推理，而是擅长模式匹配和生成可能有用的构造。真正的证明则交给符号系统。

这里的关键组件是 DDAR 推理引擎。

DDAR 的全称是 Deductive Database of Angle and Ratio，

简单理解，它其实是一个专门为几何设计的推理系统。

系统会维护一个不断扩展的“几何关系数据库”，一开始它只知道一些基础事实。比如：

A,B,C 共线
D 在 AB 上

然后不断应用几何定理，例如：

共线 → 角度为 180°
圆 → 共圆角相等
相似三角形 → 比例关系

每推导出一个新的关系，就加入数据库，然后继续推理。这个过程会一直持续，直到推导出目标结论。

换句话说，DDAR 做的事情就是把所有能推出的几何关系全部推导出来。

二、AG1 卡在哪？（这些问题我也踩过）

AG1 很强，但问题也很明显。

我从工程角度看，主要有三个卡点。

1️⃣ 表达能力太弱

AG1 的几何语言非常克制，它只支持一些基础关系，例如：

collinear(A,B,C)
parallel(l1,l2)
perpendicular(l1,l2)
concyclic(A,B,C,D)
equal_angle(...)

但很多 IMO 题目其实需要表达距离关系、比例关系、角度数值计算，这些在 AG1 中都表达不了。例如：

AB = CD
AB / CD = EF / GH
∠ABC = 60°

如果语言里没有这些表达能力，系统就无法正确理解问题。

我们给 AI 的表达空间，决定了它能做多复杂的事情。 就像人类文明的语言系统一样，当一个概念在语言里不存在时，我们很难真正理解它。

AG1 在这里明显受限，因为语言太窄了。

2️⃣ 搜索会爆炸

几何证明本质上是在巨大的可能构造空间里，找到一条对的路径。

例如：连哪条辅助线？作哪条垂线？哪些点可能共圆？

AG1 是“试一个构造 -> 跑推理 -> 不行再换”。

问题是辅助线的可能性太多了，系统很容易卡在局部搜索。

3️⃣ 数据问题

数学 AI 的最大难题之一：没有大规模高质量数据。

AG1 的解决方式是随机生成几何图，自动生成定理，自动生成证明。

但第一代系统生成的题目复杂度还是有限，这会影响模型的构造能力，让它无法真正解决复杂题目。

三、AlphaGeometry2：升级了什么

很多人会以为 AG2 的进步是因为 Gemini 底模更强了。

当然这是原因之一，但我认为下面几个升级更关键。

1️⃣ 语言扩展

AG2 扩展了几何 DSL，新增了很多 predicate。例如：

dist_eq(A,B,C,D)        → AB = CD
ratio_eq(A,B,C,D,E,F)   → AB/CD = EF
angle_compute(...)      → 角度数值关系

DSL 扩展之后，IMO 题目的表达覆盖率从 66% 提升到 88%。

换句话说上个版本 不是 AI 不会做题，而是很多题 AI 根本没法读懂。

2️⃣ 搜索方式升级

AG1 基本是单树搜索。AG2 引入了多棵搜索树 + 共享中间结论，可以理解为多个解题小组同时工作。

这显著提高了找到关键辅助线的概率。

3️⃣ 推理引擎优化

DDAR 在 AG2 中被强化：新推理规则，推理图压缩，推理速度优化。

推理更快，搜索空间自然更可控。

这不是 glamorous 的创新，但非常重要。

4️⃣ double points

AG2 里还有一个很有意思的几何 trick，叫 double points。

简单说，就是允许系统在推理中创建两个“重合点”。例如：

A ≡ A'

也就是说 A 和 A’ 实际上是同一个点，但在推理系统里可以参与不同关系。比如：

A 在直线 l 上
A' 在圆 c 上

因为 A = A’，最终可以推出：

A 在圆 c 上

这个技巧可以把很多复杂的角度问题转化为共圆问题，而共圆关系更容易被推理系统处理。

如果你做过竞赛几何，会发现这种思路其实很熟悉，AlphaGeometry2 只是把这种技巧系统化了。

四、结果对比

看最终结果，AG2 的提升其实非常明显。

在 DeepMind 的官方报告中，他们统计了 过去 25 年（2000–2024）所有 IMO 几何题。

系统	解题率
AlphaGeometry (AG1)	54%
AlphaGeometry2 (AG2)	84%

AG2 在同一套题目上，解题能力提升了 30 个百分点。

DeepMind 研究团队还给了一个很有意思的对比：

42/50 的成绩已经超过平均 IMO 金牌选手的水平。

另外一个指标是 问题覆盖率。

很多几何题在 AG1 中根本无法表达，因为语言太窄。

AG2 扩展 DSL 后：

指标	AG1	AG2
IMO 题目可表达覆盖率	66%	88%

语言一扩展，系统能力直接上了一个台阶。

DeepMind 在官方博客中也提到，在 IMO 2024 的测试环境里，AG2 在形式化之后 19 秒就解决了一道竞赛题，整体成绩达到 28/42 分，接近金牌线。

五、写在最后

AlphaGeometry2 说明了一件事：

在结构化系统里，AI 可以非常强。

如果你指望纯 LLM 能直接证明 IMO 几何题，我认为短期几年内不现实。

但 LLM + 领域语言 + 符号引擎 + 搜索系统 是一个非常稳健的方向。

站在巨人的肩膀上看一眼，可以少走很多弯路。

如果未来几年 AI 数学系统会继续进化，我猜关键词是：

• 更强的结构
• 更合理的语言
• 更精细的搜索

这可能比我们想象中重要得多。

参考资料

• DeepMind Blog – AlphaGeometry2
• AlphaGeometry: An Olympiad-level AI system for geometry
• AlphaGeometry2 GitHub
• AlphaGeometry GitHub

个人博客：luhuidev.com