The DOI matches its Crossref record; 21 of the 25 references it cites were found in a registry or an index.
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 proofs 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.1
Overview
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
Figures
![Figure 4 [Task 1] All-At-Once proofs can be verified by checking each step as a separate QA query.](/paper-figures/063dd318c078425ab0814082c0fc932b/proofwriter-generating-implications-proofs-and-abductive-statements-over-natural-figure-4.png)
Verification
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?
The cited source doesn’t support the claim as written.
In the citing paper
“ProofWriter (Tafjord et al., 2021) is a synthetic dataset created to assess deductive reasoning abilities of LLMs.”
From OpenHands: An Open Platform for AI Software Developers as Generalist Agents (2024) · cites this paper as Tafjord et al., 2021
Checked by a reasoning model — may be wrong.
Experimental — accuracy not yet measuredThe cited source doesn’t support the claim as written.
In the citing paper
“ProofWriter, meanwhile, is a synthetically generated dataset for logical reasoning over natural language.”
From LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers (2023) · cites this paper as Tafjord et al., 2021
Checked by a reasoning model — may be wrong.
Experimental — accuracy not yet measuredThe cited source says what the claim attributes to it.
In the citing paper
“Early work on deductive reasoning benchmarks such as RuleTaker (Clark et al., 2020) and ProofWriter (Tafjord et al., 2021) established the basic setup of query answering over sets of rules and facts, with ProofWriter reaching a maximum proof depth of five steps.ProntoQA (Saparov and He, 2023) introduces proof-structure controls and formal error attribution, also evaluated up to five hops.”
From Probing for Long-Horizon Deductive Reasoning Capabilities in Language Models with Prolog (2026) · cites this paper as Tafjord et al., 2021
The cited source says what the claim attributes to it.
In the citing paper
“These benchmarks revealed that models at the time struggle as proof depth increases, but the depths studied remain shallow.”
From Probing for Long-Horizon Deductive Reasoning Capabilities in Language Models with Prolog (2026) · cites this paper as Tafjord et al., 2021
The cited source says what the claim attributes to it.
In the citing paper
“This process is algorithmic; a model that has learned a robust implementation of this algorithm should, in principle, generalize beyond the shallow depths seen in previous benchmarks (Clark et al., 2020;Tafjord et al., 2021;Saparov and He, 2023).”
From Probing for Long-Horizon Deductive Reasoning Capabilities in Language Models with Prolog (2026) · cites this paper as Tafjord et al., 2021
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Citations
Cites
Hobbs, J. R., Stickel, M. E., Appelt, D. E., & Martin, P. (1988) · Artificial Intelligence · doi:10.1016/0004-3702(93)90015-4 · Cited by 1,222
Applications of circumscription to formalizing common-sense knowledge
McCarthy, J. (1986) · Artificial Intelligence · doi:10.1016/0004-3702(86)90032-9 · Cited by 1,114
McCarthy, J. (1960) · Cited by 799
Language Models as Knowledge Bases?Preprint
Petroni, F., Rocktäschel, T., Lewis, P., Bakhtin, A., Wu, Y., Miller, A., & Riedel, S. (2019) · arXiv (Cornell University) · doi:10.48550/arxiv.1909.01066 · Cited by 714
What you always wanted to know about Datalog (and never dared to ask)
Ceri, S., Gottlob, G., & Tanca, L. (1989) · IEEE Transactions on Knowledge and Data Engineering · doi:10.1109/69.43410 · Cited by 704
ERASER: A Benchmark to Evaluate Rationalized NLP Models
DeYoung, J., Jain, S., Rajani, N. F., Lehman, E., Xiong, C., Socher, R., & Wallace, B. C. (2020) · Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics · doi:10.18653/v1/2020.acl-main.408 · Cited by 561
e-SNLI: Natural language inference with natural language explanations
Camburu, O.-M., Rocktäschel, T., Lukasiewicz, T., & Blunsom, P. (2018) · arXiv · doi:10.48550/arxiv.1812.01193 · Cited by 367 · cited 2×
“Similarly, work on explanations has sought to gen-Proof erate human-style justifications, which again are typically supporting evidence rather than a fully-formed line of reasoning, and without explicit reasoning rules (Camburu et al., 2018; Jhamtani and Clark, 2020; Inoue et al., 2020).”
BackgroundWT5?! Training Text-to-Text Models to Explain their PredictionsPreprint
Narang, S., Raffel, C., Lee, K., Roberts, A., Fiedel, N., & Malkan, K. (2020) · arXiv (Cornell University) · doi:10.48550/arxiv.2004.14546 · Cited by 221
Transformers as Soft Reasoners over Language
Clark, P., Tafjord, O., & Richardson, K. (2020) · Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence · doi:10.24963/ijcai.2020/537 · Cited by 176
Self-citationA Survey on Semantic ParsingPreprint
Kamath, A., & Das, R. (2018) · arXiv (Cornell University) · doi:10.48550/arxiv.1812.00978 · Cited by 117
Research works printed but not linked: 4
- 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.
- Tim Rocktäschel and S. Riedel. 2017. End-to-end dif- ferentiable proving. In NeurIPS.
- 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.
- 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.
Cited by
Sorted by citations
Items 101–132 of 132
Ghosal, D., Aditya, S., & Choudhury, M. (2023) · International Joint Conference on Natural Language Processing and Conference of the Asia-Pacific Chapter of the Association for Computational Linguistics (IJCNLP-AACL) · doi:10.18653/v1/2023.ijcnlp-main.56
Exploring Abductive Reasoning in Language Models for Data-to-Text Generation
Onderková, K., & Nickles, M. (2023) · Irish Conference on Artificial Intelligence and Cognitive Science (AICS) · doi:10.1109/aics60730.2023.10470804
ProofsNavigator: A Bootstrap Base Method for Explainable Knowledge Reasoning
韦, 泽. (2024) · Computer Science and Application · doi:10.12677/csa.2024.147159
Reasoning in Transformers – Mitigating Spurious Correlations and Reasoning Shortcuts
Enström, D., Kjellberg, V., & Johansson, M. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-71170-1_18
Case-Based Deduction for Entailment Tree Generation
Shi, J., Ding, X., & Liu, T. (2024) · Mathematics · doi:10.3390/math12182893
Leveraging Semantic Parsing using Text Embeddings and Reinforcement Learning
Piza-Londoño, J., & Andrade-Lotero, E. J. (2024) · IEEE Latin American Conference on Computational Intelligence (LA-CCI) · doi:10.1109/la-cci62337.2024.10814850
Type-agnostic and form-oriented deductive conclusion generation
Wu, X., Bu, Y., Cai, Y., Chen, Y., & Leung, H.-F. (2025) · Neural Networks · doi:10.1016/j.neunet.2025.107968
Tan, X., Li, B., Xu, W., Qu, C., Chu, W., Xu, Y., Qi, Y., & Qiu, X. (2025) · Lecture notes in computer science · doi:10.1007/978-3-032-05127-1_40
Data-And Knowledge-Driven Visual Abductive Reasoning
Liang, C., Wang, W., Chen, L., & Yang, Y. (2025) · IEEE Transactions on Pattern Analysis and Machine Intelligence · doi:10.1109/tpami.2025.3613712
FoVer: First-Order Logic Verification for Natural Language Reasoning
Pei, Y., Du, Y., & Jin, X. (2025) · Transactions of the Association for Computational Linguistics · doi:10.1162/tacl.a.41
Reasoning with LLMs aided by Knowledge Bases and by Context
Garcez, L. R., & Cozman, F. G. (2025) · doi:10.5753/eniac.2025.12362
Zheng, X., Li, N., Luan, X., Wang, K., Shi, L., Sun, M., & Wang, H. (2026) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1145/3744916.3787820 · Cited by 6
Li, R., Sun, K., Shi, B., & Dong, B. (2025) · IEEE International Conference on Big Data (BigData) · doi:10.1109/bigdata66926.2025.11401932
Next-Gen Theorem Proving: A Multi-Agent Paradigm for Automated Reasoning
Chigullapally, A. G., Dantu, R., Zaman, S., & Pokharel, A. (2025) · IEEE International Conference on Cognitive Machine Intelligence (CogMI) · doi:10.1109/cogmi67134.2025.00013
Analysis of Semantic Communication for Logic-based Hypothesis Deduction
Saz, A. F., Xiong, S., & Fekri, F. (2025) · Globecom · doi:10.1109/globecom59602.2025.11432447
Nurhidayati, H., Nurchayati, Z., & Sugiarto (2026) · Research Square · doi:10.21203/rs.3.rs-8994226/v1
Zhu, J., Kou, G., & Wan, Z. (2026) · International Conference on Communication Networks and Machine Learning (CNML) · doi:10.1109/cnml68938.2026.11453070
Punchihewa, Y. (2026) · International Conference on Advanced Research in Computing (ICARC) · doi:10.1109/icarc68737.2026.11454006
A framework for the continuous curation of a knowledge base system
Ahmadi, N. (2021) · theses.fr (ABES) · doi:10.70675/7f54e1cez3f33z4329z8915z355f69842034
Employing Transformers and Humans for Textual-Claim Verification
Saeed, M. (2022) · theses.fr (ABES) · doi:10.70675/3e02a3a6z8281z4d84z8f38ze617eaaf969b
Intelligibility of Recurrent Neural Networks via Finite State Machines
Marzouk, M. R. (2024) · theses.fr (ABES) · doi:10.70675/67c57743zf027z4a51zbd70zddd2e546358f
DualAST: AST-Guided Exemplar Retrieval for In-Context Learning in Multi-Step Reasoning
Huang, H., Liu, C., & Yuan, M. (2026) · IEEE International Conference on Acoustics Speech and Signal Processing · doi:10.1109/icassp55912.2026.11462067
SoGRE: Boosting Logical Reasoning of LLMs via Solver-Guided Reasoning Enhancement
Wang, Z., Zhang, L., Zhang, M., Li, Q. P., & Zhang, M. (2026) · IEEE International Conference on Acoustics Speech and Signal Processing · doi:10.1109/icassp55912.2026.11463079
Exploring Confidence As A Reward to Advance LLMS Reasoning
Du, H., Li, B., Xie, C., Gao, C., Chen, K., & Tao, D. (2026) · IEEE International Conference on Acoustics Speech and Signal Processing · doi:10.1109/icassp55912.2026.11462883
Matrix as Plan: Structured Logical Reasoning with Feedback-Driven Replanning
Chen, K., Zeng, J., Peng, Z., Guo, L., Zhang, G., & Wang, T. (2026) · International World Wide Web Conference (WWW) · doi:10.1145/3774904.3792213
Automation of Polynomial Formal Verification using Large Language Models
Müller, L., Qayyum, K., Hugo, N., Hassan, M., & Drechsler, R. (2026) · IEEE VLSI Test Symposium (VTS) · doi:10.1109/vts69484.2026.11563380
Wang, Y., Seggoju, R. H., & Paschke, A. (2026) · Neurosymbolic Artificial Intelligence · doi:10.1177/29498732261469484
Neurosymbolic Large Language Models: A Survey of Symbolic Integration, Reasoning and Explainability
Rani, M., Mishra, B. K., & Thakker, D. (2026) · Information Systems Frontiers · doi:10.1007/s10796-026-10794-4 · Cited by 2
Kadyrbek, N., & Мансурова, М. (2026) · Machine Learning and Knowledge Extraction · doi:10.3390/make8090269
Guo, M., Chen, C., Wang, T., & Cheng, L. (2026) · IEEE International Conference on Automation Science and Engineering (CASE) · doi:10.1109/case69030.2026.11704166
Xu, S., & Asadinia, M. (2026) · IEEE International Conference on Omni-layer Intelligent Systems (COINS) · doi:10.1109/coins69995.2026.11715614
SLR: Automated Synthesis for Scalable Logical Reasoning
Helff, L., Omar, A., Friedrich, F., Wüst, A., Shindo, H., Mitchell, R., Woydt, T., Schramowski, P., Stammer, W., & Kersting, K. (2026) · Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) · doi:10.18653/v1/2026.acl-long.16
Metadata
- Authors
- Tafjord, O., Dalvi, B., & Clark, P.
- Affiliations
- Allen Institute for Artificial Intelligence (US)
- ORCID
- Clark, Peter
- Venue
- Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021
- Published
- 2021
- Pages
- 3621-3634
- OpenAlex
- W3115201256
- Cited by
- 122
- References
- 25
- 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
- cc-by
- 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
