# Natural Language to First-Order Logic LLM-based Autoformalization

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 17 of its 66 references that are in the map.
- First posted on arXiv 8 Oct 2026.

## Builds on (most cited first, 17 of 17)

- [Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems](https://mlsanity.com/paper/2405.06624/) (2024)
- [LogiQA: A Challenge Dataset for Machine Reading Comprehension with Logical Reasoning](https://mlsanity.com/paper/2007.08124/) (2020)
- [A Survey on Semantic Parsing](https://mlsanity.com/paper/1812.00978/) (2018)
- [AR-LSAT: Investigating Analytical Reasoning of Text](https://mlsanity.com/paper/2104.06598/) (2021)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [Enhancing Reasoning Capabilities of LLMs via Principled Synthetic Logic Corpus](https://mlsanity.com/paper/2411.12498/) (2024)
- [Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection](https://mlsanity.com/paper/2405.02318/) (2024)
- [From Natural Language to SQL: Review of LLM-based Text-to-SQL Systems](https://mlsanity.com/paper/2410.01066/) (2024)
- [LOGIC-LM++: Multi-Step Refinement for Symbolic Formulations](https://mlsanity.com/paper/2407.02514/) (2024)
- [VERUS-LM: a Versatile Framework for Combining LLMs with Symbolic Reasoning](https://mlsanity.com/paper/2501.14540/) (2025)
- [Strategies for Improving NL-to-FOL Translation with LLMs: Data Generation, Incremental Fine-Tuning, and Verification](https://mlsanity.com/paper/2409.16461/) (2024)
- [Faithful Autoformalization via Roundtrip Verification and Repair](https://mlsanity.com/paper/2604.25031/) (2026)
- [A Short Review for Ontology Learning: Stride to Large Language Models Trend](https://mlsanity.com/paper/2404.14991/) (2024)
- [LOGicalThought: Logic-Based Ontological Grounding of LLMs for High-Assurance Reasoning](https://mlsanity.com/paper/2510.01530/) (2025)
- [forallutoexistsval: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks](https://mlsanity.com/paper/2403.18327/) (2024)
- [LOGICPO: Efficient Translation of NL-based Logical Problems to FOL using LLMs and Preference Optimization](https://mlsanity.com/paper/2506.18383/) (2025)
- [Fixing FOLIO and MALLS: Verified Annotations and an LLM-assisted Framework to Focus Human Relabeling](https://mlsanity.com/paper/2606.02837/) (2026)

## Abstract (arXiv)

Large Language Models (LLMs) have renewed interest in autoformalization. Yet, when First-Order Logic (FOL) is considered as the target formalism, the field still lacks a unified task formulation and a systematic survey. This paper addresses this gap: we first provide a principled definition for the FOL-autoformalization task by distinguishing Ontology Extraction from Logical Translation, showing how their conflation obscures (cross-study) evaluation; we review existing datasets, evaluation metrics, and LLM-based methods, including fine-tuning, prompting, and verification-based refinement; we identify open challenges in benchmarking, semantic evaluation, ontology-aware methods, and end-to-end applications.