DDAR 是什么？AlphaGeometry 推导几何结论的符号引擎

演绎数据库算术推理（Deductive Database Arithmetic Reasoning，DDAR）是 AlphaGeometry 系统中负责严格推导的符号推理引擎，由谷歌 DeepMind 开发，2025 年 2 月发表的 AlphaGeometry2 论文《用 AlphaGeometry2 在奥林匹克几何题求解中达到金牌水平》对它做了大幅改进。

它做什么：计算演绎闭包

DDAR 是一种计算“演绎闭包”的算法。演绎闭包是指：给定一组核心的初始事实，所有能从它们推导出来的事实的集合。比如已知“AB 等于 AC”“D 是 BC 的中点”，可以推出“AD 垂直于 BC”，再推出更多的角度关系、相似三角形，等等。DDAR 遵循一组固定的演绎规则来构建这个闭包：每一轮都检查所有规则，看能否根据已知事实推出新的事实，把新事实加入集合，然后继续下一轮，迭代地扩充，直到再也推不出新的事实为止。如果要证明的结论出现在这个闭包里，题目就证完了，而且每一步推导都有严格的依据，可以还原出完整的证明过程。

名字里的“演绎数据库”指的是用类似数据库查询的方式匹配推理规则，“算术推理”指它还能处理关于角度、比例、长度的代数关系，比如角度相加等于 180 度这类线性方程。

和语言模型的分工

DDAR 很严谨，但它只能从已有的条件出发往下推，自己想不出“添加一条辅助线”这样的创造性构造。很多奥数几何题，不添加辅助点就无法证明。这部分由 AlphaGeometry 的语言模型负责：当 DDAR 推不出结论时，语言模型提出一个辅助构造，DDAR 再在新的条件下重新推导，两者配合，就像人类解题时“灵感加严谨推导”的过程。

AlphaGeometry2 的改进

在 AlphaGeometry2 中，DDAR 的能力得到了扩展，比如能处理一些重合点、更多类型的几何关系，同时速度大幅提升：研究团队用更高效的算法和 C++ 实现重写了它，比原来快了一个数量级以上。更快的符号引擎意味着在同样的时间里能尝试更多的辅助构造，这是 AlphaGeometry2 能达到金牌水平的重要原因之一。