Are Language Models Efficient Reasoners? A Perspective from Logic Programming

TL;DR

We propose a formal, logic-programming–driven lens to evaluate LM reasoning efficiency by treating proofs as shortest $(S, v)$-hyperpaths in a proof hypergraph and by mapping LM-generated natural-language proofs to verbalized logic-program proofs via a disjoint verbalizer. The study constructs GSM word problems with multiple irrelevant axiom sets and analyzes how lexical overlap and the number of distractors affect accuracy and the prevalence of irrelevant intermediate theorems. Across models and settings, accuracy declines when irrelevant content is introduced, and LM proofs frequently detour through unnecessary steps, with efficiency quantified by the ratio of the length of the LM-produced proof to the shortest possible proof. The results demonstrate that token-based measures miss critical aspects of reasoning quality and highlight the value of a formal, proof-centric framework to diagnose and improve LM reasoning efficiency in structured tasks like math word problems. Overall, the paper provides a principled approach to assess and guide efficient deductive reasoning in LMs, with practical implications for designing prompts, architectures, and training objectives that encourage minimal, goal-directed inference. $| ext{Proof}^*|/| ext{Proof}|$ and the shortest $(S, v)$-hyperpath formalism offer concrete metrics and tools for future research on efficient reasoning in language models.

Abstract

Modern language models (LMs) exhibit strong deductive reasoning capabilities, yet standard evaluations emphasize correctness while overlooking a key aspect of human-like 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.

Figures (2)

• Figure 1: Example of a proof $\EuScript{P}$ of a goal theorem for the logic program presented in \ref{['tab:rules']}, with a shortest proof $\EuScript{P}^\star$ in blue and irrelevant theorems in red. We propose measuring efficiency as the size of the proof $|\EuScript{P}|$ relative to the size of the shortest proof $|\EuScript{P}^\star|$, penalizing the LM's proof for containing irrelevant theorems. We have omitted built-in predicates from this diagram for brevity.
• Figure 2: Examples of verbalized grounded atoms, i.e., elements of $\nu_{\mathcal{P}_{\text{W}}}(b)$ for some $b \in H$. Built-ins are not verbalized other than as part of the conclusion; \ref{['sec:prompt']} shows how this was done in our prompt. We additionally note that time is not verbalized directly but implicitly through the use of a past form depending on context.