Towards Logically Sound Natural Language Reasoning with Logic-Enhanced Language Model Agents

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

purpose and result

LELMA validates natural-language reasoning by coupling an LLM reasoner and translator to a symbolic Prolog solver. The testbed uses obfuscated Prisoner’s Dilemma, Stag Hunt, and Hawk–Dove games. The paper defines the architecture as “a framework that integrates LLMs with formal logic to enable validation and refinement of natural language reasoning.” (Abstract, p. 1) Comparing its failed-predicate signal on the initial attempts with manual correctness labels, detection accuracy is 84% for GPT-4o and 86% for Gemini 1.0 Pro (Tables 8–9, §5.2.1, p. 6; §6, p. 7). Feedback raises average correctness (mean of the three per-game percentages) from 22.22% to 77.78% for GPT-4o and from 18.79% to 36.65% for Gemini (Table 7 and §5.1.3, p. 6). The paper gives no single combined sample count for these averages. Inference: the Gemini percentages in Table 7 (e.g. 25.81, 17.24, 34.48) correspond to denominators of 31 and 29, not 30, so the Gemini per-game sample counts are not all equal to the 30 repetitions in Table 4; the paper does not explain this.

technique 1: separate reasoner, translator, and solver

Use this when an agent emits open-ended prose whose factual claims can be expressed as logic queries. LELMA has three components: the Reasoner generates natural-language reasoning, the Translator maps statements to queries, and a Prolog Solver evaluates those queries (§3.1, p. 3; implemented in Python and SWI-Prolog). A fourth element, the feedback loop, returns natural-language feedback to the Reasoner when a query fails (§3.1, Fig. 1, p. 3). The paper states: “The source code of the framework and the results of the experimental evaluation are publicly available.” (§3.1, p. 3)

Steps:

1. Give the payoff matrix and task instruction to the Reasoner.
2. Pass its reasoning to the Translator (if it yields no queries, Algorithm 1 accepts the reasoning as is), which emits a set Q of predicates such as higher(1,3) or highest_mutual_payoff(R,R) (Table 3, §3.3, p. 4). Translation is one-shot: the prompt lists predicates with sample arguments and natural-language descriptions, and the predicate set comes from “a preliminary analysis of common LLM reasoning errors in the evaluation task” (§3.3, pp. 4–5). GPT-4o is the Translator in both setups (§4.2, p. 5).
3. Evaluate each query in the Solver; discard syntactically invalid or unexpected query forms and replace constants outside the allowable set with variables (§3.3, p. 5).
4. If every query is true, accept the reasoning; otherwise the Solver identifies correct variable values for failed predicates, these are translated back into natural language as feedback (§3.3, p. 5), and the Reasoner retries up to the attempt limit.

Inference: In Verus, this is a useful separation of concerns: a ghost/specification layer should encode the claims, and a verified function should establish postconditions. Verus can prove the encoded predicates but cannot validate that an LLM mapped prose to the right predicates. Keep the translator’s mapping auditable and treat it as an assumption unless independently reviewed.

technique 2: executable situation-calculus game model

Use this when reasoning depends on state transitions and payoffs rather than isolated arithmetic. The solver’s game-independent rules recursively move from an initial situation to a final one: game(F,F) if final(F) and game(S,F) if not final(S) and legal(M,S) and game(do(M,S),F) (§3.2.1, p. 3). Fluents persist unless an abnormal rule terminates them (§3.2.1, p. 3). A game-dependent specification defines initial, legal, initially, effect, abnormal, final, and finally predicates (§3.2.2, p. 4).

For the Prisoner’s Dilemma, define players and roles in s0, represent moves as choice(P,M), declare D or C possible for each player and legal only for a player with control, record effect(did(P,M),choice(P,M),S), and terminate control after a move (§3.2.2, p. 4). Declare the four payoff facts, then query game(s0,F), finally(goal(p1,5),F); the solver returns both legal move orders that give p1 utility 5 (§3.2.2, p. 4).

Inference: A Verus form would model a finite game state as a Rust datatype or ghost sequence and state transition invariants with invariant blocks on loops. Use requires for legal-state assumptions and ensures for payoff claims. The Prolog model’s closed-world negation and backtracking do not carry over automatically; they must be represented as explicit predicates and proved.

technique 3: check-then-refine reasoning loop

Use this when an agent can improve its explanation after receiving precise logical failures. Algorithm 1 initializes attempts, generates reasoning, translates it, returns immediately if no queries exist, otherwise solves the queries, returns if all succeed, or replaces the instruction with feedback from failed queries; it stops at max_attempts and returns the last reasoning (Algorithm 1, p. 3; §3.4, p. 5 calls it “Listing 1”). The Figure 1 caption states the purpose: “If any of the queries fail, the Reasoner is prompted to refine its reasoning in light of the facts derived from the failed queries.” (Fig. 1, p. 3)

The feedback example turns a false comparison, “payoff 3 is higher than 5,” into the correction “payoff 3 is lower than payoff 5” (§3.4, p. 5). The feedback prompt also lets the agent reaffirm its original reasoning, to allow for incorrectly translated queries (false positives). The paper says the Solver “guarantees the correctness of the generated feedback,” but some feedback, such as that suggesting a particular choice yields a higher guaranteed payoff, “may potentially bias the agent’s reasoning toward that option” (§3.4, p. 5).

Inference: In Verus, use verifier diagnostics to propose a new contract or proof step, then rerun verification. Never let the agent mutate a verified specification silently: record each attempt, require the final contract to pass semantic review, and cap retries to prevent unbounded proof search.

technique 4: conservative correctness evaluation

Use this when the target output is open-ended prose and “correct” means no logical or mathematical error, rather than one required action. The authors deliberately obfuscate familiar game labels (actions become ‘B’ and ‘R’; §4.1, p. 5) and treat both actions as valid when justified by risk aversion or cooperativeness (§4.3, p. 5). Three independent evaluators review every sample; a sample is correct only if all agree (§4.3, p. 5). The paper says: “A reasoning sample is marked as incorrect only if it contains logical or mathematical errors related to payoff assignment or inference” (§4.3, p. 5), and misuse of game-theoretic terminology does not count against correctness.

Detection accuracy compares the manual label (ground truth) with whether any predicate failed (predicted correctness), on initial attempts: 84% for GPT-4o and 86% for Gemini, with Hawk–Dove the hardest (73% and 81%, respectively; Tables 8–9, §5.2.1, p. 6). Human inter-rater Fleiss κ is 0.31 for GPT-4o and 0.59 for Gemini (§5.2.2, p. 6). LLM judges are unreliable in the harder GPT-4o case: Claude 3.7 Sonnet’s agreement with aggregated human judgment is κ=0.301, while GPT-4o as judge is κ=0.159; for Gemini’s reasoning the values are 0.555 (Claude) and 0.044 (GPT-4o) (§5.2.2, p. 7).

Inference: the paper says “false positives were more common than false negatives” and defines a false positive as correct reasoning flagged as erroneous (§5.2.1, p. 6). The matrices do not show that: wrongly flagged correct samples number 2 (Gemini) and 5 (GPT-4o), while missed errors number 11 and 9. The paper’s Limitations paragraph (§6, p. 7) also swaps the consequences of the two error types relative to §5.2.1, so its false-positive and false-negative terminology is inconsistent.

Inference: For verified Rust, use a rubric that distinguishes contract validity from behavioral desirability and requires unanimous or adjudicated review for semantic correctness. A judge model can prioritize cases but cannot replace proof or human review.

evidence, trust, and limits

Setup: 30 repetitions per game, five maximum attempts, temperature 1, 1024 maximum output tokens (Table 4, p. 5); the Reasoner is GPT-4o or Gemini 1.0 Pro, the Translator GPT-4o (§4.2, p. 5). Table 5 counts sum to 90 for each model. GPT-4o needed one or two attempts for 78% of samples; Gemini reached the five-attempt limit for 27%, and 83% of those remained incorrect (§5.1.1, p. 5). In the GPT-4o experiments, the model generated an average of 1224.38 response tokens and a reasoning attempt took 16.53 seconds on average; a Gemini attempt took 34.66 seconds (§5.2.3, p. 7). The solver is trusted for the encoded rules, but translation, predicate coverage, and human labels remain failure points. The authors note that Gemini produced payoff errors outside the predicate set and that imperfect translation can cause false negatives and false positives (§6 Limitations, p. 7). The evaluation was manual, which the authors say limited the sample size (§6, p. 7). Inference: for agent-written verified Rust, the threat is a complete proof of an incomplete predicate vocabulary; adding more solver rules does not establish coverage of all relevant behavior.

what VL should reuse

Reuse modular natural-language-to-query translation, executable state-transition specifications, bounded feedback loops, and conservative semantic review. VL should not treat solver success as evidence that the natural-language reasoning was fully represented; measure translation coverage and inspect false positives caused by unsupported predicates.

techniques for the catalog

• modular reasoner–translator–solver — separate prose generation, logical extraction, and symbolic checking
• executable state model — encode legal transitions, fluents, termination, and payoffs as a logic program
• check-then-refine loop — feed failed predicates back to the reasoner for bounded self-correction
• conservative semantic evaluation — require independent reviewers to agree that reasoning has no payoff error Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Thus, we adopted a conservative aggregation method, labeling a sample as correct only if all evaluators agreed on its correctness.”): read the whole paper text and checked every quotation, number (Tables 4-9, accuracies, kappas, tokens, times), algorithm step, Prolog rule description and section/page reference against it, with PDF page numbers from pdftotext; changed the page references for §3.1, Algorithm 1, Figure 1, §3.3, §3.4, §4.3 and §5.2.2, attributed the “If any of the queries fail” sentence to the Figure 1 caption, corrected the bias claim in §3.4, completed the technique steps and setup details, added an Inference on the Table 7 sample sizes, added an Inference on the paper’s inconsistent false-positive wording, and switched the link to https. Not checked: the linked repository, the cited references, and the Verus-related Inference paragraphs, which are my own reasoning and not claims of the paper.

Last edited: 2026-10-17