Premise selection for theorem proving by deep graph embedding

Mingzhe Wang, Yihe Tang, Jian Wang, Jia Deng

Research output: Contribution to journalConference articlepeer-review

64 Scopus citations


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

Original languageEnglish (US)
Pages (from-to)2787-2797
Number of pages11
JournalAdvances in Neural Information Processing Systems
StatePublished - 2017
Externally publishedYes
Event31st Annual Conference on Neural Information Processing Systems, NIPS 2017 - Long Beach, United States
Duration: Dec 4 2017Dec 9 2017

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Information Systems
  • Signal Processing


Dive into the research topics of 'Premise selection for theorem proving by deep graph embedding'. Together they form a unique fingerprint.

Cite this