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
in Probabilistic Methods, Applications »

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

Author Information

Mingzhe Wang (University of Michigan)
Yihe Tang (Carnegie Mellon University)
Jian Wang (University of Michigan)
Jia Deng (University of Michigan)

Related Events (a corresponding poster, oral, or spotlight)

More from the Same Authors