Generating Intermediate Steps for NLI with Next-Step Supervision

Complex NLP tasks such as Natural Language Inference (NLI) and Question-Answering (QA) often requires reasoning over multiple steps using multiple facts and implicit commonsense knowledge  trivedi-etal-2020-multihop; DBLP:conf/aaai/SapBABLRRSC19; camburu2018snli. It has been long argued that DBLP:journals/cacm/Lipton18, the state-of-the-art Deep Learning models should also output some sort of explanation (such as intermediate steps or a textual explanation) alongwith the final answer. The opaque performance and poor out-of-distribution generalization performance of Transformers-based models kaushik2019learning; ribeiro-etal-2020-beyond have refuelled this discussion. However, it is unclear how these intermediate steps can be generated for unconstrained natural language Premise-hypothesis pairs (such as in crowd-sourced NLI datasets) as it is non-trivial to collect crowd-sourced fine-grained explanations or generate them synthetically. Most importantly, it is unclear how such steps can be utilized further for the NLI task.

Despite some efforts camburu2018snli crowd-sourced collection of intermediate steps comes with complications, as human-written explanation can be subjective, and it is hard to automatically verify or utilize such explanations. Recently, researchers have explored synthetic generation of intermediate steps (or proof trees) DBLP:conf/ijcai/ClarkTR20; DBLP:conf/acl/TafjordDC21; DBLP:conf/emnlp/SahaGSB20, where the main goal was to test whether Transformers (the backbone for NLP models) can perform deductive reasoning over natural language statements. Provided their examples come from an underlying symbolic system with closed world rules and facts, it is unclear how this strategy of generating proof tree can be extended to unconstrained natural language premise-hypothesis pairs. In comparably structured domains, such as code snippet retrieval, knowledge-graph based QA and symbolic mathematics, DBLP:journals/corr/abs-2112-00114; DBLP:conf/wsdm/HeL0ZW21; agarwal2021analyzing have shown how to generate such intermediate steps automatically, and how utilizing such steps can enhance end-to-end task performance.

We take inspiration from these domains. We assume that an ideal NLI system reaches a series of intermediate conclusions to derive the final conclusion (entailment/contradiction/neutral) and we call these intermediate steps as proof. Since such proofs can widely vary linguistically, logically and in length; to make verification and generation easier, we impose various constraints of correctness, minimality, and atomicity on what we expect as natural language proofs for a given premise-hypothesis pair. Alongwith human verification, we propose corresponding automated metrics for verification. As human annotation and synthetic generation of such groundtruth proofs is non-trivial, we utilize single-step supervision to train a T5 encoder-decoder model raffel2019exploring on various available entailment datasets; learning various aspects of proof generation from SNLI, Monotonicity Entailment Dataset, and Entailment Bank. To enrich single-step generation with external knowledge, we build a fact retriever and sentence composition model; that retrieves facts from external knowledge bases and learns to deduce new facts. We then explore search-based methods that utilizes the fact-augmented T5 model to generate multiple-step proofs. Our automated and human verification results show the efficacy of the proof generation process. We further use these generated proofs as additional training data and show improvement in end-to-end NLI task performance.

Our contributions include, 1) using only next-step supervision to train a T5 encoder-decoder based model, and external fact composition model; and then use search to generate sequence of knowledge-enriched intermediate steps. We 2) propose and use automated and human verification metrics to show the correctness of the generated proofs. Lastly, 3) we also show that augmenting such proofs during training can help enhance an NLI system’s performance on MNLI, and MED (under low-training data regimes).

In NLI, a premise-hypothesis pair is provided in natural language, and the task is to determine whether the hypothesis is entailed by, contradicts, or is neutral with respect to the premise. Ideally, an NLI system follows a logical sequence of steps (or proof) to come to such a conclusion. However, many valid proofs may exist due to linguistic variability and multiple ways of reaching a conclusion from the context. Hence, to make generation and verification easier, we resort to defining logical properties that valid proofs should have.

Given a premise ($P$), a hypothesis ($H$), and an implicit knowledge base $KB$ ¹¹1Following dagan2005pascal, we assume $KB$ encodes commonly assumed knowledge as facts and rules., an NLI proof $⟨P,H⟩$ (or $⟨P,\neg H⟩$ for contradiction) is a sequence of sentences ($Y_1,\dots ,Y_m$), where $Y_j$ is either an inferred intermediate step (denoted by $I_j$), or an external fact or rule (denoted by $F_j$). A valid proof should satisfy the following properties: i) (Correctness 1) each step is either a generic rule, or a fact which is a entailed by the premise; ii) (Correctness 2) hypothesis (or negated hypothesis) is a valid entailment of premise and intermediate steps; iii) (Minimality 1) each proof upto $Y_j$ (including $H$) should be minimal proof for $⟨P,Y_j⟩$, iv) (Minimality 2) the sentences in the intermediate step ($I_j$) should not be trivially decomposable (using common linguistic or logical constructs)²²2M1 captures redundancy (see E4 in Tab. 1). M2 captures some aspects of atomicity. Sentences should not be compound in nature. We prefer “John is going to Paris. Mia is going to Paris.” over “John and Mia are going to Paris”. It also entails that intermediate conclusions should correspond to a semantic frame (which can not be trivially decomposable without losing context). However the latter is quiet hard to verify. and consecutive inferred steps should be sufficiently different, and v) (Order) a step can only be generated with the help of previous steps.

We provide few example proofs in Table 1, highlighting the properties of correctness and minimality. These constraints motivate our method to generate proofs for arbitrary P-H pairs with only next-step supervision. In Figure 1, we show two types of proof that we generate, i) inference chains (i.e. only intermediate entailments) and ii) proofs with external (commonsense) facts (or rules) in sequence. For neutral cases, such properties are hard to define. Inspired from DBLP:conf/acl/KumarT20, we proposed a method for intermediate step generation of neutral instances which is used only for data augmentation experiments.

A typical possibility to build provers is by training on an NLI dataset with groundtruth proofs, collected using crowd-sourcing or created using formal logic. However, crowd-sourced explanations are highly subjective and diverse; hence not easily verifiable. Similarly, following ProofWriter, generating formal logic-based proof is possible but hard to scale for arbitrary P-H pairs. We instead rely on various NLI datasets, from which models can learn multiple ways of generating entailments, contradictions, and intermediate steps. We then enhance such provers with facts retrieved from knowledge bases and sentence composition methods. We use these techniques effectively to search for more generalized multiple-step proofs. We start from the premise P and generate the steps of the proof recursively with the Prover model. We use the term Prover to collectively denote the models in Section 3.1 and Section 3.2 as discussed next.

We generate proofs with two different methods as described below, and provide some examples of generated proofs in Figure 1 and Table 2.

We perform two sets of experiments – i) we use human and automatic evaluation to evaluate different aspects of the proofs generated from our proposed method, and ii) we use the generated proofs as additional labeled data for NLI and analyze its effect on the NLI classification task performance.

We explore generation of multiple-step natural language proofs for the NLI task. For verification and generation, we take inspiration from the automated theorem proving and research in deductive reasoning with Transformers. We also explore how proofs can be further utilized.

Categories of Proofs: The NLP community has introduced several NLU tasks and datasets with accompanying explanations wiegreffe-marasovic-2021-review, ranging from highlighted context, natural language based or structured proof trees. Highlighted explanations hardly help in scenarios requiring external knowledge. Human-provided natural language explanations camburu2018snli are hard to validate; and structured explanations are hard to scale. For certain closed-world setting DBLP:conf/acl/TafjordDC21 and symbolic domains, synthetically generated explanations has been popular. Authors in DBLP:journals/corr/abs-2112-00114 explore NaturalProofs, where the proof consists of both natural language and mathematical symbols. However, the underlying reasoning task being mathematical, makes the task more well-defined. A large body of work in the ATP community DBLP:conf/aaai/PaliwalLRBS20; aygun2020learning; agarwal2021analyzing generates synthetic fine-grained steps as proofs for symbolic domains. Here, we define constraints over natural language proofs to ease validation and generation.

Iterative Proof Generation and Search: DBLP:conf/acl/TafjordDC21 utilize synthetically generated end-to-end proof trees as supervision. Authors train a strong encoder-decoder model such as T5 to iteratively generate the next step of a proof, and use search to generate full proofs. Similarly, in the Automated Theorem Proving literature, recent work DBLP:conf/aaai/PaliwalLRBS20; aygun2020learning; agarwal2021analyzing has shown that Graph Neural Networks and Transformers can be trained to perform impressively on the theorem-proving task as part of a neuro-symbolic system. Theorem-proving is a multiple-step search-based task, where the neural method learns to simplify an input goal into several sub-goals. This is done recursively using search, until all sub-goals are proven (i.e., simplified to empty goals). Further, These proof systems are easier to define as the number of operations (or theorems or tactics) comes from a known closed set. Thus, it is non-trivial to extend above methods to generate natural language proof without full end-to-end supervision.

Proofs to Improve End-task Accuracy: DBLP:conf/wsdm/HeL0ZW21 and DBLP:conf/acl/KumarT20 has demonstrated the utility of generating proofs (or natural language explanations). In Knowledge-graph based QA context, DBLP:conf/wsdm/HeL0ZW21 show how a teacher network trained on additional intermediate hops can be used to enhance the performance of a student network, that is exposed only to the final output supervision. Most importantly, DBLP:conf/acl/KumarT20 uses label-specific explanations and use them directly to generate the NLI conclusion. While the authors show how explanations are used to generate the conclusion, the authors do not generate fine-grained steps. Authors also compare with a non-recent baseline by camburu2018snli on MNLI, instead of SOTA methods such as RoBERTA-large.

We study multi-step reasoning for the NLI task; where connecting a premise and hypothesis may require external knowledge (including free-form fuzzy commonsense rules). The closest to our work is RuleTaker and ProofWriter DBLP:conf/acl/TafjordDC21; where authors explore deductive abilities of Transformers over natural language. We differ from their work, as we do not provide the required rules explicitly and do not restrict the natural language input in any form. Our fact retrieval method is inspired from DBLP:conf/icml/GuuLTPC20; NEURIPS2020_fc84ad56. NEURIPS2020_fc84ad56 proposes to combine a non-parametric retriever model with a parametric generator for knowledge-augmented NLP tasks. While the goals are similar, we use a custom retrieval method as we do not have knowledge-augmented sentence composition supervision for learning retrieval and generation in an end-to-end fashion.

We propose a method to generate knowledge-enriched multiple-step textual proofs (intermediate conclusions) for the NLI task utilizing only next-step supervision. We train a T5 model to generate the next step given a premise-hypothesis pair, and use external fact augmentation, search for more generalized proofs. To ease generation and automatic verification, we introduce constraints over expected proofs, and associated automated metrics. Both human and automated verification show the effectiveness of our proposed method. We also show that our generated proofs can be used to improve NLI task performance using standard data augmentation techniques (on low-data scenarios).