无需人工演示的奥林匹克几何求解

AlphaGeometry原链接

Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He & Thang Luong

自然杂志 625卷，476–482页 (2024年)

摘要

在奥林匹克级别上证明数学定理代表了人类级自动推理的一个显著里程碑，因其被世界上最优秀的中学生数学人才公认为具有难度。然而，目前的机器学习方法在大多数数学领域中不适用，因为将人类证明转化为机器可验证格式的成本很高。对于几何学来说，这个问题尤为严重，因为其独特的翻译挑战导致训练数据严重稀缺。我们提出了AlphaGeometry，一种欧几里得平面几何定理证明器，通过在不同复杂度级别上合成数百万个定理和证明，绕过了对人工演示的需求。AlphaGeometry是一个神经符号系统，使用从头开始在我们大规模合成数据上训练的神经语言模型，通过挑战性问题中的无限分支点来引导符号推理引擎。在30个最新的奥林匹克级别问题的测试集中，AlphaGeometry解决了其中的25个问题，优于之前只解决10个问题的最佳方法，并接近平均国际数学奥林匹克（IMO）金牌得主的表现。值得注意的是，AlphaGeometry生成了可读的证明，在人类专家评估下解决了IMO 2000和2015年的所有几何问题，并发现了2004年翻译的IMO定理的广义版本。

主体部分

证明定理展示了对逻辑推理的掌握和在无限大的动作空间中朝着目标进行搜索的能力，标志着一种非凡的解决问题的技能。自1950年代以来，更好的定理证明能力的追求一直是人工智能（AI）研究的一个恒定焦点。数学奥林匹克是世界上最著名的定理证明比赛，拥有与1959年开始的悠久历史相似的历史，在识别解决问题的杰出人才方面发挥了重要作用。在奥林匹克级别上与顶尖人类表现相匹敌已成为AI研究的一个显著里程碑。

对于基于学习的方法来说，定理证明是困难的，因为将人类证明翻译成机器可验证语言的训练数据在大多数数学领域中都很稀缺。几何学在奥林匹克领域中尤为突出，因为它在通用数学语言（如Lean）中几乎没有证明例子，这归因于几何学独特的翻译困难。另一方面，几何特定语言定义狭窄，无法表达使用几何范围之外工具（如复数）的人类证明。总体而言，这造成了数据瓶颈，使几何学在最近使用人类演示的方法中落后。因此，目前的几何学方法仍主要依赖于符号方法和人工设计的硬编码搜索启发式算法。

我们提出了一种使用合成数据的替代定理证明方法，从而绕过了对人工提供的证明示例的翻译需求。我们专注于欧几里得平面几何，排除几何不等式和组合几何等主题。通过在多样化的随机定理前提上使用现有符号引擎，我们提取了1亿个合成定理及其证明，其中许多证明步骤超过200步，是奥林匹克定理平均证明长度的四倍。我们进一步定义并使用合成证明生成中的依赖差异概念，使我们的方法能够生成近1000万个合成证明步骤，这些步骤构造了辅助点，超出了纯符号推理的范围。辅助构造是几何学中的外生项生成实例，代表定理证明的无限分支因子，在其他数学领域中被广泛认为是证明许多难定理的关键挑战。我们的工作因此展示了生成合成数据并学习解决这一关键挑战的成功案例。通过这个解决方案，我们提出了一个通用的指导框架，并在“AlphaGeometry框架及其在其他领域的适用性”部分讨论其在其他领域的适用性。

我们在所有生成的合成数据上预训练一个语言模型，并对其进行微调，以在证明搜索过程中专注于辅助构造，将所有推理证明步骤委托给专门的符号引擎。这遵循了文献中的标准设置，其中像GPT-f这样的语言模型在被训练在人类证明示例上后，可以生成外生证明项作为输入，供快速且准确的符号引擎使用，如nlinarith或ring，结合了两者的最佳优势。我们的几何定理证明器AlphaGeometry，见图1，生成了可读的证明，显著优于之前的最先进几何定理证明计算机程序，并在一组30个经典几何问题的测试集上接近平均IMO金牌得主的表现，这些问题是从IMO中翻译而来的，如图2所示。

我们的方法生成合成数据的过程如图3所示。我们首先抽取一组随机的定理前提，作为符号推理引擎的输入以生成其推论。我们在工作中抽取了近10亿个这样的前提，在方法部分描述了高度并行化的设置。请注意，我们没有使用任何来自人工设计问题集的现有定理前提，并均匀随机抽取符合条件的构造。

接下来，我们在抽取的前提上使用符号推理引擎。引擎通过遵循前向推理规则快速推导出新的真实陈述，如图3b所示。这返回了一个所有可达结论的有向无环图。通过跟踪算法，我们对每个节点进行追溯以找到其最小必要前提和依赖推论。举例来说，对于最右边的某个图节点，追溯返回绿色子图。最小前提和相应的子图构成一个合成问题及其解决方案。在下面的示例中，点E和D参与了证明，尽管与HA和BC的构造无关，因此它们被语言模型学习为辅助构造。

在几何学中，符号推理引擎是推论数据库，能够通过几何规则有效地从前提推导出新陈述。DD遵循形式为确定性Horn子句的推论规则，即

Q(x) \leftarrow P1(x),…,Pk(x)

，其中x是点对象，P1,…,Pk和Q是谓词，如“相等线段”或“共线”。推论规则的完整列表见参考文献10。为了扩大生成的合成定理和证明的范围，我们还在符号引擎中引入了另一个组件，可以通过代数规则推导新陈述。在许多奥林匹克级别的证明中，经常需要角度、比例和距离追踪。我们在扩展数据表2中包含了AR的具体示例。DD+AR的组合，包括其前向推论和追溯算法，是我们工作中的新贡献，并代表了几何推理中的新状态。

超越符号推理生成证明

到目前为止，生成的证明仅由高效的符号推理引擎DD+AR已经可达的推论步骤组成。然而，要解决奥林匹克级别的问题，关键缺失的是生成新的证明项。在上面的算法中，可以看到这些项形成了N独立的P子集。换句话说，这些项是结论陈述和结论对象之间的依赖差异。我们将这一差异从P移至证明，使生成模型学习生成证明并学会构建它们，如图3c所示。这些证明步骤执行符号推理引擎无法完成的辅助构造。在一般定理证明背景下，辅助构造是外生项生成的一个实例，是所有证明搜索算法的一个显著挑战，因为它为搜索树引入了无限分支点。几何定理证明中，辅助构造自1959年该领域诞生以来一直是研究的重点。生成它们的方法基于手工制作的模板和领域特定的启发式方法，受限于一组可通过硬编码规则表达的人类经验子集。另一方面，任何在我们合成数据上训练的神经求解器都能从头学习执行辅助构造而无需人工演示。

在合成数据上训练语言模型

transformer语言模型是一种强大的深度神经网络，通过下一个令牌预测学习生成文本序列，推动了生成性AI技术的重大进展。我们将(P, N, G(N))序列化为具有“”结构的文本

字符串。通过训练这样的符号序列，语言模型有效地学习生成证明，以定理前提和结论为条件。

结合语言建模和符号引擎

在高层次上，证明搜索是一个循环，其中语言模型和符号推理引擎轮流运行，如图1b,c所示。证明搜索在找到定理结论或循环达到最大迭代次数时终止。语言模型用问题陈述字符串作为种子，每次生成一个额外的句子，以问题陈述和过去的构造为条件，描述一个新的辅助构造，如“构造点X，使得ABCX为平行四边形”。每次语言模型生成一个这样的构造，符号引擎将获得新的输入，因此其推论闭包会扩展，可能达到结论。我们使用束搜索探索语言模型生成的前k个构造，并在方法中描述了这一证明搜索算法的并行化。

经验评估

几何学的奥林匹克级基准

现有的奥林匹克数学基准不涵盖几何学，因为其专注于通用数学语言的形式化，几何表示提出了巨大挑战。解决这些挑战需要深厚的专业知识和大量研究投资，超出了我们工作范围，我们专注于一种定理证明方法。为此，我们将自2000年以来的IMO竞赛几何问题改编为用于交互图形证明助手的经典几何环境中使用的更狭窄、更专业的环境，如方法中所述。在所有非组合几何相关问题中，75%可以表示，形成了30个经典几何问题的测试集。几何不等式和组合几何等问题无法翻译，因为其表述与经典几何显著不同。我们在补充信息中包括了所有30个问题的陈述和翻译。最终测试集名为IMO-AG-30，突出了其来源、翻译方法和当前规模。

几何定理证明基准

文献中的几何定理证明分为两类。第一类是计算机代数方法，将几何陈述视为其点坐标的多项式方程。通过大型多项式的专用变换来证明。Gröbner基和吴方法是这一类方法的代表，理论上可以成功决定IMO-AG-30中所有几何定理的真值，尽管没有可读的证明。因为这些方法在处理IMO大小问题时通常具有很大的时间和内存复杂性，我们通过分配成功来报告其结果，前提是任何现有实现能够在48小时内解决问题。

AlphaGeometry属于第二类求解器，通常被描述为搜索/公理方法，有时称为“合成”方法。这些方法将定理证明问题视为使用几何公理的逐步搜索问题。由于这一点，它们通常返回高度可解释的证明，易于人类读者理解。这一类别中的基准通常包括配备人工设计启发式的符号引擎。例如，Chou等人提供了18个启发式，如“如果OA \perp OB且OA = OB，则在OA的对射线上构造点C，使得OC = OA”，此外还有75个符号引擎的推论规则。大语言模型如GPT-4可以认为属于这一类别。大语言模型在各种推理任务中展示了非凡的推理能力。然而，当在IMO-AG-30上生成完整的自然语言证明时，GPT-4的成功率为0%，其输出中常出现句法和语义错误，几乎没有几何知识和问题陈述本身的理解。请注意，GPT-4在IMO问题上的表现可能会被其训练数据中的公共解决方案所污染。因此，更好的GPT-4表现仍无法与其他求解器相比。总体而言，搜索方法在其证明性能上没有理论保证，已知其比计算机代数方法弱。

合成数据生成重新发现已知定理及更多

我们发现我们的合成数据生成可以重新发现几何文献中一些相当复杂的定理和引理，如图4所示，尽管从随机抽取的定理前提开始。这可以归因于扩展数据表1中描述的复合动作的使用，如“取重心”或“取外心”，在我们描述的方法部分的大规模探索设置中，通过随机抽取的方式形成了一组已知定理前提的超集。为了研究合成证明的复杂性，图4显示了合成证明长度的直方图与奥林匹克问题测试集中证明长度的对比。尽管合成证明长度偏向较短的证明，但其中一小部分的长度仍比IMO测试集中最难的问题长30%。我们发现，通过这个过程发现的合成定理不受人类审美偏见（如对称）的限制，因此涵盖了欧几里得几何已知场景的更广泛集合。我们按照方法中描述的进行重复数据删除，得到了超过1亿个独特的定理和证明，没有发现任何IMO-AG-30定理，表明可能的几何定理空间仍比我们发现的集合要大得多。

我们首先在所有1亿个合成生成的证明上预训练语言模型，包括纯符号推理的证明。然后我们在需要辅助构造的证明子集（约占预训练数据总量的9%，即900万证明）上对语言模型进行微调，以便在证明搜索过程中更好地专注于其分配的任务。

在IMO-AG-30上的证明结果

我们在IMO-AG-30基准上报告了十种不同求解器的性能，其中包括八种基于搜索的方法。除了提示GPT-4生成完整的自然语言证明并进行多轮反思和修订外，我们还结合GPT-4与DD+AR作为另一个基准，以提高其推理准确性。为此，我们在提示中使用详细指示和少量示例，帮助GPT-4成功与DD+AR接口，以正确的语法提供辅助构造。补充信息中包括了涉及GPT-4基准的提示细节。

AlphaGeometry取得了最佳结果，共解决了25个问题。之前的最先进方法（吴方法）解决了十个问题，而最强的基准（DD+AR+人工设计的启发式）解决了18个问题，利用了本文开发的代数推理引擎和Chou等人设计的人工启发式。为了匹配AlphaGeometry的测试时间计算，该最强基准使用了250个并行工作者，每个工作者运行1.5小时，尝试不同集合的人工启发式建议的辅助构造，直到成功或超时。其他基准如吴方法或全角法不受并行计算资源的影响，因为它们执行固定的逐步算法直到终止。

通过测量在基础符号推理引擎（DD）上的改进，我们发现结合代数推理增加了七个解决问题的总数（DD+AR），而语言模型的辅助构造显著增加了另外11个解决问题，最终总数为25个。如扩展数据图6所示，我们发现使用仅20%的训练数据，AlphaGeometry仍然实现了最先进的结果，解决了21个问题。同样，在测试时间使用不到2%的搜索预算（束大小为8，而不是512），AlphaGeometry仍能解决21个问题。在一个更大且更多样化的231个几何问题的测试集中，包括教科书练习、地区奥林匹克和著名定理，我们发现表1中的基准仍保持相同的性能排名，AlphaGeometry几乎解决了所有问题（98.7%），而吴方法解决了75%，DD+AR+人工设计的启发式解决了92.2%。

值得注意的是，AlphaGeometry解决了2000年和2015年同年的两个几何问题，这是IMO中被广泛认为对普通参赛者来说是困难的门槛。此外，AlphaGeometry的追溯过程在翻译的IMO 2004 P1中发现了一个未使用的前提，如图5所示，从而发现了翻译的IMO定理本身的更广泛版本。我们在补充信息中包括了IMO-AG-30中所有问题的AlphaGeometry解决方案，并在扩展数据图2–5中手动分析了一些显著的AlphaGeometry解决方案和失败情况。总体而言，我们发现AlphaGeometry使用的证明工具远低于人类，限制了合成数据的覆盖范围、测试时间性能和证明可读性。

AlphaGeometry发现了翻译的IMO 2004 P1的更广泛定理。

因为AlphaGeometry输出高度可解释的证明，我们使用一个简单模板自动将其解决方案翻译成自然语言。为了获得2000年和2015年两年的专家评估，在这两年中AlphaGeometry解决了所有几何问题，并可能通过了奖牌门槛，我们将这些解决方案提交给了美国IMO队教练，他在数学奥林匹克评分方面经验丰富，并撰写了奥林匹克几何培训书籍。AlphaGeometry解决方案被建议

获得满分，从而通过了对应年份的14/42奖牌门槛。我们注意到，IMO测试还评估了几何之外的其他三个数学领域，并在没有计算器使用或4.5小时时间限制等人类中心限制下评估人类。我们在方法中研究了AlphaGeometry的4.5小时和1.5小时时间限制设置，并在扩展数据图1中报告了结果。

学习预测符号引擎输出提高了语言模型的辅助构造

原则上，辅助构造策略必须依赖于推理搜索过程中与之协作的特定推理引擎的细节。我们发现，一个没有预训练的语言模型只解决了21个问题。这表明在纯符号推理证明上进行预训练提高了辅助构造的成功率。另一方面，一个没有微调的语言模型也会降低性能，但没有那么严重，解决了23个问题，而AlphaGeometry的完整设置解决了25个问题。

困难问题反映在AlphaGeometry证明长度中

图6通过人类参赛者在IMO上的公开分数衡量解决问题的难度，并将其与相应的AlphaGeometry证明长度进行对比。结果显示，对于得分最低的三个问题，AlphaGeometry也需要异常长的证明和语言模型构造的帮助来解决问题。然而，对于较容易的问题（平均人类得分>3.5），我们观察到平均人类得分与AlphaGeometry证明长度之间没有相关性（p=-0.06）。

结论

AlphaGeometry是第一个在证明欧几里得平面几何定理方面超过平均IMO参赛者表现的计算机程序，优于强大的计算机代数和搜索基准。值得注意的是，通过AlphaGeometry，我们展示了一种通过大规模探索从头开始进行定理证明的神经符号方法，绕过了对人工注释的证明示例和人工策划的问题陈述的需求。我们生成和训练语言模型在纯粹合成数据上的方法为面临同样数据稀缺问题的数学领域提供了一个通用的指导框架。

方法

几何表示

通用形式化语言（如Lean）仍需要大量基础工作来描述目前的大多数IMO几何问题。我们没有直接解决这一挑战，因为它需要深厚的专业知识和大量研究投资，超出了定理证明方法的范围。为了绕过这一障碍，我们采用了更专业的语言，用于GEX、JGEX、MMP/Geometer和GeoLogic的工作，旨在为合成几何定理提供一个具有类人非退化性和拓扑假设的逻辑和图形环境。图1d,f中展示了这种语言的示例。由于其狭窄的表述，75%的IMO几何问题可以适应这种表示。在这种几何环境中，每个证明步骤都经过逻辑和数值验证，并且可以由人类读者评估，仿佛是IMO参赛者编写的，因为语言的语法非常自然。为了涵盖更具表达力的代数和算术推理，我们还将整数、分数和几何常数添加到这种语言的词汇中。我们不进一步推动几何表示的完整解决方案，因为这是一个独立且极具挑战性的研究课题，要求数学形式化社区投入大量投资。

一致定理前提的抽样

我们开发了一种类似于JGEX使用的构造图形生成器语言，通过每次构造前提中的一个对象，避免生成自相矛盾的前提集合。扩展数据表1中显示了构造动作的完整列表。这些动作包括构造与其他对象相关的新点，如共线、内心/外心等，以及以一个数为参数的构造，例如“构造点X，使得给定一个数α，∠ABX=α”。可以通过扩展该列表以更复杂的动作来描述更具表达力的几何场景，提高合成数据的多样性和测试集的覆盖率。一个更通用和表达力更强的图形生成器语言见参考文献32。我们使用了一个更简单的语言，足以描述IMO-AG-30中的问题，并能与符号引擎DD良好协作。

符号推理引擎

引擎的核心功能是给定定理前提推导新的真实陈述。可以通过几何规则进行推导，如“如果X则Y”，其中X和Y是几何陈述的集合，如“共线的A、B、C”。我们使用结构化DD的方法，因为它可以在标准非加速硬件上在几秒钟内找到推理闭包。为了进一步增强推理，我们还在AlphaGeometry中构建了通过AR进行推理的能力。AR使证明步骤能够进行角度/比例/距离追踪。扩展数据表2中显示了AR的具体示例。这样的证明步骤在几何证明中无处不在，但不被几何规则涵盖。我们扩展了GeoLogic中实现的高斯消元过程，以在几秒钟内找到所有可能的线性运算符的推理闭包。我们的符号推理引擎是DD和AR的复杂整合，我们交替应用它们以扩展已知真实陈述的联合闭包，直到扩展停止。这一过程通常在标准非加速硬件上几秒钟到几分钟内完成。

代数推理

几何定理证明文献中尚无完整的代数推理处理。例如，iGeoTutor使用Z3处理算术推理，但不涵盖代数操作。DD通过在有限推理规则下表达它们来处理代数推理，因此无法表达更复杂的操作，留下算术推理未涵盖。迄今为止最通用的处理方法类似于用于仅角度定理发现的过程，并在GeoLogic中实现，涵盖角度和比例。我们扩展了这一表述，以涵盖所有关于角度、比例和点之间距离的推理，并包括几何常数的算术推理，如“pi”或“1:2”。扩展数据表2中给出了代数推理的具体示例。

在高层次上，我们首先将输入线性方程转化为它们系数的矩阵。特别地，我们创建一个系数矩阵A，其中N是变量的数量，M是输入方程的数量。在几何中，任何等式的形式为a−b=c−d⇔a−b−c+d=0。例如，角度等式∠ABC=∠XYZ表示为s(AB)−s(BC)=s(XY)−s(YZ)，其中s(AB)是AB和x方向之间的角度，模pi。同样，比例AB:CD=EF:GH表示为log(AB)−log(CD)=log(EF)−log(GH)，其中log(AB)是线段AB长度的对数。对于距离，每个变量是一个（点、线）对，表示特定点在特定线上。

因为所有等式的形式为“a−b−c+d=0”，我们在人行道的每行填充值+1，−1，−1，+1，在相应变量的列中填充。运行高斯消元在A上返回一个新的矩阵，在每列都有领先1，基本上表示每个变量是所有剩余变量的唯一线性组合。例如，假设我们有“a−b=b−c”，“d−c=a−d”和“b−c=c−e”作为输入等式，运行高斯消元过程（在以下等式中表示为GE）返回以下结果：

从这一结果中，我们可以确定性和穷尽地推导所有新的等式，检查x1=x2或x1−x2=x2−x3或x1−x2=x3−x4，其中{x1,x2,x3,x4}是所有变量的任意4-置换。在上面的高斯消元中，例如，AR从三个输入等式中推导出b=d。为了处理几何常数如“0.5pi”或“5:12”，我们将“pi”和“1”作为默认变量包含在所有系数矩阵中。

推理数据库实现

不同于DD的原始实现，我们使用图数据结构来捕捉几何的对称性，而不是使用规范形式的字符串。通过图数据结构，我们不仅捕捉了函数参数的对称置换，还捕捉了相等性、共线性和共圆性的传递性。这个图数据结构将一些在DD几何规则列表中显式声明的推理规则内置到自身中。因此，这些推理规则在探索中没有被任何地方使用，但在最终证明序列化为文本时隐式使用并显式拼写。

追溯找出最小证明

每个推理步骤需要与追溯算法耦合，返回推导步骤结论陈述的最小必要祖先陈述集。这是提取证明图和最小前提的核心构建块。最小

前提提取算法是必要的，以避免对通过不必要的传递性辅助构造的多余构造。例如，“a=b”和“b=c”可能是不必要的，如果“a=c”可以通过其他推理链直接获得。

几何规则推理的追溯

为此，我们记录了相等传递图。例如，如果“a=b”，“b=c”，“c=d”和“a=d”被推导，结果是节点a，b，c和d连接到同一个“相等节点”e，我们在e内维护一个图，其中有边[(a,b)，(b,c)，(c,d)，(a,d)]。这允许追溯算法执行广度优先搜索，以找到a，b，c和d之间任何变量对之间的最短路径。然而，对于共线性和共圆性，表示更复杂。在这些情况下，超图G(V,E)带有3-边或4-边用作相等传递图。追溯相当于找到目标节点集的最小生成树，权重是其超边的并集的基数：

这种优化是NP难问题，因为它是顶点覆盖决策版本的化简。我们在这种情况下简单地使用贪婪算法找到一个尽力的最小生成树。

代数推理的追溯

通过高斯消元进行追溯可以通过识别它等同于一个混合整数线性规划问题来完成。给定前几部分描述的输入方程的系数矩阵A和一个目标方程系数向量b，我们通过定义非负整数决策向量x,y并解决以下混合整数线性规划问题，确定b的最小前提集合：

最小立即父节点集将是相应决策值为非零的第i方程（A中的第i行）。

整合DD和AR

DD和AR交替应用以扩展其联合推理闭包。DD的输出由推理规则推导出的新陈述，作为AR的输入，反之亦然。例如，如果DD推导出“AB平行于CD”，AB和CD的斜率将在AR的系数矩阵A中更新为相等变量，即在斜率（AB）和斜率（CD）的列中添加一个新行，值为“1”和“-1”。AR执行时再次运行高斯消元和混合整数线性规划，生成新的等式作为下一个DD迭代的输入。这个循环重复，直到联合推理闭包停止扩展。DD和AR都是确定性过程，仅依赖于定理前提，因此它们在实现中不需要任何设计选择。

证明修剪

虽然任何节点的立即祖先集是最小的，但这并不保证完全追溯的依赖子图G(N)和必要前提P是最小的。在这里，我们定义最小性为G(N)和P无法进一步修剪而不失去结论可达性的属性。没有最小性，我们获得了许多具有空洞辅助构造的合成证明，与实际证明关系浅薄，可以完全丢弃。为了解决这个问题，我们执行穷尽试验和错误，丢弃每个辅助点的子集，并在较小的前提集上重新运行DD+AR以验证目标可达性。最终，我们返回所有试验中可获得的最小证明。这个证明修剪程序在合成数据生成期间和测试时间的每次成功证明搜索后都进行。

并行化数据生成和重复数据删除

我们在大量并行CPU工作者上运行合成数据生成过程，每个工作者使用不同的随机种子以减少重复。在100,000个CPU工作者上运行72小时后，我们获得了大约5亿个合成证明示例。我们将证明陈述重新格式化为规范形式（例如，排序单个术语的参数和同一证明步骤内的术语等），以避免与自己和测试集的浅层重复数据删除。最终，我们获得了1亿个独特的定理-证明示例。共有900万个示例涉及至少一个辅助构造。我们在合成数据中没有发现IMO-AG-30问题。在JGEX中收集的几何问题集中，主要包括中等难度的问题和著名定理，我们在合成数据中发现了近20个问题。这表明训练数据覆盖了几何学中的相当数量的常识，但更复杂定理的空间仍然大得多。

语言模型架构和训练

我们使用Meliad库进行transformer训练，采用其基本设置。transformer有12层，嵌入维度为1,024，八个注意力头和一个嵌入层后方的4,096维密集层，激活函数为ReLU。总体上，transformer有1.51亿参数，不包括输入和输出头的嵌入层。我们的定制分词器使用SentencePiece以“word”模式训练，词汇表大小为757。我们将最大上下文长度限制为1,024个标记，并使用T5样式的相对位置嵌入。由于90%以上的序列长度在200以内，我们也使用了序列打包。在训练期间，在注意力前和密集层后应用5%的dropout率。使用4×4 TPUv3作为硬件加速器。对于预训练，我们用每核心批量大小16和从0.01到0.001在10,000,000步中衰减的余弦学习率计划训练transformer。对于微调，我们保持最终学习率0.001，再训练1,000,000步。对于没有预训练的设置，我们在1,000,000步中从0.01到0.001衰减学习率。我们不进行任何超参数调整。这些超参数值要么被选择为大圆数（训练步数），要么在Meliad代码库中默认提供。

并行化证明搜索

因为语言模型解码过程返回k个不同序列描述k个替代辅助构造，我们在这些k个选项上执行束搜索，使用每个束的得分作为其价值函数。这一设置在束之间高度并行化，当有并行计算资源时允许大幅加速。在我们的实验中，我们使用束大小k=512，最大迭代次数为16，每个节点的分支因子（解码批量大小）为32。这是我们的transformer大小在GPU V100内存中适合的最大推理时间批量大小。扩展这些因子以检查更大部分搜索空间可能进一步提高AlphaGeometry结果。

对于每个问题，我们使用一个由四个GPU工作者组成的池，每个工作者托管一个transformer语言模型副本，以在替代束之间分工，并使用10,000个CPU工作者的池托管符号求解器，在所有束之间和所有30个问题之间共享。这样，一个问题早期终止可以将其计算能力贡献给较长运行的问题。我们记录了符号求解器在每个单独问题上的运行时间，这一设计使其在所有束之间大致恒定。我们使用此和语言模型解码速度推断每个问题在孤立情况下所需的并行度，以在扩展数据图1中保持在IMO的不同时间限制下。

数据和搜索的效果

我们在原始训练数据的较小部分（20%、40%、60%和80%）上训练AlphaGeometry，发现即使在20%的训练数据上，AlphaGeometry仍解决了21个问题，超过最强基准（DD+AR+人工设计启发式）解决的18个问题。如扩展数据图6所示，束大小和搜索深度的减少分别在证明搜索期间，我们报告了结果。我们发现，使用8的束大小，即从原始束大小512减少64倍，AlphaGeometry仍解决了21个问题。通过减少搜索深度从16到仅2，同时保持束大小恒定为512，我们也获得了21个问题的相似结果。

在更大测试集上的评估

我们在一个更大的231个几何问题测试集中评估了AlphaGeometry和其他基准，这个集合涵盖了IMO竞赛之外的更广泛来源：教科书示例和练习、地区奥林匹克和著名几何定理；有些甚至比典型IMO问题更复杂，如五圆定理、Morley定理或Sawayama和Thébault定理。结果在扩展数据图6中报告。不同方法的总体排名与表1相同，AlphaGeometry几乎解决了所有问题（98.7%）。最强基准DD+AR+人工设计启发式解决了92.2%，而之前的最先进方法解决了75%。

AlphaGeometry框架及其在其他领域的适用性

AlphaGeometry的神经符号设置的强项在于生成辅助构造，这在许多数学领域是解决方案的重要组成部分。扩展数据表3中，我们给出了其他四个数学领域中的示例，辅助构造是解决方案的关键。在扩展数据表4中，我们逐行比较了1964年IMO问题2的几何证明和不等式证明，强调它们如何都适应相

同的框架。

我们的论文表明，语言模型可以通过在合成数据上学习生成辅助构造，其中问题陈述和辅助构造一起随机生成，然后使用追溯算法分离，以识别依赖差异。具体而言，AlphaGeometry框架需要以下组成部分：

  1. 域对象和定义的实现。

  2. 随机前提采样器。

  3. 符号引擎，适用于实现（1）。

  4. 符号引擎的追溯程序。

使用这些四个组成部分和主文本中描述的算法，可以为任何目标域生成合成数据。如我们论文所示，在构建每个组成部分时存在非平凡的工程挑战。例如，当前的组合数学形式化非常初级，给（1）和（2）带来挑战。同样，为不同领域构建强大的符号引擎需要深厚的领域专业知识，给（3）和（4）带来挑战。我们将这一框架应用于更广范围视为未来工作，期待进一步的创新来应对这些挑战。

transformer在定理证明中的应用

自动定理证明的研究有着自1950年代以来的悠久历史，产生了高度优化的一阶逻辑求解器，如E或Vampire。在2010年代，深度学习成为自动定理证明的新强大工具，在前提选择和证明指导以及SAT求解中展示了巨大的成功。另一方面，transformer展示了在各种任务中的出色推理能力。transformer语言模型在定理证明中的首次成功应用是GPT-f。其后续扩展进一步发展了这一方向，首次允许机器解决一些奥林匹克级问题。proof-search算法和在线训练的创新也改善了transformer-based方法，解决了总计10个（适应的）IMO代数和数论问题。这些进展依赖于大量人工证明示例和由人设计和策划的独立问题陈述。

几何定理证明

几何定理证明在完全独立的空间中发展。其文献分为两个分支，一个是计算机代数方法，一个是搜索方法。前者自吴方法引入以来被广泛认为已经解决，它理论上可以决定任何几何相等类型陈述的真值，建立在早期作品引入的专用代数工具基础上。尽管计算机代数具有强大的理论保证，但其性能在实践中可能受限于大时间和空间复杂性。此外，计算机代数的方法论对AI研究不感兴趣，AI研究寻求通过搜索方法证明定理，这是一种更类人且通用的过程。

搜索方法也早在1950年代开始，并在整个二十世纪不断发展。随着DD、面积方法和全角方法的引入，几何求解器使用比塔斯基或希尔伯特公理更高级的推理规则，能够证明比在形式语言中操作的求解器更复杂的大量定理。然而，今天的几何定理证明仍依赖于人工设计的启发式辅助构造。几何定理证明在近期的机器学习进展中落后，因为其在形式数学库中的存在非常有限。

定理证明中的合成数据

合成数据长期以来被公认为定理证明中的重要成分。最先进的机器学习方法使用专家迭代生成合成证明课程。然而，他们的方法仅为预定义的固定问题生成合成证明，这些问题由人设计和选择。我们的方法从头生成合成问题和证明。Aygun等人通过类似于我们工作的后见经验重放生成合成证明，提供了一个平滑的定理难度范围以辅助学习。然而，AlphaGeometry不是在由人策划的现有猜想上训练的，也不从目标定理的证明尝试中学习。他们的方法因此是正交的，可以进一步改进AlphaGeometry。与我们工作最相似的是Firoiu等人，他们的方法使用向前提议者通过深度优先探索生成合成数据，并在这些合成数据上训练神经网络。我们的工作则使用广度优先探索，必要的获取最小证明和前提，并使用追溯算法识别辅助构造，从而引入向前提议者无法提出的新符号和假设。