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 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.

References in corpus (2)

• Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
• Internal Guidance for Satallax

Cited by in corpus (14)

• End-to-End Differentiable Proving
• GamePad: A Learning Environment for Theorem Proving
• Premise Selection for Theorem Proving by Deep Graph Embedding
• HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
• A Formal Proof of PAC Learnability for Decision Stumps
• Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning
• Proof Artifact Co-training for Theorem Proving with Language Models
• Guiding High-Performance SAT Solvers with Unsat-Core Predictions
• Automated proof synthesis for propositional logic with deep neural networks
• Verifying Security Protocols using Dynamic Strategies
• Real-time Burst Photo Selection Using a Light-Head Adversarial Network
• BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
• Towards Concise, Machine-discovered Proofs of Gödel's Two Incompleteness Theorems
• Graph Contrastive Pre-training for Effective Theorem Reasoning