# Towards a Common Framework for Autoformalization

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 34 of its 78 references that are in the map.
- First posted on arXiv 11 Sep 2025.

## Builds on (most cited first, 30 of 34)

- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [The Illusion of Thinking: Understanding the Strengths and Limitations of Reasoning Models via the Lens of Problem Complexity](https://mlsanity.com/paper/2506.06941/) (2025)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [A Survey on Semantic Parsing](https://mlsanity.com/paper/1812.00978/) (2018)
- [Coupling Large Language Models with Logic Programming for Robust and General Reasoning from Text](https://mlsanity.com/paper/2307.07696/) (2023)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://mlsanity.com/paper/1912.02636/) (2019)
- [Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specification](https://mlsanity.com/paper/2303.08006/) (2023)
- [Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving](https://mlsanity.com/paper/2405.01379/) (2024)
- [Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://mlsanity.com/paper/2301.02195/) (2023)
- [Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning](https://mlsanity.com/paper/2410.08047/) (2024)
- [Ontology Generation using Large Language Models](https://mlsanity.com/paper/2503.05388/) (2025)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [PDE-Controller: LLMs for Autoformalization and Reasoning of PDEs](https://mlsanity.com/paper/2502.00963/) (2025)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [On the Limit of Language Models as Planning Formalizers](https://mlsanity.com/paper/2412.09879/) (2024)
- [TRIP-PAL: Travel Planning with Guarantees by Combining Large Language Models and Automated Planners](https://mlsanity.com/paper/2406.10196/) (2024)
- [Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification](https://mlsanity.com/paper/2506.04592/) (2025)
- [Strategies for Improving NL-to-FOL Translation with LLMs: Data Generation, Incremental Fine-Tuning, and Verification](https://mlsanity.com/paper/2409.16461/) (2024)
- [Domain Knowledge Distillation from Large Language Model: An Empirical Study in the Autonomous Driving Domain](https://mlsanity.com/paper/2307.11769/) (2023)
- [Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control](https://mlsanity.com/paper/2406.07400/) (2024)
- [Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description](https://mlsanity.com/paper/1405.3451/) (2014)
- [StepProof: Step-by-step verification of natural language mathematical proofs](https://mlsanity.com/paper/2506.10558/) (2025)
- [Generative Agents for Multi-Agent Autoformalization of Interaction Scenarios](https://mlsanity.com/paper/2412.08805/) (2024)

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

- [OpInf-LLM: Parametric PDE Solving with LLMs via Operator Inference](https://mlsanity.com/paper/2602.01493/) (2026)
- [FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean](https://mlsanity.com/paper/2604.23002/) (2026)
- [Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases](https://mlsanity.com/paper/2607.13292/) (2026)
- [Monotonic Reference-Free Refinement for Autoformalization](https://mlsanity.com/paper/2601.23166/) (2026)
- [PYTHEN: A Flexible Framework for Legal Reasoning in Python](https://mlsanity.com/paper/2603.15317/) (2026)
- [Fixing FOLIO and MALLS: Verified Annotations and an LLM-assisted Framework to Focus Human Relabeling](https://mlsanity.com/paper/2606.02837/) (2026)
- [PrologMCP: A Standardized Prolog Tool Interface for LLM Agents](https://mlsanity.com/paper/2606.14935/) (2026)

## Abstract (arXiv)

Autoformalization has emerged as a term referring to the automation of formalization - specifically, the formalization of mathematics using interactive theorem provers (proof assistants). Its rapid development has been driven by progress in deep learning, especially large language models (LLMs). More recently, the term has expanded beyond mathematics to describe the broader task of translating informal input into formal logical representations. At the same time, a growing body of research explores using LLMs to translate informal language into formal representations for reasoning, planning, and knowledge representation - often without explicitly referring to this process as autoformalization. As a result, despite addressing similar tasks, the largely independent development of these research areas has limited opportunities for shared methodologies, benchmarks, and theoretical frameworks that could accelerate progress. The goal of this paper is to review - explicit or implicit - instances of what can be considered autoformalization and to propose a unified framework, encouraging cross-pollination between different fields to advance the development of next generation AI systems.