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

我们提出了PROVER，一种可解释的transform-based模型，能够同时回答基于规则的二元问题并生成相应的证明，经过实验表明，在QA任务中，PROVER的证明生成精度为87％，而在零-shot评估中，与RuleTakers相比，在QA任务中的表现得到保留或提高（最多提高6％）；并在更深层次上（最多提高15％）更好地泛化，仅使用40％的训练数据即可获得近乎完美的QA准确性，但对于需要更深入推理的问题，证明生成变得具有挑战性，准确性下降到65％，这表明未来仍有大量研究价值。

PRover: 可解释推理的证明生成系统