Elamur Research
☰
home / papers / 2021 / ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language

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

Written for the Research library (claude-opus-5-5) from the paper text. Original — aclanthology.org/2021.findings-acl.317.pdf

Summary

Earlier work (RuleTaker) showed that transformers can label candidate conclusions as true or false given rules and facts written in English. These models could not produce the conclusions themselves, and the proofs reconstructed by PRover were imperfect and not guaranteed to match the model's actual reasoning. ProofWriter addresses this with a generative approach built on T5-11B, covering three tasks:

  • answering a question together with a proof,
  • listing all implications of a theory,
  • a restricted form of abduction: finding a missing fact that would make an unprovable statement provable.

Proofs are linearized into a Polish-notation string that references sentence identifiers. In the Iterative variant, the model repeatedly derives single-step inferences, adds them back to the context, and assembles full proofs from these fragments. Because the proofs come from the model's own inference steps, they are faithful rather than post-hoc rationalizations. On the RuleTaker data, proof accuracy improves by 9 points absolute over prior work. The method also generalizes to deeper proofs and to out-of-domain rulebases, which makes neural reasoning over natural language more practical and explainable.

Key points

  • Supports both closed-world (negation as failure) and open-world (True/False/Unknown) Datalog-style semantics. Proofs are DAGs that alternate between fact nodes and rule nodes and include intermediate conclusions.
  • Proof generation strategies:
    • All-At-Once is simple and efficient but generalizes less well to proofs deeper than those seen in training.
    • Iterative is robust to depth because single-step inference is highly reliable.
  • Abduction, trained on D3-Ab and tested on D3-Ab and D5-Ab:
    • F1 and exact-match accuracy are above 85%.
    • Recall falls as the required proof depth increases.
  • Zero-shot abduction on Birds-Electricity (OWA): perfect on the Birds rulebases, but dropping to 64% F1 and 62% accuracy on harder Electricity theories.
  • Limitations and resources:
    • The Iterative approach is unguided forward-chaining and can exceed T5's 512-token input limit.
    • The datasets are released at allenai.org/data/proofwriter.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

Fields: Natural language processing

Cited by

214 papers of our library cite it (of the 140673 whose bibliographies we read); 15 of them have a page here, 199 not yet.

Cite

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2021.findings-acl.317 · arXiv 2012.13048

@inproceedings{tafjord2021proofwriter,
  title = {{ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language}},
  author = {Tafjord, Oyvind and Dalvi, Bhavana and Clark, Peter},
  booktitle = {Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021},
  year = {2021},
  doi = {10.18653/v1/2021.findings-acl.317},
  eprint = {2012.13048},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.18653/v1/2021.findings-acl.317}
}

References

26 references, 5 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Chandra Bhagavatula, Ronan Le Bras, Chaitanya Malaviya, Keisuke Sakaguchi, Ari Holtzman, Hannah Rashkin, Doug Downey, S. Yih, and Yejin Choi. 2020. Abductive commonsense reasoning. In ICLR’20. find our card
  2. Oana-Maria Camburu, Tim Rocktäschel, Thomas Lukasiewicz, and Phil Blunsom. 2018. e-SNLI: Natural language inference with natural language explanations. In Advances in Neural Information Processing Systems, pages 9539–9549. find our card
  3. 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. find
  4. 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. find our card
  5. Stanislas Polu and Ilya Sutskever. 2020. Generative language modeling for automated theorem proving. ArXiv, abs/2009.03393. find our card
  6. S. Ceri, G. Gottlob, and L. Tanca. 1989. What you always wanted to know about datalog (and never dared to ask). IEEE Trans. Knowl. Data Eng., 1:146–166. find
  7. Colin Raffel, Noam Shazeer, Adam Roberts, Katherine Lee, Sharan Narang, M. Matena, Yanqi Zhou, W. Li, and Peter J. Liu. 2020. Exploring the limits of transfer learning with a unified text-to-text transformer. J. Mach. Learn. Res., 21:140:1–140:67. find
  8. Peter Clark, Oyvind Tafjord, and Kyle Richardson. 2020. Transformers as soft reasoners over language. In IJCAI’20. find our card
  9. Tim Rocktäschel and S. Riedel. 2017. End-to-end differentiable proving. In NeurIPS. find
  10. 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. find
  11. Nicolas Gontier, Koustuv Sinha, Siva Reddy, and C. Pal. 2020. Measuring systematic generalization in neural proof generation with transformers. In NeurIPS’20. find
  12. J. Hobbs, Mark E. Stickel, Douglas E. Appelt, and P. Martin. 1993. Interpretation as abduction. Artificial Intelligence, 63:69–142. find
  13. Swarnadeep Saha, Sayan Ghosh, Shashank Srivastava, and Mohit Bansal. 2020. PRover: Proof generation for interpretable reasoning over rules. In EMNLP’20. find
  14. 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. find
  15. 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. find
  16. 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. find
  17. Alon Talmor, Oyvind Tafjord, P. Clark, Y. Goldberg, and Jonathan Berant. 2020. LeapOfThought: Teaching pre-trained models to systematically reason over implicit knowledge. In NeurIPS. find
  18. Harsh Jhamtani and P. Clark. 2020. Learning to explain: Datasets and models for identifying valid reasoning chains in multihop question-answering. In EMNLP. find
  19. Ming-Zhe Wang and Jun Deng. 2020. Learning to prove theorems by learning to generate theorems. In NeurIPS. find
  20. Aishwarya Kamath and Rajarshi Das. 2019. A survey on semantic parsing. In AKBC’19. find
  21. Leon Weber, Pasquale Minervini, Jannes Münchmeyer, Ulf Leser, and Tim Rocktäschel. 2019. Nlprolog: Reasoning with weak unification for question answering in natural language. In ACL. find
  22. K. Konolige. 1997. Abductive theories in artificial intelligence. In Principles of Knowledge Representation. find
  23. John McCarthy. 1984. Applications of circumscription to formalizing common sense knowledge. In NMR. find
  24. John W. McCarthy. 1959. Programs with common sense. In Proc. Tedding Conf. on the Mechanization of Thought Processes, pages 75–91. find
  25. Mark A Musen and Johan Van der Lei. 1988. Of brittleness and bottlenecks: Challenges in the creation of pattern-recognition and expert-system models. In Machine Intelligence and Pattern Recognition, volume 7, pages 335–352. Elsevier. find
  26. Appendix: ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language find