Research map / Learning theory and algorithms / Combinatorial and search optimization
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's title only (no summary yet). Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use a 1D CNN instead of logistic regression | Unconditioned proof step classification · HolStep, char input | accuracy: 0.71 -> 0.82 | Helped |
| Use a 1D CNN instead of logistic regression | Unconditioned proof step classification · HolStep, token input | accuracy: 0.71 -> 0.83 | Helped |
| Use a 1D CNN-LSTM instead of a 1D CNN | Unconditioned proof step classification · HolStep | accuracy: 0.82 -> 0.83 (char input); 0.83 -> 0.77 (token input) | Mixed |
| Use token-level rather than char-level input (ablation) | Unconditioned logistic regression · HolStep | accuracy: 0.71 -> 0.71 | No clear effect |
| Use token-level rather than char-level input (ablation) | Unconditioned 1D CNN · HolStep | accuracy: 0.82 -> 0.83 | No clear effect |
| Use token-level rather than char-level input (ablation) | Unconditioned 1D CNN-LSTM · HolStep | accuracy: 0.83 -> 0.77 | Hurt |
| Condition proof-step classification on the conjecture (ablation) | HolStep baseline classifiers · HolStep proof step classification | accuracy: 0.83 -> 0.83 (CNN-LSTM, char input); 0.83 -> 0.82 (CNN, token input) | No clear effect |
Closest papers by meaning
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.89)
- Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (NeurIPS 2025 · similarity 0.89)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.88)
- miniCTX: Neural Theorem Proving with (Long-)Contexts (ICLR 2025 · similarity 0.88)
- REFACTOR: Learning to Extract Theorems from Proofs (ICLR 2024 · similarity 0.88)
- MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation (NeurIPS 2025 · similarity 0.88)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.