Timezone: »
Poster
Premise Selection for Theorem Proving by Deep Graph Embedding
Mingzhe Wang · Yihe Tang · Jian Wang · Jia Deng
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)
-
2017 Spotlight: Premise Selection for Theorem Proving by Deep Graph Embedding »
Thu. Dec 7th 01:45 -- 01:50 AM Room Hall C
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