A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving


  • Maxwell Crouse Northwestern University
  • Ibrahim Abdelaziz IBM Research
  • Bassem Makni IBM Research
  • Spencer Whitehead University of Illinois at Urbana-Champaign
  • Cristina Cornelio IBM Research
  • Pavan Kapanipathi IBM Research
  • Kavitha Srinivas IBM Research
  • Veronika Thost MIT-IBM Watson AI Lab
  • Michael Witbrock The University of Auckland
  • Achille Fokoue IBM Research




Automated Reasoning and Theorem Proving


Automated theorem provers have traditionally relied on manually tuned heuristics to guide how they perform proof search. Deep reinforcement learning has been proposed as a way to obviate the need for such heuristics, however, its deployment in automated theorem proving remains a challenge. In this paper we introduce TRAIL, a system that applies deep reinforcement learning to saturation-based theorem proving. TRAIL leverages (a) a novel neural representation of the state of a theorem prover and (b) a novel characterization of the inference selection process in terms of an attention-based action policy. We show through systematic analysis that these mechanisms allow TRAIL to significantly outperform previous reinforcement-learning-based theorem provers on two benchmark datasets for first-order logic automated theorem proving (proving around 15% more theorems).




How to Cite

Crouse, M., Abdelaziz, I., Makni, B., Whitehead, S., Cornelio, C., Kapanipathi, P., Srinivas, K., Thost, V., Witbrock, M., & Fokoue, A. (2021). A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving. Proceedings of the AAAI Conference on Artificial Intelligence, 35(7), 6279-6287. https://doi.org/10.1609/aaai.v35i7.16780



AAAI Technical Track on Knowledge Representation and Reasoning