In plain words: A free toolkit turns the HOL Light prover's library of theorems into an arena where AI systems learn to prove statements in higher-order logic. A reinforcement-learning prover trained in it shows strong results on a benchmark drawn from calculus and the Kepler conjecture proof.
Abstract · HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
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.
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox
arXiv:1904.03241 · cs.LO, cs.AI, cs.LG · submitted Apr 5, 2019 · updated Nov 1, 2019
abstract · pdf · html · Accepted at ICML 2019
I'd be delighted to see "deep learning" produce a non-trivial breakthrough, but it feels like theorem proving must be about as hard as it gets for just learning a heuristic from piles of examples.
In particular, it's very easy to prove boring theorems, very hard to prove outstanding conjectures, and downright impossible to work out which theorems will turn out to be interesting.