ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language
Open accessAbstract
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.
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
LINC has shown significant performance gains on the FOLIO and ProofWriter datasets compared to CoT prompting.
“This method has shown significant performance gains on the FOLIO (Han et al., 2022) and ProofWriter (Tafjord et al., 2020) datasets compared to CoT prompting.”
From Reliable Reasoning Beyond Natural Language (2024) · cites this paper as Tafjord et al., 2020
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Cites
No references could be resolved yet.
Research works printed but not linked: 20
- Chandra Bhagavatula, Ronan Le Bras, Chaitanya Malaviya, Keisuke Sakaguchi, Ari Holtzman, Han- nah Rashkin, Doug Downey, S. Yih, and Yejin Choi. 2020. Abductive commonsense reasoning. In ICLR'20.
- Oana-Maria Camburu, Tim Rocktäschel, Thomas Lukasiewicz, and Phil Blunsom. 2018. e-SNLI: Nat- ural language inference with natural language expla- nations. In Advances in Neural Information Process- ing Systems, pages 9539-9549.
- S. Ceri, G. Gottlob, and L. Tanca. 1989. What you al- ways wanted to know about datalog (and never dared to ask). IEEE Trans. Knowl. Data Eng., 1:146-166.
- Peter Clark, Oyvind Tafjord, and Kyle Richardson. 2020. Transformers as soft reasoners over language. In IJCAI'20.
- Jay DeYoung, Sarthak Jain, Nazneen Rajani, E. Lehman, Caiming Xiong, R. Socher, and Byron C. Wallace. 2019. ERASER: A benchmark to evaluate rationalized nlp models. In ACL.
- Nicolas Gontier, Koustuv Sinha, Siva Reddy, and C. Pal. 2020. Measuring systematic generalization in neural proof generation with transformers. In NeurIPS'20.
- N. Inoue, Pontus Stenetorp, and Kentaro Inui. 2020. R4C: A benchmark for evaluating RC systems to get the right answer for the right reason. In ACL.
- Harsh Jhamtani and P. Clark. 2020. Learning to ex- plain: Datasets and models for identifying valid rea- soning chains in multihop question-answering. In EMNLP.
- John W. McCarthy. 1959. Programs with common sense. In Proc. Tedding Conf. on the Mechanization of Thought Processes, pages 75-91.
- Mark A Musen and Johan Van der Lei. 1988. Of brit- tleness and bottlenecks: Challenges in the creation of pattern-recognition and expert-system models. In Machine Intelligence and Pattern Recognition, vol- ume 7, pages 335-352. Elsevier.
- Sharan Narang, Colin Raffel, Katherine Lee, A. Roberts, Noah Fiedel, and Karishma Malkan. 2020. WT5?! training text-to-text models to explain their predictions. ArXiv, abs/2004.14546. · arXiv
- F. Petroni, Tim Rocktäschel, Patrick Lewis, A. Bakhtin, Y. Wu, Alexander H. Miller, and S. Riedel. 2019. Language models as knowledge bases? In EMNLP.
- Stanislas Polu and Ilya Sutskever. 2020. Generative language modeling for automated theorem proving. ArXiv, abs/2009.03393. · arXiv
- Tim Rocktäschel and S. Riedel. 2017. End-to-end dif- ferentiable proving. In NeurIPS.
- Swarnadeep Saha, Sayan Ghosh, Shashank Srivastava, and Mohit Bansal. 2020. PRover: Proof gener- ation for interpretable reasoning over rules. In EMNLP'20.
- Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. 2019. Learning a SAT solver from single-bit supervision. In ICLR.
- Sanjay Subramanian, Ben Bogin, Nitish Gupta, Tomer Wolfson, Sameer Singh, Jonathan Berant, and Matt Gardner. 2020. Obtaining faithful interpretations from compositional neural networks. In ACL.
- Alon Talmor, Oyvind Tafjord, P. Clark, Y. Goldberg, and Jonathan Berant. 2020. LeapOfThought: Teach- ing pre-trained models to systematically reason over implicit knowledge. In NeurIPS.
- Ming-Zhe Wang and Jun Deng. 2020. Learning to prove theorems by learning to generate theorems. In NeurIPS.
- Leon Weber, Pasquale Minervini, Jannes Münchmeyer, Ulf Leser, and Tim Rocktäschel. 2019. Nlprolog: Reasoning with weak unification for question an- swering in natural language. In ACL.
Cited by
Sorted by citations
Reliable Reasoning Beyond Natural Language
Borazjanizadeh, N., & Piantadosi, S. T. (2024) · arXiv · doi:10.48550/arxiv.2407.11373 · Cited by 3 · see citing works
- Authors
- Tafjord, O., Mishra, B. D., & Clark, P.
- Affiliations
- Allen Institute for Artificial Intelligence (US)
- ORCID
- Clark, Peter
- Venue
- arXiv
- Publisher
- arXiv
- Published
- 2020
- Pages
- 3621-3634
- arXiv
- 2012.13048
- OpenAlex
- W3115201256
- Cited by
- 122
- References
- 0
- Citations by year
- 2026: 22 · 2025: 18 · 2024: 14 · 2023: 32 · 2022: 27 · 2021: 9
- FWCI
- 9.47
- Type
- conference paper
- Language
- en
- Open access
- hybrid
- doi.org
- Licence
- Locations
- Findings of the Association for Computational Linguistics: ACL (Findings of ACL) (publishedVersion, cc-by)
- arXiv (Cornell University) (submittedVersion)
- arXiv (Cornell University)
- Topics
- Physical Sciences › Computer Science › Artificial Intelligence › Topic Modeling
- Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
- Physical Sciences › Computer Science › Artificial Intelligence › Natural Language Processing Techniques
- Keywords
- proof generation, abductive reasoning, large language models, generative models
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
