HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving.

Large computer-understandable proofs consist of millions of intermediatelogical steps. The vast majority of such steps originate from manuallyselected and manually guided heuristics applied to intermediate goals.So far, machine learning has generally not been used to filter orgenerate these steps. In this paper, we introduce a new dataset based onHigher-Order Logic (HOL) proofs, for the purpose of developing newmachine learning-based theorem-proving strategies. We make this datasetpublicly available under the BSD license. We propose various machinelearning tasks that can be performed on this dataset, and discuss theirsignificance for theorem proving. We also benchmark a set of simple baselinemachine learning models suited for the tasks (including logistic regressionconvolutional neural networks and recurrent neural networks). The results of ourbaseline models show the promise of applying machine learning to HOLtheorem proving.