Research map / Large language models / Agents, code and math

Are Language Models Efficient Reasoners? A Perspective from Logic Programming

NeurIPS 2025 · Large language models › Agents, code and math · approach: LLM-guided program synthesis · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Proposes a logic-programming framework that measures LM reasoning efficiency by comparing natural-language proofs to shortest hyperpaths, using GSM-style problems injected with irrelevant axioms.

Problem

Standard LM reasoning evaluations measure only final-answer correctness and ignore efficiency, i.e., whether models avoid unnecessary inference steps when irrelevant information is present.

Approach

Verbalized logic programs map each theorem to natural-language strings, so an LM's natural-language proof can be parsed into theorems and compared against the shortest proof (hyperpath) found by forward chaining; efficiency is the ratio of shortest-proof size to model-proof size, disentangling unnecessary steps from verbosity.

Key results

• Accuracy drops with irrelevant axioms for Llama-3.1-8B (65.0 base to 41.0 with multiple irrelevant trees) and Qwen2.5-Math-7B (52.8 base to 23.5 with multiple trees).
• Efficiency scores for non-ground queries with no overlap are 60.2 (Llama-3.1-8B) and 43.7 (Qwen2.5-Math), falling to 34.0 and 31.1 when both agent and entity overlap.
• DeepSeek-R1 is nearly saturated at 97.6-99.4% accuracy across conditions.

Measured effects reported in the paper

Surprising findings

• QwQ-32B performs significantly better on control problems than on base problems, an outlier relative to other models.
• Llama-3.1-8B performance with one irrelevant axiom exceeds its length-matched control.

Limitations

• Only one domain (GSM-style math word problems) with synthetic verbalizations via templates.
• Efficiency analysis restricted to Llama-3.1-8B and Qwen2.5-Math-7B due to formatting; other models analyzed with a cruder arithmetic-only method.
• Shortest-proof size defined by number of vertices, a non-standard hypergraph size definition.

Experimental setup

Datasets: GSM8K

Benchmarks: synthetic GSM problems with irrelevant axioms (500 problems)

Metrics: answer accuracy efficiency (shortest proof vertices / model proof vertices) efficiency on non-axioms exact matches correct theorems proportion

Baselines: Qwen2.5-Math-7B-Instruct QwQ-32B DeepSeek-R1

Builds on: logic programming forward chaining GSM8K

Closest papers by meaning

• Reasoning-as-Logic-Units: Scaling Test-Time Reasoning in Large Language Models Through Logic Unit Alignment (ICML 2025 · similarity 0.90)
• Putnam-AXIOM: A Functional & Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs (ICML 2025 · similarity 0.89)
• RULEBREAKERS: Challenging LLMs at the Crossroads between Formal Logic and Human-like Reasoning (ICML 2025 · similarity 0.89)
• Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness (NeurIPS 2026 · similarity 0.89)
• ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning (ICML 2025 · similarity 0.89)
• Training Language Models to Reason Efficiently (NeurIPS 2025 · similarity 0.89)