# HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving Source: [HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving]() Collection index: [llms.txt]() Data updated: 2026-01-04T02:54:55.289Z Authors: Cezary Kaliszyk, Fran\\c{c}ois Chollet, Christian Szegedy Published: 2017-03-01T18:20:19.000Z ## Abstract Large computer-understandable proofs consist of millions of intermediate logical steps. The vast majority of such steps originate from manually selected and manually guided heuristics applied to intermediate goals. So far, machine learning has generally not been used to filter or generate these steps. In this paper, we introduce a new dataset based on Higher-Order Logic (HOL) proofs, for the purpose of developing new machine learning-based theorem-proving strategies. We make this dataset publicly available under the BSD license. We propose various machine learning tasks that can be performed on this dataset, and discuss their significance for theorem proving. We also benchmark a set of simple baseline machine learning models suited for the tasks (including logistic regression, convolutional neural networks and recurrent neural networks). The results of our baseline models show the promise of applying machine learning to HOL theorem proving. ## Recorded benchmark results A research result applies to its stated dataset, split, metric and evaluation configuration. Compare like-for-like settings, preserve the metric's unit and direction, and distinguish paper-reported results from independent reproduction. The best result recorded here is not a claim of exhaustive, current global coverage. - [Premise Selection on HolStep (test)](): Premise Selection; HolStep (test); Accuracy: 83. - [Proof step classification on Holstep (test)](): Proof step classification; HolStep (test); Accuracy: 83. ## Original sources and implementation [Original paper]() [PDF]() [Implementation]()