Premise Selection for Theorem Proving by Deep Graph Embedding
arXiv:1709.09994
Abstract
We propose a deep learning-based approach to the problem of premise selection: selecting mathematical statements relevant for proving a given conjecture. We represent a higher-order logic formula as a graph that is invariant to variable renaming but still fully preserves syntactic and semantic information. We then embed the graph into a vector via a novel embedding method that preserves the information of edge ordering. Our approach achieves state-of-the-art results on the HolStep dataset, improving the classification accuracy from 83% to 90.3%.
Mingzhe Wang and Yihe Tang contributed equally
References in corpus (8)
- Semi-Supervised Classification with Graph Convolutional Networks
- Deep Convolutional Networks on Graph-Structured Data
- Learning Convolutional Neural Networks for Graphs
- Gated Graph Sequence Neural Networks
- Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
- HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
- Holophrasm: a neural Automated Theorem Prover for higher-order logic
- Internal Guidance for Satallax