multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning

Proceedings of the 2021 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, pages 3662–3677 June 6–11, 2021. ©2021 Association for Computational Linguistics 3662 MULTIPROVER: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning Swarnadeep Saha Prateek Yadav Mohit Bansal UNC Chapel Hill {swarna, prateek, mbansal}@cs.unc.edu Abstract We focus on a type of linguistic formal rea- soning where the goal is to reason over ex- plicit knowledge in the form of natural lan- guage facts and rules (Clark et al., 2020). A re- cent work, named PROVER (Saha et al., 2020), performs such reasoning by answering a ques- tion and also generating a proof graph that ex- plains the answer. However, compositional reasoning is not always unique and there may be multiple ways of reaching the correct an- swer. Thus, in our work, we address a new and challenging problem of generating multi- ple proof graphs for reasoning over natural lan- guage rule-bases. Each proof provides a differ- ent rationale for the answer, thereby improv- ing the interpretability of such reasoning sys- tems. 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 struc- tured output spaces where each proof is rep- resented 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 condi- tioning between the proofs; while the sec- ond model, Iterative-MULTIPROVER, gener- ates proofs iteratively by explicitly condition- ing on the previously generated proofs. Exper- iments on multiple synthetic, zero-shot, and human-paraphrased datasets reveal that both MULTIPROVER models significantly outper- form 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 requir- ing higher depths of reasoning where multiple proofs are more frequent. 1 Introduction Formal reasoning over explicit multi-sentence knowledge (Newell and Simon, 1956) has often proved to be challenging (Musen and Van Der Lei, 1988), owing to the difficulty in creating logical forms from such sentences, thereby restricting the application of semantic parsers (Zettlemoyer and Collins, 2005; Berant et al., 2013; Berant and Liang, 2014). Thus, in a recent work, Clark et al. (2020) bypass the creation of intermediate logi- cal forms and show that transformers (Vaswani et al., 2017) can act as “soft theorem provers" by an- swering questions over natural language (English) rule-bases, consisting of facts and rules. In or- der to reliably interpret these predicted answers, Saha et al. (2020) propose PROVER, a transformer- based model that generates the corresponding proof graph, thus emulating formal reasoning closely. Consider the two example rule-bases with two ques- tions 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 …

Content truncated to 500 words