PRover: Proof Generation for Interpretable Reasoning over Rules

TL;DR

PRover is an interpretable transformer model that jointly answers questions over rule-bases and generates formal proofs, demonstrating strong accuracy and generalization in reasoning tasks.

Contribution

It introduces a novel proof-generating transformer model that produces valid proof graphs, improving interpretability and reasoning capabilities over prior QA models.

Findings

Achieves 87% proof accuracy and up to 6% QA improvement over RuleTakers.

Generalizes better to higher reasoning depths with 15% improvement.

Reaches 98% QA accuracy with only 40% training data.

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. Our code and models are publicly available at https://github.com/swarnaHub/PRover