PRover: Proof Generation for Interpretable Reasoning over Rules

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. 1 Facts : F 1 : The bald eagle eats the lion. F2: The bald eagle sees the tiger. F3: The lion chases the bald eagle. F 4 : The lion eats the mouse. F5: The mouse eats the tiger. F6: The tiger eats the bald eagle. F 7 : The tiger is red. Rules : R1: If the lion is green and the lion is not kind then the lion sees the bald eagle. R2: If someone sees the lion then they eat the mouse. R 3 : If someone is kind and not green then they see the bald eagle. R4: If someone is rough then they see the lion. R5: If someone sees the lion and they do not eat the tiger then the tiger is rough. R 6 : If someone eats the bald eagle and the bald eagle is not kind then the bald eagle is rough. R7: If someone does not eat the lion then the lion is big. R8: If someone is kind then they do not eat the mouse. Q4: The bald eagle eats the mouse. [ Answer : T ] Q5: The tiger does not eat the mouse.