A Deep Reinforcement Learning Approach to First-Order Logic 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).
Cite
Text
Crouse et al. "A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving." AAAI Conference on Artificial Intelligence, 2021. doi:10.1609/AAAI.V35I7.16780Markdown
[Crouse et al. "A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving." AAAI Conference on Artificial Intelligence, 2021.](https://mlanthology.org/aaai/2021/crouse2021aaai-deep/) doi:10.1609/AAAI.V35I7.16780BibTeX
@inproceedings{crouse2021aaai-deep,
title = {{A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving}},
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},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2021},
pages = {6279-6287},
doi = {10.1609/AAAI.V35I7.16780},
url = {https://mlanthology.org/aaai/2021/crouse2021aaai-deep/}
}