Aristotle AI：自动定理证明系统的革命性突破

狭间

1. Aristotle AI系统概述

Aristotle AI是一个革命性的自动定理证明系统，它成功结合了形式化验证的严谨性和非正式推理的灵活性，在2025年国际数学奥林匹克竞赛(IMO)中取得了相当于金牌级别的成绩。这个系统由Harmonic团队开发，能够为IMO级别的数学问题生成完整的、机器可验证的证明。

1.1 系统核心架构

Aristotle AI由三个主要子系统组成：

Lean证明搜索系统：基于蒙特卡洛图搜索(MCGS)算法，使用大型Transformer模型作为策略和价值函数。这个系统能够接收Lean证明草图，并尝试填补所有未证明的目标。
非正式推理系统：生成数学陈述的非正式证明，将这些证明分解为引理，将每个引理形式化为Lean代码，并根据形式化反馈迭代这个过程。
专用几何求解器：处理平面几何问题，采用基于AlphaGeometry的方法，但进行了显著的性能优化。

提示：Aristotle的创新之处在于它不满足于仅生成非正式证明，而是坚持为每个解决方案提供完整的、机器验证的形式化证明，这大大提高了结果的可靠性。

1.2 技术突破与意义

Aristotle代表了自动定理证明领域的重要突破，其意义体现在多个方面：

验证可靠性：系统只认为问题被解决当它能在Lean 4证明语言及其数学库Mathlib中生成完整证明，没有漏洞或不健全的公理。
性能表现：在2025年IMO中，Aristotle为六道题目中的五道提供了正确的形式化解决方案，达到了金牌级别的表现。
扩展能力：虽然针对竞赛数学进行了微调，但Aristotle也展示了在更高级数学主题上的能力，如范畴论和同调代数。

2. 核心技术与实现细节

2.1 Lean证明搜索算法

2.1.1 搜索基础架构

Aristotle的证明搜索算法建立在蒙特卡洛树搜索(MCTS)基础上，结合了学习到的价值函数，灵感来自专家迭代(Expert Iteration)和AlphaZero。算法接收一个Lean代码块，并尝试用证明替换代码中的所有"sorry"语句。

搜索过程使用生成策略从Lean战术的大动作空间中逐步扩大采样，条件基于Lean证明状态、证明历史，以及可用的非正式证明。同一个模型和提示(最多到一个任务标记)被用来计算指导搜索的价值函数。

2.1.2 状态与动作处理

搜索算法可以从执行初始Lean代码片段获得的任何Lean状态集合开始。状态按目标分裂直到元变量：

如果初始代码片段或搜索期间采取的动作产生多个目标且没有目标包含元变量，则为每个目标创建一个状态
否则，保留代表目标集合的单一状态
例外情况是由显式"sorry"占位符创建的目标，这些目标不允许有任何元变量

动作是被解释为Lean代码片段的文本字符串，可以包括单个Lean战术或多个战术序列，也可以包含非正式注释。执行一个动作可能导致多个状态，形成所谓的"超树"。

2.1.3 等价性与图搜索

Aristotle将仅在表面上不同的状态视为等价，对动作也采用类似处理。这种等价性处理将搜索超树转变为搜索超图，使搜索算法更准确地成为一种蒙特卡洛图搜索(MCGS)。

这种图搜索虽然在最坏情况下每一步的复杂度从树的O(D)降级为图的O(V)，但在实践中并未观察到CPU瓶颈。

2.2 引理基础推理系统

2.2.1 引理生成流程

虽然搜索算法本身很有效，但当作为更大的引理基础推理系统的一部分部署时，它会变得更强大。这个策略的早期实现是"Draft, Sketch, and Prove"算法，Aristotle的实现在图1中进行了总结。

流程从目标定理开始，通过一系列自然语言查询处理它：

首先，要求定理的非正式证明
接着，要求将(1)中的证明重构为一系列相互建立的引理，每个引理都有非常简短的证明
然后，要求将(2)中产生的引理陈述形式化
最后，在将(3)中的形式化发送到Lean REPL后，传回任何错误消息并要求更正

2.2.2 形式反馈迭代

当Aristotle仍然无法证明目标定理时，可以迭代应用这个引理架构。在失败尝试结束时，通常会证明一些引理而其他引理(以及目标定理)仍未证明。我们通过标记每个引理为已证明或未证明来注释用于尝试的引理列表，然后将其用作原始查询序列修改版本的输入。

3. 几何求解器技术

3.1 Yuclid引擎

Aristotle的几何求解器基于Yuclid，这是一个非常快速的C++ DD/AR(演绎数据库和代数推理)引擎。Yuclid已经以Apache 2.0许可证在GitHub上发布，其所有部分都考虑了速度优化，使其比AlphaGeometry-1快达500倍。

3.1.1 性能优化

Yuclid中采用了几项关键优化：

数值规则匹配器：在运行主DD/AR循环前，Yuclid找到所有数值匹配的规则，即其假设和结论在数值上为真的规则。为避免冗余工作，匹配器在图中找到某些配置(如相似三角形对、中点、三角形平分线等)，然后将关于这些配置的所有规则添加到列表中。
陈述去重：在主DD/AR循环中，Yuclid遍历所有数值匹配的规则，并尝试从AR推导它们的假设和结论。为此，它将当前证明陈述的进展存储在字典中，从而在不同出现的相同陈述之间去重工作。
AR优化：代数推理使用高斯消元法实现，有一些优化可以避免重复工作。例如，我们存储线性系统的当前阶梯形式，每次建立新陈述时更新它。对于每个我们尝试通过AR证明的陈述，我们还存储它相对于已建立方程的当前简化形式。
内存管理：C++语言的特性以及STL和Boost容器允许我们优化内存管理。例如，我们将所有待处理AR方程的简化形式存储在字典中，相应的陈述存储指向该字典中对象的原始指针，而不是键。

3.1.2 其他特性

除了性能优化，Yuclid还引入了与AlphaGeometry-1相比的几个扩展：

新的AR表：除了长度和对数长度的AR表外，Yuclid引入了平方长度的新AR表。这个表允许我们有效地陈述毕达哥拉斯定理及其更一般的形式。
正弦定律：可选地，Yuclid可以将角度的正弦添加到比率AR表中，与正弦定律一起。这个扩展允许它通过DD/AR证明AG-30中的一个新问题，但也使Yuclid减慢约10倍，因此在推荐配置中关闭。
作为陈述的方程：在Yuclid中，三个AR表中的任何AR方程都可以包装成Statement。这样我们可以添加例如平行四边形法则，而不需要添加规则特定的谓词。
新规则：第一次运行数据生成后，我们搜索输出中需要辅助构造的最多4个点的问题，将其中几个转化为后续使用的新规则。

4. 性能评估与应用成果

4.1 IMO 2025表现

在2025年IMO上，Aristotle为六道题目中的五道提供了正确的形式化解决方案，达到了金牌级别的表现。这些问题涵盖了代数、数论、几何和组合数学等领域。

获得系统的最大性能需要在三个正交方向上进行扩展：

使用具有超过200B参数的模型运行搜索算法
运行许多并行实例的引理基础推理管道，从非正式证明和形式草图的空间中广泛采样
在单个实例上多次迭代这个管道的形式反馈循环，以最大化错误纠正的潜力

4.1.1 问题1：Sunny Lines

"Sunny Lines"问题的证明与大多数人看到的证明不同。这个问题涉及通过三角形内多个格点的直线，证明的典型步骤使用了一个事实：一条直线最多可以通过凸体(这里是三角形)的两个边。这个事实在几何上是显而易见的，但在Lean中形式化和证明却很繁琐。相反，Aristotle产生了一个不同的、更代数的证明，研究了问题中隐含出现的某些错位(没有固定点的排列)。它通过检查n=5的点找到了一个明确的例子，排除了所有更大n的构造。

4.1.2 问题3：Bonza函数

"Bonza函数"问题需要描述满足同余式ba ≡ f(b)f(a) (mod f(a))的函数f:N→N。在问题解决的早期阶段，Aristotle开始根据某个集合S来描述这些函数，它最终将其形式化为：

lean复制def S (f : N+ →N+) : Set N+:= {p | Nat.Prime (p : N) ∧f (p) > 1}

这个集合在几个引理的最终证明中被使用，但不是由问题陈述直接定义或建议的。因此，它说明了Aristotle定义和使用新的辅助定义的能力，就像人类数学家一样。

4.1.3 问题4：三个除数的和

问题4涉及关于其适当除数满足某种递推关系的无限数列的可能性。Aristotle开发的论证使用了与典型人类解决方案相同的逻辑——本质上只有一个论证——但导致证明的过程包含了几个例子，说明形式化在识别和纠正非正式推理错误方面的力量。

考虑Aristotle的非正式证明中的一个摘录，这个证明最终导致了形式化证明：

"...在这种情况下，an+1 < an。如果序列进入这种状态，它就会严格递减。对于正整数无限序列，这只有在它最终变成常数时才可能，即达到固定点。"

在这里，非正式推理混淆了严格递减序列、弱递减序列和在某些点递减的序列之间的区别——在周围的文本中，它把所有这三种都称为"递减序列"。这种微妙的语言错误是验证AI生成的自然语言证明所面临的挑战的典型。

然而，在随后的形式化过程中，Aristotle修复了这个错误(和一些相关错误)，使用有缺陷的非正式证明中的关键思想，但根据需要填补其逻辑空白。此外，由于最终证明中的伴随非正式注释遵循Lean代码的验证结构，它们提供了最终逻辑的更正的非正式说明。

4.1.4 问题5：Inekoalaty游戏

"Inekoalaty游戏"的解决方案需要为某个游戏中的两个玩家确定最优游戏策略，并证明在什么条件下它们会强制获胜和平局。像问题3一样，Aristotle确定了适当的游戏策略并在Lean中形式化了它们的定义，但更有趣的是引入了与证明相关但不由陈述本身建议的辅助定义。具体来说，它定义了函数f(k) := k√2/(2k -1)，这个函数在证明过程中变成了一个有用的不变量。

在这个问题中，Aristotle还展示了它对比IMO问题所需更高级主题的流畅性，原则上IMO问题可以仅用高中数学概念解决。它的引理lemBazzaObjectiveUpperBound的初始证明使用微积分从另一个辅助量Φ(k, q) = √(k -1)q+√2k -q的极大值中获得某个有用的上界，通过其在q中的导数计算。然而，后来它用使用nlinarith战术的更直接证明替换了这个基于微积分的证明。

另一个例子是它出人意料地使用了filter_upwards战术。这个战术通常用于操作过滤器，通常在本科数学课程中不会出现，但用于Mathlib中极限的底层定义。Aristotle使用这个战术来证明上述量f(k)接近1/√2。这可以用其他方式完成，但使用这种过滤器操作说明了Aristotle部署广泛技术的能力，包括相对晦涩的技术。

4.2 其他数学成果

除了IMO表现，Aristotle已经在一些不那么人为的数学环境中展示了其实用性。在训练期间，Aristotle证明了Mathlib中缺失的几个重要定理，包括Niven定理、Gauss-Lucas定理、特征值是特征多项式的根的事实以及其他技术引理。

Aristotle还解决了涉及竞赛或本科水平以外的数学问题。作为说明，我们在附录C中包含了它证明涉及同调代数和Eisenstein级数的基本陈述的两个实例。这些预示着我们正在构建到Aristotle未来版本中的更广泛的数学能力，因为我们正在将其开发成一个工作的数学研究助手。

Aristotle还能够为Mathlib以外的其他存储库做出贡献。Aristotle为多项式Freiman-Ruzsa形式化项目贡献了两个引理。它还为由Terence Tao编写的基于Lean的真实分析教科书的重要部分进行了验证。在处理书中的几章后，Aristotle发现了四个按书面形式错误的练习，提供了明确的例子。Aristotle能够证明它被呈现的所有其他练习，并且对于其中两个，注意到给学生的一个假设对于完成证明是不必要的。

5. 系统创新与未来方向

5.1 技术整合创新

Aristotle系统最显著的创新在于它将三种不同的数学推理方法整合到一个统一的框架中：

形式化验证的严谨性：通过Lean 4和Mathlib确保每个证明的绝对正确性
非正式推理的灵活性：利用自然语言处理和生成能力模拟人类数学家的直觉
几何专用求解器：针对几何问题优化的高性能引擎

这种整合不是简单的拼接，而是通过强化学习实现了各组件之间的协同优化，使得整个系统的能力大于各部分之和。

5.2 测试时训练(Test-Time Training)

Aristotle在部署时还使用了一种测试时训练(TTT)形式，使其能够在推理时从自己的经验中学习。这包括迭代应用以下交替步骤：

多次尝试解决主要问题，以及由第2.2节描述的外部推理循环生成的许多引理
如果主要问题仍未解决，根据这些尝试提取的搜索轨迹重新训练模型

在IMO之前和期间观察到，TTT提高了Aristotle在给定问题上的尝试效率和专门化。在IMO之前，我们发现使用TTT允许Aristotle解决我们的基础模型在相同搜索预算下未解决的困难问题。TTT还与Aristotle的引理生成管道特别建设性地交互，允许来自不同证明草图的引理之间的交叉授粉，并加速了Aristotle在我们IMO评估期间处理引理的速率。

在另一个方向上，TTT有助于处理新的Lean抽象(或Mathlib中较少见的抽象)，这些抽象只有基本API。证明涉及这些的陈述需要从基本命令的复杂链中合成高级构造。TTT在允许模型从以这种方式链接基本命令的初始尝试中学习是非常宝贵的，有效地使其在以后的尝试中访问更强大的API。