ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language
Oyvind Tafjord, Bhavana Dalvi Mishra, Peter Clark Allen Institute for AI, Seattle, WA
Abstract
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 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 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 sys
中文速览
大型语言模型（Transformer）已能判断一个推论是否为真，但还不能主动生成推论、也无法给出可靠的推理证明，这正是本文要解决的问题。研究者提出了 ProofWriter 系统，核心思路是将多步推理拆解为反复执行"单步推断（1-hop inference）"：每次只从当前已知事实和规则推出一个新结论，把它加入知识库后再推下一步，最终将这些单步片段拼装成完整的自然语言证明（natural language proof）；此外还实现了溯因推理（abduction），即在结论无法被证明时，自动补全一个缺失事实使证明成立。在 RuleTaker 数据集上，ProofWriter 的证明准确率比此前最优方法高出 9 个百分点，且能泛化到训练时未见过的推理深度和领域外问题。这项工作让神经网络真正具备了"生成推论 + 给出可验证推理链"的能力，大幅提升了基于语言的系统性推理在实际应用中的可行性。
原文 arXiv:2012.13048;中英对照 + 大白话阅读 https://aha.fim.ai/paper/2012.13048v2