PaperlayerView exact revision on arXiv

Source-linked AI summary

Testing the General Deductive Reasoning Capacity of Large Language Models Using OOD Examples

Abulhair Saparov, Richard Yuanzhe Pang, Vishakh Padmakumar, Nitish Joshi, Seyed Mehran Kazemi, Najoung Kim, He He

arXiv:2305.15269v3cs.CLcs.AI

TL;DR

Because proofs can grow beyond the coverage of available examples, the paper tests whether LLMs generalize from simpler demonstrations to more complex proofs. It introduces a programmable synthetic dataset and finds more robust generalization to compositional proofs than prior work suggested, alongside difficulty with longer proofs and certain hypothetical subproofs.

  • Problem

    Prior LLM evaluations of deduction focused largely on limited rules or same-distribution examples, leaving generalization to more complex proofs insufficiently tested.

    Source: §1 · p. 1

  • Method

    The paper builds PRONTOQA-OOD, a programmable synthetic dataset that controls deduction rules, proof depth, width, and composition for evaluating LLMs.

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

  • Results

    LLMs show more robust generalization to compositional proofs than previously suggested, but struggle with longer proofs and need demonstrations for proof by cases and contradiction.

    Source: §1 · p. 2, §5 · p. 9

  • Takeaways & Limitations

    In-context examples should be simple and cover diverse deduction rules, especially less familiar ones, with distractors for examples prone to overfitting.

    Source: §1 · p. 2

    The best in-context examples often come from distributions distinct from the test examples, and existing accounts do not explain this pattern.

    Source: §5 · p. 10

Abstract

from arXiv · show

Given the intractably large size of the space of proofs, any model that is capable of general deductive reasoning must generalize to proofs of greater complexity. Recent studies have shown that large language models (LLMs) possess some abstract deductive reasoning ability given chain-of-thought prompts. However, they have primarily been tested on proofs using modus ponens or of a specific size, and from the same distribution as the in-context examples. To measure the general deductive reasoning ability of LLMs, we test on a broad set of deduction rules and measure their ability to generalize to more complex proofs from simpler demonstrations from multiple angles: depth-, width-, and compositional generalization. To facilitate systematic exploration, we construct a new synthetic and programmable reasoning dataset that enables control over deduction rules and proof complexity. Our experiments on four LLMs of various sizes and training objectives show that they are able to generalize to compositional proofs. However, they have difficulty generalizing to longer proofs, and they require explicit demonstrations to produce hypothetical subproofs, specifically in proof by cases and proof by contradiction.

1 Introduction

The paper asks whether LLMs can extrapolate from simple demonstrations to increasingly complex proofs, beyond prior evaluations focused on limited rules and in-distribution examples. It tests this across proof rules, depth, width, and composition, finding robust compositional generalization alongside important limits.

1 Introduction

  • Because proof complexity can grow without bound and data cannot cover every proof size, general reasoning requires extrapolation from simpler proofs.Prior work showed some deductive ability with in-context and chain-of-thought prompting, but often focused on modus ponens and same-distribution tests.Source: §1 · p. 1
  • The study tests whether LLMs extrapolate beyond demonstrations across deduction rules, proof depth, proof width, and proofs combining different rules.Depth is the length of a sequential chain of steps; width is the number of premises per step.Source: §1 · p. 2
  • The findings favor simple, diverse in-context examples, especially demonstrations of less familiar rules, with distractors to reduce overfitting.The paper reports that models are more prone to overfitting on examples involving proof by cases and proof by contradiction.Source: §1 · p. 2
  • Across GPT-3.5 175B, PaLM 540B, LLaMA 65B, and FLAN-T5 11B, models generalize to compositional proofs, but some rules require explicit demonstrations and model size weakly correlates with performance.The rules most needing demonstrations are proof by cases and proof by contradiction; smaller instruction-tuned models can perform comparably to larger models.Source: §1 · p. 2
  • Existing datasets marked as varying in width, depth, and compositionality are not programmable, and splitting their examples can produce highly imbalanced sets.The paper identifies controllable generation as a distinction of its evaluation approach.Source: Table 1 · p. 3

2 Related work

Prior work studied out-of-distribution generalization in several reasoning tasks, but deductive evaluations often covered limited rules or proof dimensions. Research on in-context learning also offers multiple accounts of how demonstrations shape model behavior.

2 Related work

  • OOD studies span bit parity, variable assignment, semantic parsing, deduction, and arithmetic, but deductive reasoning studies were limited to modus ponens.On parity and variable assignment, scratchpad prompting enabled some generalization to longer inputs, though accuracy degraded as inputs grew.Source: §2 · p. 3
  • Many reasoning datasets rely on label accuracy, omit proof-width and compositional generalization, or focus on modus ponens; PRONTOQA is closest but lacks the broader rule and composition coverage.Some datasets contain examples of varying width, depth, and compositionality but are not programmable and yield imbalanced splits when divided.Source: §2 · p. 3
  • Prior accounts describe in-context learning as internal gradient descent or topic inference, while other work finds benefits from diverse, relevant, individually simple demonstrations.This paper situates its findings as evidence that in-context generalization differs from supervised learning and is not explained by gradient-descent accounts alone.Source: §2 · p. 3

3 Approach

PRONTOQA-OOD is a programmable synthetic dataset for testing reasoning over controllable proof rules and complexity. It generates proofs across propositional connectives, varying depth and width, and combines deduction rules recursively; distractors and formal proof checking support the evaluation.

3 Approach

  • PRONTOQA-OOD generates synthetic questions with premises, a query, and a gold chain-of-thought proof, with deduction rules, depth, and width as controllable parameters.It extends PRONTOQA, which generated proofs using modus ponens, to support systematic tests of proof complexity.Source: §3 · pp. 3–4
  • The dataset generates proofs using rules for conjunction, disjunction, implication, and negation, following natural deduction with some rules omitted from natural-text evaluation.Negation introduction and elimination, truth introduction, and falsity elimination are omitted; proof by contradiction is used to reason over negation.Source: §3 · p. 4
  • Proof depth is controlled by appending steps to a target depth, while proof width sets the number of premises in each deduction rule.Proofs are represented as trees whose nodes are steps and whose parent nodes are premises.Source: §3 · p. 5
  • Compositional proofs are generated recursively by selecting a deduction rule, choosing its premises, and generating a subproof for each premise.The recursive process yields proofs combining different types of deduction rules.Source: §3 · p. 5
  • Distractor sentences make shortcut heuristics less informative by requiring the model to choose the correct premise from multiple options.For example, a distractor adds a second possible consequence for the same category, so the model must select the valid next step.Source: §3 · p. 5
  • Predicted proofs are evaluated by parsing each chain-of-thought sentence into first-order logic, checking deduction steps, and verifying a path from premises to goal.The evaluation requires each step to be valid and to immediately follow one of its premises.Source: §3 · p. 5

4 Results

With 8-shot chain-of-thought prompting, the experiments compare in-distribution and out-of-distribution demonstrations across deduction rules, proof composition and size, and distractors. Models often generalize compositionally, but larger proof depth remains difficult and some rules require explicit demonstrations.

4 Results

  • The experiments used 8-shot chain-of-thought prompts and compared demonstrations drawn from the test distribution with demonstrations drawn from a different distribution.Results were reported with 95% confidence intervals.Source: §4 · p. 5

4.1 Can LLMs use deduction rules other than modus ponens?

  • Most models used the tested deduction rules reasonably well, with GPT-3.5 performing best; FLAN-T5 handled implication and conjunction elimination but not the other rules.The authors report no strong correlation between model size and performance; LLaMA performed comparably to PaLM despite being smaller.Source: §4.1 · p. 6, Figure 4 · p. 6

4.2.1 Can LLMs generalize to unseen deduction rules?

  • Without demonstrations of the test rule, models still used conjunction introduction, conjunction elimination, disjunction introduction, and, to some extent, implication elimination; no model used disjunction elimination or proof by contradiction without demonstrations.GPT-3.5 used modus tollens as an alternative route for proof by contradiction in some cases.Source: Figure 4 · p. 6, §4.2.1 · p. 7

4.2.2 Can LLMs generalize to compositional proofs?

  • In all but three experiments, the gap between in-distribution and out-of-distribution accuracy on compositional proofs was close to zero; GPT-3.5 and PaLM struggled with four rule types.Some models performed better with out-of-distribution demonstrations than with in-distribution demonstrations.Source: §4.2.2 · pp. 7–8, Figure 6 · p. 7

4.2.3 Can LLMs generalize to bigger proofs?

  • As proof depth increased, both in-distribution and out-of-distribution accuracy decreased; width generalization was stronger on conjunction elimination, while only GPT-3.5 generalized to wider conjunction-introduction proofs.GPT-3.5 on conjunction elimination was a notable exception: in-distribution accuracy stayed high as out-of-distribution accuracy fell.Source: §4.2.3 · p. 8, Figure 7 · p. 8

4.3 Do distractors help OOD generalization?

  • Performance was largely unaffected by distractors, with exceptions for a few rules and models; GPT-3.5 sometimes copied distractor sentences in implication and disjunction elimination.The authors attribute the copying to a likely heuristic learned from in-context demonstrations.Source: §4.3 · pp. 8–9, Figure 8 · p. 9

5 Conclusion and future work

The study systematically tests rule-, depth-, width-, and compositional generalization, finding mixed generalization to unseen rules but more robust generalization to compositional proofs. It leaves the mechanisms of in-context learning and chain-of-thought prompting, and how to choose demonstrations, as open questions.

5 Conclusion and future work

  • LLMs show mixed generalization to unseen deduction rules but more robust generalization to compositional proofs than previously suggested.Source: §5 · p. 9
  • The study tests rule-, depth-, width-, and compositional generalization of LLMs.Source: §5 · p. 9
  • The mechanism of ICL and CoT prompting remains a future research direction; current theories cited do not explain why the best examples often come from a different distribution than the test example.Source: §5 · p. 10
  • Further study is needed to characterize how example simplicity, rule diversity, and rules with poor OOD generalization affect demonstration choice.Source: §5 · p. 10

Reproducibility statement

The paper makes its generated data and analysis materials available, while noting that PaLM outputs are excluded. It also records when the reported model experiments were run.

Reproducibility statement

  • Model outputs except PaLM outputs, data-generation code, and analysis code are freely available under a permissive open-source license.Source: Reproducibility statement · p. 10
  • Generated data for all experiments is available in generated_ood_data.zip, and python make_plots.py produces the paper’s figures.Source: Reproducibility statement · p. 10
  • GPT-3.5 experiments ran April 20–23, 2023, while Figure 7 and the bottom row of Figure 8 experiments ran August 3–7, 2023.Source: Reproducibility statement · p. 10

A.1 Example from PRONTOQA-OOD

The example asks for a proof of a disjunctive conclusion about Polly and gives a chain-of-thought that derives one disjunct. The figure identifies it as a compositional example with minimum depth 4 and three rule types.

A.1 Example from PRONTOQA-OOD

  • The query asks to prove that Polly is a lempus, impus, or yumpus, and the expected chain concludes Polly is a lempus.Source: §A.1 · p. 15
  • The expected proof derives Polly’s lempus status from Polly being a wumpus and the rule that wumpuses are vumpuses, sterpuses, and brimpuses.Source: §A.1 · p. 15
  • The figure describes this as a compositional example with minimum depth 4 and three rule types, coloring the question blue, query red, and chain-of-thought/answer green.Source: Figure 10 · p. 15

A.2 Results with absolute accuracy

The figures report proof accuracy across deduction rules, compositional examples, and distractor conditions. Their captions specify the evaluation settings but do not state numerical outcomes.

A.2 Results with absolute accuracy

  • Figure 11 compares proof accuracy across deduction rules in same-distribution and out-of-demonstration settings, with dotted bars marking in-demonstration accuracy in the latter.The caption also specifies proof widths and depths for the rule-specific examples.Source: Figure 11 · p. 15
  • Figure 12 compares compositional-test accuracy when demonstrations are compositional at matching minimum depth and rule count versus demonstrations of individual rules.Source: Figure 12 · p. 16
  • Figure 13 compares distractor settings: distractors in both demonstrations and tests, distractors only in tests with different sentence ordering, and irrelevant-sentence replacements in demonstrations.The caption specifies rule-specific proof widths and depths.Source: Figure 13 · p. 16

A.3 Full examples of incorrect predicted proofs

The examples contrast incorrect generated proofs with expected proofs, showing how models can mishandle disjunction elimination and proof by contradiction. Other examples illustrate incorrect OOD proofs involving distractors or multiple rule types.

A.3 Full examples of incorrect predicted proofs

  • For Max, the predicted proof derives the goal using a single disjunct, while the expected proof assumes each disjunct in turn and establishes the goal in every case.The example makes the missing hypothetical subproofs explicit.Source: §A.3 · p. 17
  • The figures show incorrect GPT-3.5 proofs for OOD disjunction elimination, an example with minimum depth 2 and four rule types, and implication elimination with test distractors absent from demonstrations.The figure captions identify premises in blue and invalid steps in red.Source: Figure 14, Figure 15, Figure 16
  • For Polly, the predicted proof concludes she is not a lempus directly, whereas the expected proof assumes she is a lempus and derives a contradiction.The expected proof derives that Polly is a lorpus, conflicting with the premise that she is not a lorpus.Source: §A.3 · p. 17
  • The Sally example’s predicted proof includes several unrelated deductions before concluding she is dull, unlike the shorter expected proof from her being a brimpus.The expected chain uses the rule that every brimpus is a grimpus, then that every grimpus is dull.Source: §A.3 · p. 17

A.4 Generative process details

The appendix describes how examples for individual deduction rules are generated, with controls over proof depth and width. It also notes that implication introduction is omitted because its natural-language examples are difficult to control by those dimensions.

A.4 Generative process details

  • Linear ontologies and random walks generate implication-elimination examples of controllable depth, but their proof width is fixed at 1.Ontology edges become question sentences, and random-walk steps become the gold chain of thought.Source: §A.4 · p. 18
  • Conjunction introduction examples require proving all antecedent conjuncts before applying implication elimination, and the resulting conclusion can extend proof depth.The generated implication rule has a conjunction of n antecedents, where n is the proof width.Source: §A.4 · p. 18
  • Conjunction elimination examples place the conjunction in a rule’s consequent, allowing one of its conjuncts to be proved.The rule form has a consequent containing n conjuncts, where n is the proof width.Source: §A.4 · p. 18
  • Disjunction introduction examples use a disjunctive antecedent, for which one known disjunct suffices; the other disjuncts need no grounded axioms.The antecedent’s number of disjuncts is the proof width.Source: §A.4 · p. 18
  • Disjunction elimination examples require a disjunction and a subproof from each disjunct to a shared conclusion, with depth fixed at 1.The rule’s number of disjuncts is the proof width.Source: §A.4 · p. 18
  • Proof by contradiction examples use a negated goal-related axiom and subproofs, but their depth is fixed at 1 because nested applications are unnaturally complex.The target is a conjunction of negated premises; the proof also uses disjunction introduction, implication elimination, and conjunction introduction.Source: §A.4 · p. 18
  • The listed rules omit implication introduction because the authors say its natural-language examples are difficult to control by proof depth or width.The omission leaves the listed set short of a complete set of propositional natural-deduction rules.Source: §A.4 · p. 18

A.5 Generating compositional proofs

Compositional proofs are generated recursively from deduction rules and premises, while the evaluation procedure checks generated chains of thought against formalized logical steps. The appendix also describes distractors added to make proof steps less reliant on simple heuristics.

A.5 Generating compositional proofs

  • Compositional proofs are built by selecting a rule, selecting its premises, and recursively generating subproofs, with minimum depth and rule-type count configurable.Generation checks for contradictory axioms and avoids directly adjacent introduction and elimination rules.Source: §A.5 · p. 20, §A.6 · p. 20

A.6 Further details on evaluation of CoT

  • CoT evaluation parses sentences into first-order logic and checks whether each step follows from earlier forms using deduction rules, with flexibility for orderings of conjuncts and disjuncts.The evaluation also permits two additional inference rules, including modus tollens.Source: §A.6 · pp. 20–21

A.7 Generating distractors

  • Distractors add unhelpful concepts, rules, or axioms alongside proof-relevant material; disjunction elimination and contradiction receive multiple distractors to discourage heuristic solutions.The generator avoids existing predicates in distractor-rule consequents to prevent inconsistencies.Source: §A.7 · p. 21

Related papers

Loading 2305.15269v3…