💻 computer science

MathAtlas: A Benchmark for Autoformalization in the Wild

本文介绍了 MathAtlas，这是首个大规模自动形式化基准，包含来自 103 本教科书的约 52,000 个研究生级别的数学概念，揭示了当前模型在处理复杂且依赖关系丰富的研究数学时面临的极端困难。

原作者： Nilay Patel, Noah Arias, Davit Babayan, Victoria Cochran, Timothy Libman, Hafsah Mahmood, Liam McCarty, Soli Munoz, Laurel Willey, Jeffrey Flanigan

发布于 2026-05-15

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Nilay Patel, Noah Arias, Davit Babayan, Victoria Cochran, Timothy Libman, Hafsah Mahmood, Liam McCarty, Soli Munoz, Laurel Willey, Jeffrey Flanigan

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你拥有一位才华横溢的翻译官，能够将人类的故事转化为一种严格、计算机可读的语言，称为"Lean"。长期以来，这位翻译官仅接受过简单故事的测试——例如高中数学题或基础谜题。计算机能够轻松翻译这些内容，因为规则简单，且计算机此前已见过类似的规则。

但当你要求这位翻译官翻译一篇复杂、研究生级别的学术论文时，会发生什么？这正是MathAtlas所解决的问题。

以下是对该论文工作的简要拆解，辅以一些日常类比：

1. 问题：“图书馆”过于庞大

想象你正试图基于一份蓝图（数学教科书）建造一座房屋（形式化证明）。

旧基准测试：先前的测试仅要求翻译官建造一个小棚屋。所有材料都整齐地放在工具箱里，说明文字也很简短。
现实世界：研究生级别的数学就像建造摩天大楼。要建造顶层，你需要第 50 层；要建造第 50 层，你需要第 49 层，依此类推，一直追溯到地基。
核心问题：在高等数学中，“地基”（定义和理论）往往尚未用计算机语言构建完成。如果翻译官不知道“李代数”（一个复杂概念）的定义，它就无法翻译使用该概念的定理。

2. 解决方案：MathAtlas（“野生”地图）

作者创建了MathAtlas，这是一个全新的、规模宏大的测试集。

规模：他们爬取了 103 本研究生级别的数学教科书。这相当于将 52,000 页高等数学的图书馆转化为一张数字地图。
“依赖图”：这是该论文的超能力所在。想象一本“选择你自己的冒险”书籍，其中每一页都有箭头指向你需要先阅读的其他页面。MathAtlas 绘制了这些箭头。它表明，要理解“命题 15"，你首先需要理解“戴德金环”，而后者又需要“素理想”。
重要性：它迫使人工智能不仅仅翻译单个句子，而是要弄清楚：“我是否有构建此内容的工具？如果没有，我能否先找到或构建这些工具？”

3. 结果：人工智能陷入泥潭

作者在 MathAtlas 上测试了当时最先进的人工智能模型，结果令人谦卑。

得分：即使是最佳的人工智能，其定理陈述的正确率也不到10%。对于定义，正确率约为16%。
“深度”陷阱：“依赖树”越深（即需要回溯查找定义的步骤越多），人工智能的表现就越差。
- 类比：如果人工智能需要查阅 10 个先前的概念才能翻译一个句子，它就会感到困惑并放弃。在最难的问题上（依赖树最深），人工智能的正确率仅为2.6%。
"Mathlib"效应：当人工智能需要翻译的概念已经存在于一个名为"Mathlib"的著名库中时（这就像一个它可能已经研究过的预制工具箱），其表现会稍好一些。如果概念是新的且不在该库中，人工智能的困难程度则大得多。

4. “信任”测试（MA-Align）

该论文还创建了一个名为MA-Align的新测试。

问题：有时，人工智能将句子翻译成代码，代码看起来完美无缺且运行无误，但实际上其含义与原始数学内容完全不同。这就像将“猫坐在垫子上”翻译成一段计算机程序，该程序却说“狗吃了披萨”。程序能运行，但它是错的。
测试：他们请人工智能裁判检查翻译是否“忠实”（即是否忠于原意）。他们发现，即使是最佳的人工智能裁判也经常被误导，尤其是在处理复杂的研究生级别定义时。

结论

该论文得出结论：虽然人工智能在简单数学方面表现日益出色，但在翻译复杂、现实世界的研究生数学方面，目前仍极差。主要的瓶颈不仅仅在于翻译文字，而在于理解思想之间庞大的连接网络，并知道在建造“房屋”（定理）之前如何构建必要的“工具”（定义）。

MathAtlas 现已向所有人开放，作为一个挑战课程，帮助人工智能学习如何处理这些深层、复杂的依赖关系。

技术摘要：MathAtlas：面向真实场景的自动形式化基准

问题陈述

当前的自动形式化基准主要集中于较简单的领域，如奥林匹克数学或本科数学，这些领域的前置材料有限，且往往已在 Mathlib 等库中完成形式化。然而，研究生级别及研究级别的数学仍属未被充分探索的领域。在这些高级领域中，自动形式化显著更为复杂，原因如下：

前置深度：高级数学依赖于广泛的前置理论，其中大部分尚未形式化。一个有效的系统不仅要形式化目标陈述，还必须检索或合成必要的依赖理论。
定义缺口：现有基准在很大程度上忽略了数学定义的形式化。仅能处理定理陈述的系统受限于现有的形式化理论；它们无法形式化涉及那些尚无定义的概念的定理。
缺乏真实世界数据：目前缺乏大规模、真实世界的基准来捕捉研究生级别数学“真实场景”下的复杂性，包括丰富的上下文依赖和实体间关系。

方法论

数据集构建：MathAtlas

作者引入了MathAtlas，这是首个面向研究生数学的大规模自动形式化基准。

来源材料：该数据集提取自 103 本研究生级别数学教科书，涵盖 87 个不同领域（如实分析、微分几何、范畴论、量子群）。
规模与构成：MathAtlas 包含约52,052 个实体，包括：
- 约 18,000 个定理
- 约 10,000 个习题
- 约 10,000 个定义
- 约 10,000 个证明
- 约 5,000 个示例
依赖图：该数据集的一个关键特征是 enriched 了包含约 178,000 个关系的数学依赖图。该图将实体链接至：
- 对象引用：需要外部定义的命名数学概念（例如“戴德金环”）。
- 实体引用：文本中其他特定定理或定义的引用。
- 局部变量引用：未显式局部引入的符号。
- 依赖深度：实体依赖树的最大高度（平均深度为 30，最高达 80），且因领域而异（例如，李代数的依赖树比集合论更深）。

构建流程：

转换：使用 Nougat 将 PDF 转换为数学 Markdown（MMD）。
提取：通过少样本提示的 LLM（gpt-oss-120b）提取实体（定义、定理等）及其标识符。
引用提取：第二个模型在提取的文本中识别对象、实体和局部变量引用。
关系提取：一个系统将引用与目标实体进行匹配（使用 LeanSearch 进行 Mathlib 基础对齐，使用 LLM 进行内部匹配），以构建依赖图。
质量控制：对随机样本的人工评估显示，实体提取的有效率为 90.4%，关系提取的 F1 得分为 94.8%。

评估指标

本文使用名为**Correctness（正确性）**的综合指标来评估自动形式化性能，该指标要求形式化结果满足两个条件：

编译：生成的 Lean 4 代码必须成功编译。
语义忠实性：形式化陈述必须在语义上等同于非形式化源文本。
- 为了衡量忠实性，作者引入了MA-Align，这是一个包含 MathAtlas 中 200 个实体（陈述和定义）的二分类基准，标注为“对齐”或“未对齐”。
- 他们评估了现有的"LLM-as-judge"系统（如 CriticLean），发现虽然这些系统在之前的基准（ConsistencyCheck、CriticLeanBench）上表现良好，但在 MA-Align 上的准确率显著下降，凸显了在评估研究生级别定义方面的差距。

实验设置

作者在 MathAtlas 上测试了各种基线，包括：

提示模型：使用 gpt-oss-20b 和 gpt-oss-120b 进行零样本和少样本提示。
微调模型：Herald、Kimina、ATLAS-L、Goedel 和 ReForm。
消融研究：测试局部上下文（前 500 个 token）、工程化提示和特定训练示例的影响。
MA-Hard 子集：一个包含约 700 个实体的特定子集，这些实体拥有最深的依赖树（平均深度 >50），用于测试当前系统的极限。

关键结果

整体性能

MathAtlas 被证明是一个极具挑战性的基准。强大的基线模型仅实现了较低的正确率：

陈述（定理、示例、习题）：最佳基线（ReForm 8B）的正确率仅为9.8%。
定义：最佳基线（配合少样本提示的 gpt-oss-120b）的正确率为16.7%。
差异：编译率与正确率之间存在显著差距（例如，Kimina 7B 编译了 27.3% 的陈述，但仅有 2.3% 是忠实的），表明语法上的成功并不能保证语义上的准确性。

依赖深度与难度

随着依赖深度的增加，性能显著下降：

在MA-Hard（700 个拥有最深依赖树的实体）上，最佳模型仅实现了**2.6%**的正确率。
统计分析（Kolmogorov–Smirnov 检验）证实，浅层与深层依赖树之间的正确率分布存在显著差异（ $p < 0.001$ ）。

上下文与基础对齐

局部上下文：在提示中添加局部上下文（前 500 个 token）降低了提示模型的性能（定义的正确率从 20.3% 降至 17.4%），这表明当前模型难以有效整合长距离上下文。
Mathlib 基础对齐：能够与 Mathlib 中现有形式化结果进行基础对齐的实体，更有可能被正确形式化（27.9% 对比未对齐定义的 16.8%），这表明 LLM 受益于训练数据中先前对形式化理论的接触。

意义与贡献

本文声称对领域具有以下意义：

首个研究生级别基准：MathAtlas 是首个面向研究生数学的大规模、"真实场景"基准，超越了奥林匹克和本科数据集的限制。
感知依赖的评估：这是首个包含丰富依赖图和实体间关系的基准，使得能够评估那些必须处理前置理论和定义合成的系统。
凸显定义缺口：结果表明，当前最先进的模型在定义和深层依赖链方面存在显著困难，揭示了将自动形式化扩展到高级数学的关键瓶颈。
忠实性指标的局限性：MA-Align 的引入及随后的实验表明，现有的语义忠实性指标（如 CriticLean）无法很好地泛化到研究生级别的定义，需要新的评估方法。
社区资源：作者发布了 MathAtlas、MA-Align 和实验代码，以促进未来关于感知依赖的自动形式化及高级数学概念形式化的研究。

作者总结道，尽管当前系统展现出希望，但现有能力与研究生级别数学的需求之间仍存在巨大差距，特别是在前置理论的合成和定义的形式化方面。