Are Language Models Efficient Reasoners? A Perspective from Logic Programming

AI summary

Overview

• Research area: Natural language processing and the evaluation of deductive reasoning in language models, framed through logic programming and formal proof theory.
• Technical level: Advanced. The paper builds on typed logic programs, fixpoint (least-model) semantics, hypergraphs and hyperpaths, proof forests, and forward-chaining theorem proving.
• Scope: The paper proposes a framework for measuring how efficient—not merely correct—a language model's deductive reasoning is, by aligning natural-language proofs generated by an LM with shortest proofs obtained by executing an underlying logic program, and demonstrates the framework on grade school math word problems injected with irrelevant axioms.

What This Paper Is About

Standard evaluations of language model reasoning check whether the final answer is correct, not whether the reasoning path was economical. In realistic problems, most available information is irrelevant, and an efficient reasoner must ignore it rather than chase true-but-useless conclusions. The paper asks how well current LMs avoid unnecessary inference, defines efficiency formally via logic programming, and empirically tests LMs on math word problems deliberately polluted with irrelevant axioms.

Key Contributions

1. A logic-programming framework for reasoning efficiency. The paper formalizes deductive reasoning as proof search in a logic program, defines a proof as an (A, h_g)-proof, defines the shortest proof as the (A, h_g)-proof with the fewest vertices, and quantifies efficiency as efficiency(P) = |P★| / |P|, where |P★| is the number of vertices in a shortest proof and |P| is the number of vertices in the LM's proof. Axioms that appear in no shortest proof are defined as irrelevant.

2. Verbalized logic programs as a bridge from natural language to proofs. Each theorem in a logic program is associated with a set of natural language strings, so that a natural-language proof produced by an LM can be mapped onto the deductions of the logic program. The authors argue this disentangles two sources of inefficiency that token-count proxies conflate: (1) unnecessary deduction steps and (2) verbosity in the natural-language strings expressing those steps—with the experiments emphasizing the former.

3. A dataset of GSM word problems with controllable irrelevant axioms. The paper constructs verbalized logic programs for grade school math word problems (GSM; Cobbe et al., 2021; Li et al., 2024; Zhang et al., 2024), adopting methods from Opedal et al. (2025), and injects irrelevant axioms that vary both in number and in semantic overlap with the goal theorem. This generalizes prior datasets that include only a single irrelevant statement (Shi et al., 2023; Mirzadeh et al., 2025). Problems are generated from scratch to avoid bias from memorizing the efficient solution seen during training.

4. Empirical characterization of LM accuracy and proof efficiency under distraction. The paper reports accuracy degradation and proof-level inefficiency, including an analysis of whether LMs exploit lexical overlap with the goal as a search heuristic.

Main Findings

• Accuracy drops with irrelevant information, even when minimal. Current LMs are less accurate on problems containing irrelevant axioms than on equivalent problems without them. The gap often persists in the simplest case—a single irrelevant axiom from the same domain—and grows larger as more irrelevant axioms are added.
• The drop is not just an input-length effect. The authors confirm the accuracy reduction is not due to longer inputs alone: LMs usually perform better on control problems of equal length that lack irrelevant content.
• LMs often get the goal but take unnecessary detours. For problems where an LM correctly produces the goal theorem, it predicts most of the correct intermediate theorems, but its proofs are frequently inefficient, exhibiting detours through irrelevant inferences.
• Inefficiency is severe once half the axioms are distractors. For GSM problems where about half of the axioms are irrelevant, more than half of the LM's predicted theorems are also irrelevant, i.e., not needed to prove the goal.
• Semantic overlap with the query drives inefficiency. The LMs are particularly inefficient when irrelevant axioms overlap semantically with the query—for example, when the question asks "how many cats does Ryan have?" and the irrelevant axioms also mention "Ryan" or "cats."
• Overlap may also be a useful heuristic. The same overlap results suggest that the LMs' search procedure sometimes employs a useful heuristic based on overlap with the goal theorem, analogous in spirit to goal-aware search strategies such as Earley's algorithm or magic templates.

Methodology in Plain English

The authors express each math word problem as a logic program: a set of axioms (facts such as "Ryan has 5 cats") plus inference rules that combine facts into new conclusions. Theorems that follow are computed by repeatedly applying the program's fixpoint operator starting from the axioms, giving a minimal Herbrand model. Because the programs include arithmetic and set-theoretic built-ins (integer addition, subtraction, multiplication, equality, comparison; set union, intersection, cardinality, set equality, cardinality comparison), deciding provability is undecidable in general; the authors restrict attention to queries whose variables range over a fixed, finite domain.

Reasoning in such a program can be viewed as finding a hyperpath in a hypergraph, where a hyperedge's tail nodes jointly produce its head node. A proof is a set of such hyperedges together with a labeling back to theorems; the shortest proof has the fewest vertices, and can be found by forward chaining (a search from axioms toward the goal, instantiable as DFS, BFS, Dijkstra's algorithm, A*, or goal-aware strategies such as magic templates).

To connect this to LMs, the authors use verbalized logic programs: every theorem is associated with natural language strings, so an LM's natural-language proof can be automatically parsed and aligned with theorems in the program. Alignment lets the authors compute the efficiency ratio |P★| / |P| for each LM proof. They then generate GSM problems and inject varying numbers of irrelevant axioms, varying how much those axioms overlap semantically with the goal theorem, and compare LM accuracy against control problems of equal length but without irrelevant content. The available text describes the modeling setup and experimental design; specific dataset sizes, model names, and numeric accuracy values are not reported in the provided paper content.

Why This Matters

• Research impact: The paper argues that correctness of a final answer does not guarantee a correct or economical proof, and that number of generated tokens is an ambiguous proxy for efficiency. It offers an automatic alternative—parsing LM output into logic-program proofs—instead of relying on manual scrutiny, heuristic proof checks, or proof assistants such as Lean, for which LMs may have less training data. It also positions efficiency as a first-class evaluation dimension alongside accuracy.
• Mathematical word-problem tutoring: systems that must grade not just the final answer but the solution path a student (or model) takes, including whether the path contains irrelevant steps.
• Reasoning over noisy contexts: legal, medical, or enterprise question answering where most retrieved or provided facts are irrelevant and where "true but irrelevant" conclusions are easy to derive.
• Retrieval-augmented and agentic pipelines: distinguishing models that waste steps on distractors from models that prune them, which matters for multi-step tool use and planning.
• Cost and compute control: reasoning models often generate far more tokens than necessary (Chen et al., 2025; Pu et al., 2025); a step-level efficiency metric supports training objectives such as length rewards while avoiding the failure mode of simply skipping necessary steps for a shorter output.

Industry relevance: the metric targets a real cost driver—lavish test-time compute in reasoning models—and offers a diagnostic that separates "the model rambles" from "the model searched the wrong part of the problem."

Future Directions

• Alternative graph-size definitions. The paper notes its definition of hypergraph size as |V| is non-standard (more commonly the number of hyperedges or the sum of their cardinalities) and that future work could easily adapt the efficiency metric to other definitions.
• Beyond finite-domain queries. The current setup restricts queries to variables with a known, finite domain, avoiding the full complexity of unification and non-ground reasoning; lifting this restriction is a natural extension.
• Other domains and scales. The experiments use GSM word problems; extending verbalized logic programs to other reasoning domains, and testing more models and scales, would test generality.
• Turning the diagnosis into a remedy. The finding that LMs are inefficient—but sometimes exploit goal-overlap heuristics—raises the question of how prompting, training, or search-time guidance could push models toward shortest proofs without dropping necessary steps.

Target Audience

Researchers in NLP and LLM reasoning evaluation; formal-methods and logic-programming researchers interested in connecting proof theory to natural language; practitioners building or auditing reasoning systems where solution-path quality and inference cost matter; and readers interested in automatic, non-manual evaluation of LM-generated proofs. Some background in logic programming or formal semantics is helpful, given the paper's use of signatures, Herbrand bases, fixpoint semantics, and hypergraphs.

Authors’ abstract

Modern language models (LMs) exhibit strong deductive reasoning capabilities, yet standard evaluations emphasize correctness while overlooking a key aspect of reasoning: efficiency. In real-world reasoning scenarios, much of the available information is irrelevant, and effective deductive inference requires identifying and ignoring such distractions. We propose a framework for assessing LM reasoning efficiency through the lens of logic programming, introducing a simple method to align proofs written in natural language -- as generated by an LM -- with shortest proofs found by executing the logic program. Efficiency is quantified by measuring how well a model avoids unnecessary inference. Empirically, we construct a dataset of math word problems injected with various number of irrelevant axioms that vary in semantic overlap with the goal theorem. We find that current LMs show marked accuracy declines under such conditions -- even with minimal, domain-consistent distractions -- and the proofs they generate frequently exhibit detours through irrelevant inferences.