Are Language Models Efficient Reasoners? A Perspective from Logic Programming

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

scope and contribution

This paper (NeurIPS 2025) builds a logic-programming testbed that separates arriving at a correct theorem from taking an efficient proof path. It represents grade-school math word problems as typed verbalized logic programs, generates shortest proofs, prompts language models to write natural-language proofs, parses those outputs back into theorem sequences, and compares them with the shortest proof. The formal object is a hypergraph proof forest. The paper defines efficiency as “EFFICIENCY(P) = |P⋆ |/|P| where |P⋆ | is the number of vertices in a shortest (A, hg )-proof” (section 3.2, p. 5). The experiments use two models whose outputs the parser can handle (Llama-3.1-8B-Instruct, Qwen2.5-Math-7B-Instruct) plus two reasoning models (QwQ-32B, DeepSeek-R1) that get only a cruder arithmetic-expression analysis (section 5, p. 9; section 5.2, p. 10; App. D.4, p. 28).

technique: typed logic programs and least-fixpoint semantics

What it is. Encode facts as typed atoms (cont, comp, transfer, rate, compeq) and rules as inference rules whose bodies may include arithmetic built-ins (table 1, p. 6). One rule (Rule 6, the frame-problem rule) uses negation. The least Herbrand model is obtained by iterating the fixpoint operator. The paper says “M is TP ’s least fixpoint” and calls its elements theorems (section 3.1, p. 4). Because of the built-ins, the paper says computing M is undecidable in general (section 3.1, p. 4); it shows decidability for its GSM program family under numerically consistent axiom sets (section 4.1, p. 7; App. B, p. 19).

How to do it. (1) choose typed predicate signatures; (2) define inference rules (all range restricted, section 3.1, p. 3); (3) choose a numerically consistent axiom set; (4) run forward chaining until the goal atom is proved (App. A.2, p. 19; Alg. 1, p. 20); (5) the query is answered by whether the goal atom is derived. Numerical consistency forbids two different quantities for the same agent set, entity and timestamp (section 4.1, p. 7). The paper’s example of a consistent axiom set is cont({ryan}, 5, cat, 2) with comp({eleanor}, {ryan}, 3, cat, 2); adding cont({andreas}, 7, cat, 2) and comp({eleanor}, {andreas}, 3, cat, 2) would make it inconsistent (section 4.1, p. 7).

Verus form. Inference: represent each atom as a Rust enum, rules as pure functions, and the finite model as a Set or sequence. Prove a loop invariant that every inserted atom is justified by an axiom or rule and a postcondition that the returned model is closed under the encoded rules. Termination requires a finite-domain bound; Verus does not automatically provide least-fixpoint semantics.

technique: verbalization with deterministic parsing

What it is. Map every grounded atom to a set of natural-language strings (a verbalizer); the sets for different atoms are disjoint, and each string ends in a period that appears nowhere else in the string. The paper states that these assumptions “allow for trivial linear-time parsing of natural language text into a sequence of atoms in the verbalized logic programs” (section 4.2, p. 7). The strings are generated with hand-written templates (section 4.2, p. 7).

How to do it. (1) create a finite set of hand-written templates for each atom; (2) keep the template sets disjoint; (3) end each string with the period separator; (4) prompt the LM with verbalized axioms and five verbalized shortest-proof examples (section 5, p. 9); (5) match each period-terminated string to an atom; (6) Inference: treat sentences with no template match as unmatched. In the paper’s manual check of the parser, an extra class represents that there is no match with any annotated theorem (footnote 14, p. 10). Built-ins are not verbalized except as part of the conclusion, and time is not verbalized directly but through a past form depending on context (Fig. 2, p. 7). The figure’s examples include “Alice has 3 apples.” and “Bob has 2 more apples than Alice.” (Fig. 2, p. 7).

Verus form. Inference: implement a deterministic parser over a finite vocabulary and prove that accepted strings map to exactly one atom. The uniqueness proof relies on the paper’s disjoint-template assumption; free-form language outside the templates is untrusted. The paper could parse only two of its four models’ outputs this way, since QwQ-32B and DeepSeek-R1 did not generate output in the verbalized format (section 5.2, p. 10; App. D.4, p. 28).

technique: shortest-proof generation and efficiency metric

What it is. Build a proof forest as a hypergraph whose hyperedges represent rule applications, then find a shortest source-to-goal hyperpath. The size of a proof is its number of vertices, and a model proof scores 1 only when it has as many vertices as the shortest proof (section 3.2, p. 5, including footnote 9). The paper says “A shortest proof can be found by forward-chaining” (section 3.2, p. 5), and that finding a shortest hyperpath can be done in polynomial time (section 3.2, p. 5).

How to do it in the paper’s experiments. The shortest proofs are not found by searching; they are sampled top-down from a goal theorem and are shortest by construction (Alg. 2, App. C.2, p. 22). (1) sample a goal cont atom, a maximum depth D from {1, 2, 3}, and an agent set of size 1 to 4 (App. C.2, pp. 21–22); (2) repeatedly sample an inference rule and a substitution for the current conclusion, using new agents so that no theorem is reused (App. C.2, p. 22); (3) for an elimination rule, make the last premise an axiom instead of expanding it (App. C.2, p. 22); (4) reject and resample when the arithmetic constraints cannot be satisfied (up to 1000 retries, App. C.2, p. 23); (5) score a model proof by |P⋆|/|P|, ignoring duplicate theorems and built-ins (section 5.2, p. 10, footnote 15). The paper proves that generated proofs are shortest and unique, including when irrelevant axioms are added, under conditions on the rules (Theorem 1 and Lemmas 1-2, App. C.4, pp. 23–25). By construction the relevant axioms are numerically consistent and all are used in the proof of the goal (section 4.3, p. 7).

Verus form. Inference: use a bounded queue and ghost predecessor map, with an invariant that each queue entry has a valid derivation. Prove that the returned path length is minimal only under finite, nonnegative edge costs and exhaustive exploration; those algorithmic assumptions must be made explicit. The paper’s generation route would instead need the C-conserving, E-monotonic and harmony conditions of App. C.

technique: two-stage prompting and proof parsing

The experiment gives five fixed in-context shortest-proof examples (section 5, p. 9), asks the model for a natural-language proof, maps it to a proof in the verbalized logic program, then prompts again conditioned on that proof to produce the goal theorem; the paper attributes the two-step strategy to Kojima et al. (2022) (section 5.1, p. 9; prompt in Fig. 6, App. D.2, p. 27). The paper states: “In the first step, the model is prompted to produce a natural-language proof outlining its reasoning process” (section 5.1, p. 9). Generation uses ancestral sampling with the context length restricted to 4000 tokens (section 5, p. 9).

Evidence. The dataset has 500 problems; the efficiency analysis is done on the problems with multiple irrelevant trees (section 5, p. 8; section 5.2, p. 9). Table 3 reports efficiency and exact matches for Llama-3.1-8B and Qwen2.5-Math-7B under query/overlap conditions; for example, Llama non-ground/no-overlap efficiency is 60.2 and exact matches are 15, while Qwen’s are 43.7 and 8 (Table 3, p. 10). The caption says these are “computed based on the problems for which the model got the correct final answer.” Parser spot checks, on theorems from 20 randomly sampled examples, were 394/397 = 99.2% for Llama and 381/384 = 99.2% for Qwen (footnote 14, p. 10). The denominator and model matter: these are conditional proof-efficiency results, not overall theorem accuracy. For QwQ-32B and DeepSeek-R1, the cruder arithmetic-only parser gives non-axiom efficiency of 77.1, 63.8, 72.2, 63.1 and 89.4, 67.7, 77.3, 67.8 across none, entity, agent and both overlap (Table 4, p. 29), with parsing accuracy of 94.4% and 94.8% on 20 problems (App. D.4, p. 28).

findings, trust, and VL implications

Adding irrelevant axioms lowers answer accuracy for all four models (Table 2, p. 8), most clearly for Llama-3.1-8B and Qwen2.5-Math-7B; DeepSeek-R1 is nearly saturated and shows only slight decreases (section 5.1, p. 9). Accuracy on problems with irrelevant axioms is almost always below that on length-matched control problems; the exception is Llama-3.1 with one irrelevant axiom (section 5.1, p. 9). The conclusion reports “proofs that exhibit frequent detours through irrelevant theorems” (section 6, p. 10). Inference: trusted components of the paper’s measurement include the hand-written rule system, template verbalizer, parser, arithmetic built-ins, and the assumption that sampled axioms are consistent. Inference: a Verus workflow can apply the same separation by measuring shortest verified proof obligations and flagging generated lemmas that are irrelevant, but proof minimality is a performance metric rather than a safety theorem. Inference: threat to VeruLaw is moderate: irrelevant generated lemmas increase review and solver cost, while formal postconditions still determine correctness.

techniques for the catalog

• typed least-fixpoint programs — represent facts and rules as a finite typed logic program and compute justified theorems by forward chaining
• disjoint verbalization — map atoms to uniquely parseable natural-language templates with separators
• shortest hypergraph proofs — generate minimum theorem paths by top-down sampling (or find them by forward chaining), then score detours by |P⋆|/|P|
• two-stage proof prompting — elicit a natural-language proof, parse it formally, and condition a final answer on that proof Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Our work highlights the need to improve models in terms of reasoning efficiency, as well as the advantages to viewing deductive reasoning through the lens of logic programming.”): read the whole paper text, including the appendices, and checked the quotations, Table 2, 3 and 4 numbers, section, page and footnote references, and the technique steps against it; changed the Horn-style wording, the “unique period separator” wording, the “reject unmatched text” step (the paper has a no-match class), the shortest-proof steps (the paper samples proofs top-down by Alg. 2 rather than reconstructing them from forward chaining), the page for the numerical-consistency guarantee (p. 7), the section pointer for the five-example prompt (section 5, p. 9), and the “all models” accuracy claim; added the reasoning-model analysis and parser limits; marked own conclusions as Inference; did not check the cited external works, the proofs in App. C beyond reading them, the code repository, or figures 3, 4, 5, 7 and 8 in detail.

Last edited: 2026-10-17