MathAtlas：野外自动形式化基准测试

# 野外自动形式化基准源：https://arxiv.org/html/2605.14061 Nilay Patel†\* [email protected] &Noah Arias [email protected] &Davit Babayan [email protected] Victoria Cochran [email protected] &Timothy Libman [email protected] &Hafsah Mahmood [email protected] &Liam McCarty [email protected] &Soli Munoz [email protected] &Laurel Willey [email protected] Jeffrey Flanigan\* [email protected] 加州大学圣克鲁兹分校 \*主要作者 †通讯 ###### 摘要 当前的自动形式化基准主要集中在奥林匹克或本科数学上，而研究生和研究级别的数学仍未被充分探索。在本文中，我们介绍了**MathAtlas**，这是首个大规模研究生级别数学的“野外”自动形式化基准，包含从103本研究生数学教材中提取的约5.2万个定理、定义、练习、例题和证明。**MathAtlas**配备了包含约17.8万个关系的数学依赖图，是首个包含此类关系的自动形式化基准，有助于评估和开发依赖感知的自动形式化系统。我们的大量实验表明，**MathAtlas**质量高但极具挑战性：强基线在定理陈述上的正确率最多为9.8%，在定义上的正确率为16.7%。此外，我们发现最先进的模型性能随依赖深度显著下降：在**MA-Hard**（一个包含700个最深依赖树实体的子集）上，最佳模型在该挑战性数据集上的自动形式化正确率仅为2.6%。我们将**MathAtlas**发布给社区，作为大规模研究生级别数学“野外”自动形式化的基准集。 ## 1 引言 近年来，形式化数学（计算机可验证数学）在数学界中的流行度急剧增长[30 (https://arxiv.org/html/2605.14061#bib.bib1),32 (https://arxiv.org/html/2605.14061#bib.bib2),15 (https://arxiv.org/html/2605.14061#bib.bib67)]。伴随着人工智能的进步，这引发了对[自动形式化](https://arxiv.org/html/2605.14061)的巨大兴趣，该任务旨在自动将自然语言数学转换为可验证的形式化语言，如Lean[24 (https://arxiv.org/html/2605.14061#bib.bib75)]。 参见标题 图 1：**MathAtlas**中的一个实体及其依赖树的子图。黄色的（底部）是一个待形式化的目标定理陈述（命题15）。命题15包含三个对先前定义的数学概念的“对象引用”：戴德金环、素理想和主理想环，这些是正确形式化该定理所需的依赖项。这些对象各自有自己的依赖树（以红色边框显示），依此类推。对象的可能已有形式化版本（例如，在Mathlib中），或者需要在形式化目标陈述之前先合成出来。 直到最近，自动形式化工作主要集中于更简单的场景，如奥林匹克或本科数学[2 (https://arxiv.org/html/2605.14061#bib.bib20),36 (https://arxiv.org/html/2605.14061#bib.bib16),41 (https://arxiv.org/html/2605.14061#bib.bib26),9 (https://arxiv.org/html/2605.14061#bib.bib25),1 (https://arxiv.org/html/2605.14061#bib.bib12),12 (https://arxiv.org/html/2605.14061#bib.bib68),19 (https://arxiv.org/html/2605.14061#bib.bib69)]，其中数学陈述需要有限的前提材料才能正确形式化，而且这些材料中的大部分已由人类在Mathlib[22 (https://arxiv.org/html/2605.14061#bib.bib62)]等库中形式化。然而，在更高级的数学中，自动形式化变得更加复杂。高级数学有大量前提理论，其中许多尚未被形式化。这意味着自动形式化系统必须首先检索或生成必要的依赖理论，正确地形式化它们，然后形式化原始的目标陈述。此外，现有基准通常侧重于定理陈述，而忽略了数学**定义**的形式化。只能自动形式化定理陈述的系统其范围受限于现有理论的水平，因为它们无法形式化那些它们还没有定义的数学概念所涉及的定理。因此，构建可扩展的自动形式化系统需要研究定义自动形式化，而目前缺乏大规模真实世界的基准[39 (https://arxiv.org/html/2605.14061#bib.bib70),34 (https://arxiv.org/html/2605.14061#bib.bib73)]。 为了全面评估自动形式化方法在高级数学中的性能，我们提出了 **MathAtlas**1，这是一个大规模的研究生级别基准，旨在衡量数学“野外”的自动形式化性能。**MathAtlas** 包含约 5.1 万个非形式化实体，分为陈述（定理、例题和练习）、定义和证明，这些实体从 103 本研究生数学教材中提取。**MathAtlas** 中的实体涵盖 87 个数学领域，包括实分析、微分几何、范畴论、拓扑、量子群等。**MathAtlas** 中的一些实体可以在 Mathlib 之上形式化，但许多实体需要额外的不一定存在的形式理论。为了便于访问这些必要的依赖项，我们为每个实体丰富了长距离依赖关系、局部变量引用和局部上下文（见图 1 (https://arxiv.org/html/2605.14061#S1.F1)）。**MathAtlas** 是首个大规模、研究生级别数学“野外”的自动形式化基准，首个包含丰富上下文和依赖数据的基准，也是首个标注实体间依赖关系的基准。 我们的大量实验表明，**MathAtlas** 非常具有挑战性：强基线方法在 **MathAtlas** 上的自动形式化正确率较低（陈述为 10.5%，定义为 20.3%）。此外，我们发现这种性能与实体的**依赖深度**相关：我们最强的基线在 **MA-Hard**（一个包含 700 个最深依赖树实体的子集）上的总体正确率仅为 2.6%。最后，我们研究了现有的自动形式化语义忠实度指标在 **MathAtlas** 上的泛化情况。我们提出了 **MA-Align**2，这是一个包含 200 个 **MathAtlas** 实体的二分类基准。与之前的基准（如 ConsistencyCheck[6 (https://arxiv.org/html/2605.14061#bib.bib86)] 和 CriticLeanBench[28 (https://arxiv.org/html/2605.14061#bib.bib91)]）不同，**MA-Align** 包含定理陈述和定义的标记示例，并涵盖了研究生级别的广泛数学领域。我们的实验表明，先前的基线在 **MA-Align** 上还有很大的改进空间。 本文的其余部分组织如下：在第 2 节 (https://arxiv.org/html/2605.14061#S2) 中，我们介绍 **MathAtlas** 及其构建、内容和质量。然后我们讨论基准的自动形式化指标（第 3 节 (https://arxiv.org/html/2605.14061#S3)），接着进行自动形式化实验并分析结果（第 4 节 (https://arxiv.org/html/2605.14061#S4)）。最后，我们讨论相关工作（第 5 节 (https://arxiv.org/html/2605.14061#S5)）并总结（第 6 节 (https://arxiv.org/html/2605.14061#S6)）。 ## 2 MathAtlas 基准 定义 2.7.10（不变双线性形式）：设 \(V=V_{\bar{0}}\oplus V_{\bar{1}}\) 是一个超空间，并承载李代数 \(\mathfrak{g}\) 的一个表示。双线性形式 \((\cdot|\cdot)\) 称为**不变**的，如果对任意齐次元素 \(X\in\mathfrak{g}\) 和 \(v,w\in V\)，有 \((Xv|w)+p(v,X)(v|Xw)=0\)。此外，如果 \(V\) 是伴随表示的表示空间，则该双线性形式称为**伴随不变**的。 推论 3.A.24：设 \(X\) 是一个紧凯勒流形。则包含映射 \(i:(\mathcal{A}^*(X)^c,d)\subset(\mathcal{A}^*(X),d)\) 是一个微分分次代数的拟同构。 例 5.1.14：找出例 5.1.11 中线性齐次系统的两个基本矩阵。 图 2：来自 **MathAtlas** 的几个不同类型的实体：(1) 一个定义实体，定义了两个项：“不变”和“伴随不变”。(2) 一个来自复几何的推论定理陈述。(3) 一个来自常微分方程教材的例题。 **MathAtlas** 是从教材文档中自动构建的。我们讨论了 **MathAtlas** 中的实体和关系类型，然后讨论我们的实体和关系提取流程。我们还通过人工评估测量了 **MathAtlas** 的质量。 ### 2.1 MathAtlas 的结构 **MathAtlas** 的结构如下，附带一些相关统计信息。 #### 实体 我们用术语**实体**来表示一段可形式化的非形式化文本，例如教材中的一个定理。在 **MathAtlas** 中，实体可以是定义、定理、证明、例题或练习（见图 2 (https://arxiv.org/html/2605.14061#S2.F2)）。实体可以有（但并非总是有）标识符，例如“定理 4.3”。这些标识符有时会被其他实体引用（见图 1 (https://arxiv.org/html/2605.14061#S1.F1)）。重要的是，实体有时包含多个可形式化的项。例如，在图 2 (https://arxiv.org/html/2605.14061#S2.F2) 中，定义 2.7.10 实际上定义了两个对象，因此其形式化可能需要两个定义。 #### 引用 实体可以包含对其他实体、依赖的数学对象或实体内未明确定义的局部变量的**引用**。我们分别称之为**实体引用**、**对象引用**和**局部变量引用**。 #### 关系 我们还包含实体引用与目标实体之间，以及对象引用与定义这些对象的实体之间的关系。例如，一个实体 \(e_{met}\) 可能定义一个**度量空间**，并包含一个对**拓扑空间**的对象引用 \(r_{top}\)，而该拓扑空间是在实体 \(e_{top}\) 中定义的。在这种情况下，我们添加一个关系 \(\langle e_{met}, e_{top}\rangle\)（见图 1 (https://arxiv.org/html/2605.14061#S1.F1)）。我们将**依赖深度**定义为某个项依赖树的最大高度，其中节点是实体（例如，定义或定理），边是对象引用。类似地，我们将**依赖大小**定义为特定实体依赖树中唯一节点的总数。 #### 统计信息 我们现在讨论 **MathAtlas** 的一些统计信息。总体而言，**MathAtlas** 包含 52,052 个实体，其中包括约 1.8 万个定理、约 1 万个练习、约 1 万个定义、约 1 万个证明和 5.5 千个例题。约 90% 的实体包含至少一个对象引用。总共有约 19.3 万个对象引用，平均每个实体 3.69 个。其中，我们的关系提取系统为 83.7% 的对象引用找到了匹配的目标实体，在整个图中总共产生了约 16.1 万个对象关系。此外，20.5% 的实体包含一个实体引用，总计约 1.7 万个实体引用。其中，超过 99.8% 的实体引用与目标实体匹配。 我们现在简要介绍 **MathAtlas** 依赖图的一些特征。节点的平均依赖深度为 30（中位数为 17），但范围从 0 到 80。我们还发现依赖深度因数学领域而异。例如，来自李代数或量子群教材的实体平均深度约为 50，而来自集合论和逻辑学教材的实体平均深度约为 6。这与直觉相符，即某些数学领域有更多先修知识，因此依赖树更深。 ### 2.2 MathAtlas 的构建 这里我们概述数据集构建流程。有关更多详细信息，请参见附录 A (https://arxiv.org/html/2605.14061#A1)。 为了构建 **MathAtlas**，我们从各种来源收集了 103 本数学教材的 PDF，涵盖多个数学领域，包括代数、分析、几何、数论、概率、量子理论、范畴论、拓扑等子领域。这些数学教材总共涵盖 87 个数学领域和子领域。按照我们的流程（图 5 (https://arxiv.org/html/2605.14061#A1.F5)），我们将 PDF 转换为 MMD（数学标记语言）文件，并过滤掉包含元数据（如索引或词汇表）的页面。然后，我们在 MMD 上运行实体提取模型，识别与实体类型对应的文本跨度，以及实体中找到的任何标识符（例如，“例 3.4”）。接下来，对任何提取的实体，我们运行引用提取器来识别对其他实体、对象或局部变量的任何引用。最后，对**定义**实体，我们运行名称提取系统，识别所定义对象的名称。 提取实体和相关元数据后，我们通过关系提取系统构建依赖图（系统详情见附录 A (https://arxiv.org/html/2605.14061#A1)）。我们在实体引用与其目标实体之间，以及在对象引用与定义该对象的实体（如果存在）之间添加“引用”关系。最后，我们在证明实体与其所证明的定理实体之间添加“证明”关系。 ### 2.3 MathAtlas 的质量分析 我们测量了 **MathAtlas** 中实体的内在实体和关系提取质量。为了评估实体提取质量，我们从 **MathAtlas** 中随机抽取了 250 个提取的实体进行标注，每种类型 50 个，基于实体是否有效进行判定。3 一个实体要有效，它必须是完整的（例如，开头或结尾没有被截断，没有因 PDF 到标记语言转换不当而丢失的片段），并且具有正确标注的类型。我们发现，总体上有 90.4% 的标注实体被正确提取（见表 1 (https://arxiv.org/html/2605.14061#S2.T1)）。 我们还标注了 100 个随机抽取的引用，包括 50 个对象引用和 50 个实体引用。与之前一样，如果引用是完整的并且标注了正确的类型，则被认为是正确的。我们发现 96% 的引用被正确提取。在四个有错误的例子中，有三个是标识符被误认为实体引用，一个是名称被误认为对象引用。 最后，我们测量了关系提取系统的性能。对于上述 100 个随机抽取的引用，我们使用 LeanSearch 检索 10 个候选目标，并标注哪些（如果有）是正确的。我们计算自动系统与人类标注之间的精确率、召回率和 F1 分数。总体而言，我们发现 F1 分数为 94.8%（见表 1(a) (https://arxiv.org/html/2605.14061#S2.T1.st1)）。 表 1：**MathAtlas** 的内在数据质量分析。 (a) 我们的关系提取系统在人工标注的 100 个提取关系子集（每种类型 50 个）上的性能。为了测量召回率，我们从检索到的候选中标注金标准目标实体；如果没有选中的候选是合适的匹配，则假定不存在。 (b) 我们的实体提取系统在人工标注的 250 个例子子集（每种类型 50 个）上的精确率。 ## 3 MathAtlas 的自动形式化指标 遵循先前的工作，我们使用自动形式化的标准指标：编译率。4 我们使用