PR over: Proof Generation for Interpretable Reasoning over Rules (2020)

Abstract: Recent work by Clark et al. (2020) shows that transformers can act as “soft theorem provers” by answering questions over explicitly provided knowledge in natural language. In our work, we take a step closer to emulating formal theorem provers, by proposing PRover, an interpretable transformer-based model that jointly answers binary questions over rule-bases and generates the corresponding proofs. Our model learns to predict nodes and edges corresponding to proof graphs in an efficient constrained training paradigm. During inference, a valid proof, satisfying a set of global constraints is generated. We conduct experiments on synthetic, hand-authored, and human-paraphrased rule-bases to show promising results for QA and proof generation, with strong generalization performance. First, PRover generates proofs with an accuracy of 87%, while retaining or improving performance on the QA task, compared to RuleTakers (up to 6% improvement on zero-shot evaluation). Second, when trained on questions requiring lower depths of reasoning, it generalizes significantly better to higher depths (up to 15% improvement). Third, PRover obtains near perfect QA accuracy of 98% using only 40% of the training data. However, generating proofs for questions requiring higher depths of reasoning becomes challenging, and the accuracy drops to 65% for “depth 5”, indicating significant scope for future work.

## introduction developing systems that can understand and reason over explicitly provided knowledge has been a fundamental goal of ai @xcite . owing to the challenges posed in reasoning over formal representations (musen and van der lei, 1 our code and models are publicly available at https: //github.com/swarnahub/prover . 1988), and backed by the recent successes of transformers @xcite in nlp, @xcite propose a new version of the problem by replacing the formal representations of rule-bases with natural language (english). specifically, their task requires predicting the truth value of a statement by reasoning over a set of facts and rules, all expressed in natural language. figure 2 shows some examples of the task. @xcite propose ruletakers, a fine-tuned roberta model @xcite to show that transformers can act as "soft theorem provers" by predicting the final answer in such reasoning-based problems with high accuracy. we argue that to use transformers for natural language reasoning reliably, they should be able to generate proofs that provide rationales for the predicted answer. proof generation is vital for emulating formal reasoning but also for moving towards human-interpretable models that alleviate concerns about the black-box nature of deep architectures @xcite . towards this, we present prover, a transformer-based model that jointly answers questions over natural language rule-bases and generates corresponding proofs. figure 1 illustrates our method as a closer linguistic analog of formal reasoning, as it generates proofs along with answers. however, unlike formal reasoners, prover can operate on natural language text that provides the underlying theory, rather than rely on formal logical representations. such methods that combine interpretability and flexibility in reasoning can have wide applications across domains. prover's architecture consists of three modules that together generate answers along with proofs. in this work, proofs are represented as directed graphs consisting of the relevant rules and facts needed to prove or disprove the question statement. section 3.1 contains details of this representation. a qa module predicts a binary answer for the question, a node module chooses which rules and facts are part of the proof, and an edge module predicts the presence and the direction of the edges between the chosen nodes. model training minimizes a joint cross-entropy loss over the three modules. to guide the model to predict edges between valid nodes only, we enforce global constraints on the structure of the proof during training, by masking out labels for impossible edges, resulting in a more efficient learning problem. prover generates valid proofs during inference by solving an ilp over the edge potentials, subject to multiple semantic constraints, such as ensuring proof graph connectivity. our contributions are: our work is related to multiple bodies of previous work in nlp and formal reasoning. qa and nli: the rule reasoning task is related to reasoning tasks that have been proposed recently. these include tasks in the babi dataset @xcite , synthetically generated probe tasks @xcite or reading comprehension tasks in datasets such as quartz @xcite and ropes @xcite . unlike our task, most of these require reasoning over implicit rules, the focus being on language understanding and one step of rule application. multi-hop qa datasets like hotpotqa @xcite require multiple reasoning steps, but the inference rules needed are again implicitly inferred, rather than explicitly provided. our task also bears similarity with natural language inference (maccartney and manning, 2014), but nli also allows unsupported inferences by filling gaps in explicitly stated knowledge @xcite . formal reasoning and neural theorem proving: semantic parsing @xcite @xcite of multi-sentence texts into logical forms has proved to be challenging, restricting the application of semantic parsers to formal reasoning systems @xcite . prover bypasses this expensive and error-prone process and attempts to solve the problem in an end-to-end manner, without any intermediate logical representations. our approach is conceptually similar to a body of work on neural theorem proving @xcite that has focused on developing theorem provers by combining reasoning from symbolic techniques with the possibility of differentiable learning from neural networks. these include neuro-symbolic methods for table comprehension @xcite , executing basic compositional programs @xcite , sat solving @xcite , formula embedding @xcite , approximate (dnf) model counting @xcite , etc. however, prover diverges from these in working with free-form natural language input to generate proofs similar to formal reasoners. model interpretability: prover follows a significant body of previous work on developing interpretable neural models for nlp tasks to foster explainability. several approaches have focused on formalizing the notion of interpretability @xcite @xcite , tweaking features for local model interpretability @xcite and exploring interpretability in latent spaces @xcite . our work can be seen as generating explanations in the form of proofs for an nlp task. while there has been prior work on generating natural language explanations for multiple nlp tasks, including nli (camburu et al., 2018), commonsense reasoning (rajani @xcite and generic text classification tasks @xcite , our novelty lies in generating compositional explanations consisting of proof graphs that detail the chain of reasoning, starting from language. we use a maxflow ilp formulation for checking proof graph connectivity @xcite . multiple approaches for nlp tasks such as sentiment analysis and content selection @xcite @xcite have been framed as optimal flow problems on graphs. program synthesis with transformers: existing works show that transformers already capture some knowledge from pre-training for algorithm emulation @xcite or can be fine-tuned for tasks like semantic parsing (he and choi, 2020), translation @xcite , symbolic integration (lample and charton, 2020) and mathematics @xcite . in our work, we also employ a transformer-based pre-trained language model (roberta @xcite ) but for the downstream task of rule-based reasoning. ## method each input to prover is a context c (consisting of facts f and rules r) and a question q, about the context. prover predicts the answer @xmath0, f alse} and generates a proof p. ## experiments our experiments evaluate the effectiveness of prover (pr), our joint qa, and proof model against ruletakers (rt). details of our experimental setup are in the appendix. ## conclusion we introduce prover, an interpretable joint model that answers binary questions over natural language rule-bases and generates corresponding proofs. the proofs are generated through the node and edge modules of the model in the presence of multiple global constraints during training and ilp inference. our model improves state-of-theart qa accuracy in the zero-shot scenario by 6% and generates proofs accurately. prover also generalizes much better to higher depth questions with up to 15% absolute improvement in qa performance over ruletakers. prover's modeling is relatively generic, and similar proof generation methods can be explored in traditional multi-hop qa tasks. prover can also be a helpful aid to formal reasoners in scenarios where rules are fuzzy and creating rule-bases in a formal language is tedious or infeasible. train, validation and test split, except for the zeroshot test-only one. further details about these can be found in @xcite .