PaperlayerView exact revision on arXiv

Source-linked AI summary

Natural Language to First-Order Logic LLM-based Autoformalization

Andrea Brunello, Cristian Curaba, Luca Geatti, Michele Mignani, Angelo Montanari, Nicola Saccomanno

arXiv:2610.12030v1cs.CL

TL;DR

FOL autoformalization lacks a unified task formulation and systematic survey, limiting a consistent account of its evaluation and methods. The paper clarifies the task and surveys datasets, metrics, and LLM approaches; it concludes that strong results and cross-paper comparisons are qualified by evaluation and benchmark issues.

  • Problem

    FOL autoformalization lacks a unified task formulation and a systematic survey, despite its relevance to applications that require precise logical representations.

    Source: §1 · p. 1

  • Method

    The paper clarifies FOL autoformalization by distinguishing ontology information from logical translation and surveys datasets, metrics, LLM methods, and open problems.

    Source: §1 · pp. 1–2, §2.2 · p. 2, §2.4 · p. 3

  • Results

    The survey concludes that frontier reasoning models with simple CoT achieve strong results on LT, while nonstandard evaluation protocols and benchmark annotation noise make cross-paper conclusions difficult.

    Source: §4.3.2 · p. 9

  • Takeaways & Limitations

    Reliable end-to-end formalization of natural-language specification corpora remains a key next step, with application requirements able to steer research.

    Source: §5 · p. 9

    The survey provides no comparative empirical analysis across enhancement strategies or LLMs, partly because standardized evaluation protocols are absent.

    Source: Limitations · p. 9

Abstract

from arXiv · show

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.

1 Introduction

Autoformalization research lacks a unified task formulation and systematic survey when First-Order Logic is the target. This paper clarifies the task and surveys evaluation, LLM methods, and open problems.

1 Introduction

  • FOL autoformalization lacks a unified formulation and systematic survey, despite its role in converting natural-language tasks into representations for symbolic reasoning.The paper also notes applications in formal verification, legal reasoning, AI safety, and other areas.Source: §1 · p. 1
  • The paper clarifies FOL autoformalization by describing the task and addressing ambiguities in its formulation.Source: §1 · p. 1
  • It surveys datasets and metrics, LLM-based methods, and open problems and directions for future research.Source: §1 · p. 2

2 Autoformalization Definition

FOL autoformalization requires more than a formula: its meaning depends on an ontology specifying vocabulary, intended meanings, and background theory. The paper formalizes this task and distinguishes ontology construction from translation, clarifying why formula-only comparisons can conflate different representational choices.

2.1 Formulas and Ontological Commitments

  • A formula’s signature does not determine what its symbols mean, so comparing formulas or judging faithfulness without intended meanings is not well-defined.The paper treats ontology as the structure relative to which a formula represents natural-language content.Source: §2.1 · p. 2

2.2 Ontology: Signature, Labelling, Theory

  • An ontology comprises a signature, a possibly partial symbol-to-natural-language labelling, and a possibly empty background theory.The labelled signature supports faithfulness assessment; theory can encode axioms and domain assumptions that matter for reasoning or verification.Source: §2.2 · p. 2

2.3 (Not) Uniqueness of Ontological Choices

  • Different signatures suit different contexts: representing exams as individuals preserves exam identity, while a grade-aware signature can represent grades.Without further information, there is no principled reason to prefer one signature; these choices determine what can be represented and inferred.Source: §2.3 · p. 3
  • Comparing formulas without their ontologies conflates translation disagreements with differences in how content is represented.The paper argues that this decomposition distinguishes separate sources of error and enables theoretically grounded evaluation.Source: §2.3 · p. 3, §2.4 · p. 4

2.4 FOL-autoformalization Definition

  • FOL autoformalization maps natural-language text and optional knowledge to a formula–ontology pair, with the formula representing the text relative to that ontology.The ontology’s labelling and theory may be implicit, but richer ontology specification makes the output more verifiable.Source: §2.4 · p. 3
  • The unified definition spans raw translation, which outputs only a formula, and full autoformalization, which outputs the complete ontology as well.Logical Translation assumes an ontology as input; complementary Ontology Extraction constructs the ontology needed to formalize the text.Source: §2.4 · pp. 3–4

3 Autoformalization Evaluation

The section surveys evaluation for FOL autoformalization, covering datasets, proxy tasks, and direct formula metrics. It argues that task formulation and semantic evaluation choices matter for comparing studies.

3 Autoformalization Evaluation

  • Existing work does not explicitly evaluate signature quality, and only a small portion of the literature considers theory quality.Signature quality is inferred from formula correctness, while theory evaluation overlaps with ontology learning and commonsense knowledge acquisition.Source: §3 · p. 4
  • Proxy tasks assess whether formalizations work in downstream applications, offering an alternative when expert ground-truth formulas make large-scale direct evaluation costly.NLI is the most common proxy, but agreement can occur despite incorrect formulas, mismatches may involve any subset of sentences, and background knowledge may be uncaptured.Source: §3 · pp. 4–5

3.1 Datasets

  • Dataset generation combines human, LLM, and rule-based approaches, with differing validation: from grammar checks and partial alignment checks to solver-based label consistency or correctness by construction.Rule-based Text2log data are correct by construction but strongly template-driven; LLM-generated datasets use varied checking procedures.Source: §3.1 · p. 5
  • Expert-written, solver-checked datasets offer a strong evaluation basis, but documented annotation errors can skew model performance and have prompted corrected releases.Large LLM-generated datasets may lack explicit semantic-alignment checks, while template-driven rule-based data may not reflect realistic linguistic variation.Source: §3.1 · pp. 5–6

3.2.1 Syntactic Metrics

  • Syntactic metrics include exact match, tree edit distance, BLEU, and LogicSim, but formula-level string or structure comparisons can miss semantic content.Syntactic validity checks whether the formula conforms to the formalism’s rules.Source: §3.2.1 · p. 6

3.2.2 Semantic Metrics

  • Semantic comparison first requires matching symbols across formulas; surface-form matching can fail for synonyms or distinct concepts with the same name.Logical equivalence is theoretically grounded but binary; LE score is continuous yet discards quantifier structure.Source: §3.2.2 · p. 6
  • When direct semantic comparison is needed, provide the labelled signature as input and use logical equivalence as the sole evaluation metric.This avoids relying on currently unreliable symbol matching across different signatures.Source: §3.2.2 · p. 7

4 LLM-based Autoformalization Methods

The survey reviews fine-tuning, prompting, and verification-based refinement for FOL autoformalization, while noting that methods largely target translation rather than ontology extraction. It distinguishes syntactic checks from the harder problem of verifying semantic faithfulness.

4 LLM-based Autoformalization Methods

  • The literature lacks standalone ontology-extraction methods and direct metrics for evaluating labelled-signature quality, complicating optimization and comparison.The survey cautions that absent standardized task definitions and protocols, together with benchmark annotation noise, make cross-paper performance comparisons difficult.Source: §4 · p. 7, §4.3.2 · p. 9

4.1 Fine-tuning Strategies

  • Fine-tuning uses supervised NL–FOL pairs, reinforcement-learning rewards, or preference optimization to specialize models for autoformalization.Strategies include synthetic data, symbol renaming, BLEU and LE rewards, and DPO or KTO; KTO after SFT outperforms SFT alone and SFT with DPO.Source: §4.1 · p. 7

4.2.1 Agnostic Methods

  • General-purpose prompting approaches such as few-shot prompting, in-context learning, and chain-of-thought typically yield performance gains.Han et al. (2024) is cited as one example.Source: §4.2.1 · p. 8

4.2.2 Task-specific Methods

  • Task-specific prompts decompose formalization into stages, including ontology extraction before logical translation, theory recovery, or sequential translation of sentence components.Retrieval-augmented generation can also add similar NL–FOL examples, including prior model failures, as prompt demonstrations.Source: §4.2.2 · p. 8

4.3 Output Verification and Refinement Loops

  • Feedback-based refinement uses formal tools or an LLM to check an initial formalization and iteratively target syntactic or semantic correctness.The methods differ in the kind of correctness they seek to assess.Source: §4.3 · p. 8

4.3.1 Syntactic Verification

  • Syntactic verification feeds checker or prover errors back into prompts, repeats until validity or an iteration limit, or constrains decoding to valid continuations.Some methods also provide curated lists of common errors and fixes.Source: §4.3.1 · p. 8

4.3.2 Semantic Verification

  • Semantic verification remains difficult because checking whether a formula preserves a sentence’s meaning bridges fundamentally different representations beyond standard theorem provers.Satisfiability checks and unsatisfiable-core extraction can provide partial, theory-level feedback for corpora formalized as axioms.Source: §4.3.2 · p. 8
  • The survey describes candidate aggregation, direct LLM refinement, verifier models, and combined LLM–formal-tool approaches to semantic feedback.LLM-based verification can cover semantic judgments but lacks formal guarantees and depends heavily on model capability.Source: §4.3.2 · pp. 8–9

5 Open Problems and Future Directions

The paper identifies open directions in evaluation, methods, and applications of FOL autoformalization. It calls for standardized, higher-quality benchmarks, ontology-aware methods, and reliable end-to-end pipelines.

On evaluation protocols and benchmarks

  • Evaluation pipelines should separate ontology extraction from logical translation and use standardized protocols and larger, higher-quality benchmarks spanning domains, formula complexity, linguistic variation, and ambiguity.The paper notes that current pipelines often conflate the two stages, making it difficult to identify where models struggle.Source: §5 · p. 9

On autoformalization methods

  • FOL methods remain preliminary for structured intermediate representations, while standalone ontology extraction and methods following the OE/LT decomposition remain open research directions.The paper also recommends exchange across formalisms and closer engagement with ontology-learning research.Source: §5 · p. 9

Towards end-to-end applications

  • Reliable end-to-end pipelines for formalizing natural-language specification corpora are nearly absent, leaving connections to downstream applications largely implicit.The paper identifies application requirements as a potential guide for future research.Source: §5 · p. 9

Limitations

The survey does not compare enhancement strategies or LLMs empirically, partly because nonstandard evaluation makes cross-paper comparisons unreliable.

Limitations

  • The survey offers no comparative empirical analysis across enhancement strategies or LLMs, and only briefly contextualizes earlier symbolic and neural approaches.The authors note that surveyed results may become outdated as the literature evolves, while arguing that the conceptual contributions can retain value.Source: Limitations · p. 9

A First-Order Logic

The section briefly introduces First-Order Logic and covers concepts needed to follow the article, directing readers seeking fuller treatment to standard textbooks.

A First-Order Logic

A.1 Syntax

The section defines FOL syntax through signatures, terms, and formulas, then notes conventions for interpreting and writing those formulas.

A.1 Syntax

  • A signature σ consists of variables, constants, function symbols, and relation symbols, with functions and relations assigned arities.Terms are variables or constants, or functions applied to terms.Source: §A.1 · p. 12
  • FOL formulas are built from atomic formulas using logical connectives and quantifiers, with parentheses and precedence clarifying their structure.Negation, quantifiers, conjunction, disjunction, implication, and equivalence are included.Source: §A.1 · pp. 12–13
  • A formula with no free variables is a closed formula, also called a statement.Variables are quantified when they fall within a quantifier’s scope; otherwise they are free.Source: §A.1 · p. 13
  • The survey treats syntactic variants as largely superficial, while noting that standard symbolic representations have performed better than alternatives.Some variants follow theorem-prover syntax or encode formulas in a functional style.Source: §A.1 · p. 13

A.2 Semantic and SMT solvers

The section explains how structures and variable evaluations give FOL formulas semantics, and how SMT solvers support equivalence checking.

A.2 Semantic and SMT solvers

  • A σ-structure interprets function symbols over a domain, while variable evaluations assign variables to domain elements and extend to terms.The structure’s domain is nonempty; functions map tuples of domain elements to domain elements.Source: §A.2 · p. 13
  • Satisfaction is defined recursively for atomic formulas, connectives, and quantifiers, and formula equivalence requires matching truth across structures and assignments.For statements, equivalence can be stated across structures without dependence on variable assignments.Source: §A.2 · p. 13
  • Negation Normal Form transforms any formula into an equivalent formula in which negation appears only before atomic formulas.Source: §A.2 · p. 14
  • SMT solvers check equivalence by testing whether the negation of the formulas’ biconditional is unsatisfiable.The solver combines a Boolean solver with a theory solver.Source: §A.2 · p. 14

B Further NLI Datasets

The section describes NLI datasets as possible proxy evaluations for FOL-autoformalization, while distinguishing datasets needing manual annotation from those with recoverable formulas.

B Further NLI Datasets

  • NLI datasets support proxy evaluation only when each example’s reasoning pattern can be represented in FOL.Some datasets developed for other evaluation purposes also need additional components before use.Source: B Further NLI Datasets · p. 14
  • Table 2 covers reasoning datasets without FOL counterparts, whose NL sentences require manual FOL formalization for evaluation.Source: B Further NLI Datasets · p. 14, Table 2 · p. 15
  • Table 3 covers datasets with formulas recoverable from generation procedures, but their template-driven mappings may not represent free-form formalization difficulty.Some datasets first generate FOL reasoning skeletons and then translate them into NL using known rules.Source: B Further NLI Datasets · p. 14, Table 3 · p. 15
Loading 2610.12030v1…