mlsanityData to 14 Oct 2026

Multilingual Mathematical Autoformalization

arXiv 2311.03755 ↗First posted 7 Nov 2023cs.CL cs.LGcited by 39

Not on the map. Why?

Abstract (arXiv)

Autoformalization is the task of translating natural language materials into machine-verifiable formalisations. Progress in autoformalization research is hindered by the lack of a sizeable dataset consisting of informal-formal pairs expressing the same essence. Existing methods tend to circumvent this challenge by manually curating small corpora or using few-shot learning with large language models. But these methods suffer from data scarcity and formal language acquisition difficulty. In this work, we create textttMMA, a large, flexible, multilingual, and multi-domain dataset of informal-formal pairs, by using a language model to translate in the reverse direction, that is, from formal mathematical statements into corresponding informal ones. Experiments show that language models fine-tuned on textttMMA produce 16-18% of statements acceptable with minimal corrections on the textttminiF2F and textttProofNet benchmarks, up from 0% with the base model. We demonstrate that fine-tuning on multilingual formal data results in more capable autoformalization models even when deployed on monolingual tasks.

Key facts. Cited by 39 papers in the map (data through 14 Oct 2026). Builds on 20 of its 35 references that are in the map. First posted on arXiv 7 Nov 2023.

Builds on

20 of 35 references.

References · 20

  1. 2023GPT-4 Technical Reportcited by 18,396
  2. 2022Training language models to follow instructions with human feedbackcited by 15,971
  3. 2023LLaMA: Open and Efficient Foundation Language Modelscited by 14,132
  4. 2023Llama 2: Open Foundation and Fine-Tuned Chat Modelscited by 13,028
  5. 2021Evaluating Large Language Models Trained on Codecited by 8,320
  6. 2021RoFormer: Enhanced Transformer with Rotary Position Embeddingcited by 4,703
  7. 2020GLU Variants Improve Transformercited by 1,804
  8. 2019Root Mean Square Layer Normalizationcited by 1,480
  9. 2015Improving Neural Machine Translation Models with Monolingual Datacited by 788
  10. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  11. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  12. 2017Unsupervised Machine Translation Using Monolingual Corpora Onlycited by 273
8 more
  1. 2022Autoformalization with Large Language Modelscited by 263
  2. 2016Professor Forcing: A New Algorithm for Training Recurrent Networkscited by 216
  3. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
  4. 2017Unsupervised Neural Machine Translationcited by 149
  5. 2023Evaluating Language Models for Mathematics through Interactionscited by 70
  6. 2019The FLoRes Evaluation Datasets for Low-Resource Machine Translation: Nepali-English and Sinhala-Englishcited by 62
  7. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 53
  8. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2024: 12; 2025: 21; 2026: 6.

39 papers.

Sort:

By area:

  1. 2025Scaling up Test-Time Compute with Latent Reasoning: A Recurrent Depth Approachcited by 415
  2. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
  3. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 180
  4. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 122
  5. 2025Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2cited by 97
  6. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 79
  7. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 59
  8. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  9. 2024Process-Driven Autoformalization in Lean 4cited by 45
  10. 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Provingcited by 33
  11. 2024A Semantic Search Engine for Mathlib4cited by 31
  12. 2024Autoformalizing Euclidean Geometrycited by 27
27 more
  1. 2024FormalAlign: Automated Alignment Evaluation for Autoformalizationcited by 24
  2. 2025PDE-Controller: LLMs for Autoformalization and Reasoning of PDEscited by 23
  3. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  4. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 21
  5. 2026Large Language Model Reasoning Failurescited by 21
  6. 2025ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimizationcited by 20
  7. 2025Mathesis: Towards Formal Theorem Proving from Natural Languagescited by 18
  8. 2025StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusioncited by 16
  9. 2025Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalizationcited by 12
  10. 2025Putnam-AXIOM: A Functional and Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMscited by 11
  11. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Predictioncited by 10
  12. 2025ASSESS: A Semantic and Structural Evaluation Framework for Statement Similaritycited by 10
  13. 2024GFLean: An Autoformalisation Framework for Lean via GFcited by 9
  14. 2025FormaRL: Enhancing Autoformalization with no Labeled Datacited by 9
  15. 2024Can Transformers Do Enumerative Geometry?cited by 8
  16. 2025DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theoremscited by 8
  17. 2025Lean Finder: Semantic Search for Mathlib That Understands User Intentscited by 8
  18. 2026Semantic Search over 9 Million Mathematical Theoremscited by 8
  19. 2025Automated Formalization via Conceptual Retrieval-Augmented LLMscited by 5
  20. 2026MathAtlas: A Benchmark for Autoformalization in the Wildcited by 4
  21. 2024Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Taskscited by 2
  22. 2025Improving Autoformalization Using Direct Dependency Retrievalcited by 2
  23. 2026VALG: An Agentic System for ML Theory Researchcited by 2
  24. 2025ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Provingcited by 1
  25. 2025KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignmentcited by 1
  26. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  27. 2026An AI-Assisted Formalization of the Poincar'e Conjecturecited by 0