PaperlayerView exact revision on arXiv

Source-linked AI summary

NL2LOGIC: AST-Guided Translation of Natural Language into First-Order Logic with Large Language Models

Rizky Ramadhana Putra, Raihan Sultan Pasha Basuki, Yutong Cheng, Peng Gao

arXiv:2602.13237v1cs.AIcs.CL

TL;DR

Existing logic-translation methods often rely on shallow token prediction rather than genuine logical understanding, increasing hallucination risk for complex sentence structures. NL2LOGIC iteratively parses natural-language clauses into a first-order logic AST, then uses AST-guided deterministic generation to produce solver-compatible logic. NL2LOGIC improves semantic accuracy by an average of 30% over the strongest baseline, and Logic-LM by 31% on both syntactic and downstream reasoning task accuracy.

  • Problem

    Existing logic-translation methods often rely on shallow token prediction rather than genuine logical understanding, increasing hallucination risk for complex sentence structures.

    Source: §1 · p. 2

  • Method

    NL2LOGIC iteratively parses natural-language clauses into a first-order logic AST, then uses AST-guided deterministic generation to produce solver-compatible logic.

    Source: §1 · p. 2

  • Results

    NL2LOGIC improves semantic accuracy by an average of 30% over the strongest baseline, and Logic-LM by 31% on both syntactic and downstream reasoning task accuracy.

    Source: §1 · p. 2, §6 · p. 10

  • Takeaways & Limitations

    The results support using an AST-based separation of semantic parsing and code generation to improve syntactic control and semantic alignment in the evaluated reasoning tasks.

    Source: §1 · p. 2, §6 · p. 9

    NL2LOGIC translates one sentence at a time and does not yet handle co-reference or implicit relational links across sentences.

    Source: Limitations · p. 10

Abstract

from arXiv · show

Automated reasoning is critical in domains such as law and governance, where verifying claims against facts in documents requires both accuracy and interpretability. Recent work adopts structured reasoning pipelines that translate natural language into first-order logic and delegate inference to automated solvers. With the rise of large language models, approaches such as GCD and CODE4LOGIC leverage their reasoning and code generation capabilities to improve logic parsing. However, these methods suffer from fragile syntax control due to weak enforcement of global grammar constraints and low semantic faithfulness caused by insufficient clause-level semantic understanding. We propose NL2LOGIC, a first-order logic translation framework that introduces an abstract syntax tree as an intermediate representation. NL2LOGIC combines a recursive large language model based semantic parser with an abstract syntax tree guided generator that deterministically produces solver-ready logic code. Experiments on the FOLIO, LogicNLI, and ProofWriter benchmarks show that NL2LOGIC achieves 99 percent syntactic accuracy and improves semantic correctness by up to 30 percent over state-of-the-art baselines. Furthermore, integrating NL2LOGIC into Logic-LM yields near-perfect executability and improves downstream reasoning accuracy by 31 percent compared to Logic-LM's original few-shot unconstrained translation module.

1 Introduction

Natural-language ambiguity makes precise claim verification difficult, while existing LLM-based logic translation methods face syntax-control and semantic-faithfulness challenges. NL2LOGIC uses iterative clause parsing into an intermediate FOLAST and deterministic AST-guided generation; evaluations report near-perfect syntax correctness and improved semantic accuracy and downstream reasoning.

1 Introduction

  • Natural-language ambiguity complicates precise interpretation of logical relations needed for claim verification and compliance checking.Structured reasoning can make intermediate proof steps explicit, improving transparency and auditability over opaque neural entailment outputs.Source: §1 · p. 1
  • GCD’s local grammar constraints do not ensure variable or signature consistency, while CODE4LOGIC’s free-form grammar-tree generation can propagate errors into invalid outputs.Single-step translation also requires simultaneous comprehension and program generation, which can encourage shallow prediction and hallucinations on complex sentence structures.Source: §1 · p. 2
  • NL2LOGIC iteratively parses sentence clauses into predicates, quantifiers, and connectives, building a FOLAST whose clause-level decisions compose into a globally coherent representation.The framework is presented as an alternative to unconstrained single-step translation.Source: §1 · p. 2
  • A two-pass AST-guided generator registers constants, variables, and relation signatures before assembling scoped expressions in solver-specific grammar.The resulting executable rules are compatible with solvers such as Z3 and SMT-LIB.Source: §1 · p. 2
  • NL2LOGIC improves semantic accuracy by an average of 30% over the strongest baseline, GCD, and improves downstream reasoning by 31% over Logic-LM’s original unconstrained FOL translation module.The evaluation spans twelve models from 0.5B to 27B parameters.Source: §1 · p. 2
  • The evaluation tests syntax validity, semantic preservation for entailment prediction, and whether NL2LOGIC improves existing neuro-symbolic systems.It uses FOLIO, ProofWriter, and LogicNLI with Z3, and also integrates NL2LOGIC into Logic-LM.Source: §1 · p. 2

2 Related Work

Formal-logic translation has moved from rule-based and neural approaches to LLM-based pipelines, including methods that add structural constraints. Related work also uses LLM prompting and symbolic solvers for logical reasoning, but the cited approaches retain limitations in formal proof or semantic faithfulness.

Natural Language to Formal Logic Translation

  • Rule-based translation offers precise control but limited robustness to linguistic variation, while neural logical-form generation generalizes better but struggles with rare operators and complex syntax.More recent neuro-symbolic systems commonly integrate unconstrained few-shot LLM translation with logic solvers.Source: §2 · p. 2
  • Grammar-constrained and code-generation approaches add syntactic structure, yet resulting formulas can remain semantically unfaithful to source text.The cited methods are Raspanti et al. (2025) and Liu (2025).Source: §2 · p. 3

LLMs for Logical Reasoning

  • Chain-of-thought and step-by-step prompting break complex reasoning into intermediate steps, while other frameworks combine LLMs with automated reasoning tools or symbolic solvers.Prior work is characterized as lacking formal proof or producing unfaithful logical forms through overly simple, unconstrained translation.Source: §2 · p. 3

3 Preliminary

The preliminaries introduce first-order logic and ASTs as formal representations, then motivate separating logical parsing from solver-specific code generation. An intermediate FOLAST represents logical structure independently of the target reasoning engine.

First-Order Logic

  • First-order logic expresses statements about entities, properties, and relations using constants, variables, functions, relations, quantifiers, and logical connectives.Its strict grammar supports unambiguous interpretation and compatibility with automated reasoning systems.Source: §3 · p. 3

Abstract Syntax Tree

  • The paper extends the AST concept into a FOLAST defined by standard FOL grammar, using it as a backend-independent intermediate representation between natural language and generated code.The code is intended for execution by automated reasoning engines.Source: §3 · p. 3

Reasoning Engines and Target Languages

  • Because reasoning engines require strict engine-specific syntax that is rarely observed during LLM pretraining, direct end-to-end solver-code generation can produce syntax errors and inconsistent structures.The paper’s design decouples parsing from code generation, then deterministically compiles the engine-agnostic AST into a target reasoning language.Source: §3 · p. 3

4 NL2LOGIC Design

NL2LOGIC separates translation into a semantic parser that builds a FOL abstract syntax tree and a generator that compiles it into solver-ready code.

4 NL2LOGIC Design

  • NL2LOGIC uses a semantic parser to produce a FOLAST, then an AST-guided generator to compile it into solver-executable code.The FOLAST is defined by a standard grammar and serves as the intermediate representation between natural language and target code.Source: §4 · p. 3

4.1 Preprocessing

  • SaT identifies sentence boundaries using contextual and lexical cues, avoiding splits at abbreviations or numeric expressions before semantic parsing.The paper notes that feeding long paragraphs to the parser risks hallucination and error propagation.Source: §4.1 · p. 3

4.2 Semantic Parser

  • The recursive semantic parser classifies each sentence, parses its outermost construct, and delegates child clauses to specialized sub-parsers.Its modules extract predicates and arguments, identify quantifiers and variables, or split logical operators into operands.Source: §4.2 · p. 5

4.3 AST-Guided Generator

  • The generator first collects symbol declarations, then emits expressions with correct arity, operator precedence, and quantifier scope.The declaration environment registers identifiers and signatures; the second pass generates solver-target expressions with scoped variable bindings.Source: §4.3 · pp. 5–6

5 Evaluation

NL2LOGIC is evaluated for syntax correctness, semantic correctness, and integration into a neuro-symbolic system. Across the reported evaluations, it improves on GCD and Logic-LM, while semantic performance varies with dataset structure.

5.1 Evaluation Setup

  • The evaluation uses Gemma, Llama, Mistral, and Qwen models ranging from 0.5 to 27B parameters and evaluates 3,000 premise–hypothesis pairs, each labeled entailment, contradiction, or uncertain.For Logic-LM integration, the original pipeline is maintained while only the FOL translation component is substituted.Source: §5.1 · pp. 6–7

5.2 RQ1: Syntax Correctness

  • Up to 0.99 syntax correctness, with NL2LOGIC outperforming GCD across model families and scales.The reported syntax errors account for less than 5% of sentences and include malformed JSON or required AST fields left empty.Source: §5.2 · pp. 7–8, Table 1 · p. 7, Table 2 · p. 8

5.3 RQ2: Semantic Correctness

  • 31% average improvement over GCD on natural language inference tasks, with performance varying by dataset.NL2LOGIC performs relatively better on LogicNLI, while some larger GCD models surpass it on FOLIO.Source: §5.3 · p. 8, Table 3 · p. 8

5.4 RQ3: Integration with Neuro-Symbolic Systems

  • 0.99 executable rate across 13 models and both ProofWriter and FOLIO datasets after replacing Logic-LM’s translation module.The original few-shot translator’s executable rates range from 0.01 to 0.94.Source: §5.4 · p. 9, Table 4 · p. 9
  • ∼31% average accuracy improvement over Logic-LM on executable rules, with larger gains reported for smaller models.On ProofWriter, gemma-2-2b improves from 0.01 to 0.58, llama-3.2-3b from 0.03 to 0.68, and qwen-2.5-7b from 0.08 to 0.90.Source: §5.4 · p. 9, Table 5 · p. 9

6 Conclusion

NL2LOGIC incrementally constructs an AST to translate natural language into first-order logic, improving syntactic correctness, semantic accuracy, and Logic-LM performance.

6 Conclusion

  • NL2LOGIC achieves near-perfect syntactic correctness and improves semantic accuracy by 30% on LogicNLI, FOLIO, and ProofWriter.It is an AST-guided framework for translating natural language into first-order logic with LLMs.Source: §6 · p. 9
  • NL2LOGIC improves Logic-LM by 31% on both syntactic and downstream reasoning task accuracy.The framework incrementally constructs an AST to strengthen control over generated output.Source: §6 · pp. 9–10

Ethical Considerations

The work uses publicly available datasets and models, with no human subjects or newly collected data, and identifies interpretive risks when assessing automated proofs.

Ethical Considerations

  • The study uses public datasets and models, collects no new data, and involves no human subjects or personal, private, or sensitive information.The authors state that datasets and models are used according to their licenses.Source: Ethical Considerations · p. 10
  • An entailment result alone may not establish a hypothesis if its negation is also entailed or the premises are unsatisfiable.The paper advises examining entailment of both the hypothesis and its negation, as well as premise satisfiability.Source: Ethical Considerations · p. 10
  • The authors acknowledge using AI assistants for grammar checking and retain responsibility for the scientific claims and results.Source: Ethical Considerations · p. 10

Limitations

NL2LOGIC translates one sentence at a time, so it does not yet resolve cross-sentence coreference or implicit relational links; deployment also depends on structured-output support.

Limitations

  • Sentence-by-sentence translation does not yet handle coreference or implicit relational links across sentences.For example, separately translating “father” and “parent” can yield distinct relations, while full context could express father as parent and male.Source: Limitations · p. 10
  • NL2LOGIC relies on structured JSON output, which some LLM serving frameworks do not support natively.The paper gives llama.cpp as an example, requiring integration with lm-format-enforcer for structured output.Source: Limitations · p. 10

A System Prompts

The prompts organize parsing into recursive specialized stages, classifying sentence structure before extracting the logical components needed to build an AST.

A System Prompts

  • ParserSelector classifies each sentence as atomic, quantified, compound, or negated before routing it to a specialized parser.The remaining parsers can recursively invoke ParserSelector for child nodes.Source: A System Prompts · p. 13, Figure 7 · p. 13
  • The quantified-sentence prompt extracts the quantifier, variable, and scoped sentence, while the binary-operator prompt extracts the operator and its two operands.Source: Figure 8 · p. 13, Figure 9 · p. 14
  • The negation prompt asks the parser to extract the sentence without its negation operator.Source: Figure 10 · p. 14
  • Atomic-sentence prompts first identify predicate type, then extract the subject and predicate, adding object arguments for transitive and ditransitive structures.Ditransitive parsing also extracts direct and indirect objects, using the verb’s base form.Source: Figure 11 · p. 15, Figure 12 · p. 15, Figure 13 · p. 16
  • Ditransitive examples map sentences such as “John gave Mary a book” to a subject, base-form verb, indirect object, and direct object.Source: A System Prompts · p. 17

Related papers

Loading 2602.13237v1…