# PRover: Proof Generation for Interpretable Reasoning over Rules

arXiv: https://arxiv.org/abs/2010.02830 · HTML: https://mlsanity.com/paper/2010.02830/

## Key facts

- Cited by 53 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 Oct 2020.

## Built on by (most cited first, 30 of 53)

- [Selection-Inference: Exploiting Large Language Models for Interpretable Logical Reasoning](https://mlsanity.com/paper/2205.09712/) (2022)
- [A Review on Language Models as Knowledge Bases](https://mlsanity.com/paper/2204.06031/) (2022)
- [Explaining Answers with Entailment Trees](https://mlsanity.com/paper/2104.08661/) (2021)
- [Faithful Reasoning Using Large Language Models](https://mlsanity.com/paper/2208.14271/) (2022)
- [Unveiling Transformers with LEGO: a synthetic reasoning task](https://mlsanity.com/paper/2206.04301/) (2022)
- [NaturalProver: Grounded Mathematical Proof Generation with Language Models](https://mlsanity.com/paper/2205.12910/) (2022)
- [A Comprehensive Survey on Applications of Transformers for Deep Learning Tasks](https://mlsanity.com/paper/2306.07303/) (2023)
- [Natural Language Reasoning, A Survey](https://mlsanity.com/paper/2303.14725/) (2023)
- [ExplaGraphs: An Explanation Graph Generation Task for Structured Commonsense Reasoning](https://mlsanity.com/paper/2104.07644/) (2021)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Generating Natural Language Proofs with Verifier-Guided Search](https://mlsanity.com/paper/2205.12443/) (2022)
- [Natural Language Deduction through Search over Statement Compositions](https://mlsanity.com/paper/2201.06028/) (2022)
- [Towards LogiGLUE: A Brief Survey and A Benchmark for Analyzing Logical Reasoning Capabilities of Language Models](https://mlsanity.com/paper/2310.00836/) (2023)
- [FaiRR: Faithful and Robust Deductive Reasoning over Natural Language](https://mlsanity.com/paper/2203.10261/) (2022)
- [Enhancing Reasoning Capabilities of LLMs via Principled Synthetic Logic Corpus](https://mlsanity.com/paper/2411.12498/) (2024)
- [Flexible Generation of Natural Language Deductions](https://mlsanity.com/paper/2104.08825/) (2021)
- [Pushing the Limits of Rule Reasoning in Transformers through Natural Language Satisfiability](https://mlsanity.com/paper/2112.09054/) (2021)
- [Learning Deductive Reasoning from Synthetic Corpus based on Formal Logic](https://mlsanity.com/paper/2308.07336/) (2023)
- [AbductionRules: Training Transformers to Explain Unexpected Inputs](https://mlsanity.com/paper/2203.12186/) (2022)
- [METGEN: A Module-Based Entailment Tree Generation Framework for Answer Explanation](https://mlsanity.com/paper/2205.02593/) (2022)
- [Thinking Aloud: Dynamic Context Generation Improves Zero-Shot Reasoning Performance of GPT-2](https://mlsanity.com/paper/2103.13033/) (2021)
- [multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning](https://mlsanity.com/paper/2106.01354/) (2021)
- [NOAHQA: Numerical Reasoning with Interpretable Graph Question Answering Dataset](https://mlsanity.com/paper/2109.10604/) (2021)
- [Summarization Programs: Interpretable Abstractive Summarization with Neural Modular Trees](https://mlsanity.com/paper/2209.10492/) (2022)
- [GLoRE: Evaluating Logical Reasoning of Large Language Models](https://mlsanity.com/paper/2310.09107/) (2023)
- [Learning Symbolic Rules for Reasoning in Quasi-Natural Language](https://mlsanity.com/paper/2111.12038/) (2021)
- [Interpretable Proof Generation via Iterative Backward Reasoning](https://mlsanity.com/paper/2205.10714/) (2022)
- [A Survey on Symbolic Knowledge Distillation of Large Language Models](https://mlsanity.com/paper/2408.10210/) (2024)
- [Neural Unification for Logic Reasoning over Natural Language](https://mlsanity.com/paper/2109.08460/) (2021)
- [Explanation Graph Generation via Pre-trained Language Models: An Empirical Study with Contrastive Learning](https://mlsanity.com/paper/2204.04813/) (2022)

## Abstract (arXiv)

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