@article{Crouse_Abdelaziz_Makni_Whitehead_Cornelio_Kapanipathi_Srinivas_Thost_Witbrock_Fokoue_2021, title={A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving}, volume={35}, url={https://ojs.aaai.org/index.php/AAAI/article/view/16780}, DOI={10.1609/aaai.v35i7.16780}, abstractNote={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).}, number={7}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Crouse, Maxwell and Abdelaziz, Ibrahim and Makni, Bassem and Whitehead, Spencer and Cornelio, Cristina and Kapanipathi, Pavan and Srinivas, Kavitha and Thost, Veronika and Witbrock, Michael and Fokoue, Achille}, year={2021}, month={May}, pages={6279-6287} }