arXiv 2502.055672025-10-01cs.CLcs.AIcs.LG

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

ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data

School of Mathematical Sciences, Shanghai Jiao Tong University（上海交通大学数学科学学院）；Institute of Natural Sciences, MOE-LSC, CMA-Shanghai, Shanghai Jiao Tong University（上海交通大学自然科学研究院）；SPEIT, Shanghai Jiao Tong University（上海交通大学巴黎卓越工程师学院）；JoinTech Co., Ltd（JoinTech 有限公司）

Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao, Tao Luo

备注：: Accepted to NeurIPS 2025

阅读 PDF

arXiv 页面 ↗HTML 原文 ↗

AI总结：

针对数学自动形式化领域平行语料不足的问题，提出ATLAS数据生成框架，通过概念库、专家迭代结合知识蒸馏及新型增强策略构建大规模数据集，微调得到的翻译模型刷新基准性能。

摘要：

自动形式化是指将数学内容从自然语言自动翻译为机器可验证的形式语言的技术，在大语言模型（LLM）的发展推动下已取得显著进展。然而，进一步提升该技术的主要障碍是，将非形式化数学文本映射为对应形式化文本的平行语料库十分有限。为解决这一局限，我们提出ATLAS（Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data，即通过数据提升、增强与合成实现定理自动形式化），这是一种新型数据生成框架，旨在生成大规模、高质量的定理陈述平行语料库。与现有方法不同，ATLAS以概念库为起点，通过专家迭代结合知识蒸馏加速学生模型的优化，并提出两种利用形式语言结构特征的新型增强策略。我们将所提出的ATLAS框架运行10轮，构建了包含11.7万条定理陈述的本科水平数据集，并通过LoRA微调Llama3.1-8B-Instruct开发出ATLAS Translator。该模型创下新的最优性能，在所有基准测试中相较Herald Translator和Kimina-Autoformalizer均展现出统计显著性提升（p<0.05，双侧t检验）。此外，我们证明在ATLAS数据集上对更强的基础模型进行全参数微调可获得更优性能。数据集、模型与代码可在https://github.com/XiaoyangLiu-sjtu/ATLAS获取。

英文摘要：

Autoformalization, the automatic translation of mathematical content from natural language into machine-verifiable formal languages, has seen significant progress driven by advances in large language models (LLMs). Nonetheless, a primary barrier to further improvements is the limited availability of parallel corpora that map informal mathematical text to its formal counterpart. To address this limitation, we propose ATLAS (Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data), a novel data generation framework designed to produce large-scale, high-quality parallel corpora of theorem statements. Distinct from prior approaches, ATLAS begins with a concept repository, accelerates the improvement of the student model through expert iteration combined with knowledge distillation, and introduces two novel augmentation strategies that exploit the structural characteristics of formal languages. Running the proposed ATLAS framework for 10 iterations, we construct an undergraduate-level dataset of 117k theorem statements and develop the ATLAS Translator by fine-tuning Llama3.1-8B-Instruct with LoRA. This model establishes a new state of the art, demonstrating statistically significant improvements over both the Herald Translator and the Kimina-Autoformalizer across all benchmarks (p<0.05, two-sided t-test). Furthermore, we demonstrate that the full-parameter fine-tuning of a stronger base model on the ATLAS dataset leads to superior performance. The datasets, model, and code are available at https://github.com/XiaoyangLiu-sjtu/ATLAS.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。