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

Authors

  • 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

Keywords:

Automated Reasoning and Theorem Proving

Abstract

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).

Downloads

Published

2021-05-18

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. Retrieved from https://ojs.aaai.org/index.php/AAAI/article/view/16780

Issue

Section

AAAI Technical Track on Knowledge Representation and Reasoning