Natural Language to First-Order Logic LLM-based Autoformalization
cs.CL
Submitted: 2026-10-08
Updated: 2026-10-08
Comments: Accepted to EMNLP-2026
License: http://creativecommons.org/licenses/by/4.0/
The gist: Large Language Models (LLMs) have renewed interest in autoformalization.
Terminology
Abstract
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.
Sources
- Fixing FOLIO and MALLS: Verified Annotations and an LLM-assisted Framework to Focus Human Relabeling
- VERUS-LM: a Versatile Framework for Combining LLMs with Symbolic Reasoning
- Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems
- A Short Review for Ontology Learning: Stride to Large Language Models Trend
- Formal Specifications from Natural Language
- A Survey on Semantic Parsing
- $\forall$uto$\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks
- LOGIC-LM++: Multi-Step Refinement for Symbolic Formulations
- Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection
- LogiQA: A Challenge Dataset for Machine Reading Comprehension with Logical Reasoning
- From Natural Language to SQL: Review of LLM-based Text-to-SQL Systems
- Enhancing Reasoning Capabilities of LLMs via Principled Synthetic Logic Corpus
- LOGicalThought: Logic-Based Ontological Grounding of LLMs for High-Assurance Reasoning
- Strategies for Improving NL-to-FOL Translation with LLMs: Data Generation, Incremental Fine-Tuning, and Verification
- LOGICPO: Efficient Translation of NL-based Logical Problems to FOL using LLMs and Preference Optimization
- Advancing Natural Language Formalization to First Order Logic with Fine-tuned LLMs
- AR-LSAT: Investigating Analytical Reasoning of Text
Related papers
- Exploring Solution Divergence and Its Effect on Large Language Model Problem Solving
- Ishigaki-IDS-Bench: A Benchmark for Generating Information Delivery Specification from BIM Information Requirements
- Subliminal Steering: Stronger Encoding of Hidden Signals
- MedStruct-S: A Benchmark for Key Discovery, Key-Conditioned QA and Semi-Structured Extraction from OCR Clinical Reports
- The End of Transformers? On Challenging Attention and the Rise of Sub-Quadratic Architectures
- Untangling the Mechanisms of Misleading Context in Medical Question Answering