ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language

By Oyvind Tafjord, Bhavana Dalvi, Peter Clark. 2020

463 citations recorded by the source corpus.

Transformers have been shown to emulate logical deduction over natural language theories (logical rules expressed in natural language), reliably assigning true/false labels to candidate implications. However, their ability to generate implications of a theory has not yet been demonstrated, and methods for reconstructing proofs of answers are imperfect. In this work we show that a generative model, called ProofWriter, can reliably generate both implications of a theory and the natural language proof(s) that support them. In particular, iterating a 1-step implication generator results in proofs that are highly reliable, and represent actual model decisions (rather than post-hoc rationalizations). On the RuleTaker dataset, the accuracy of ProofWriter's proofs exceed previous methods by +9% absolute, and in a way that generalizes to proof depths unseen in training and on out-of-domain problems. We also show that generative techniques can perform a type of abduction with high precision: Given a theory and an unprovable conclusion, identify a missing fact that allows the conclusion to be proved, along with a proof. These results significantly improve the viability of neural methods for systematically reasoning over natural language.

Subfields: Natural Language Processing, Prompting & Reasoning

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Natural Language Processing

In Prompting & Reasoning

Citations in the corpus

RuleBERT: Teaching Soft Rules to Pre-Trained Language Models (2021, methodology): “, 2020) or build proof iteratively using 1-hop inference (Tafjord et al., 2021).”
Faithful Reasoning Using Large Language Models (2022, methodology): “We present results on both ProofWriter (PW) (Tafjord et al., 2021) and EntailmentBankQA (EB).”
Selection-Inference: Exploiting Large Language Models for Interpretable Logical Reasoning (2022, methodology): “, 2022), ProofWriter (Tafjord et al., 2021), and EntailmentBank (Dalvi et al.”
Explaining Answers with Entailment Trees (2021, methodology): “Inspired by this, we apply similar ideas to generating entailment trees, in particular leveraging the generative techniques used in the ProofWriter system (Tafjord et al., 2021) (Section 5).”
A Survey of Large Language Models (2023, unknown): “Complex Reasoning Knowledge Reasoning CSQA [247], StrategyQA [248], ARC [291], BoolQ [315], PIQA [295], SIQA [316], HellaSwag [317], WinoGrande [318], OpenBookQA [302], COPA [319], ScienceQA [301], proScript [320], ProPara [321], ExplaGraphs [322], ProofWriter [323], EntailmentBank [324], ProOntoQA ”
Shepherd: A Critic for Language Model Generation (2023, unknown): “Specifically, we choose Entailment Bank (deductive reasoning) (Dalvi et al., 2021), Proofwriter (logical reasoning) (Tafjord et al., 2020), GSM8K (arithmetic reasoning) (Cobbe et al., 2021), PIQA (physical reasoning) (Bisk et al., 2020b), CosmosQA (commonsense reasoning) (Huang et al., 2019), ECQA…”
Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought (2022, methodology): “P ROOF W RITER provides multi-hop proofs for each example.”
Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning (2023, methodology): “We randomly selected 300 examples from each subset of ProofWriter, ensuring a balanced label distribution.”
OpenHands: An Open Platform for AI Software Developers as Generalist Agents (2024, unknown): “ProofWriter (Tafjord et al., 2021) is a synthetic dataset created to assess deductive reasoning abilities of LLMs.”
The Abduction of Sherlock Holmes: A Dataset for Visual Abductive Reasoning (2022, background): “Abductive reasoning has recently received attention in language processing tasks [6, 11, 45, 50], proof writing [60], and dis-”
Entailment Tree Explanations via Iterative Retrieval-Generation Reasoner (2022, background): “Conditioning the retrieval of a passage on previously retrieved passages has been explored in the context of multi-hop QA (Zhao et al., 2021; Xiong et al., 2021), and multi-hop explanations (Valentino et al., 2021; Cartuyvels et al., 2020).”
Reasoning with Transformer-based Models: Deep Learning, but Shallow Reasoning (2021, background): “They can even generate the proofs [Saha et al., 2020, Tafjord et al., 2020, Gontier et al., 2020].”
LAMBADA: Backward Chaining for Automated Reasoning in Natural Language (2022, methodology): “We conduct experiments with ProofWriter (Tafjord et al., 2020) and PrOntoQA (Saparov and He, 2022) which are challenging datasets for LM reasoning containing examples requiring proof chains of up to 5 hops in length, and (in the former case) examples where the goal can neither be proved nor disprove”
Reasoning with Language Model Prompting: A Survey (2022, unknown): “thetic rule bases plus derived conclusions (Clark et al., 2020; Tafjord et al., 2021).”
Solving math word problems with process- and outcome-based feedback (2022, unknown): “However, compared to GSM8K, these datasets either contain templated problems (Proof Writer and CLUTTR) or are signiﬁcantly smaller in size (EntailmentBank and StrategyQA).”
Large Language Models Can Be Easily Distracted by Irrelevant Context (2023, background): “There exist some logical reasoning benchmarks that contain irrelevant content in task descriptions (Weston et al., 2015; Sinha et al., 2019; Clark et al., 2021; Han et al., 2022; Tafjord et al., 2020, inter alia ).”