mlsanityData to 14 Oct 2026

Autoformalization with Large Language Models

arXiv 2205.12615 ↗First posted 25 May 2022cs.LG cs.AI cs.LOcited by 263

Not on the map. Why?

Cited by 74 in LLM reasoning, but placed by its own abstract, which didn’t fit.

Abstract (arXiv)

Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs. A successful autoformalization system could advance the fields of formal verification, program synthesis, and artificial intelligence. While the long-term goal of autoformalization seemed elusive for a long time, we show large language models provide new prospects towards this goal. We make the surprising observation that LLMs can correctly translate a significant portion (25.3%) of mathematical competition problems perfectly to formal specifications in Isabelle/HOL. We demonstrate the usefulness of this process by improving a previously introduced neural theorem prover via training on these autoformalized theorems. Our methodology results in a new state-of-the-art result on the MiniF2F theorem proving benchmark, improving the proof rate from 29.6% to 35.2%.

Key facts. Cited by 263 papers in the map (data through 14 Oct 2026). Builds on 35 of its 70 references that are in the map. First posted on arXiv 25 May 2022.

Builds on

35 of 70 references.

References · 35

  1. 2017Attention Is All You Needcited by 60,361
  2. 2020Language Models are Few-Shot Learnerscited by 32,419
  3. 2021Training Verifiers to Solve Math Word Problemscited by 10,109
  4. 2021Evaluating Large Language Models Trained on Codecited by 8,320
  5. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,371
  6. 2022PaLM: Scaling Language Modeling with Pathwayscited by 5,326
  7. 2016SGDR: Stochastic Gradient Descent with Warm Restartscited by 5,045
  8. 2022Training Compute-Optimal Large Language Modelscited by 3,019
  9. 2020The Pile: An 800GB Dataset of Diverse Text for Language Modelingcited by 2,411
  10. 2017Accurate, Large Minibatch SGD: Training ImageNet in 1 Hourcited by 1,492
  11. 2022Competition-Level Code Generation with AlphaCodecited by 1,462
  12. 2017Hindsight Experience Replaycited by 1,136
23 more
  1. 2015Improving Neural Machine Translation Models with Monolingual Datacited by 788
  2. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  3. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  4. 2017Unsupervised Machine Translation Using Monolingual Corpora Onlycited by 273
  5. 2017Thinking Fast and Slow with Deep Learning and Tree Searchcited by 252
  6. 2022Memorizing Transformerscited by 226
  7. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  8. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 98
  9. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 81
  10. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 53
  11. 2020Teaching Temporal Logics to Neural Networkscited by 51
  12. 2017Deep Network Guided Proof Searchcited by 47
  13. 2018TacticToe: Learning to Prove with Tacticscited by 44
  14. 2020INT: An Inequality Benchmark for Evaluating Generalization in Theorem Provingcited by 44
  15. 2015A formal proof of the Kepler conjecturecited by 42
  16. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  17. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  18. 2019Learning to Reason in Large Theories without Imitationcited by 27
  19. 2021Unsupervised Neural Machine Translation with Generative Language Models Onlycited by 24
  20. 2021Neural Circuit Synthesis from Specification Patternscited by 17
  21. 2018Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learningcited by 15
  22. 2021Proving Theorems using Incremental Learning and Hindsight Experience Replaycited by 13
  23. 2021Generating Symbolic Reasoning Problems with Transformer GANscited by 5

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2022: 15; 2023: 39; 2024: 47; 2025: 69; 2026: 93.

263 papers.

Sort:

By area:

  1. 2023A Survey of Large Language Modelscited by 2,576
  2. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,392
  3. 2023A Survey on Evaluation of Large Language Modelscited by 1,242
  4. 2022PAL: Program-aided Language Modelscited by 652
  5. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  6. 2023Augmented Language Models: a Surveycited by 403
  7. 2023Llemma: An Open Language Model For Mathematicscited by 388
  8. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  9. 2022Reasoning with Language Model Prompting: A Surveycited by 252
  10. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
  11. 2022Re3: Generating Longer Stories With Recursive Reprompting and Revisioncited by 193
  12. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
38 more
  1. 2023LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Proverscited by 168
  2. 2022Language Models of Code are Few-Shot Commonsense Learnerscited by 160
  3. 2023Progressive-Hint Prompting Improves Reasoning in Large Language Modelscited by 147
  4. 2024Beyond Autoregression: Discrete Diffusion for Complex Reasoning and Planningcited by 135
  5. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
  6. 2023How well do Large Language Models perform in Arithmetic tasks?cited by 130
  7. 2022Text and Patterns: For Effective Chain of Thought, It Takes Two to Tangocited by 128
  8. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  9. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 122
  10. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 119
  11. 2022Teaching Algorithmic Reasoning via In-context Learningcited by 112
  12. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 109
  13. 2025Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2cited by 97
  14. 2024Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systemscited by 96
  15. 2023A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validationcited by 93
  16. 2024Transformers Can Achieve Length Generalization But Not Robustlycited by 86
  17. 2023Retrieving Multimodal Information for Augmented Generation: A Surveycited by 85
  18. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 84
  19. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 81
  20. 2024If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code Empowers Large Language Models to Serve as Intelligent Agentscited by 79
  21. 2024SynCode: LLM Generation with Grammar Augmentationcited by 69
  22. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 68
  23. 2023nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Modelscited by 60
  24. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 59
  25. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 58
  26. 2025Aristotle: IMO-level Automated Theorem Provingcited by 58
  27. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  28. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 55
  29. 2024Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalizationcited by 55
  30. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  31. 2024Process-Driven Autoformalization in Lean 4cited by 45
  32. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 44
  33. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Datacited by 43
  34. 2023Multilingual Mathematical Autoformalizationcited by 39
  35. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  36. 2024Assessing and Understanding Creativity in Large Language Modelscited by 35
  37. 2024Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Provingcited by 35
  38. 2024Planning Anything with Rigor: General-Purpose Zero-Shot Planning with LLM-based Formalized Programmingcited by 35

50 most cited of 263 All 263 (JSON)