Skip to yearly menu bar Skip to main content


HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving

Kshitij Bansal · Sarah Loos · Markus Rabe · Christian Szegedy · Stewart Wilcox

Pacific Ballroom #244

Keywords: [ Other Applications ] [ Large Scale Learning and Big Data ] [ Deep Sequence Models ] [ Deep Reinforcement Learning ] [ Algorithms ]


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.

Live content is unavailable. Log in and register to view live content