multi PR over: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning (2021)

Abstract: We focus on a type of linguistic formal reasoning where the goal is to reason over explicit knowledge in the form of natural language facts and rules (Clark et al., 2020). A recent work, named PRover (Saha et al., 2020), performs such reasoning by answering a question and also generating a proof graph that explains the answer. However, compositional reasoning is not always unique and there may be multiple ways of reaching the correct answer. Thus, in our work, we address a new and challenging problem of generating multiple proof graphs for reasoning over natural language rule-bases. Each proof provides a different rationale for the answer, thereby improving the interpretability of such reasoning systems. In order to jointly learn from all proof graphs and exploit the correlations between multiple proofs for a question, we pose this task as a set generation problem over structured output spaces where each proof is represented as a directed graph. We propose two variants of a proof-set generation model, multiPRover. Our first model, Multilabel-multiPRover, generates a set of proofs via multi-label classification and implicit conditioning between the proofs; while the second model, Iterative-multiPRover, generates proofs iteratively by explicitly conditioning on the previously generated proofs. Experiments on multiple synthetic, zero-shot, and human-paraphrased datasets reveal that both multiPRover models significantly outperform PRover on datasets containing multiple gold proofs. Iterative-multiPRover obtains state-of-the-art proof F1 in zero-shot scenarios where all examples have single correct proofs. It also generalizes better to questions requiring higher depths of reasoning where multiple proofs are more frequent.

## introduction formal reasoning over explicit multi-sentence knowledge @xcite ) has often proved to be challenging @xcite , owing to the difficulty in creating logical forms from such sentences, thereby restricting the application of semantic parsers @xcite @xcite . thus, in a recent work, @xcite bypass the creation of intermediate logical forms and show that transformers @xcite can act as "soft theorem provers" by answering questions over natural language (english) rule-bases, consisting of facts and rules. in order to reliably interpret these predicted answers, @xcite propose prover, a transformerbased model that generates the corresponding proof graph, thus emulating formal reasoning closely. consider the two example rule-bases with two questions and corresponding proofs in figure 1 , where a proof is a directed graph consisting of the relevant facts and rules from the corresponding rule-base. prover shows good single-proof generation accuracy but is designed and trained in a way to generate only a single proof for each question. this is not ideal because formal proofs are not always unique and there may be multiple correct ways of arriving at the answer. for example, q 1 and q 2 in figure 1 have three and four correct proofs respectively. hence, in order to enhance the humaninterpretability of linguistic formal reasoning systems, it is desirable to develop methods that can generate multiple proofs, each providing a different rationale for the predicted answer. such interpretable methods, while possessing the flexibility of operating over natural language, can also aid in verifying claims when constructing proofs from scratch is tedious or infeasible. we find that prover @xcite , when trained on all proofs as independent training examples (eq. 2) and extended to generate top-p proofs during inference (eq. 3), fails drastically, achieving a low proof precision of 34%. the subsequent proofs are often incorrect because it is not naf naf naf figure 1 : diagram showing two rule-bases with rules, facts, questions, answers and all possible proofs. the first question has three correct proofs while the second question has four correct proofs. multiprover answers both questions correctly and also generates all the corresponding proofs accurately for each question. a proof graph is generated through a node module which selects the relevant facts and rules as part of the proof and an edge module which determines the edges between the chosen nodes. similar to prover, we first enforce multiple structural constraints during training and inference to ensure that a generated proof is valid. next, in order to generate a set of proofs jointly, we propose our first model, multilabel-multiprover, a multi-label classification framework which performs implicit conditioning among the proofs and predicts p binary labels for each node and edge, denoting its presence or absence in each of the p proofs that we want to generate. it is efficient in terms of number of parameters and training time and also achieves a better proof f1 than prover. however, the lack of explicit conditioning between the proofs is not ideal because a question with multiple proofs often has certain common sub-graphs across the proofs. e.g., all the 3 proofs for q 1 in figure 1 have the sub-graph {f 10 → r 1 } common. thus, in order to exploit these correlations which multilabel-multiprover cannot capture explicitly, we further propose an improved variant of multi-prover, named iterative-multiprover, which generates appropriate number of proofs by stacking multiple node and edge encoders, each of which generates one proof at each time step by conditioning on the previously generated proofs. this enables the model to better learn the correlations between multiple proofs for a given question. to capture the set-based nature of the task, we train multiprover using a permutation-invariant hungarian loss (sec. 3.5), which solves an assignment problem between a set of predicted and gold proofs. empirical evaluation on synthetic and human paraphrased qa rule-bases @xcite show that both of our multiprover models achieve a significantly higher proof f1 compared to prover while retaining the qa accuracy. further, on a challenging hand-authored zero-shot dataset, where all examples have single gold proofs, iterative-multiprover achieves state-of-the-art proof f1. it also generalizes better to questions requiring higher depths of reasoning with more multiple proofs. overall, our contributions are: • we address a new and challenging problem of generating a set of multiple logical proof graphs for reasoning over natural language rule-bases by proposing two set-based joint models, multilabel-multiprover and iterative-multiprover. foot_0 • iterative-multiprover's joint training and explicit conditioning helps it to better learn the relative importance of rules and facts for a particular question and uncover common subgraphs across multiple proofs. thus, compared to multilabel-multiprover and prover, it is able to transfer well in zero-shot settings because it learns to assign a soft prior over the rule-base. ## related work the task of rule reasoning @xcite ) is related to other recently proposed tasks on qa @xcite @xcite @xcite and nli (maccartney and manning, 2014). however, most of these tasks require implicit reasoning rules as opposed to explicit ones and the focus is either on broad language understanding or on single rule application. below we discuss multiprover's relation to multiple areas of nlp and ml. ## experimental setup we experiment on synthetic, hand-authored zeroshot, and human paraphrased datasets, following @xcite ; @xcite . datasets: the five synthetic datasets du0-du5 consist of 100k questions with their own train, validation and test splits (70/10/20) and reasoning depths up to @xmath0, 1, 2, 3, 5. each example in these datasets is annotated with all possible proofs. the second dataset is a birds-electricity dataset, consisting of 5k hand-authored samples aimed at evaluating the zero-shot performance of the models. unlike the previous datasets, all examples in this dataset have a unique gold proof. third, pararules is a human-paraphrased dataset, consisting of 40k examples with all possible proofs, where the facts and rules are paraphrased by crowdworkers. further details of the datasets and model's hyperparameters can be found in the appendix. evaluation metrics: following prover, qa evaluation is done through accuracy. for proofs, we compute the following metrics: (1) node precision, recall, f1 (2) edge precision, recall, f1, (3) proof precision, recall, f1, and (4) full accuracy (fa). for each sample, given a set of gold proofs and predicted proofs, node precision is computed as the fraction of predicted proofs where the predicted node set matches exactly with a gold proof's node set. similarly, node recall for each sample is computed as the fraction of gold proofs where the corresponding node sets match exactly. the overall node precision, recall and f1 are the respective sample-wise precision, recall and f1 scores averaged over all the samples. edge metrics are computed similarly but with respect to the edges only and the proof metrics consider both nodes and edges in conjunction. our final metric, full accuracy evaluates a sample as a whole and is given by the fraction of samples where the answer and all corresponding proofs are exactly correct. we observe that prover-all has a slightly lower proof f1 than prover, because the model likely gets confused with multiple possible proofs for the same context and question. prover-top-p's huge drop in precision is unsurprising because the subsequent non-empty proofs are always incorrect, causing full accuracy to drop to 0%. when we perform careful inference over prover either by predicting the number of proofs or by thresholding and do not generate a fixed p number of proofs for all examples, we observe a boost in precision over the vanilla top-p model, with very little drop in recall. however, prover continues to be a stronger baseline than all the top-p variants because of a lot of single-proof examples in the dataset. both multiprover models improve significantly on the state-of-the-art proof f1, while retaining a near perfect qa accuracy. it-multiprover is a significantly stronger model because of its explicit conditioning mechanism and obtains up to a statistically significant foot_1 (@xmath1.001) 4% improvement on proof f1 and full accuracy. while our model is expected to improve the proof recall compared to prover and prover-all because of the generation of multiple proofs, the improvement in precision is particularly important as it shows that the subsequently generated proofs by it-multiprover are mostly correct. similarly, its improvement in proof recall compared to provertop-p also shows the strength of the model considering that prover-top-p generates the maximum number of proofs for every sample. overall, it-multiprover outperforms all other models in all metrics. in summary, careful inference strategies over a single-proof generation model like prover are largely ineffective for generating multiple proofs and an effective proof-set generation model needs to exploit and learn the inter-proof correlations during the training phase itself. our experiments on the pararules dataset demonstrate similar findings, details of which and the effect of varying p for multiprover is in the appendix. iterative-multiprover performs equally well on the subset of questions where the context has negations, achieving a high proof f1 of 90.8. as part of error analysis, we find that 58% of iterative-multiprover's wrongly predicted proofs have more nodes and edges than those in the gold proof, suggesting that our model tends to overestimate the essential rules and facts and their inter-connections. in the following subsections, we analyze multi-prover's generalization capabilities in three dif- iterative-multiprover's improvement in full accuracy over prover is statistically significant with @xmath2.001. ## conclusion we proposed multilabel-multiprover and iterative-multiprover, two variants of a proof-set generation model where the former performs implicit conditioning between the proofs to generate them in parallel while the latter generates a proof-set through explicit conditioning on the previously generated proofs. both models obtain strong proof f1 improvements on synthetic and humanparaphrased datasets and iterative-multiprover also obtains state-of-the-art proof f1 on a zero-shot dataset with single proofs. multiprover's modeling is fairly generic and similar methods can be used in generating a set of structured explanations for other nlp tasks like multi-hop qa. du0-du5: each of these consists of 100k questions with sythetic rule-bases and requires reasoning chains up to a maximum depth of d (@xmath3, 1, 2, 3, 5). the number of train, validation and test examples in each of the datasets are 70k, 10k and 20k respectively. further, each question in the datasets is annotated with all possible proofs. the total number of proofs in the du5 train set range from 1 to 1350, with a mean and median of 1.45 and 1 respectively.