PRover: Proof Generation for Interpretable Reasoning over Rules (2020.emnlp-main)
Copied to clipboard
| Challenge: | Recent work shows that transformers can act as “soft theorem provers” by answering questions over explicitly provided knowledge in natural language. |
| Approach: | They propose a transformer-based model that answers binary questions over rule-bases and generates the corresponding proofs. |
| Outcome: | The proposed model generates proofs with an accuracy of 87% while maintaining or improving performance on the QA task. |
Similar Papers
ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language (2021.findings-acl)
Copied to clipboard
| Challenge: | Recent work shows that transformers can generate both implications of a theory and the natural language proofs that support them. |
| Approach: | They propose a generative model that generates both implications of a theory and natural language proofs that support them. |
| Outcome: | The proposed model generates both implications of a theory and the natural language proofs that support them. |
Interpretable Proof Generation via Iterative Backward Reasoning (2022.naacl-main)
Copied to clipboard
| Challenge: | Existing proof generation tasks require reasoning capabilities, but they usually just request for an answer without the reasoning procedure that would make it interpretable. |
| Approach: | They propose an iterative backward reasoning model to solve the proof generation tasks on rule-based Question Answering. |
| Outcome: | The proposed model improves in-domain performance and cross-domain transferability over existing models. |
FaiRR: Faithful and Robust Deductive Reasoning over Natural Language (2022.acl-long)
Copied to clipboard
| Challenge: | Currently, black-box models generate both the proof graph and intermediate inferences within the same model and thus may be unfaithful. |
| Approach: | They propose a transformer-based model that can perform deductive reasoning on a logical rulebase containing rules and statements written in natural language. |
| Outcome: | The proposed model is robust to language perturbations and faster at inference than previous models on existing reasoning datasets. |
multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning (2021.naacl-main)
Copied to clipboard
| Challenge: | Existing work to generate proof graphs for formal reasoning over explicit knowledge is not unique and there may be multiple ways of reaching the correct answer. |
| Approach: | They propose to generate multiple proof graphs for reasoning over natural language rules and facts . they propose to combine all proofs and exploit correlations between them . |
| Outcome: | The proposed model outperforms PRover on multiple gold proofs on synthetic, zero-shot, and human-paraphrased datasets. |
Theorem Prover as a Judge for Synthetic Data Generation (2025.acl-long)
Copied to clipboard
| Challenge: | Recent studies show that large language models are increasingly capable of tackling mathematical problems. |
| Approach: | They propose an approach that iteratively refines theorem prover formalisation to mitigate errors. |
| Outcome: | The proposed method increases execution rate on the Lean prover from 60% to 87%, while human annotation is replaced with theorem prover feedback. |
SLR: Automated Synthesis for Scalable Logical Reasoning (2026.acl-long)
Copied to clipboard
Lukas Helff, Ahmad Omar, Felix Friedrich, Antonia Wüst, Hikaru Shindo, Rupert Mitchell, Tim Woydt, Patrick Schramowski, Wolfgang Stammer, Kristian Kersting
| Challenge: | Existing benchmarks intended to evaluate reasoning capabilities emphasize deductive reasoning, where conclusions necessarily follow from given premises. |
| Approach: | They propose an end-to-end framework for systematic evaluation and training of Large Language Models via Scalable Logical Reasoning. |
| Outcome: | The proposed framework doubles Llama-3-8B accuracy on SLR-Bench, achieving parity with Gemini-Flash-Thinking at a fraction of computational cost. |
ProoFVer: Natural Logic Theorem Proving for Fact Verification (2022.tacl-1)
Copied to clipboard
| Challenge: | Recent fact verification systems rely on neural network classifiers for veracity prediction, which lack explainability. |
| Approach: | They propose a model that generates natural logic-based inferences as proofs using lexical mutations between spans in the claim and the evidence retrieved. |
| Outcome: | The proposed model has highest label accuracy and second best score in the FEVER leaderboard. |
Neural Unification for Logic Reasoning over Natural Language (2021.findings-emnlp)
Copied to clipboard
| Challenge: | Automated Theorem Proving (ATP) is a computer program that can show that conjectures are logical consequences of a set of axioms. |
| Approach: | They propose a transformer-based architecture for deriving conjectures given axioms . they propose 'neural unifier' and relative training procedure to train the model . |
| Outcome: | The proposed architectures are able to answer queries with deep queries with a relatively low training time. |
Can Transformers Reason in Fragments of Natural Language? (2022.emnlp-main)
Copied to clipboard
| Challenge: | Recent work on natural language inference has identified two strands of research . |
| Approach: | They investigate whether neural networks have acquired logical principles from natural language . they use transformer-based models to detect valid inferences in controlled fragments of natural language. |
| Outcome: | The proposed model overfits to superficial patterns in the data rather than acquiring the logical principles governing reasoning in natural language fragments. |
Scaling Synthetic Logical Reasoning Datasets with Context-Sensitive Declarative Grammars (2024.emnlp-main)
Copied to clipboard
| Challenge: | Existing proof generation algorithms bias reasoning toward specific proof traces and limit extensibility. |
| Approach: | They propose a framework with flexible context-sensitive rules binding multiple languages . they propose to use English verbalization of predicates to enhance logical reasoning . |
| Outcome: | The proposed framework surpasses GPT-4 in accuracy on a human-authored logic dataset by 12%. |