# Lean-ing on Quality: How High-Quality Data Beats Diverse Multilingual Data in AutoFormalization

arXiv: https://arxiv.org/abs/2502.15795 · HTML: https://mlsanity.com/paper/2502.15795/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 17 references that are in the map.
- First posted on arXiv 18 Feb 2025.

## Builds on (most cited first, 11 of 11)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Measuring Massive Multitask Language Understanding](https://mlsanity.com/paper/2009.03300/) (2020)
- [Google's Neural Machine Translation System: Bridging the Gap between Human and Machine Translation](https://mlsanity.com/paper/1609.08144/) (2016)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [Teaching Temporal Logics to Neural Networks](https://mlsanity.com/paper/2003.04218/) (2020)
- [Unsupervised Neural Machine Translation with Generative Language Models Only](https://mlsanity.com/paper/2110.05448/) (2021)
- [Investigating Backtranslation in Neural Machine Translation](https://mlsanity.com/paper/1804.06189/) (2018)
- [On the Complementarity between Pre-Training and Back-Translation for Neural Machine Translation](https://mlsanity.com/paper/2110.01811/) (2021)

## Built on by (most cited first, 4 of 4)

- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [Towards a Common Framework for Autoformalization](https://mlsanity.com/paper/2509.09810/) (2025)
- [LLM Framework for Discovering Major Mathematical Conjectures: AI's Quest for the Next Riemann Hypothesis](https://mlsanity.com/paper/2607.28632/) (2026)
- [TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition](https://mlsanity.com/paper/2510.11944/) (2025)

## Abstract (arXiv)

Autoformalization, the process of transforming informal mathematical language into formal specifications and proofs remains a difficult task for state-of-the-art (large) language models. Existing works point to competing explanations for the performance gap. To this end, we introduce a novel methodology that leverages back-translation with hand-curated prompts to enhance the mathematical capabilities of language models, particularly addressing the challenge posed by the scarcity of labeled data. Specifically, we evaluate three primary variations of this strategy: (1) on-the-fly (online) backtranslation, (2) distilled (offline) backtranslation with few-shot amplification, and (3) line-by-line proof analysis integrated with proof state information. Each variant is designed to optimize data quality over quantity, focusing on the high fidelity of generated proofs rather than sheer data scale. Our findings provide evidence that employing our proposed approaches to generate synthetic data, which prioritizes quality over volume, improves the Autoformalization performance of LLMs as measured by standard benchmarks such as ProofNet. Crucially, our approach outperforms pretrained models using a minimal number of tokens. We also show, through strategic prompting and backtranslation, that our approaches surpass the performance of fine-tuning with extensive multilingual datasets such as MMA on ProofNet with only 1/150th of the tokens. Taken together, our methods show a promising new approach to significantly reduce the resources required to formalize proofs, thereby accelerating AI for math.