Timezone: »
Spotlight
Premise Selection for Theorem Proving by Deep Graph Embedding
Mingzhe Wang · Yihe Tang · Jian Wang · Jia Deng
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)
-
2017 Poster: Premise Selection for Theorem Proving by Deep Graph Embedding »
Thu. Dec 7th 02:30 -- 06:30 AM Room Pacific Ballroom #92
More from the Same Authors
-
2017 Poster: Pixels to Graphs by Associative Embedding »
Alejandro Newell · Jia Deng -
2017 Poster: Associative Embedding: End-to-End Learning for Joint Detection and Grouping »
Alejandro Newell · Zhiao Huang · Jia Deng -
2016 Poster: Single-Image Depth Perception in the Wild »
Weifeng Chen · Zhao Fu · Dawei Yang · Jia Deng -
2014 Workshop: Representation and Learning Methods for Complex Outputs »
Richard Zemel · Dale Schuurmans · Kilian Q Weinberger · Yuhong Guo · Jia Deng · Francesco Dinuzzo · Hal Daumé III · Honglak Lee · Noah A Smith · Richard Sutton · Jiaqian YU · Vitaly Kuznetsov · Luke Vilnis · Hanchen Xiong · Calvin Murdock · Thomas Unterthiner · Jean-Francis Roy · Martin Renqiang Min · Hichem SAHBI · Fabio Massimo Zanzotto