Language models improve translating natural language into logic formulas
Natural Language to First-Order Logic LLM-based Autoformalization
Computation and Language
Summary
Turning everyday language into precise logical statements is hard but useful. The authors explain how breaking this task into two parts—understanding the concepts (ontology extraction) and converting to logical form (logical translation)—makes it easier to evaluate and improve methods. They review existing data and techniques that use large language models to do this automatic translation. Finally, they point out challenges like better evaluation and making systems aware of broader context.
What this means in practice
- •For software engineers: Automatically convert user requirements described in natural language into formal specifications using logic-based representations.
- •For knowledge engineers: Improve building ontologies by separating concept extraction from logical formulation to enhance accuracy and evaluation.
A survey. It maps existing work.
Authors
Andrea Brunello, Cristian Curaba, Luca Geatti, Michele Mignani, Angelo Montanari, Nicola Saccomanno
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.