HolStep: a Machine Learning Dataset for Higher-Order Logic Theorem Proving
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 baseline deep learning models
suited for the tasks (including convolutional neural networks and recurrent neural
networks). The results of our baseline models shows the promise of applying deep
learning to HOL theorem proving.
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 baseline deep learning models
suited for the tasks (including convolutional neural networks and recurrent neural
networks). The results of our baseline models shows the promise of applying deep
learning to HOL theorem proving.
Research Areas
