# Consistent Autoformalization for Constructing Mathematical Libraries

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

## Key facts

- Cited by 21 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 43 references that are in the map.
- First posted on arXiv 5 Oct 2024.

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

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [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)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Analysing Mathematical Reasoning Abilities of Neural Models](https://mlsanity.com/paper/1904.01557/) (2019)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [A Survey of Deep Learning for Mathematical Reasoning](https://mlsanity.com/paper/2212.10535/) (2022)
- [ReACC: A Retrieval-Augmented Code Completion Framework](https://mlsanity.com/paper/2203.07722/) (2022)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [CodeBERTScore: Evaluating Code Generation with Pretrained Models of Code](https://mlsanity.com/paper/2302.05527/) (2023)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [Out of the BLEU: how should we assess quality of the Code Generation models?](https://mlsanity.com/paper/2208.03133/) (2022)
- [Does BLEU Score Work for Code Migration?](https://mlsanity.com/paper/1906.04903/) (2019)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [Learning to Prove Theorems by Learning to Generate Theorems](https://mlsanity.com/paper/2002.07019/) (2020)
- [Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving](https://mlsanity.com/paper/2405.01379/) (2024)
- [LeanReasoner: Boosting Complex Logical Reasoning with Lean](https://mlsanity.com/paper/2403.13312/) (2024)
- [Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://mlsanity.com/paper/2301.02195/) (2023)
- [Enhancing Ethical Explanations of Large Language Models through Iterative Symbolic Refinement](https://mlsanity.com/paper/2402.00745/) (2024)
- [Learning by Applying: A General Framework for Mathematical Reasoning via Enhancing Explicit Knowledge Learning](https://mlsanity.com/paper/2302.05717/) (2023)

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

- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://mlsanity.com/paper/2502.12065/) (2025)
- [Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization](https://mlsanity.com/paper/2507.07399/) (2025)
- [ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity](https://mlsanity.com/paper/2509.22246/) (2025)
- [Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations](https://mlsanity.com/paper/2505.24264/) (2025)
- [Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving](https://mlsanity.com/paper/2506.17104/) (2025)
- [DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems](https://mlsanity.com/paper/2510.10815/) (2025)
- [Diverse Inference and Verification for Advanced Reasoning](https://mlsanity.com/paper/2502.09955/) (2025)
- [Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning](https://mlsanity.com/paper/2506.10903/) (2025)
- [MASA: LLM-Driven Multi-Agent Systems for Autoformalization](https://mlsanity.com/paper/2510.08988/) (2025)
- [FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean](https://mlsanity.com/paper/2604.23002/) (2026)
- [Theory-Scale Auto-Formalization of Logics for Computer Science](https://mlsanity.com/paper/2606.26525/) (2026)
- [Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases](https://mlsanity.com/paper/2607.13292/) (2026)
- [Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving](https://mlsanity.com/paper/2503.11657/) (2025)
- [Improving Autoformalization Using Direct Dependency Retrieval](https://mlsanity.com/paper/2511.11990/) (2025)
- [Monotonic Reference-Free Refinement for Autoformalization](https://mlsanity.com/paper/2601.23166/) (2026)
- [Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees](https://mlsanity.com/paper/2604.19000/) (2026)
- [TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition](https://mlsanity.com/paper/2510.11944/) (2025)
- [When Tokenization is Secretly Output Supervision](https://mlsanity.com/paper/2609.01386/) (2026)
- [little m: An AI Agent for Industrial Process Optimization](https://mlsanity.com/paper/2609.16680/) (2026)
- [Aligning Faithfulness for Theory-Scale Autoformalization](https://mlsanity.com/paper/2610.18498/) (2026)

## Abstract (arXiv)

Autoformalization is the task of automatically translating mathematical content written in natural language to a formal language expression. The growing language interpretation capabilities of Large Language Models (LLMs), including in formal languages, are lowering the barriers for autoformalization. However, LLMs alone are not capable of consistently and reliably delivering autoformalization, in particular as the complexity and specialization of the target domain grows. As the field evolves into the direction of systematically applying autoformalization towards large mathematical libraries, the need to improve syntactic, terminological and semantic control increases. This paper proposes the coordinated use of three mechanisms, most-similar retrieval augmented generation (MS-RAG), denoising steps, and auto-correction with syntax error feedback (Auto-SEF) to improve autoformalization quality. The empirical analysis, across different models, demonstrates that these mechanisms can deliver autoformalizaton results which are syntactically, terminologically and semantically more consistent. These mechanisms can be applied across different LLMs and have shown to deliver improve results across different model types.