# ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language

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

## Key facts

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

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

- [A Survey of Large Language Models](https://mlsanity.com/paper/2303.18223/) (2023)
- [OpenHands: An Open Platform for AI Software Developers as Generalist Agents](https://mlsanity.com/paper/2407.16741/) (2024)
- [Solving math word problems with process- and outcome-based feedback](https://mlsanity.com/paper/2211.14275/) (2022)
- [Large Language Models Can Be Easily Distracted by Irrelevant Context](https://mlsanity.com/paper/2302.00093/) (2023)
- [Faith and Fate: Limits of Transformers on Compositionality](https://mlsanity.com/paper/2305.18654/) (2023)
- [Cognitive Architectures for Language Agents](https://mlsanity.com/paper/2309.02427/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought](https://mlsanity.com/paper/2210.01240/) (2022)
- [Selection-Inference: Exploiting Large Language Models for Interpretable Logical Reasoning](https://mlsanity.com/paper/2205.09712/) (2022)
- [Reasoning with Language Model Prompting: A Survey](https://mlsanity.com/paper/2212.09597/) (2022)
- [Reasoning or Reciting? Exploring the Capabilities and Limitations of Language Models Through Counterfactual Tasks](https://mlsanity.com/paper/2307.02477/) (2023)
- [OPT-IML: Scaling Language Model Instruction Meta Learning through the Lens of Generalization](https://mlsanity.com/paper/2212.12017/) (2022)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [BABILong: Testing the Limits of LLMs with Long Context Reasoning-in-a-Haystack](https://mlsanity.com/paper/2406.10149/) (2024)
- [ROSCOE: A Suite of Metrics for Scoring Step-by-Step Reasoning](https://mlsanity.com/paper/2212.07919/) (2022)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [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)
- [Multi-Step Reasoning with Large Language Models, a Survey](https://mlsanity.com/paper/2407.11511/) (2024)
- [UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression](https://mlsanity.com/paper/2212.02746/) (2022)
- [Exploring the Reasoning Abilities of Multimodal Large Language Models (MLLMs): A Comprehensive Survey on Emerging Trends in Multimodal Reasoning](https://mlsanity.com/paper/2401.06805/) (2024)
- [LLM Post-Training: A Deep Dive into Reasoning Large Language Models](https://mlsanity.com/paper/2502.21321/) (2025)
- [Faithful Reasoning Using Large Language Models](https://mlsanity.com/paper/2208.14271/) (2022)
- [Towards Faithful Model Explanation in NLP: A Survey](https://mlsanity.com/paper/2209.11326/) (2022)
- [BIG-Bench Extra Hard](https://mlsanity.com/paper/2502.19187/) (2025)
- [Deductive Verification of Chain-of-Thought Reasoning](https://mlsanity.com/paper/2306.03872/) (2023)
- [AI Transparency in the Age of LLMs: A Human-Centered Research Roadmap](https://mlsanity.com/paper/2306.01941/) (2023)
- [GeomVerse: A Systematic Evaluation of Large Models for Geometric Reasoning](https://mlsanity.com/paper/2312.12241/) (2023)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [Faithful Logical Reasoning via Symbolic Chain-of-Thought](https://mlsanity.com/paper/2405.18357/) (2024)

## Abstract (arXiv)

Transformers have been shown to emulate logical deduction over natural language theories (logical rules expressed in natural language), reliably assigning true/false labels to candidate implications. However, their ability to generate implications of a theory has not yet been demonstrated, and methods for reconstructing proofs of answers are imperfect. In this work we show that a generative model, called ProofWriter, can reliably generate both implications of a theory and the natural language proof(s) that support them. In particular, iterating a 1-step implication generator results in proofs that are highly reliable, and represent actual model decisions (rather than post-hoc rationalizations). On the RuleTaker dataset, the accuracy of ProofWriter's proofs exceed previous methods by +9% absolute, and in a way that generalizes to proof depths unseen in training and on out-of-domain problems. We also show that generative techniques can perform a type of abduction with high precision: Given a theory and an unprovable conclusion, identify a missing fact that allows the conclusion to be proved, along with a proof. These results significantly improve the viability of neural methods for systematically reasoning over natural language.