mlsanityData to 7 Oct 2026

Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar

arXiv 1912.02636 ↗First posted 5 Dec 2019cs.LO cs.CL cs.LGcited by 40

Not on the map. Why?

Abstract (arXiv)

In this paper we share several experiments trying to automatically translate informal mathematics into formal mathematics. In our context informal mathematics refers to human-written mathematical sentences in the LaTeX format; and formal mathematics refers to statements in the Mizar language. We conducted our experiments against three established neural network-based machine translation models that are known to deliver competitive results on translating between natural languages. To train these models we also prepared four informal-to-formal datasets. We compare and analyze our results according to whether the model is supervised or unsupervised. In order to augment the data available for auto-formalization and improve the results, we develop a custom type-elaboration mechanism and integrate it in the supervised translation.

Key facts. Cited by 40 papers in the map (data through 7 Oct 2026). First posted on arXiv 5 Dec 2019.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 6; 2022: 7; 2023: 6; 2024: 10; 2025: 9; 2026: 2.

40 papers.

Sort:

By area:

  1. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  2. 2022Autoformalization with Large Language Modelscited by 252
  3. 2022Memorizing Transformerscited by 219
  4. 2023LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Proverscited by 161
  5. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  6. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  7. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  8. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  9. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  10. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  11. 2024Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalizationcited by 53
  12. 2021LIME: Learning Inductive Bias for Primitives of Mathematical Reasoningcited by 46
28 more
  1. 2024Process-Driven Autoformalization in Lean 4cited by 45
  2. 2023Multilingual Mathematical Autoformalizationcited by 38
  3. 2023Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofscited by 27
  4. 2024Reliable Evaluation and Benchmarks for Statement Autoformalizationcited by 25
  5. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
  6. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  7. 2022Towards a Mathematics Formalisation Assistant using Large Language Modelscited by 22
  8. 2022A Survey in Mathematical Language Processingcited by 9
  9. 2024REFACTOR: Learning to Extract Theorems from Proofscited by 9
  10. 2024GFLean: An Autoformalisation Framework for Lean via GFcited by 9
  11. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 9
  12. 2024Can Transformers Do Enumerative Geometry?cited by 8
  13. 2025Towards a Common Framework for Autoformalizationcited by 7
  14. 2025StepProof: Step-by-step verification of natural language mathematical proofscited by 6
  15. 2025RLMEval: Evaluating Research-Level Neural Theorem Provingcited by 6
  16. 2025Automated Formalization via Conceptual Retrieval-Augmented LLMscited by 5
  17. 2021A Study of Continuous Vector Representationsfor Theorem Provingcited by 4
  18. 2022A Survey on Artificial Intelligence for Source Code: A Dialogue Systems Perspectivecited by 3
  19. 2021Smart Proofs via Smart Contracts: Succinct and Informative Mathematical Derivations via Decentralized Marketscited by 2
  20. 2025Improving Autoformalization Using Direct Dependency Retrievalcited by 2
  21. 2026MathAtlas: A Benchmark for Autoformalization in the Wildcited by 2
  22. 2021Disambiguating Symbolic Expressions in Informal Documentscited by 1
  23. 2023Improving the Diproche CNL through Autoformalization via Large Language Modelscited by 1
  24. 2025E-Gen: Leveraging E-Graphs to Improve Continuous Representations of Symbolic Expressionscited by 1
  25. 2025Hierarchical Attention Generates Better Proofscited by 1
  26. 2026Pipeline for Verifying LLM-Generated Mathematical Solutionscited by 1
  27. 2023Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Studentscited by 0
  28. 2024ZIP-FIT: Embedding-Free Data Selection via Compression-Based Alignmentcited by 0