HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version). Bansal, K., Loos, S. M, Rabe, M. N, Szegedy, C., & Wilcox, S. , 2019.
abstract   bibtex   
We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic. Higher-order interactive theorem provers enable the formalization of arbitrary mathematical theories and thereby present an interesting, open-ended challenge for deep learning. We provide an open-source framework based on the HOL Light theorem prover that can be used as a reinforcement learning environment. HOL Light comes with a broad coverage of basic mathematical theorems on calculus and the formal proof of the Kepler conjecture, from which we derive a challenging benchmark for automated reasoning. We also present a deep reinforcement learning driven automated theorem prover, DeepHOL, with strong initial results on this benchmark.
@Article{Bansal2019,
author = {Bansal, Kshitij and Loos, Sarah M and Rabe, Markus N and Szegedy, Christian and Wilcox, Stewart}, 
title = {HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version)}, 
journal = {}, 
volume = {}, 
number = {}, 
pages = {}, 
year = {2019}, 
abstract = {We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic. Higher-order interactive theorem provers enable the formalization of arbitrary mathematical theories and thereby present an interesting, open-ended challenge for deep learning. We provide an open-source framework based on the HOL Light theorem prover that can be used as a reinforcement learning environment. HOL Light comes with a broad coverage of basic mathematical theorems on calculus and the formal proof of the Kepler conjecture, from which we derive a challenging benchmark for automated reasoning. We also present a deep reinforcement learning driven automated theorem prover, DeepHOL, with strong initial results on this benchmark.}, 
location = {}, 
keywords = {}}

Downloads: 0