HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version)

  • 2019-04-05 19:04:33
  • Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox
  • 5


We present an environment, benchmark, and deep learning driven automatedtheorem prover for higher-order logic. Higher-order interactive theorem proversenable the formalization of arbitrary mathematical theories and thereby presentan interesting, open-ended challenge for deep learning. We provide anopen-source framework based on the HOL Light theorem prover that can be used asa reinforcement learning environment. HOL Light comes with a broad coverage ofbasic mathematical theorems on calculus and the formal proof of the Keplerconjecture, from which we derive a challenging benchmark for automatedreasoning. We also present a deep reinforcement learning driven automatedtheorem prover, DeepHOL, with strong initial results on this benchmark.


Introduction (beta)



Conclusion (beta)