swMATH ID: 43881
Software Authors: Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox
Description: 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.
Homepage: https://sites.google.com/view/holist/home
Keywords: Logic; arXiv_cs.LO; Artificial Intelligence; arXiv_cs.AI; Machine Learning; arXiv_cs.LG; Theorem Proving
Related Software: ENIGMA; E Theorem Prover; GitHub; FEMaLeCoP; VAMPIRE; ileanCoP; leanCoP; XGBoost; MaLeCoP; TacticToe; Coq; ATPboost; Adam; HOL; DeepMath; MaLARea; HOL Light; lazyCoP; TPTP; Isabelle/HOL
Cited in: 8 Publications

Cited in 1 Serial

1 Nature, London

Citations by Year