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

TL;DR

ATLAS introduces a novel data generation framework that significantly enhances autoformalization by creating large-scale parallel corpora, improving model performance through innovative augmentation strategies and iterative learning.

Contribution

The paper presents ATLAS, a new framework for generating high-quality formal-informal theorem pairs, and demonstrates its effectiveness in training superior autoformalization models.

Findings

Constructed a 117k theorem dataset using ATLAS.

Achieved state-of-the-art performance with the ATLAS Translator.

Full-parameter fine-tuning on the dataset yields even better results.

Abstract

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.