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 .
@cite_36: 
@cite_31: 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.
@cite_14: Smart premise selection is essential when using automated reasoning as a tool for large-theory formal proof development. This work develops learning-based premise selection in two ways. First, a fine-grained 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 state-of-the-art Vampire SInE system for automated reasoning in large theories.
Premise selection as a machine learning problem was introduced by @cite_14 , who constructed a corpus of proofs to train a kernelized classifier using bag-of-word features that represent the occurrences of terms in a vocabulary. Deep learning techniques were first applied to premise selection in the DeepMath work by @cite_36 , who applied recurrent networks and convolutional to formulas represented as textual sequences, and showed that deep learning approaches can achieve competitive results against baselines using hand-engineered features. Serving the needs for large datasets for training deep models, @cite_31 introduced the HolStep dataset that consists of 2M statements and 10K conjectures, an order of magnitude larger than the DeepMath dataset @cite_36 .