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

Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021, pages 3621–3634 August 1–6, 2021. ©2021 Association for Computational Linguistics 3621 ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language Oyvind Tafjord, Bhavana Dalvi Mishra, Peter Clark Allen Institute for AI, Seattle, WA {oyvindt,bhavanad,peterc}@allenai.org Abstract Transformers have been shown to emulate log- ical deduction over natural language theories (logical rules expressed in natural language), reliably assigning true/false labels to candi- date implications. However, their ability to generate implications of a theory has not yet been demonstrated, and methods for recon- structing 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 lan- guage proofs 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 per- form a type of abduction with high precision: Given a theory and an unprovable conclusion, identify a missing fact that allows the conclu- sion to be proved, along with a proof. These re- sults significantly improve the viability of neu- ral methods for systematically reasoning over natural language.1 1 Introduction A fundamental goal for AI, dating back to its earliest years, is automated reasoning: the abil- ity to draw valid conclusions from explicitly pro- vided knowledge (McCarthy, 1959). However, ap- proaches relying on expressing knowledge in a formal representation language have sometimes proved challenging (Musen and Van der Lei, 1988). Recent work on RuleTaker (Clark et al., 2020) demonstrated a modern approach to this goal, in which transformers emulate deductive reasoning 1Datasets available at https://allenai.org/data/proofwriter Figure 1: Given facts, rules, and a question all ex- pressed in natural language, ProofWriter answers the question and generates a proof of the answer. over statements expressed in natural language, by reliably assigning true/false labels to candidate im- plications. However, simply assigning true/false labels is limiting. For practical purposes, systems should also generate proofs of those labels, so that their conclusions can be verified and a human- understandable rationale be produced. Recent work on PRover, by Saha et al. (2020), provided first results towards this goal, assembling proofs by first classifying which facts, rules, and connections should be in the proof tree then using an Integer Linear Programming (ILP) module to enforce consistency constraints. However, the gen- 3622 Figure 2: ProofWriter iteratively generates 1-step im- plications and their proofs, and adds implications back into into the context for deeper reasoning. The step- wise proof fragments are assembled into full proofs of N-hop conclusions. erated proofs were imperfect, and there were no guarantees that the model “believed” the proofs that it was reciting, i.e., that its QA module would agree with the steps shown in the proof. In this …

Content truncated to 500 words