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

Following prior work, we adopt the semantics of Datalog Ceri et al. (1989): A fact is true if it is either known (i.e., explicitly stated in the context $C$), or (recursively) is the conclusion of a rule whose conditions are true (is “supported”). For handling negation, we use two alternative Datalog semantics: The first, following prior work, makes the closed-world assumption (CWA) and uses negation as failure (NAF), so that any fact not provable is assumed false. Under this semantics, negated facts and negative rule conclusions are not allowed (redundant under the CWA). The second makes an open-world assumption (OWA), and does allow negative facts and rule conclusions. Under this semantics, a third truth value Unknown is also possible.

We define a proof $P$ of a fact $f_{q}$ as a directed acyclic graph $(N,E)$ with nodes $n\in N$ and (directed, untyped) edges $e\in E$. Each node in $P$ is either a fact $f$ (a ground literal) or a rule $r$ (a logical implication), expressed in English. Each edge in the proof either connects a fact to a rule, denoting that the fact helps satisfy the rule’s condition, or connects a rule to a fact, denoting that the fact follows from the instantiated rule. Thus nodes in any branch of the proof will alternate between facts and rules. Note this definition differs from (and is richer than) that in PRover, where intermediate conclusions were not part of the proof.

Facts in the proof are one of three types: known facts $f_{i}\in F$, negated facts $f_{naf}$ that cannot be proven (false under negation-as-failure (NAF)), and facts $f_{conc}$ that are the conclusions of rules. $f_{i}$ and $f_{naf}$ are leaf nodes of the proof, while the $f_{conc}$ are intermediate nodes within the proof. Note that $f_{naf}$ and $f_{conc}$ are by definition not in $F$. Example proofs are shown in Figures 1 and 3.

As we wish to generate proofs, we need to encode $P$ as a linear structure that can be output by a generative model. Facts and rules in the context are explicitly labeled with identifiers (fact1, …, rule1, …) that the proof can refer to, see Figures 1 and 3.²²2 In practice we name these sent1, sent2, … without a fact/rule distinction, but for expository purposes it is helpful to use different identifiers. Then, in the linear proof, rule nodes are denoted by their identifier (rule1, …), while fact nodes are denoted by three types of identifiers: fact1, fact2, … for facts in the context; naf1, naf2, … for facts not in the context and assumed false; and conc1, conc2, … for facts concluded by rules. To decode the naf* and conc* identifiers (which by definition are not in the context), an additional sequence of the form “with conc1: sentence1. conc2: sentence2. …” is appended to the proof.

To linearize the proof in a format convenient for a generative model, we conjoin rules and their conclusions using a “%” symbol, express conjunctive rule conditions with a “&” symbol, and use “#” to denote the inverse implication (“$\leftarrow$”). We then express the tree using Polish notation. E.g., the proof tree “((fact1 & fact2) $\rightarrow$ rule1 $\rightarrow$ conc1)” (i.e., fact1 and fact2 satisfy rule1, concluding conc1) would be expressed “# rule1%conc1 & fact1 fact2”. Thus the 3-step proof from Figure 1 is encoded:

# rule18%conc1 & fact5 # rule12%conc2 # rule11%conc3 fact16 ; with conc1: Charlie is quiet. ; conc2: Charlie is young. ; conc3: Charlie is kind.

If the question is a known fact, the “depth 0 proof” is simply the fact itself (e.g., fact1). If no proof exists, the symbol “None” is used.

The ProofWriter models are built on top of the text-to-text pretrained T5 transformer Raffel et al. (2020) (T5-11B). We use different textual prompts for the different tasks. For the task of generating an answer and a proof, the input to the model is of the form: “ $question$ = question ; $context$ = theory-sentences”, for example: “$question$ = Erin is big. ; $context$ = sent1: Erin is young. sent2: If …” The output is of the form: “$answer$ = True/False/Unknown : $proof$ = proof ;”, where proof is encoded as described in Section 3.4. For training instances where multiple outputs are valid, we select a single one at random (for multiple proofs, we select among the shortest proofs). Appendix D lists the hyperperameters and gives input/output examples for each task.

We evaluate two methods of proof generation:

• All-At-Once:

  We train a model to generate the full proof and answer in one go (theory + question $\rightarrow$ answer + proof).

• Iterative:

  We first train a model to generate a single 1-step implication (theory $\rightarrow$ implication + 1-step-proof), where the implication follows from a single rule application. Then at test time, we apply this model iteratively, adding each implication to the theory and repeating until no more implications can be found (i.e., exhaustive forward-chaining). The proof for any given implication can then be assembled from the 1-step-proof fragments (Figure 2).

A second desirable reasoning skill is enumerating implications of a theory (rather than just assign True/False to a hypothesis). This capability is important for practical application of the technology. In fact, the Iterative ProofWriter already does this by design, a substantial advantage. To evaluate this (later), we compare this with an “all at once” strategy of generating all implications as a single output string, analogous to the All-At-Once strategy for generating the full proof as a single string. For training this All-At-Once enumerator, and testing both, we gather the list of all implications $I_{i}$ of each theory $C$ in the train/test data. Each train/test example is of then of the form: given $C$, predict all the $I_{i}$. An example input/output is in Appendix D.3.

A third desirable reasoning skill is abduction over natural language theories, again made possible by generative models. Abduction has previously been studied extensively in formal logic, e.g., Konolige (1997), and in NLP, e.g., Hobbs et al. (1993); Bhagavatula et al. (2020). Here we evaluate whether a generative approach can combine logic and NLP, performing logical abduction over natural language knowledge. We do this for a restricted form of abduction, namely single-fact abduction: Given a theory $C$ and a possible implication $Q$ not provable from $C$, identify a new fact $f_{m}$ (other than the trivial $Q$ itself) such that $C\cup\{f_{m}\}$ implies $Q$.

We restrict this task to the OWA (open-world) setting where questions can naturally have unknown truth values. To train and test an abductive model over our datasets, we create an abductive version as follows: For each theory $C$ in the train/test data, for each unprovable fact $Q$, identify all alternative “missing facts” $factM$ that, when added to $C$, make $Q$ True. To do this, recall that each NL theory was originally generated from a formal one $C_{formal}$ in a formal representation language (Datalog). We first exhaustively enumerate all possible $Q_{formal}$ and $factM_{formal}$ in the formal language (this is feasible as the space of predicates and individuals is small), then use a theorem prover to test if $C_{formal}\cup\{factM_{formal}\}$ implies $Q_{formal}$ for all pairs $(factM_{formal},Q_{formal})$. For each success, we generate the NL equivalents $Q$ and $factM$ using simple NL generation templates. We then collect the alternative $factM$s for each $Q$. The abduction task is then, given $C$ and $Q$, identify the set of all alternative $factM$s, i.e.:
          $C,Q\rightarrow factM_{1},...,factM_{i}$
If there is no single $factM$ that can be added to make $Q$ true, then the symbol “None” is output.

First, we compare ProofWriter’s ability to generate proofs with PRover, the current state-of-the-art. We evaluate both answer accuracy and proof correctness. For proof correctness, for a fair comparison, we ignore the intermediate conclusion nodes (which PRover does not generate). We then use the same strict scoring metric as in PRover (called FA or Full Accuracy in the PRover paper): the proof graph must exactly match a gold proof (i.e., be perfectly correct); otherwise, the proof scores 0.

Second, we compare our two approaches to proof generation, All-At-Once vs. Iterative, in more detail. We show that although they have almost identical performance for proofs with depths seen in training, the Iterative model generalizes better to proofs of longer depths than seen in training. For these comparisons, we use the new D*(CWA) datasets (which fix some minor errors in D*(orig)), and also the D*(OWA) datasets to explore performance in an open-world setting.

Proofs from the Iterative ProofWriter have an additional desirable property: each proof step is one that the model explicitly took during the iteration, i.e., the model “believes” the step. In contrast, the All-At-Once proofs are a post hoc generated string of symbols, and may not reflect steps that ProofWriter would actually make. However, because proofs include intermediate conclusions, we can alleviate this concern by verifying individual steps in the All-At-Once proofs. For example, if a generated proof step states that fact2 + fact3 + rule4 implies conc1, we can simply ask ProofWriter in QA mode if this is true (Figure 4). Given the almost perfect performance for such simple depth 1 questions in QA mode (with no distractor facts or rules), the ability to verify a correct proof corresponds to the accuracy of correctly generating the correct intermediate conclusions conc* in the first place. (Note that an unverified proof is not necessarily wrong, rather cannot be verified as right). OWA proofs can be fully verified in this way. For CWA theories with NAFs, the verification is only partial as NAFs are presumed negative statements which require the full theory to verify.

We measured the percentage of correct, verified proofs, shown in Table 6. Provided proofs are within the depths seen during training, almost all correct proofs can be verified. However, at depths deeper than seen at training, the proportion that can be verified drops rapidly. In contrast, the Iterative ProofWriter’s proofs are always verified, as by definition they are assembled from single step inferences that the model actually took.

Third, we evaluate ProofWriter’s performance on a new task, namely enumerating implications of a theory (rather than just assign True/False to a hypothesis). We compare the All-At-Once and Iterative strategies as described in Section 3.7.

To train All-At-Once, and test both, we created an enumerative dataset of $C\rightarrow\{I_{1},...,I_{n}\}$ examples (Section 3.7). For this we sample theories $C$ in the D0-D3 datasets and gather the list of all implications $I_{i}$ for each theory $C$. We call this enumerative dataset D3+Enum. We similarly create a D5-Enum dataset from theories in (only) D5 to test OOD conclusion generation. We create CWA and OWA versions of both.

We train All-At-Once on D3-Enum (train), then test both models on D3-Enum (test) and D5-Enum (test). For metrics, we measure F1 scores by comparing the individual predicted implications with the gold $I_{i}$, as well as the exact-match correctness of the predicted set of implications $\{I_{1},...,I_{n}\}$ (one point if the set exactly matches the gold, bar ordering, zero otherwise). The results are shown in Table 7, and show that the Iterative ProofWriter is better at implication enumeration than the simple All-At-Once strategy. In particular, the All-At-Once strategy struggles for problems at depths unseen in training (second row), although it does well on its own test set despite the complicated unordered output it has to generate (up to 16 different implications in D3, 21 in D5).

Fourth and finally, we evaluate performance on a second new task, namely abduction over natural language theories, again made possible by generative models. Analogous to implication enumeration, we create a derivative abductive dataset of $C,Q\rightarrow factM_{1},...,factM_{i}$ examples, where $C\cup\{factM_{i}\}$ results in $Q$ becoming provable as described in Section 3.8. We create such D*-Ab datasets from the D*(OWA) datasets.

While the All-At-Once approach to proof generation is simple, efficient, and effective, it does not generalize as well to proofs of greater depth than seen at training. In contrast, the Iterative approach is robust to generalization. Even though errors at each iteration accumulate, the reliability of 1-step inference is so high that such error accumulations remain small. The Iterative architecture, namely a simple model embedded in a recursive loop (rather than single seq2seq model), illustrates how transformers can be used in a “scale-invariant” way, i.e., performance is largely unchanged by the scale (here reasoning depth) of the problem. In addition, as proofs are built from actual inference steps taken by the model, they are by definition “faithful” to the model’s inference steps, rather than being a post hoc rationalization.

However, there are also some drawbacks to the Iterative approach: First, it is inefficient and unguided, proving everything possible and only then looking for the answer and proof for a particular question. In fact, this is a limitation of unconstrained forward-chaining in general, hence established techniques for guiding forward-chaining could be applied, e.g., a best-first expansion strategy, or using a backward-chaining strategy instead (which would similarly need to be controlled). Second, as the theory grows by one fact per iteration, there is a risk of exceeding the transformer’s input token limit (512 tokens by default), hence limiting the size of theories that can be handled. For larger theories, a retrieval mechanism might be needed to manage the facts and rules available to the reasoner.

Recently, LeapOfThought Talmor et al. (2020) showed that RuleTaker-like models could be retrained to reason with a combination of explicit and implicit knowledge, rather than requiring all rules to be stated explicitly (the implicit knowledge coming from the latent knowledge acquired during pretraining Petroni et al. (2019)). Now, given an abductive capability such as the one we have presented, we have a mechanism for materializing the implicit knowledge used to answer a question, and hence generating the full proof of its answer: Given a LeapOfThought conclusion, first abduce the “missing” (implicit) fact(s) required for an explicit proof, then use ProofWriter to generate that proof. This is a significant step forward to help understand a model’s decisions when both implicit and explicit knowledge has been used.