ATLAS：通过提升、扩增与合成数据实现自动形式化定理

自动形式化是将数学内容从自然语言自动翻译到机器可验证形式语言的过程，近年来受到大型语言模型 (LLM) 进步的推动。然而，主要障碍之一是映射非正式数学文本到其形式化对应物的平行语料库的可用性有限。为此，我们提出 ATLAS (Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data)，一种新颖的数据生成框架，用于生产大规模高质量的定理语句平行语料库。与先前方法不同，ATLAS 从概念存储库开始，通过专家迭代结合知识蒸馏加速学生模型的改进，引入两种新颖的扩增策略，这些策略利用形式语言的结构特征。我们运行 ATLAS 框架 10 次迭代，构建了一个包含 11.7 万个定理语句的本科生水平数据集，并开发了 ATLAS Translator，通过在 Llama3.1-8B-Instruct 上进行 LoRA 微调获得。该模型在所有基准测试中均显著优于 Herald Translator 和 Kimina-Autoformalizer（p<0.05，双侧 t 检验）。此外，我们证明了在 ATLAS 数据集上对更强基座模型进行全参数微调可获得更好性能。数据集、模型和代码均可在 https://github.com/XiaoyangLiu-sjtu/ATLAS 获取。