HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
arXiv:1904.03241
Abstract
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.
arXiv commentAccepted at ICML 2019
References in corpus (10)
- Adam: A Method for Stochastic Optimization
- WaveNet: A Generative Model for Raw Audio
- SQuAD: 100,000+ Questions for Machine Comprehension of Text
- Learning-Assisted Automated Reasoning with Flyspeck
- Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
- MizAR 40 for Mizar 40
- GamePad: A Learning Environment for Theorem Proving
- Premise Selection and External Provers for HOL4
- HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
- Holophrasm: a neural Automated Theorem Prover for higher-order logic
Cited by in corpus (8)
- The Ramanujan Machine: Automatically Generated Conjectures on Fundamental Constants
- Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling
- Learning to Reason in Large Theories without Imitation
- Mathematical Reasoning in Latent Space
- NaturalProofs: Mathematical Theorem Proving in Natural Language
- Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints
- Teaching Temporal Logics to Neural Networks
- Training a First-Order Theorem Prover from Synthetic Data