2019/04/05 by Kshitij Bansal, Bansal, Kshitij, Sarah M. Loos +7 · 3 voices
Computer Science · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Mathematics, Computing, and Information Processing
paper · pdf · doi:10.48550/arxiv.1904.03241
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.