Timezone: »

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

Wed Dec 06 06:30 PM -- 10:30 PM (PST) @ Pacific Ballroom #92

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

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