Datasets › HolStep
HolStep
HolStep is a dataset based on higher-order logic (HOL) proofs, for the purpose of developing new machine learning-based theorem-proving strategies.
Source: HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
Benchmarks archive 2025-07-28
All 2 leaderboards whose dataset resolves to this page shown (sort by any header). "First row" is the archive's own first row at snapshot, in the archive's row order; nothing here re-ranks and metric direction is not asserted.
| First row (archive order) | Paper | Code | ||||
|---|---|---|---|---|---|---|
| Automated Theorem Proving | HolStep (Conditional) | MPNN-DagLSTM Classification Accuracy 0.916 | Improving Graph Neural Network Representations of... | IBM/LogicalFormulaEmbedder | 5 | Compare |
| Automated Theorem Proving | HolStep (Unconditional) | FormulaNet Classification Accuracy 0.900 | Premise Selection for Theorem Proving by Deep Graph Embedding | princeton-vl/FormulaNet | 4 | Compare |
Papers archive 2025-07-28
3 shown of 3 papers with a leaderboard row on this dataset's benchmarks, newest first. The archive's own "papers using this dataset" list was never published, so this is the benchmark-backed subset; the archive's count for this dataset is 10. The Syntology column is from Syntology's graph (read 2026-09-24), stated per sample; it is not part of any archive number.
| Date | Samples run Syntology | |||
|---|---|---|---|---|
| Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling | 1 | 1 | 15 Nov 2019 | ran 0 of 3 samples (3 unverified) |
| Premise Selection for Theorem Proving by Deep Graph Embedding | 1 | 4 | 28 Sep 2017 | ran 1 of 1 samples (0 unverified) |
| HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving | 1 | 4 | 1 Mar 2017 | ran 0 of 6 samples (6 unverified) |
Dataset loaders archive 2025-07-28
No loader listed in the archive.
Tasks archive 2025-07-28
License archive 2025-07-28
BSD-3-Clause
Modalities archive 2025-07-28
No modality tagged.
Languages archive 2025-07-28
No language tagged.
Variants archive 2025-07-28
- HolStep (Conditional)
- HolStep (Unconditional)
- HolStep
3 variant names, as the archive lists them.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections