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

摘要

当前的自动形式化基准主要聚焦于奥林匹克或本科数学，而研究生与研究级数学仍未得到充分探索。在本文中，我们介绍MathAtlas，这是首个针对真实场景研究生级数学的大规模自动形式化基准，包含从103本研究生数学教材中提取的约5.2万个定理、定义、习题、例子与证明。MathAtlas还配备一个包含约17.8万条关系的数学依赖图，是首个纳入此类关系的自动形式化基准，有助于依赖感知的自动形式化系统的评估与开发。我们的大量实验表明MathAtlas质量高但极具挑战性：强基线在定理陈述上最多达到9.8%的正确率，在定义上为16.7%。此外，我们发现最先进模型的性能随依赖深度显著下降：在MA-Hard（一个由依赖树最深的700个实体组成的子集）上，最佳模型在该挑战性数据集上自动形式化的正确率仅2.6%。我们将MathAtlas发布给社区，作为对真实场景研究生级数学进行大规模自动形式化的基准集。

MathAtlas：面向真实场景的自动形式化基准：论文配图 — 图 1：MathAtlas 中的实体及其依赖树的子图。黄色（底部）表示我们有一个需要形式化的目标定理陈述（命题 15）。命题 15 包含对先前定义的数学概念的三个“对象引用”：德德金环、素理想和主理想环，它们是正确形式化定理所需的依赖项。这些对象每个都有自己的依赖树（用红色边框显示），等等。对象的形式化可能已经存在（例如，在 Mathlib 中），或者需要在目标语句形式化之前综合它们。