HOList 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 all top 5 Cited by 29 Authors 5 Urban, Josef 3 Zombori, Zsolt 2 Kaliszyk, Cezary 1 Balog, Matej 1 Barekatain, Mohammadamin 1 Blaauwbroek, Lasse 1 Brown, Chad Edward 1 Černỳ, Prokop 1 Csiszárik, Adrián 1 Fawzi, Alhussein 1 Hassabis, Demis 1 Heskes, Tom M. 1 Huang, Aja 1 Hubert, Thomas 1 Janota, Mikoláš 1 Kohli, Pushmeet 1 Koutsoukou-Argyraki, Angeliki 1 Michalewski, Henryk 1 Olšák, Miroslav 1 Piepenbrock, Jelle 1 Piotrowski, Bartosz 1 Rawson, Michael 1 Reger, Giles 1 Romera-Paredes, Bernardino 1 Ruiz, Francisco J. R. 1 Schrittwieser, Julian 1 Silver, David M. 1 Świrszcz, Grzegorz M. 1 Zhang, Liao Cited in 1 Serial 1 Nature, London Cited in 3 Fields 8 Computer science (68-XX) 1 Group theory and generalizations (20-XX) 1 Numerical analysis (65-XX) Citations by Year