PaperlayerView exact revision on arXiv

Source-linked AI summary

Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought

Abulhair Saparov, He He

arXiv:2210.01240v4cs.CL

TL;DR

It is unclear whether LLMs genuinely reason through chain-of-thought or exploit pretrained knowledge and shortcuts. Using PRONTOQA to formally analyze symbolic proofs, the paper finds that models make valid deduction steps but struggle to plan proofs when multiple steps are available.

  • Problem

    Existing benchmarks do not clearly distinguish genuine chain-of-thought reasoning from retrieving pretrained knowledge or exploiting task shortcuts.

  • Method

    The authors create PRONTOQA, a synthetic fictional QA dataset generated from symbolic ontologies and proofs whose chain-of-thought can be parsed into formal proofs.

  • Results

    LLMs generally produce valid individual proof steps, but struggle to select the correct path when multiple valid steps are available.

  • Takeaways & Limitations

    PRONTOQA shows that LLM reasoning can be formally assessed beyond answer accuracy, revealing a distinction between local deduction and proof planning.

Abstract

from arXiv · show

Large language models (LLMs) have shown remarkable reasoning capabilities given chain-of-thought prompts (examples with intermediate reasoning steps). Existing benchmarks measure reasoning ability indirectly, by evaluating accuracy on downstream tasks such as mathematical reasoning. However, it is unclear how these models obtain the answers and whether they rely on simple heuristics rather than the generated chain-of-thought. To enable systematic exploration of the reasoning ability of LLMs, we present a new synthetic question-answering dataset called PrOntoQA, where each example is generated from a synthetic world model represented in first-order logic. This allows us to parse the generated chain-of-thought into symbolic proofs for formal analysis. Our analysis on InstructGPT and GPT-3 shows that LLMs are quite capable of making correct individual deduction steps, and so are generally capable of reasoning, even in fictional contexts. However, they have difficulty with proof planning: When multiple valid deduction steps are available, they are not able to systematically explore the different options.

1 INTRODUCTION

Chain-of-thought prompting improves LLM performance on reasoning tasks, but existing evaluations leave their underlying reasoning ability unclear. The study therefore evaluates InstructGPT and GPT-3 on PRONTOQA, finding strong individual proof-step validity but difficulty with proof planning.

  • 1 INTRODUCTION: LLMs achieve much higher question-answering accuracy with chain-of-thought examples than with standard question-answer prompting.Each example pairs a question with intermediate reasoning and a label.
  • 1 INTRODUCTION: Existing evaluations make LLM reasoning ability difficult to isolate because they primarily use real-world question-answering tasks such as math word problems.These settings introduce confounding factors beyond the reasoning process itself.
  • 1 INTRODUCTION: PRONTOQA supports systematic evaluation by generating an ontology and then constructing a proof from that ontology for each example.The study varies task-complexity factors including ontology type and the number of required proof steps.
  • 1 INTRODUCTION: InstructGPT and GPT-3 generally produce valid individual proof steps, including for fictional and counterfactual ontologies, but struggle with proof planning.The planning difficulty arises when models must navigate among multiple possible deduction steps.

2 RELATED WORK

The work positions PrOntoQA among formal and natural-language reasoning datasets while emphasizing parseable proofs and direct measurement of chain-of-thought reasoning. It also distinguishes this goal from prompting extensions and prior in-context-learning studies focused on non-reasoning tasks.

  • Reasoning datasets: PrOntoQA is most closely related to PROOFWRITER (Tafjord et al., 2021) and FOLIO (Han et al., 2022), but FOLIO lacks easily parseable proofs or chain-of-thought examples.FOLIO evaluates predicted labels, which may not necessarily reflect the reasoning process.
  • Chain-of-thought prompting: CoT prompting extensions can improve elicited reasoning behavior, including for smaller models, but this work measures reasoning ability elicited by CoT rather than proposing a new prompting method.The related prompting studies include Creswell et al. (2022), Wang et al. (2022), Creswell & Shanahan (2022), Anil et al. (2022), and Dohan et al. (2022).
  • Reasoning paradigms: Prior work studies reasoning over formal symbolic languages or directly over natural language, whereas this work connects fictional-world question answering with formal analysis.The cited approaches include neuro-symbolic methods, semantic parsing, and natural-language reasoning.
  • In-context learning: Prior in-context-learning studies found prompt-sensitive performance on sentiment classification and simple arithmetic, leaving unclear whether their findings generalize to reasoning.Those tasks could potentially be solved through retrieval rather than reasoning.

3 PRONTOQA: A SYNTHETIC DATASET FOR LOGICAL REASONING

PRONTOQA is a synthetic question-answering dataset generated from symbolic ontologies and proofs to enable formal analysis of predicted chain-of-thought. Its examples are uniquely parsable into logical forms, with controllable proof sizes and true-or-false queries derived from proof conclusions or their negations.

  • PRONTOQA generates each question from a symbolic ontology and proof, enabling formal analysis of the predicted chain-of-thought.The dataset is designed so its natural-language examples can be mapped back to symbolic structures.
  • Proofs are built by chaining modus ponens, allowing their sizes to be controlled systematically.Modus ponens derives g(a) from ∀x(f(x) →g(x)) and f(a), providing a simple compositional deduction rule.
  • Each example contains a context, query, chain-of-thought, and label, with sentences uniquely translated into symbolic logical forms for analysis.The inverse translation from examples to formal representations is intentionally simple.
  • Queries use the proof grammar to express an initial axiom and randomly ask whether the proof conclusion or its negation is false, with probability 0.5.The generated natural-language query is paired with a corresponding true-or-false label.

4 FORMAL ANALYSIS OF PREDICTED PROOFS

The analysis evaluates whether predicted chain-of-thought derives answers for the right reasons by testing both local deduction correctness and global proof planning. It parses each sentence into logical form and categorizes proof steps by validity and usefulness toward the goal.

  • 4 FORMAL ANALYSIS OF PREDICTED PROOFS: Predicted proofs are analyzed for both local correctness of individual deduction steps and global correctness in planning toward the query’s proof.This moves beyond evaluating only whether the final answer is “true” or “false.”
  • 4 FORMAL ANALYSIS OF PREDICTED PROOFS: Each chain-of-thought sentence is recursively parsed into logical form, then checked for provability from preceding forms using deduction rules.The resulting logical form represents the conclusion of a proof step.
  • 4 FORMAL ANALYSIS OF PREDICTED PROOFS: Proof steps are categorized by validity, distinguishing strictly-valid steps derivable with gold-proof rules from broadly-valid steps requiring a more powerful calculus.Unparseable steps are marked incorrect, while strictly-valid atomic correct steps are called canonical steps.
  • 4 FORMAL ANALYSIS OF PREDICTED PROOFS: A strictly-valid step can still be misleading when it does not advance the proof toward the target query.For example, proving that Fae is a mammal is valid but does not help establish that Fae is not herbivorous.

5 RESULTS

Across PrOntoQA experiments, LLMs often produce valid individual proof steps but struggle with proof planning, especially for longer or directionally difficult proofs. Reasoning performance also depends strongly on model size and real-world knowledge, while label accuracy does not reliably measure proof correctness.

  • Evaluation metrics: Label accuracy is not well correlated with strict or broad proof accuracy, indicating that correct labels can arise without correct generated proofs.Label accuracy correlates better with skip and valid-proof accuracy than with strict or broad proof accuracy.
  • Model size: Only text-davinci-002 reasons better than chance; larger models improve proof accuracy and produce fewer invalid steps.Proof accuracy increases from 350M to 1.3B and 6.7B models, but only text-davinci-002 performs better than chance.
  • Ontology type: The model performs comparably on fictional and “false” ontologies but relies heavily on real-world knowledge, limiting generalization to novel settings.The fictional and “false” ontology settings yield comparable performance, whereas reasoning is substantially affected by whether the ontology aligns with real-world knowledge.
  • Proof complexity: Reasoning handles 1- and 3-hop examples but falls to chance on 5-hop top-down proofs, with traversal-direction sensitivity increasing as proofs lengthen.Top-down traversal reverses the bottom-up ordering mirrored by the gold proof steps, which may make longer proofs more difficult.
  • Proof-step analysis: Most predicted proof steps are strictly valid, but incorrect proofs usually contain misleading or invalid steps, while some correct proofs recover after such mistakes.In 5-hop fictional examples, 93.2% of steps are strictly valid, 2.4% broadly valid, and 5.9% invalid; 2.4% are non-atomic.
  • Proof planning: INSTRUCTGPT most often first makes a strictly-valid atomic misleading step, then cannot return from an incorrect branch, revealing a proof-planning weakness.Smaller models more often begin with invalid or non-atomic steps, whereas larger models more often begin with strictly-valid atomic misleading steps.

6 CONCLUSION AND FUTURE WORK

The work introduces PRONTOQA, a synthetic fictional QA dataset for evaluating LLM reasoning, and finds that models can reason but struggle with proof planning when multiple proof steps are available. The dataset and approach may support comparisons with human reasoning and further study of LLM reasoning.

  • Conclusion: PRONTOQA evaluates LLM reasoning in synthetic fictional worlds; INSTRUCTGPT and GPT-3 generally reason correctly but struggle to select proof steps when multiple options exist.The largest model was generally able to perform reasoning, while having difficulty with proof planning.
  • Future work: PRONTOQA and the broader approach could support comparisons between LLM and human reasoning and exploration of LLM reasoning capabilities.
  • Reproducibility: The authors provide model outputs, data-generation code, and analysis code under a permissive open-source license for reproducibility.The main experiments used the OpenAI API on September 9–11, 2022; self-consistency ran October 29–30, and DFS ran November 16.

A APPENDIX · A.1 DEDUCTION RULES

PRONTOQA uses a restricted proof calculus with two deduction rules, and every proof is composed solely of instances of these rules. The appendix illustrates the rules through generic notation and a cat-to-carnivore example.

  • A.1 DEDUCTION RULES: The deduction-rule presentation pairs formal schemas with concrete examples to clarify how the restricted calculus operates.The appendix labels the rules in general form and then shows their application to the Fae example.
  • A.1 DEDUCTION RULES: One illustrated deduction concludes that Fae is a carnivore from Fae being a cat and all cats being carnivores.This example instantiates the rule with the facts “Fae is a cat” and “All cats are carnivores.”
  • A.1 DEDUCTION RULES: The example treats “Fae is a cat” as an axiom before applying the deduction.The axiom is represented as cat(fae).
  • A.1 DEDUCTION RULES: PRONTOQA proofs use only two deduction rules in the restricted proof calculus.These two rules constitute the calculus used in the experiments, and all proofs are composed of their instances.
  • A.1 DEDUCTION RULES: The rules are specified in general form using arbitrary expressions A, f(a), and g(a).In f(a) and g(a), variables are substituted with terms a.
  • A.1 DEDUCTION RULES: Figure 6 provides the formal specification of the two rules used throughout PRONTOQA proofs.It defines the expression notation and the substitution convention underlying the calculus.

A.2 AVOIDING SHORTCUTS

PrOntoQA removes question shortcuts that let InstructGPT guess truth labels without reasoning. Because the model can use property mentions as a heuristic, the dataset adds disconnected distractor concepts with the queried negation property.

  • A.2 AVOIDING SHORTCUTS: PrOntoQA removes shortcuts because, without distractors, InstructGPT predicts “true”/“false” labels almost perfectly.
  • A.2 AVOIDING SHORTCUTS: InstructGPT can infer truth from whether the queried property is mentioned in the context, regardless of the blank’s content.
  • A.2 AVOIDING SHORTCUTS: To neutralize this heuristic, each example adds a disconnected novel concept assigned the queried negation property as a distractor.

A.3 EXAMPLE INSTRUCTGPT MISPREDICTION

An InstructGPT example shows that one misleading deduction can derail an otherwise mostly canonical proof, causing failure to establish the correct answer. The five-hop PrOntoQA case expects “False” because Alex is not hot.

  • A.3 EXAMPLE INSTRUCTGPT MISPREDICTION: In the 5-hop example, the expected answer is False because Alex is derived to be a dumpus and therefore not hot.The proof proceeds from zumpus to tumpus, wumpus, impus, and dumpus before applying the rule that every dumpus is not hot.
  • A.3 EXAMPLE INSTRUCTGPT MISPREDICTION: InstructGPT makes one misleading deduction amid mostly canonical steps, then an invalid step, which prevents it from proving the goal.The figure identifies the misleading and invalid steps as the errors responsible for the failed proof.

A.4 HOW WE EVALUATE THE CHAIN-OF-THOUGHT

The evaluation reconstructs proofs from predicted and gold chains of thought, then assesses each predicted step and the final conclusion against parsed logical context. It distinguishes strictly valid, broadly valid, misleading, and invalid reasoning steps using provability checks.

  • Proof reconstruction and evaluation: The algorithm parses the context, gold chain of thought, and predicted chain of thought before evaluating predicted proof steps against accumulated conclusions.It initializes a set of previous conclusions and processes each predicted sentence sequentially.
  • Step-level criteria: Each step is classified by whether its logical form is provable, whether it is atomic, and whether it is misleading relative to the gold proof.A step can be misleading when its premises occur in the gold proof but its conclusion does not.
  • Provability procedure: The provability procedure accepts axiom steps and Hop-rule deductions as strictly valid, while graph paths under additional deduction rules provide broadly valid proofs.For graph-based proofs, the algorithm returns the axioms corresponding to path edges and the path length.
  • Proof correctness: A step is invalid when its logical form is not provable, and the overall proof is correct when the final conclusion is provable.The procedure represents an unprovable step with an empty premise set and a negative validity indicator.

A.5 PROOF ACCURACY VS MODEL SIZE · A.6 ADDITIONAL ERROR ANALYSIS · A.7 DO OTHER PROMPTING STRATEGIES HELP?

The appendix examines proof accuracy across model sizes and proof-step types, analyzes error patterns, and tests whether alternative prompting strategies improve proof recovery. Self-consistency produces valid-proof accuracy of 0.56 versus 0.545, which is not significantly different.

  • A.5 PROOF ACCURACY VS MODEL SIZE: Figure 8 measures proof accuracy across model size, ontology type, hop count, and six proof-step categories using top-down traversal.The categories include strictly-valid non-atomic misleading and correct steps, strictly-valid atomic misleading steps, broadly-valid misleading and correct steps, and another step type detailed in Figure 2.
  • A.6 ADDITIONAL ERROR ANALYSIS: Figure 9 analyzes incorrect proofs by the type of their first error, hop count, and ontology traversal direction.The analysis focuses on three-hop experiments in bottom-up and top-down directions and omits one-hop results.
  • A.6 ADDITIONAL ERROR ANALYSIS: Figure 10 depicts how many steps follow a strictly-valid atomic misleading step before the proof returns to the gold proof.The histograms cover model-specific three-hop settings, including false and true ontologies with top-down traversal.
  • A.7.1 SELF-CONSISTENCY: Self-consistency samples 40 chains-of-thought per example at temperature 0.7, groups samples by semantic parse, and selects the logical-form sequence with the highest summed quantity.In 100 five-hop fictional-ontology top-down examples, valid-proof accuracy is 0.56 versus 0.545, not significantly different.
  • A.7.2 CAN THE MODEL LEARN TO DO DEPTH-FIRST SEARCH FROM IN-CONTEXT EXAMPLES?: The depth-first-search prompting strategy allows in-context examples to contain misleading steps, aiming to teach recovery after a mistaken but recoverable proof step.This proposal follows observations that INSTRUCTGPT sometimes returned to the correct proof after a misleading step.
  • A.7.2 CAN THE MODEL LEARN TO DO DEPTH-FIRST SEARCH FROM IN-CONTEXT EXAMPLES?: A PrOntoQA example contrasts the expected proof that Polly is angry with a sampled proof that reaches Polly is not angry through additional deductions.The sampled incorrect chain has average log probability -0.07272354467015028, while another reported sample has -0.02227105943358164.
Loading 2210.01240v4…