mlsanityData to 14 Oct 2026

Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs

arXiv 2301.02195 ↗First posted 5 Jan 2023cs.CL cs.AI cs.LOcited by 27

Not on the map. Why?

Abstract (arXiv)

The ever-growing complexity of mathematical proofs makes their manual verification by mathematicians very cognitively demanding. Autoformalization seeks to address this by translating proofs written in natural language into a formal representation that is computer-verifiable via interactive theorem provers. In this paper, we introduce a semantic parsing approach, based on the Universal Transformer architecture, that translates elementary mathematical proofs into an equivalent formalization in the language of the Coq interactive theorem prover. The same architecture is also trained to translate simple imperative code decorated with Hoare triples into formally verifiable proofs of correctness in Coq. Experiments on a limited domain of artificial and human-written proofs show that the models generalize well to intermediate lengths not seen during training and variations in natural language.

Key facts. Cited by 27 papers in the map (data through 14 Oct 2026). Builds on 11 of its 32 references that are in the map. First posted on arXiv 5 Jan 2023.

Builds on

11 of 32 references.

References · 11

  1. 2017Attention Is All You Needcited by 60,361
  2. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,371
  3. 2018Self-Attention with Relative Position Representationscited by 1,120
  4. 2018Universal Transformerscited by 647
  5. 2022Autoformalization with Large Language Modelscited by 263
  6. 2016Incorporating Copying Mechanism in Sequence-to-Sequence Learningcited by 218
  7. 2021The Devil is in the Detail: Simple Tricks Improve Systematic Generalization of Transformerscited by 117
  8. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 53
  9. 2015A formal proof of the Kepler conjecturecited by 42
  10. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  11. 2021Symbolic Brittleness in Sequence Models: on Systematic Generalization in Symbolic Mathematicscited by 27

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2023: 5; 2024: 4; 2025: 16; 2026: 2.

27 papers.

Sort:

By area:

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  2. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 119
  3. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  4. 2024Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Provingcited by 35
  5. 2023FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solvingcited by 27
  6. 2024Autoformalizing Euclidean Geometrycited by 27
  7. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  8. 2025Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitionscited by 22
  9. 2024Consistent Autoformalization for Constructing Mathematical Librariescited by 21
  10. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 21
  11. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 21
  12. 2023Adapting Large Language Models for Education: Foundational Capabilities, Potentials, and Challengescited by 13
15 more
  1. 2025Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalizationcited by 12
  2. 2025ASSESS: A Semantic and Structural Evaluation Framework for Statement Similaritycited by 10
  3. 2025FormaRL: Enhancing Autoformalization with no Labeled Datacited by 9
  4. 2025Towards a Common Framework for Autoformalizationcited by 7
  5. 2025Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoningcited by 6
  6. 2025LeanTutor: Towards a Verified AI Mathematical Proof Tutorcited by 4
  7. 2025Thinking Machines: Mathematical Reasoning in the Age of LLMscited by 4
  8. 2025Do LLMs Really Struggle at NL-FOL Translation? Revealing their Strengths via a Novel Benchmarking Strategycited by 2
  9. 2025Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Enginecited by 1
  10. 2025KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignmentcited by 1
  11. 2026Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Treescited by 1
  12. 2023Safety without alignmentcited by 0
  13. 2025Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verificationcited by 0
  14. 2025Towards Autoformalization of LLM-generated Outputs for Requirement Verificationcited by 0
  15. 2026LeanTutor: Towards a Verified AI Mathematical Proof Tutorcited by 0