HolStep extracts intermediate statements and conjectures from HOL Light proofs, canonicalizes their textual representation and pairs useful proof steps with negative examples.
Cezary Kaliszyk, François Chollet and Christian Szegedy released HolStep, a BSD-licensed dataset derived from 11,400 HOL Light proofs with more than two million labeled training and test proof-step examples, together with benchmark tasks and baseline logistic-regression, convolutional and recurrent neural models for classifying useful proof steps.
HolStep extracts intermediate statements and conjectures from HOL Light proofs, canonicalizes their textual representation and pairs useful proof steps with negative examples. The release defines conditioned and unconditioned proof-step classification tasks and provides baseline code so researchers can compare learned representations and relevance models on a common formal-mathematics corpus.
The project helped shift machine learning for theorem proving from small bespoke experiments toward reusable datasets and reproducible evaluation. HolStep subsequently became a benchmark for neural architectures and an important historical precursor to later environment-plus-benchmark systems for formal mathematics.
Significance rationale: HolStep turned large-scale HOL Light proof traces into a public machine-learning dataset and benchmark with millions of labeled proof-step examples. By making premise usefulness and proof-step relevance measurable on real higher-order-logic mathematics, it supplied an early common substrate for neural theorem-proving research and directly enabled later work such as FormulaNet while anticipating richer HOL Light learning environments such as HOList.
—
—
The arXiv and ICLR research records establish the HolStep dataset, benchmark tasks and reported baseline experiments.
The public Deepmath repository retains HolStep baseline code and the original research record identifies the public dataset release. E3 records artifact-level inspectability rather than independent reproduction of every reported baseline result.
No corrections recorded.
