Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
arXiv:1108.3446 · doi:10.1007/s10817-013-9286-5
Abstract
Smart premise selection is essential when using automated reasoning as a tool for large-theory formal proof development. A good method for premise selection in complex mathematical libraries is the application of machine learning to large corpora of proofs. This work develops learning-based premise selection in two ways. First, a newly available minimal dependency analysis of existing high-level formal mathematical proofs is used to build a large knowledge base of proof dependencies, providing precise data for ATP-based re-verification and for training premise selection algorithms. Second, a new machine learning algorithm for premise selection based on kernel methods is proposed and implemented. To evaluate the impact of both techniques, a benchmark consisting of 2078 large-theory mathematical problems is constructed,extending the older MPTP Challenge benchmark. The combined effect of the techniques results in a 50% improvement on the benchmark over the Vampire/SInE state-of-the-art system for automated reasoning in large theories.
26 pages
References in corpus (4)
Cited by in corpus (35)
- Learning-Assisted Automated Reasoning with Flyspeck
- MizAR 40 for Mizar 40
- HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
- Premise Selection for Theorem Proving by Deep Graph Embedding
- Holophrasm: a neural Automated Theorem Prover for higher-order logic
- Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling
- Property Invariant Embedding for Automated Reasoning
- Hammering Mizar by Learning Clause Guidance
- HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
- Learning to Reason in Large Theories without Imitation
- Developments in Formal Proofs
- Learning Guided Automated Reasoning: A Brief Survey
- GRUNGE: A Grand Unified ATP Challenge
- Monte Carlo Tableau Proof Search
- ProofWatch: Watchlist Guidance for Large Theories in E
- Proof Artifact Co-training for Theorem Proving with Language Models
- Number Theory and Axiomatic Geometry in the Diproche System
- Natural Language Premise Selection: Finding Supporting Statements for Mathematical Text
- An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic
- New developments in parsing Mizar
- Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
- Mining State-Based Models from Proof Corpora
- A Curiously Effective Backtracking Strategy for Connection Tableaux
- Constraint Learning for Non-confluent Proof Search
- First Experiments with Neural cvc5
- Controlling Search in Very large Commonsense Knowledge Bases: A Machine Learning Approach
- Extending E Prover with Similarity Based Clause Selection Strategies
- Vampire With a Brain Is a Good ITP Hammer
- Certified Connection Tableaux Proofs for HOL Light and TPTP
- BliStrTune: Hierarchical Invention of Theorem Proving Strategies
- Machine Learning for Quantifier Selection in cvc5
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- Machine Learning Guidance and Proof Certification for Connection Tableaux
- Learning-assisted Theorem Proving with Millions of Lemmas
- Lemma Mining over HOL Light