PRover: Proof Generation for Interpretable Reasoning over Rules

By Swarnadeep Saha, Sayan Ghosh, Shashank Srivastava, Mohit Bansal. 2020

84 citations recorded by the source corpus.

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. Our code and models are publicly available at this https URL

Subfields: Artificial Intelligence, Natural Language Processing

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Natural Language Processing

Citations in the corpus

Explainable Multi-hop Verbal Reasoning Through Internal Monologue (2021, background): “The second baseline is PROVER (Saha et al., 2020), which handles the reasoning problem as a graph problem.”
Flexible Generation of Natural Language Deductions (2021, background): “Systems like PRover (Saha et al., 2020) and Leap-of-Thought (Talmor et al., 2020) have some broadly similar goals to ours, but only retrieve facts and do not generate novel conclusions.”
Faithful Reasoning Using Large Language Models (2022, background): “We highlight several works that use language models to produce reasoning traces (Bostrom et al., 2022; Dalvi et al., 2021; Kojima et al., 2022; Saha et al., 2020; Tafjord et al., 2021; Wei et al., 2022; Zelikman et al., 2022), and assess the reasoning validity of each approach.”
Selection-Inference: Exploiting Large Language Models for Interpretable Logical Reasoning (2022, background): “…the more common approach of obtaining post-hoc rationalisation , where the answer produced by the model has no direct dependence on the explanation, since the explanation is produced either in parallel to the answer or after the fact (Cobbe et al., 2021; Lampinen et al., 2021; Saha et al., 2020).”
Thinking Aloud: Dynamic Context Generation Improves Zero-Shot Reasoning Performance of GPT-2 (2021, methodology): “PRover [Saha et al., 2020] is a multi-head model based on RoBERTa [Liu et al., 2019b], which both constructs proof chains and predicts answers for a deductive reasoning task [Clark et al., 2020].”
Explaining Answers with Entailment Trees (2021, background): “Recent work in deductive reasoning has shown that transformers can generate formal proofs with high reliability, both in a formal setting (Polu and Sutskever, 2020; Wang and Deng, 2020) and with rules expressed in natural language (Saha et al., 2020).”
Reasoning with Transformer-based Models: Deep Learning, but Shallow Reasoning (2021, background): “They can even generate the proofs [Saha et al., 2020, Tafjord et al., 2020, Gontier et al., 2020].”
ExplaGraphs: An Explanation Graph Generation Task for Structured Commonsense Reasoning (2021, methodology): “Following prior work (Saha et al., 2020), we achieve this through an Integer Linear Program (ILP) by maximizing a global score over the edge probabilities as described below.”
NaturalProver: Grounded Mathematical Proof Generation with Language Models (2022, background): “Related areas in NLP. Systematic reasoning in natural language (outside of math) has been studied with synthetic proofs [36, 40], single-step deductions [4], or entailment trees [8], which differ from proving real-world mathematical theorems.”
multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning (2021, methodology): “Following past work (Clark et al., 2020; Saha et al., 2020 and test set in Tables 8 and 9 respectively.”
A Review on Language Models as Knowledge Bases (2022, background): “LMs can also generate proofs demonstrating their ‘chain of thought’ (Saha et al., 2020; Tafjord et al., 2021; Polu et al., 2022).”
A Comprehensive Survey on Applications of Transformers for Deep Learning Tasks (2023, background): “, 2020) (Saha et al., 2020) Binary Classification, Sequence Generation 2020 PRover [RoBERTabased](Encoder) No NA RuleTaker”
Critical Thinking for Language Models (2020, background): “PRover extends RuleTaker by a component for proof generation (Saha et al., 2020).”
Natural Language Deduction through Search over Statement Compositions (2022, background): “This condition differs from prior work on question answering with multi-hop reasoning (Yang et al., 2018; Chen et al., 2019) or models that build a proof structure but do not generate new statements (Saha et al., 2020, 2021).”