`

Timezone: »

Spotlight
Premise Selection for Theorem Proving by Deep Graph Embedding
Mingzhe Wang · Yihe Tang · Jian Wang · Jia Deng

Wed Dec 06 05:45 PM -- 05:50 PM (PST) @ Hall C

We propose a deep learning approach to premise selection: selecting relevant mathematical statements for the automated proof of a given conjecture. We represent a higher-order logic formula as a graph that is invariant to variable renaming, but at the same time fully preserves syntactic and semantic information. We then embed the graph into a continuous vector via a novel embedding method that preserves the information of edge ordering. Our approach achieves the state-of-the-art results on the HolStep dataset, improving the classification accuracy from 83% to 90.3%.