arXiv:2502.05567v1 Announce Type: cross 摘要：自动形式化，即将自然语言数学自动转换为可机器验证的形式语言的过程，在大型语言模型（LLMs）的进步中已经展示了进展。然而，进一步进展的一个关键障碍是缺乏将自然语言与形式语言对齐的配对数据集。为了应对这一挑战，我们引入了ATLAS（自动形式化定理通过提升、增强和数据合成），这是一种迭代数据生成框架，用于生成大规模、高质量的并列定理陈述。通过运行提出的ATLAS 10次迭代，我们构建了一个包含30万个定理陈述的本科生级别数据集，并开发了ATLAS翻译器，在ProofNet上的准确率为80.59%（pass@8）和92.99%（pass@128），显著优于基模型（23.99%和47.17%）和InternLM2-Math-Plus-7B（50.94%和80.32%）。此外，ATLAS翻译器还在本工作中引入的高中级别miniF2F数据集和研究生级别的MathQual数据集上达到了最先进的性能。这些数据集、模型和代码即将对公众发布。