# Characterizing Paraphrase-Induced Failures in Lean 4 Autoformalization

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 19 references that are in the map.
- First posted on arXiv 25 Apr 2026.

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

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [MATH-Perturb: Benchmarking LLMs' Math Reasoning Abilities against Hard Perturbations](https://mlsanity.com/paper/2502.06453/) (2025)
- [On the Robustness of Code Generation Techniques: An Empirical Study on GitHub Copilot](https://mlsanity.com/paper/2302.00438/) (2023)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [Reliable Evaluation and Benchmarks for Statement Autoformalization](https://mlsanity.com/paper/2406.07222/) (2024)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [NLPerturbator: Studying the Robustness of Code LLMs to Natural Language Variations](https://mlsanity.com/paper/2406.19783/) (2024)
- [Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization](https://mlsanity.com/paper/2507.07399/) (2025)
- [An Investigation of Robustness of LLMs in Mathematical Reasoning: Benchmarking with Mathematically-Equivalent Transformation of Advanced Mathematical Problems](https://mlsanity.com/paper/2508.08833/) (2025)
- [Evaluating Autoformalization Robustness via Semantically Similar Paraphrasing](https://mlsanity.com/paper/2511.12784/) (2025)

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

- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)

## Abstract (arXiv)

Lean 4 autoformalization has become increasingly popular in recent years, with frontier language models and open-weight autoformalizers now producing valid formalizations of mathematical theorems. However, these evaluations often rely on single canonical phrasings of theorems and rarely probe whether outputs are robust to natural variation in inputs, while prior work has shown that semantically equivalent paraphrases often induce divergent formal outputs. We study the structure of these divergences in Lean 4 by applying deterministic paraphrase rules to datasets of undergraduate and Olympiad-level math problems. Across four frontier models and three open-weight autoformalizers, we find that paraphrase sensitivity is dominated by failures at the code-generation layer, and that these failures are typed differently by dataset. Furthermore, these patterns generalize to open-weight models, showing that state-of-the-art autoformalizers still struggle to generate valid Lean code. Our results provide a failure-mode taxonomy for autoformalization and motivate training-time interventions targeted at specific compilation failures.