HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving
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 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 approaches. We also present a deep reinforcement learning driven automated theorem prover, DeepHOL, that gives strong initial results on this benchmark.
Cite
Text
Bansal et al. "HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving." International Conference on Machine Learning, 2019.Markdown
[Bansal et al. "HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving." International Conference on Machine Learning, 2019.](https://mlanthology.org/icml/2019/bansal2019icml-holist/)BibTeX
@inproceedings{bansal2019icml-holist,
title = {{HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving}},
author = {Bansal, Kshitij and Loos, Sarah and Rabe, Markus and Szegedy, Christian and Wilcox, Stewart},
booktitle = {International Conference on Machine Learning},
year = {2019},
pages = {454-463},
volume = {97},
url = {https://mlanthology.org/icml/2019/bansal2019icml-holist/}
}