Do LLMs Really Struggle at NL-FOL Translation? Revealing their Strengths via a Novel Benchmarking Strategy

AI summary

Overview

• Research area: Artificial Intelligence / Natural Language Processing, specifically autoformalization and semantic parsing — the translation of natural language (NL) into First-Order Logic (FOL).
• Technical level: Intermediate. The paper's argument is readable without deep expertise, but it uses FOL notation (quantifiers, connectives, logical equivalence) and assumes some familiarity with LLM benchmarking and evaluation metrics such as BLEU.
• Scope: The paper critiques existing NL-FOL evaluation protocols, proposes a new theoretically grounded benchmarking strategy, and applies it to six models across two datasets.

What This Paper Is About

The authors address why prior studies disagree about whether Large Language Models can translate natural language into First-Order Logic. Some work (Yang et al. 2024, referred to as MALLS) reports roughly 80% performance, while other work (Han et al. 2024, referred to as FOLIO) reports roughly 52% zero-shot accuracy for GPT-4 and 62% few-shot. The paper argues that these conflicting results stem from flawed datasets and evaluation protocols, then introduces a new way of measuring NL-FOL ability that separates genuine logical understanding from pattern matching, memorization and dataset contamination.

Key Contributions

1. A critical assessment of existing evaluations. The authors examine the two most recent and comprehensive NL-FOL benchmarking works, FOLIO and MALLS, and identify specific problems in both their datasets and their test protocols that may misrepresent LLM capabilities.

2. A novel, general, theoretically grounded benchmarking strategy. The new protocol restructures formula generation into two distinct phases — Ontology Extraction and Logical Translation — and adds new subtasks (most similar and ranking) designed to distinguish genuine semantic-level logical understanding from superficial pattern recognition, memorization and dataset contamination.

3. An empirical demonstration. Applying the strategy to six models on two datasets, the authors report that dialogue-oriented LLMs (GPT-4o-mini, o3-mini, Qwen3-8B, Qwen3-30B-A3B) achieve strong NL-FOL translation performance with an authentic grasp of sentence-level logic, whereas embedding-centric models (Qwen3-Embedding-8B and Gemini-Embedding-001) perform markedly worse.

4. A decomposition of the task. The paper separates NL-FOL translation into Ontology Extraction (identifying the logical signature and the meaning of each symbol) and Logical Translation (producing a formula given that signature), arguing this separation makes verification tractable and lets researchers isolate where models fail.

Main Findings

• Prior protocols collapse two distinct problems. FOLIO and MALLS merge Ontology Extraction and Logical Translation into a single task. The authors argue this obscures whether a model fails at extracting a signature or at translating logic, and makes automatic verification harder because each generated formula may use its own symbols.

• FOLIO's scoring is a poor proxy for translation quality. FOLIO judges formalization by whether the generated premises imply, contradict, or leave undetermined the generated conclusion's formula, rather than by comparing against ground-truth formulas. The authors note this assigns the same score whether every sentence is mistranslated or only one is wrong, since the logical deduction step may fail either way. The dataset contains 487 expert-written stories, each with premises and on average three conclusions, and each story may repeat multiple times.

• MALLS's Logical Equivalence (LE) score is fundamentally flawed. In the paper's example, the correct prediction ∀y CountryInEU(y) → EUCountry(y) for "Every country located in EU is an EU country" receives an LE score of 7/8 = 0.875 rather than 1. The authors give two reasons: the metric treats FOL formulas as propositional, assigning fixed truth values to predicate symbols even though a predicate's truth may vary with the objects it involves; and its columns function as world models, some of which are semantically meaningless (any column giving 1 to EUCountry while giving 0 to Country violates the constraint that every EU country is a country).

• BLEU does not capture logical semantics. Applied to formula strings, BLEU performs poorly on logic: expressions differing only by systematic predicate renaming, or that are logically but not syntactically equivalent, receive low scores. In the paper's running example, treating every symbol as a separate token yields an overall raw BLEU score of 0.18.

• MALLS's human-verification guidelines introduce ground-truth errors. The guidelines allow either ∀ or ∃ when the NL sentence lacks explicit quantifier hints, which the authors say produces errors such as treating "A child plays with a toy in a playground" as a universal assertion and translating "Birds can fly, while fish can swim, and elephants can neither fly nor swim" with existential quantifiers despite the reference to entire subject classes. The guidelines also claim →, ∧ and ↔ are sometimes interchangeable, which the authors call theoretically wrong and unacceptable for rigorous logical capability assessment. MALLS consists of 28000 GPT-4-generated pairs, of which 1000 human-verified instances form the test set.

• Dialogue-oriented models perform strongly on logical translation. Average scores over five repetitions:

  • On D_Stanford: GPT-4o-mini .84 ± .03, o3-mini .94 ± .00, Qwen3-8B .84 ± .01, Qwen3-30B .85 ± .01.
  • On D_FOLIO: GPT-4o-mini .73 ± .01, o3-mini .80 ± .00, Qwen3-8B .72 ± .00, Qwen3-30B .74 ± .01.

• Selecting the closest formula or sentence is easier than ranking. On the most similar task, dialogue models score highly across both datasets, in both NL and FOL variants — for example o3-mini reaches 1.0 ± .00 on the FOL variant of D_Stanford and .99 ± .00 on the NL variant, while GPT-4o-mini ranges from .88 ± .02 to .91 ± .00. Ranking is much harder: GPT-4o-mini's Ranking-Equivalence scores are .50 ± .03 (NL) and .57 ± .01 (FOL) on D_Stanford and .52 ± .01 (NL) and .64 ± .01 (FOL) on D_FOLIO, while o3-mini reaches .93 ± .02 (NL) and .98 ± .00 (FOL) on D_Stanford and .91 ± .01 (NL) and .94 ± .00 (FOL) on D_FOLIO. Ranking-Negation scores are lower still for the smaller models — GPT-4o-mini sits near chance at .49 ± .02 and .51 ± .02 on D_Stanford, and Qwen3-8B at .52 ± .05 and .56 ± .01.

• Embedding-centric models perform markedly worse. This is stated in the abstract and introduction; the specific numeric results for Qwen-Emb and Gemini-Emb appear in tables that fall outside the truncated portion of the paper provided here, so they are not reported in this summary.

• The Ranking-Both results are not fully reported. The table containing them is cut off in the supplied content after the D_Stanford, GPT-4o-mini row.

Methodology in Plain English

The authors start by dividing NL-FOL translation into two steps: figuring out the vocabulary (which predicates, functions and constants to use, and what each means), and writing the actual logic formula using that vocabulary. They argue existing benchmarks blur these two steps together, so you cannot tell what a model is actually failing at.

Their benchmark hands the model a pre-defined vocabulary — an ontology consisting of a signature and a natural-language glossary of every symbol — and asks it to produce a formula for a given sentence. The candidate formula is then checked for logical equivalence to a reference formula using the Z3 SMT solver, giving a clean pass/fail.

Because that task alone could be beaten by memorization or by mechanically turning sentences into formulas, the authors add two more tasks. In the most similar task, the model is given the sentence plus the correct formula mixed with eight randomly perturbed versions (perturbations swap connectives such as ∧ with ∨, switch quantifiers such as ∀ with ∃, or insert or remove a negation) and must pick the correct one; a parallel version of the task presents the formulas rendered back into English. In the ranking task, the model must order a small set of candidates from most to least similar to the sentence, where the set contains the original formula, three perturbations, a logically equivalent rewording of the original (produced with DeMorgan's laws, double negation, commutativity, distributivity or implication expansion), and both the plain negation and the negation-normal-form version of the original. Ranking is scored on whether the formula and its equivalent land in the top two positions (Ranking-Equivalence), whether the two negations land in the bottom two (Ranking-Negation), and whether both hold (Ranking-Both). Because these candidate sets are generated on the fly and go beyond the original dataset, the authors argue they are far less vulnerable to memorization and contamination.

Experiments used two datasets. The first is a 2001–2010 extract of the Grade Grinder Corpus Release 1.0, consisting of 159 high-quality instances from students working through exercises in Language, Proof and Logic, with one manually defined ontology applied to all items. The second is the FOLIO dataset; the authors used only its training split (339 stories), took only the premises, attached a manually defined ontology to each story, flattened the premises into 1667 triples, and removed triplets containing XOR to leave 1565 instances.

Four dialogue-oriented models were tested with zero-shot Automatic Chain of Thought Prompting, each prompt issued five times with only the seed parameter changed. Two embedding-centric models were tested once each, using cosine similarity between the sentence embedding and the candidate formula embeddings; Qwen-Emb was tested both plain and with a task instruction prepended, and Gemini-Emb was run with the SEMANTIC_SIMILARITY task type. Server-side training was disabled for OpenAI's models, Qwen models ran entirely on local hardware, and Google Cloud states customer data are not used for training.

Why This Matters

Impact on research. The paper argues that the field's contradictory claims about LLM logical competence come from measurement problems rather than model behavior, and offers a protocol designed to be replicated and compared across studies. By isolating Logical Translation and providing a fixed ontology, it gives a cleaner signal than end-to-end NLI-style scoring or flawed string-similarity metrics, and its on-the-fly candidate generation directly targets memorization and dataset contamination. The authors deliberately leave Ontology Extraction out of scope, framing their work as the second half of a larger evaluation pipeline.

Real-world applications.

• Specifying and verifying the behavior of critical systems, where domain experts must define wanted and unwanted behavior precisely for formal verification.
• AI safety, including real-time monitoring of LLM behavior by translating their outputs and reasoning (such as Chain-of-Thought) into logic.
• Assisting in the creation and online updating of formal world models and safety specifications.
• Making formal methods usable by people without a strong mathematical background, since interpreting and writing logic formulas currently demands specialized training.

Industry relevance. Retrieval, semantic-similarity and reranking pipelines are built on embedding-centric models, and the paper reports that these models handle NL-FOL semantics markedly worse than dialogue-oriented models. That has direct implications for anyone choosing a model architecture for logic-heavy tasks such as verification tooling, safety monitoring, or translating to formalisms like LTL and SQL.

Future Directions

• Evaluating Ontology Extraction. The authors explicitly exclude OE from this work, noting that ontology learning lacks unified evaluation metrics and standardized benchmarks, and that a rigorous analysis comparable to their LT critique is needed. They suggest indirect evaluation through a proxy task once Logical Translation ability is established.

• Completing the full NL-FOL evaluation pipeline. With OE addressed, the two-phase pipeline described here would be fully implemented.

• Broader model comparisons. The authors did not run the dialogue-versus-embedding comparison within the Gemini and OpenAI families, citing missing public documentation of which dialogue models correspond to the embedding models and the high computational cost. The Qwen family allowed this comparison because Qwen3-Embedding-8B and Qwen3-8B are both derived from Qwen3-8B-Base.

• More and harder datasets. The authors state they are unaware of other well-founded, non-synthetic NL-FOL datasets challenging enough to serve as a benchmark, having excluded the MALLS test set for its flawed validation pipeline and LogicNLI for limited complexity and syntactic variation. The absence of such datasets is an open gap.

Target Audience

Researchers and practitioners working on autoformalization, semantic parsing, and neuro-symbolic AI; evaluation and benchmarking specialists concerned with memorization and dataset contamination; and engineers applying LLMs to formal verification, AI safety monitoring, or translation into formal languages such as FOL, LTL and SQL. Readers evaluating whether to use dialogue-oriented or embedding-centric models for logic-heavy tasks will find the comparative results and the critique of existing metrics most directly useful.

Authors’ abstract

Due to its expressiveness and unambiguous nature, First-Order Logic (FOL) is a powerful formalism for representing concepts expressed in natural language (NL). This is useful, e.g., for specifying and verifying desired system properties. While translating FOL into human-readable English is relatively straightforward, the inverse problem, converting NL to FOL (NL-FOL translation), has remained a longstanding challenge, for both humans and machines. Although the emergence of Large Language Models (LLMs) promised a breakthrough, recent literature provides contrasting results on their ability to perform NL-FOL translation. In this work, we provide a threefold contribution. First, we critically examine existing datasets and protocols for evaluating NL-FOL translation performance, revealing key limitations that may cause a misrepresentation of LLMs' actual capabilities. Second, to overcome these shortcomings, we propose a novel evaluation protocol explicitly designed to distinguish genuine semantic-level logical understanding from superficial pattern recognition, memorization, and dataset contamination. Third, using this new approach, we show that state-of-the-art, dialogue-oriented LLMs demonstrate strong NL-FOL translation skills and a genuine grasp of sentence-level logic, whereas embedding-centric models perform markedly worse.