PaperlayerView exact revision on arXiv

Source-linked AI summary

Probing for Long-Horizon Deductive Reasoning Capabilities in Language Models with Prolog

Hadeel Al-Negheimish, Jasna Ilieva, Yoon Kim

arXiv:2610.11592v1cs.CL

TL;DR

The paper asks whether frontier language models can sustain deductive reasoning over long contexts rather than merely retrieve information. It constructs a Prolog benchmark varying reasoning depth and context length, then finds that performance degrades substantially as depth grows.

  • Problem

    The paper asks how well language models can perform deductive reasoning as proof depth and context length grow, beyond retrieval over extended contexts.

    Source: §1 · p. 1

  • Method

    The authors construct PROLONG, a synthetic Prolog benchmark of 2,400 programs with reasoning depths up to 22 and contexts reaching 62k tokens.

    Source: §1 · p. 2, §3.3 · p. 3

  • Results

    Across 8 models, accuracy falls toward chance beyond depth 10, with GPT-5.5 at 67% accuracy at depth 20.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The results indicate that frontier models have not learned robust, generalizable backward-chaining inference even for simple linear proofs.

    Source: §5 · p. 5

    The generated programs exclude recursion, reasoning loops, and negation, and higher output-token budgets could improve accuracy at longer depths.

    Source: Limitations · p. 6

Abstract

from arXiv · show

Current frontier LLMs can theoretically process long contexts with 1M tokens or more. But to what extent can they go beyond simple retrieval and perform deeper reasoning over such long contexts? We empirically investigate long-horizon reasoning capabilities of LLMs, focusing on deductive logic expressed in Prolog. We construct ProloNg, a synthetic testbed to probe Prolog Long Reasoning, which systematically varies the complexity (reasoning depth) of problems, where the hardest case has a reasoning depth of 22 and 62k context length. We study 8 reasoning models across 5 families of frontier LLMs, and find that performance degrades substantially as reasoning depth grows, with the majority of models approaching chance beyond depth 10.

1 Introduction

The paper asks how far language models can sustain deductive reasoning as proof depth and context grow. It evaluates this with Prolog problems and finds substantial performance decline at greater depths.

1 Introduction

  • The motivating question is where reasoning models’ performance breaks down as they tackle deductions from premises using valid inference rules.The paper notes that such inferences matter in applications including policy compliance.Source: §1 · p. 1
  • The study operationalizes deductive reasoning as deciding whether a query follows from explicitly stated Prolog rules and facts.Correct answers require unifying variables, tracking argument order, and resolving subgoals against rules and facts.Source: §1 · pp. 1–2
  • PROLONG comprises 2,400 Prolog programs with reasoning depths up to 22, and context length grows with depth to a median of 62k tokens.The benchmark is designed to probe long-horizon reasoning alongside long-context processing.Source: §1 · p. 2
  • At depth 20, GPT-5.5 reaches 67% accuracy, while most evaluated models fail to perform above chance beyond depth 10.The authors attribute the broader difficulty to maintaining chains of substitutions and fact lookups as proof depth and context size scale.Source: §1 · p. 2

2 Related Work

Prior rule-based deduction benchmarks studied query answering but generally used shallow proof depths. This paper distinguishes its evaluation through deeper Prolog proofs and long contexts where every rule and fact is needed.

2 Related Work

  • RuleTaker, ProofWriter, and ProntoQA studied query answering over rules and facts, but ProofWriter and ProntoQA reached only five proof steps or hops.Earlier benchmarks found increasing difficulty as proof depth rose, while ZebraLogic reported sharp accuracy decline beyond a search space of 10^7 possibilities.Source: §2 · p. 2
  • Using Prolog rather than natural language avoids ambiguity and content effects that could let models draw on prior knowledge instead of the stated context.The cited concern is that natural-language evaluations may be affected by ambiguity and content effects.Source: §2 · p. 2
  • Unlike most extended-context retrieval and QA benchmarks, PROLONG requires every program rule and fact in the proof, preventing success by locating only a few relevant pieces.LongBench-v2, RULER, and HELMET generally treat reasoning and retrieval as independent axes in most tasks.Source: §2 · p. 2

3 PROLONG: Prolog Long Reasoning

PROLONG uses Prolog query answering to construct controlled tests of deductive reasoning. Its generated programs vary proof depth while constraining program structure and scaling context size.

3.1 Background: Prolog

  • Prolog programs contain facts and rules, and an interpreter evaluates a query by backward chaining until all subgoals are satisfied.A rule states that its head holds when its body literals hold; facts state unconditional truths.Source: §3.1 · p. 2

3.2 Data generation

  • The generator recursively builds rules for a provable query, then creates an unprovable counterpart by mutating a fact and balances both query types within each program context.Programs are restricted to acyclic rule structures without recursion or loops, enabling a single-chain proof without backtracking or unsuccessful branches.Source: §3.2 · pp. 2–3

3.3 PROLONG Benchmark

  • PROLONG contains 2,400 samples across depths up to 22, with median input length ranging from 133 tokens at depth 0 to 62k tokens at depth 22.Labels are verified using the SWI-Prolog interpreter.Source: §3.3 · p. 3

4 Results

Across the evaluated models, accuracy declines as proof depth grows, and many increasingly default to “unprovable.” Trace analyses find unfaithful explanations, while a shared-context evaluation finds that both context length and proof depth affect performance.

4.1 Experimental setup

  • The evaluation covers eight frontier reasoning models, with maximum output tokens set to 64k except for Qwen models, for which 82k tokens were recommended.When available, reasoning effort was set to high.Source: §4.1 · p. 3

4.2 How does depth affect performance?

  • Beyond depth 10, several models approach chance; GPT-5.5 maintains high accuracy through depth 16 before declining at depths 20–22.Claude-Opus-4.7 remains competitive with GPT-5.5 through depth 12, then deteriorates sharply and settles near chance at depth 22; context lengths remain within advertised limits.Source: §4.2 · p. 4

4.3 Models become more conservative

  • With labels balanced at every depth, many models increasingly predict “unprovable” as program complexity grows.Claude-Opus-4.7, DeepSeek-V4-Pro, and Kimi-K2.6 show pronounced bias beyond depth 10; Qwen3.5 models instead run out of tokens before answering, even at depth 10.Source: §4.3 · p. 4

4.4 What does the trace say?

  • Among GPT-5.5’s 84 true negatives, only 34 correctly cited the planted missing fact; DeepSeek-V4-Pro correctly identified it in only 11% of its true negatives.Most analyzed explanations did not faithfully track the derivation, and 97 of 100 provable queries in DeepSeek-V4-Pro traces were falsely claimed to be unsupported.Source: §4.4 · p. 5

4.5 Is it just context length?

  • With context length fixed across depths, both context length and proof depth have statistically significant, comparable effects on accuracy (β = −0.54 and β = −0.36, respectively; both p < 0.001).In the original benchmark, depth and context length are tightly correlated (r = 0.97), complicating attribution; in the shared-context setting their correlation is r = 0.0003.Source: §4.5 · p. 5

5 Conclusion

The paper studies long-horizon deductive reasoning in frontier LLMs using Prolog. It finds declining accuracy, conservative answer bias, and unfaithful traces, while a shared-context evaluation shows that both context length and proof depth affect performance.

5 Conclusion

  • The paper presents an empirical study of long-horizon deductive reasoning in frontier LLMs using Prolog.Across eight models, accuracy collapses toward chance beyond depth 10, driven largely by a conservative bias toward predicting queries are unprovable.Source: §5 · p. 5
  • Reasoning traces are often unfaithful to the actual derivation, citing missing facts or blockers that are not present.By disentangling depth from context length in a shared-context setting, the paper finds both independently and comparably degrade performance despite their near-perfect correlation in the original benchmark.Source: §5 · p. 5
  • The results suggest frontier models have not learned robust, generalizable backward-chaining inference, even for simple linear proofs.Source: §5 · p. 5

Limitations

The study is limited to a simple class of generated Prolog programs and faces constraints on reasoning-trace access, compute cost, and output-token budgets. It evaluates eight named frontier reasoning models.

Limitations

  • Generated programs exclude recursion, reasoning loops, and negation, limiting the framework to deductive reasoning at its simplest.The study also evaluates eight frontier reasoning models, both open-weight and proprietary.Source: Limitations · p. 6
  • Closed-source models provide only reasoning summaries, not the actual reasoning tokens, limiting analysis of their reasoning traces.Running the models is computationally expensive, and API access carries substantial costs.Source: Limitations · p. 6

A Models

  • Output-token budgets were 64k for most models and 82k for Qwen models; higher budgets might increase accuracy, especially at longer depths.The listed models are Claude-Opus-4.7, GPT-5.5, GPT-5.4-mini, DeepSeek-V4-Pro, Kimi-K2.6, Qwen3.6-27B, Qwen3.5-27B, and Qwen3.5-4B.Source: Limitations · p. 6, A Models · p. 6

B Practical Example

The practical example represents policy compliance as a Prolog query over rules and facts: whether Alice may access the HR portal. Its rules specify conditions for access and approval.

B Practical Example

  • The example frames policy compliance as the query of whether Alice may access the HR portal.It presents facts about system authorization, employee training, and identity confirmation alongside rules for access and approval.Source: B Practical Example · pp. 6–7
  • Access requires system approval and employee training; approval requires an authorized system and a verified employee.The example defines these conditions in the may_access and approved rules.Source: B Practical Example · p. 7
  • A separate background_checked rule is also included in the displayed program.The supplied example shows the predicate and rule heading but no rule body.Source: B Practical Example · p. 7

C PROLONG Data

PROLONG data context size grows with reasoning depth, and the section describes its context graph and symbolic-solver analyses. Accuracy declines more sharply for provable than unprovable queries as depth increases.

C PROLONG Data

  • Input-token boxplots for DeepSeek-V4-Pro show context size growing significantly with depth, with similar patterns across models and a slight increase for Claude-Opus-4.7.Figure 5 presents the context DAG for the example program.Source: C PROLONG Data · p. 7, Figure 4 · p. 7, Figure 5 · p. 7
  • The section reports SWI-Prolog median run times and reasoning traces by depth for provable and unprovable queries.It points to Tables 4 and 5 but provides no values here.Source: C PROLONG Data · p. 7

D Accuracy by provability

  • Accuracy deteriorates less drastically for unprovable queries than for provable queries as depth increases.The analysis divides accuracy by depth and target provability.Source: D Accuracy by provability · p. 7

E Growth of reasoning trace with complexity

Reasoning-trace length varies across models as depth grows. Some produce relatively short traces, while Qwen models show distinct non-monotonic or increasing output-length patterns.

E Growth of reasoning trace with complexity

  • GPT-5.5, Claude-Opus-4.7, DeepSeek-V4-Pro, and GPT-5.4-mini generate fewer than 20k output tokens across depths, with only modest increases.The passage suggests these models allocate reasoning budget efficiently regardless of problem complexity.Source: E Growth of reasoning trace with… · pp. 7–8
  • Qwen3.5 models’ output length continues to grow at the deepest levels, without necessarily improving their derivations.The passage describes this as expanding the thinking trace without necessarily improving derivations.Source: E Growth of reasoning trace with… · p. 8
  • Qwen3.6-27B output length peaks around depths 8–10 before plateauing at approximately 40k tokens; Kimi-K2.6 peaks around depth 16 before declining.The maximum output budget was 82k tokens.Source: E Growth of reasoning trace with… · p. 8

F Mixed-Effects Model Details

The section reports mixed-effects analyses of correctness across original and disentangled datasets, and describes the prompt used to elicit Prolog query answers.

F Mixed-Effects Model Details

G Prompt Template

  • The prompt defines variable/constants and negation-by-failure conventions, asks whether the `?-` query is provable, and requests a boxed 1/0 answer.Source: G Prompt Template · p. 9

H Full Example

The full worked example proves the query `p(o1, o2)` and returns 1.

H Full Example

  • Proving `p(o1, o2)` requires `q(o2, o1)` and `s(o1)`; `q(o2, o1)` follows from `r(o2)` and `t(o1)`, with `t(o1)` derived through `u(o1)` from `v(o1)`.The program supplies `s(o1)`, `r(o2)`, and `v(o1)` as facts.Source: H Full Example · p. 10
  • The example uses only positive literals; negation by failure is described but does not appear in the rules or query.The reasoning treats lowercase `o1` and `o2` as constants substituted for rule variables.Source: H Full Example · pp. 10–11
  • The query `p(o1, o2)` is provable, so the requested answer is 1.The example concludes that all subgoals are satisfied.Source: H Full Example · pp. 10–11
  • The proof concludes that `p(o1, o2)` is true and returns 1.Its required subgoals are satisfied by the facts and rules, with no negated literals or failures preventing the proof.Source: H Full Example · p. 12
Loading 2610.11592v1…