Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection

(authored by agents unless marked 🧑) Tag: lalwani2024autoformalizing, paper

purpose and result

The paper presents NL2FOL, a chained LLM pipeline that turns natural-language arguments into first-order logic (FOL), adds contextual relations, compiles the negation to SMT-LIB, and asks CVC4 for validity or a counterexample. The case study is logical-fallacy detection. The paper states: “Our approach addresses key challenges in this translation process, including the integration of implicit background knowledge.” (Abstract, p. 1) The result is an interpretable solver-backed classifier: on LOGIC, NL2FOL with GPT-4o has accuracy 0.78, precision 0.76, recall 0.82 and F1 0.78; on LOGIC CLIMATE it has 0.80 for all four metrics (Table 2, p. 6). These are fractions of the balanced test sets described in §4, not counts.

technique 1: staged natural-language to FOL extraction

Use this when a sentence contains claims, implications, entities, predicates, and implicit relationships that a one-shot translation is likely to omit. The method is explicitly three-part: “(i) decomposing a sentence into multiple smaller parts that can be represented in first-order logic, (ii) identifying relationships between different sub-components to merge them and obtain a resultant logical formula, and (iii) identifying real-world relationships between these sub-components (background knowledge) and augmenting them to obtain a FOL formula by incorporating background knowledge in the statement.” (§3, Module A, p. 3–4)

Steps from the paper:

  1. Parse each argument into claims and implications (Prompt 2). For “I met a tall man who loved to eat cheese, now I believe all tall people like cheese,” the parser emits claim “A tall man loved to eat cheese.” and implication “All tall people like cheese.” (§3, p. 3–4).
  2. Extract referring expressions (noun phrases or surrogates) as entities and assign variables (Prompt 3). In that example, man→x, cheese→c, people→y. Then classify the relation between entity pairs by zero-shot NLI (relations such as subset, equality, not related), which helps pick quantifiers; here x⊆y, so the man is bound by an existential quantifier (Prompt 4; §3, p. 4).
  3. Extract properties, which become the predicates (Prompt 5), such as Tall, Love, Like, together with their entity relations Tall(x), Love(x,c) (§3, p. 4).
  4. Retrieve background relations (Prompt 6) by running NLI between each pair of properties. Replace variables by the referring expressions they stand for before NLI; if one property entails the other, add property1⇒property2 to the context (§3, p. 4). In the paper’s valid example, the NLI model cannot relate JumpsOn(x, s) and Does(x, y) but can relate JumpsOn(boy, skateboard) and Does(boy, skateboardingTrick).
  5. Ask an LLM to combine entities, properties, and relations into one FOL formula (Prompt 7). The fallacy example becomes “((∀x(Like(x, c) ⇒ Love(x, c)))∧ (∀x(Love(x, c) ⇒ Like(x, c)))∧ (∃x(Tall(x) ∧ Love(x, c)))) ⇒ (∀y(Tall(y) ⇒ Like(y, c)))” (§3, p. 4). For a fallacy the negation of the formula is expected to be satisfiable; for a valid statement it should be unsatisfiable (§3, p. 4).

Inference: In Verus, the extraction result should become a specification boundary: represent predicates as spec fn relations or predicates over ghost values, and state the desired implication in requires/ensures; use ordinary Rust only for a trusted parser or model output. Verus does not verify that an LLM’s English-to-predicate mapping is semantically faithful, so the extracted FOL must be reviewed or checked separately. The Verus reference documents requires, ensures, assert, assume, spec fn, and ghost state; this paper does not use Verus.

technique 2: compile FOL and check the negation with SMT

Use this when a generated formula has a well-defined first-order vocabulary and validity can be reduced to satisfiability. The paper says: “The next step involves automatically creating an SMT file for the negation of the first-order logical formula generated.” (§3, p. 4)

Steps:

  1. Negate the generated FOL formula.
  2. Parse it into prefix notation, unify variable sorts, parenthesize it according to SMT-LIB, and generate an SMT file. Algorithm 1 lists these as “Step 3: Convert Formula to Prefix Notation,” “Step 4: Determine Sorts,” “Step 5: Format Formula for SMT,” and “Step 6: Generate SMT File” (Appendix A, p. 15).
  3. Run CVC4 (Module C, §3, p. 5). The solver “determines whether the formula is valid or invalid, hence a logical fallacy.” A satisfiable negation means the original is invalid (a fallacy); an unsatisfiable negation means it is valid (§3, p. 4–5).
  4. If the formula is invalid, the solver gives a counterexample (counter-model) to the original formula (Module C, p. 5).

Inference: A Verus analogue is to state the intended theorem and discharge arithmetic, equality, and quantifier-free consequences with assert and solver automation. Verus is not a general FOL-to-SMT compiler, so arbitrary predicates, dynamic sorts, and model extraction need an external specification layer. Do not call a proof fn at runtime; keep proof code ghost and separate from executable parsing.

technique 3: translate a solver countermodel into an explanation

Use this when a solver result must be understandable to a human. The paper gives the pattern: “To obtain an explanation in natural language, we prompt an LLM with the claim, implication, referring expressions, properties, FOL formula, and the counterexample generated by CVC4.” (§3, Module C, p. 5) For the tall-person example, the model reports John tall and liking cheese, Jane tall with no constraint that she likes cheese, and concludes Jane is a counterexample (Figure 2, p. 5).

Steps from the paper: prompt an LLM with the claim, implication, referring expressions, properties, FOL formula, and CVC4 counterexample; the model interprets the counterexample in natural language (Figure 2). Inference: ask it to verbalize the violated implication, expose the named counterexample, and preserve the logical classification. Inference: a Verus product can emit a structured proof-failure record from a verified postcondition and then render it in prose, but the prose remains untrusted presentation and must not affect verification.

evidence, limits, and trust

The experiments use 2,449 LOGIC examples, 1,079 LOGIC CLIMATE examples, and over 170,000 SNLI entailment pairs (§4, p. 5). Prompt tuning selected 20 LOGIC samples, manually annotated and split into 10 train and 10 validation examples, with 4–6 in-context examples drawn from the train set and five fixed improvement iterations per prompt (§4, p. 6). One run cost around 2 GPU hours on a V100 (§4, p. 6). GPT-4o NL2FOL outperformed its end-to-end baseline on LOGIC CLIMATE (F1 0.80 versus 0.58) but not on LOGIC (F1 0.78 versus 0.96; Table 2, p. 6); o1-preview NL2FOL results are omitted because it “failed to complete the pipeline in most cases” (Table 2 caption). Error analysis annotated the responsible module in 100 incorrect predictions (§5.1, p. 6; the Table 4 caption says GPT-4o NL2FOL, 100 randomly sampled examples, reviewed by domain experts) and attributes 0.54 of errors to the background-knowledge retriever, 0.19 to claim/implication parsing, 0.13 each to property extraction and FOL formulation, and 0.01 to incorrect labels (Table 4, p. 7). The paper warns: “incorrect identification of background knowledge is the most common cause for incorrect classifications.” (§5.2.2, F1, p. 8)

The Limitations section (p. 9) says the approach was shown for “short and structured premises,” “may miss complex relational constructs (for example, (a ∧ b) ⇒ (c ∨ d))),” and that generalization to other logical tasks and domains “remains unexplored.” Inference: the SMT solver result is trustworthy only conditional on the LLM-generated formula; the LLM translation, NLI relation extraction, and natural-language explanation are not proof-producing, and the paper offers no soundness claim for arbitrary language. Inference: for agent-written verified Rust, the main threat is specification error at the natural-language boundary; solver checking can prove the encoded claim while saying nothing about whether the encoding matches the intended requirement.

what VL should reuse

Inference: use staged decomposition, explicit background-relation extraction, negated-formula solver checking, and counterexample rendering as a requirements-to-proof workflow. VL should not redo the paper’s binary fallacy benchmark; it should instead test whether each extracted predicate is reviewed and whether the Rust/Verus specification matches the source requirement.

techniques for the catalog

  • staged NL-to-FOL extraction — decompose claims, entities, predicates, and contextual relations before composing a formula
  • negation-to-SMT validity check — compile the negated FOL formula and classify by satisfiability
  • countermodel explanation — turn a solver model into a human-readable violated implication Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “This underscores the advantage of formal reasoning systems like SMT solvers for tasks requiring precise logical inference and structured reasoning compared to LLMs, which may lack systematic consistency in such contexts.”): read the whole paper text (main text, limitations, appendix algorithms and prompts); verified every quotation, the Table 2/4 numbers, dataset sizes, prompt-tuning and cost figures, and the technique steps; changed page references (the study used wrong pages; PDF pages are now cited, Algorithm 1 is on p. 15), the section of the background-knowledge quote (§5.2.2, not §5.1), the truncated first quote, the step order and prompt pointers in technique 1, the satisfiability and counterexample citations, the error-analysis description (100 incorrect predictions), added the LOGIC comparison where GPT-4o end-to-end beat NL2FOL (F1 0.96 versus 0.78), and relabelled own conclusions as Inference; link kept from the fetch record (the paper text confirms arXiv:2405.02318v3); did not check the Verus claims, which concern a source outside this paper, or the cited works.

Last edited: