Research map / Large language models / Instruction and fine-tuning
ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes ATLAS, a concept-driven expert-iteration and distillation framework with proof- and contraposition-based augmentation that builds a 117k-pair Lean 4 autoformalization dataset and fine-tunes Llama3.1-8B-Instruct into a state-of-the-art translator.
Problem
Autoformalization of natural-language theorem statements into Lean 4 is limited by the scarcity of large, high-quality parallel corpora; prior sources are either limited to Mathlib or require heavy preprocessing of web-scraped text.
Approach
Start from Mathlib-derived concepts (Data Lifting) to synthesize NL statements, use teacher-student knowledge distillation with Lean compiler feedback, and augment data via proof-state extraction from Infoview and hypothesis contraposition, iterated via expert iteration.
Key results
- ATLAS Translator (Llama3.1-8B LoRA) reaches 39.46% pass@1 on ProofNet vs 31.43% for Herald Translator and 18.82% for DeepSeek-V3.
- On MathQual, ATLAS Translator achieves 22.75% pass@1 vs 19.01% for Kimina-Autoformalizer.
- Full-parameter fine-tuning of DeepSeek-Prover-V1.5-7B-Base on the ATLAS dataset reaches 54.99% pass@1 on ProofNet and 42.49% on PutnamBench.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| add synthetic data to training (ablation) | ATLAS Translator · ProofNet | pass@1: 24.10% -> 39.46% | Helped |
| add synthetic data to training (ablation) | ATLAS Translator · PutnamBench | pass@1: 15.99% -> 23.16% | Helped |
| add synthetic data to training (ablation) | ATLAS Translator · MathQual | pass@1: 11.79% -> 22.75% | Helped |
| add proof augmentation data (ablation) | ATLAS Translator · ProofNet | pass@1: 37.41% -> 39.46% | Helped |
| add proof augmentation data (ablation) | ATLAS Translator · PutnamBench | pass@1: 22.88% -> 23.16% | Helped |
| add proof augmentation data (ablation) | ATLAS Translator · MathQual | pass@1: 22.97% -> 22.75% | Hurt |
| add contraposition augmentation data (ablation) | ATLAS Translator · ProofNet | pass@1: 39.03% -> 39.46% | Helped |
| add contraposition augmentation data (ablation) | ATLAS Translator · PutnamBench | pass@1: 22.70% -> 23.16% | Helped |
| add contraposition augmentation data (ablation) | ATLAS Translator · MathQual | pass@1: 22.97% -> 22.75% | Hurt |
Surprising findings
- About 40% of sampled ATLAS propositions were judged false by an expert panel, yet the authors argue correctness is secondary for autoformalization.
- Augmentation-via-proof produced less textually diverse statements (BLEU 0.6709) than contraposition augmentation (BLEU 0.6026).
Limitations
- Synthetic propositions are not verified for correctness; a sampled audit found about 40% false.
- Proof-based augmentation has limited diversity, especially with trivial tactics.
- Evaluation relies on an LLM-based back-translation and NLI check, which can produce false positives, although human evaluation was done on ProofNet only.
Experimental setup
Datasets: Mathlib LeanDojo Lean Workbook ProofNet PutnamBench miniF2F
Benchmarks: ProofNet PutnamBench MathQual miniF2F
Metrics: pass@1 pass@8 pass@32
Baselines: DeepSeek-V3 Llama3.1-Initialization Herald Translator Kimina-Autoformalizer
Builds on: expert iteration knowledge distillation MUSTARD Herald Lean Workbook
Closest papers by meaning
- Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency (NeurIPS 2024 · similarity 0.92)
- FormalAlign: Automated Alignment Evaluation for Autoformalization (ICLR 2025 · similarity 0.89)
- Autoformalizing Euclidean Geometry (ICML 2024 · similarity 0.88)
- Multi-language Diversity Benefits Autoformalization (NeurIPS 2024 · similarity 0.88)
- Herald: A Natural Language Annotated Lean 4 Dataset (ICLR 2025 · similarity 0.87)
- RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics (NeurIPS 2025 · similarity 0.87)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.