诸如Lean31之类的通用形式语言仍然需要大量基础工作来描述目前大多数IMO几何问题。我们不直接应对这一挑战，因为它需要深入的专业知识和大量研究，而在定理方法的范围之外。为了避开这一障碍，我们采用了GEX10，JGEX17，MMP/Geometer13和Geologic19中使用的更专业的语言，这是一种旨在提供逻辑和图形图形环境的合成几何定理的工作线，并具有类似人类的非学分和拓扑假设。该语言的示例如图1d，f。由于其狭窄的配方，所有IMO几何问题中有75％可以适应此表示。在这种类型的几何环境中，每个证明步骤在逻辑和数字上都经过验证，也可以由人类读者评估，就好像是由IMO参赛者编写的，这要归功于该语言的高度自然语法。为了涵盖更具表现力的代数和算术推理，我们还将整数，分数和几何常数添加到该语言的词汇中。我们不会进一步寻求完整的几何形状表示，因为它是一个独立且极具挑战性的研究主题，要求从数学形式化社区进行大量投资。

　　我们开发了一种建设性图的构建器语言，类似于JGEX17一次在前提中构造一个对象的构建语言，而不是自由地对许多涉及几个对象的前提进行采样，因此避免产生一组自相矛盾的前提。在扩展数据表1中显示了详尽的施工动作列表。这些动作包括以某种方式创建与他人相关的新点的构造，即，界线，incentre/cententre/excentre等，以及将数字作为其参数的构造，例如，“构造点x构造点X构造X构造，因此给定数字α，ABX =α”。可以通过更复杂的动作扩展此列表，以描述更具表现力的几何场景集，从而改善了合成数据多样性和测试集覆盖范围。参考文献中可以找到更通用和表达的构建器语言。32。我们利用一种更简单的语言，足以描述IMO-AG-30中的问题，并且可以很好地与符号发动机DD一起使用。

　　引擎的核心功能是在定理前提下推导新的真实语句。可以通过几何规则（例如X then Y”等几何规则进行扣除，其中X和Y是几何语句，例如“ A，B，C为colinear”。我们为此目的使用结构化DD10,17的方法，因为它可以在标准的非加速器硬件上仅几秒钟内找到扣除额。为了进一步增强演绎，我们还内置了通过AR执行推论的能力。AR启用执行角度/比率/距离追逐的证明步骤。在扩展数据表2中显示了AR的详细示例。这些证明步骤在几何证明中无处不在，但几何规则却没有涵盖。我们扩展了地质19中实施的高斯消除过程，以在短短几秒钟内为所有可能的线性操作员找到扣除额。我们的符号扣除引擎是DD和AR的复杂整合，我们将其另一种应用来扩展已知真实陈述的关节关闭，直到扩展停止。这个过程通常在几秒钟内完成，最多可以在标准的非加速器硬件上完成几分钟。

　　在几何定理的文献中，尚未完全治疗代数扣除。例如，在Igeotutor12中，Z3（参考文献33）用于处理算术推断，但未涵盖代数操作。DD（参考文献17）通过根据一些有限的推论规则表达代数扣除来处理代数扣除，因此，它无法表达更复杂的操作，而算术算术推断未涵盖。到目前为止，最通用的治疗方法是参考文献中的一个过程。34对于仅角度定理发现，并在地质19中实现了角度和比率。我们扩展了这种表述，以涵盖有关点，比率和距离之间的所有推理以及与“ PI”或“ 1：2”等几何常数的算术推理。代数推理的具体示例在扩展数据表2中给出。

　　在高水平上，我们首先将输入线性方程式转换为其系数的矩阵。特别是，我们创建了一个系数矩阵A rm×n，其中n是变量的数量，m是输入方程的数量。在几何形状中，任何平等的形式均为a-b = c-d a-b - c+d = 0。类似地，比率AB：CD = EF：GH表示为log（ab） - log（cd）= log（ef） - log（gh），其中log（ab）是段AB长度的日志。对于距离，每个变量是一个（点，线）对，代表特定线上的特定点。

　　因为所有平等性均为“ A -B -C +D = 0”的形式，所以我们在每个平等的行中填充了+1，-1，-1，-1，1，+1的列，列的列，与变量A，B，C和D相对应。在A上运行高斯消除将返回一个新矩阵，每列在每个列上具有领先的1s，从本质上代表每个变量是所有其余变量的唯一线性组合。例如，假设我们将“ a -b = b - c”，“ d -c = a -d”和“ b - c = c = c - e”为输入平等，运行高斯消除过程（以下等式表示为ge）将返回以下结果：

　　从这个结果，我们可以通过检查x1 = x2或x1- x2 = x2 = x2 - x3或x1- x2 = x3 - x4来确定性和详尽地推断出所有新的平等性，其中{x1，x2，x3，x4}是所有变量的任何4个permoten。例如，在上面的高斯消除中，AR从三个输入相等性中推论出B = D。为了处理“ 0.5 pi”或“ 5:12”之类的几何常数，我们将“ pi”和“ 1”作为所有系数矩阵中的默认变量。

　　与DD的原始实现不同，我们使用图形数据结构来捕获几何形状的对称性，而不是使用规范形式的字符串。使用图数据结构，我们不仅捕获了函数参数的对称排列，还捕获了平等，共线性和相关性的传递性。该图数据结构将其烘烤到本身中，在DD中使用的几何规则列表中明确说明了一些扣除规则。因此，原始列表中的这些扣除规则在探索中没有使用，而是在探索中的任何地方使用，而当将最终证明序列化为文本时，请隐式使用和明确列出。

　　每个扣除步骤都需要与追溯算法相结合，该算法返回最小的直接祖先语句集，以推断该步骤的结论说明所必需的。这是提取正文中描述的证明图和最小场所的核心构建块。为了避免多余的辅助结构，必须通过不必要的传递性来促进证明的多余辅助构建算法，这是必要的最小挑选算法。例如，如果可以通过其他推理链直接获得“ a = c”，则“ a = b”和“ b = c”可能无需。

　　为此，我们记录了相等性传递性图。例如，如果推断出“ a = b”，“ b = c”，“ c = d”和“ a = d”，则会导致nodes a，b，c和d连接到相同的“ equality node” e，我们在e中维护一个e边缘的图[（a，b），（b），（b），（b，c），（c，d），（a，d），（a，d），（a，d）。这允许追溯算法执行广度优先搜索，以找到A，B，C和D之间任何一对变量之间的最短相等性的最短路径。但是，对于共线性和依赖性，表示形式更为复杂。在这些情况下，使用3个边缘或4个边缘的超图G（V，E）用作等值透射率图。现在，追溯等同于为节点的目标集（三个collinear节点或四个concyclic节点）找到最小跨越树（以下等式表示MST），其重量是其Hyperedges E''：：

　　这样的优化是NP-固定的，因为它是从顶点盖的决策版本减少的。在这种情况下，我们只需使用一种贪婪的算法即可找到最佳的最小生成树。

　　可以通过认识到它等同于混合整数线性编程问题来完成通过高斯消除的追溯。鉴于输入方程的系数矩阵A如前所述构造的A构造和具有系数矢量b rn的目标方程式，我们通过定义非阴性整数X，Y ZM来确定B的最小固体集合，并溶解以下以下混合智能线性编程问题：

　　B代表的平等的最小直接父节点将是ITH方程（A）中的ITH方程（ITH行），其相应的决策值（Xi-Yi）为非零。

　　DD和AR交替使用以扩大其关节扣除额。DD的输出由推论规则推论的新声明组成，反之亦然。例如，如果DD推导的“ AB平行于CD平行”，则将在“代数推理”部分中定义的AR系数矩阵A中更新线AB和CD的斜率为相等的变量。也就是说，将在与斜率（CD）列的变量斜率（AB）和“ -1”相对应的列中添加一个新行。高斯淘汰和混合企业线性编程会在AR执行时再次运行，从而产生新的平等性，作为DD的下一个迭代的输入。该循环重复，直到关节扣除闭合停止扩展。DD和AR都是仅取决于定理前提的确定性过程，因此它们在实施中不需要任何设计选择。

　　尽管任何节点的直接祖先集合很小，但这并不能保证完全跟踪的背部依赖项G（n）和必要的前提P是最小的。在这里，我们将最小化定义为g（n）和p不能在不失去结论达到的情况下进一步修剪的属性。没有最小的情况，我们获得了许多综合证明，它具有空置的辅助结构，与实际证明具有较浅的关系，并且可以完全丢弃。为了解决这个问题，我们执行详尽的反复试验，丢弃辅助点的每个子集，并在较小的房屋子集上重新启动DD+AR，以验证目标达到的性能。最后，我们返回所有试验中可获得的最低证明。在综合数据生成和测试期间每次成功的证明搜索之后，都会完成此证明程序。

　　我们在大量平行的CPU工人上运行合成数据生成过程，每个工人都用不同的随机种子播种以减少重复。在对100,000名CPU工人进行72小时的过程中运行此过程后，我们获得了大约5亿个合成证明示例。我们将证明声明重新格式化为其规范形式（例如，在同一证明步骤等内对单个术语进行排序等，以避免对自身和测试集的浅删除术语进行排序。最后，我们获得了1亿个独特的定理实例。共有900万个例子涉及至少一个辅助建筑。我们在合成数据中没有发现IMO-AG-30问题。在JGEX17中收集的一系列几何问题上，该问题主要由中等难度和知名定理的问题组成，我们在合成数据中发现了近20个问题。这表明训练数据涵盖了几何学中的相当数量的知识，但是更复杂的定理空间仍然更大。

　　我们使用Meliad Library35进行及其基础设置的变压器培训。变压器具有12层，嵌入1,024的尺寸，8个注意力头和一个尺寸4,096的注意力间密度层，并具有relu激活。总体而言，变压器具有1.51亿个参数，不包括其输入和输出头的嵌入层。我们自定义的令牌仪使用sentepiece36训练了“单词”模式，并且词汇尺寸为757。我们将最大上下文长度限制在1,024个令牌上，并使用T5风格的相对位置Embedding37。还使用了序列包装38,39，因为我们90％以上的序列长度低于200。在培训期间，辍学率为5％的掉落率为5％。将4×4片TPUV3（参考文献41）用作其硬件加速器。对于训练，我们以每核的批量大小为16，余弦学习率的时间表从10,000,000步中衰减到0.01降低到0.001。为了进行微调，我们将最终学习率保持在另外1,000,000个步骤中的0.001。对于没有预处理的设置，我们以1,000,000步的速度将学习率从0.01降低到0.001。我们没有执行任何超参数调整。这些高参数值要么选择为一个大的圆数（训练步骤），要么是Meliad Codebase中默认提供的。

　　由于语言模型解码过程返回K不同的序列描述K替代辅助结构，因此我们使用每个梁的分数作为其值函数，对这些K选项进行梁搜索。该设置在横梁之间高度可行，可以在有平行的计算资源时进行大幅加速。在我们的实验中，我们使用k = 512的光束尺寸，最大迭代次数为16，每个节点的分支因子（即解码批次尺寸）为32。这是我们变压器大小的GPU V100的最大推理时间批次大小。扩展这些因素以检查较大的搜索空间可能会进一步改善字母计量结果。

　　对于每个问题，我们使用了四个GPU工人的池，每个工人托管了变压器语言模型的副本，以在替代梁之间进行工作，而将10,000名CPU工人组成的池来托管符号求解器，在所有30个问题上共享了所有梁。这样，早期终止的问题可以贡献其计算能力的份额。我们将符号求解器的运行时间记录在每个问题上，通过设计，这些问题在所有光束上都大致恒定。我们使用此问题和语言模型解码速度来推断每个问题所需的必要的并行性，以隔离，以在图1的扩展数据中保持在IMO的不同时间限制。

　　我们对原始培训数据的较小分数（20％，40％，60％和80％）进行了训练，并发现，即使在20％的训练数据中，载载计仍然解决了21个问题，比最强的基线（DD+AR+人为启发术）还要解决了18个问题，如有18个问题解决了，如图6a所示。为了研究光束搜索对语言模型的影响，我们在证明搜索过程中分别降低了梁的大小和搜索深度，并报告了扩展数据中的结果图6C，d。我们发现，梁尺寸为8，即，从原始梁的大小为512的64倍，字母度计算仍可以解决21个问题。可以通过将搜索深度从16减少到两个，同时将光束尺寸恒定保持在512，从而获得了21个问题的类似结果。

　　我们在参考文献中策划的231个几何问题的较大测试集上评估了耗载法和其他基准。17。该场景涵盖了IMO竞赛以外的广泛来源：教科书的例子和练习，区域奥林匹克运动会和著名的几何定理；有些甚至比典型的IMO问题更复杂，例如五个圆形定理，莫利的定理或萨瓦亚玛和thébault的定理。结果在扩展数据中报告了图6b。不同方法的总排名与表1中的总排名保持不变，并且字母度计解决了几乎所有问题（98.7％）。最强的基线DD+AR+人为设计的启发式方法解决了92.2％，而先前的最新状态解决了75％。

　　载语计量学的强度神经符号设置在于其产生辅助构建体的能力，这是许多数学领域的重要成分。在扩展数据表3中，我们在其他四个数学域中给出了示例，其中提出辅助构造是解决方案的关键。在扩展数据表4中，我们对IMO 1964问题2的几何形状证明和不平等证明进行了逐行比较，突出了它们如何适合同一框架。

　　我们的论文表明，语言模型可以学会从合成数据中提出辅助构造，其中问题陈述和辅助构建物是随机生成的，然后使用Trackback算法分离以识别依赖关系差异。具体而言，字母测定框架需要以下成分：

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

　　自动定理的研究证明，历史悠久的历史可以追溯到1950年代（参考文献6,42,43），从而产生了高度优化的一阶逻辑求解器，例如E（参考文献44）或Vampire45。在2010年代，深度学习成为一种新的强大工具，用于自动定理，证明了前提选择和证明指南的成功46,47,47,48,49以及SAT解决方案50。另一方面，Transformer18在各种任务中具有出色的推理能力51,52,53。将变压器语言模型应用于定理的第一个成功是GPT-F（参考文献15）。它的后续扩展2,16进一步发展了这个方向，使机器可以首次解决一些奥林匹克级问题。证明搜索算法和在线培训中的创新3还改善了基于变压器的方法，解决了代数和数字理论中总共十个（适应）IMO问题。但是，这些进步是基于大量的人类证明实例和独立的问题陈述，并由人类设计和策划。

　　几何定理证明在一个完全独立的空间中演变。它的文献分为两个分支，一种计算机代数方法和一种搜索方法。自从引入WU的Method21以来，前者可以在很大程度上被考虑，从理论上讲，这可以从较早的作品中引入的专门代数工具基础上决定任何平等类型的几何陈述的真实价值54,55。即使计算机代数具有强大的理论保证，但由于其庞大的时间和空间复杂性，其实践中的性能可能会受到限制56。此外，计算机代数的方法不引起AI研究的兴趣，AI研究试图使用搜索方法证明定理，这是一种更类似人类的通用过程。

　　搜索方法也早在1950年代就开始了（参考文献6,7），并在整个20世纪57,57,58,59,60中继续发展。随着DD10,17的引入，区域方法61和全角方法30，几何求解器比Tarski或Hilbert的公理使用更高的扣除规则，并且能够证明比用正式语言运作的定理更为复杂。然而，今天证明的几何定理仍依赖于人为设计的辅助构造的启发式方法10,11,12,13,14。几何定理证明了机器学习最近取得的进步，因为它在诸如Lean31或Isabelle62之类的形式数学库中的存在非常有限。

　　长期以来，综合数据已被识别并用作定理中的重要成分，证明为63,64,65,66。最先进的机器学习方法利用专家迭代来生成合成证明的课程2,3,15。但是，他们的方法仅对人类设计和选择的一组固定的预定义问题产生合成证明。另一方面，我们的方法完全从头开始产生合成问题和证明。Aygun等人67类似地生成了带有事后经验重播的合成证明68，提供了与我们的工作相似的学习的平滑定理困难范围。但是，载流量法没有受到人类策划的现有猜想的训练，也没有从目标定理的证明尝试中学习。因此，它们的方法是正交的，可用于进一步改善字母计。与我们的工作最相似的是Firoiu等人。69，其方法使用远期建议者通过深度优先探索来生成合成数据，并纯粹基于这些综合数据训练神经网络。另一方面，我们的工作使用广度优先的探索，对于获得最小的证明和前提，并使用追溯算法来识别辅助结构，从而引入了远期提议者无法提出的新符号和假设。