Premise selection for theorem proving by deep graph embedding

Mingzhe Wang; Yihe Tang; Jian Wang; Jia Deng

Premise selection for theorem proving by deep graph embedding

Mingzhe Wang
, Yihe Tang
, Jian Wang
, Jia Deng

Research output: Contribution to journal › Conference article › peer-review

Abstract

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 language	English (US)
Pages (from-to)	2787-2797
Number of pages	11
Journal	Advances in Neural Information Processing Systems
Volume	2017-December
State	Published - 2017
Externally published	Yes
Event	31st Annual Conference on Neural Information Processing Systems, NIPS 2017 - Long Beach, United States Duration: Dec 4 2017 → Dec 9 2017

All Science Journal Classification (ASJC) codes

Computer Networks and Communications
Information Systems
Signal Processing

Cite this

@article{da73b40c3d984fabaae34195a9e042e7,

title = "Premise selection for theorem proving by deep graph embedding",

abstract = "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 = "Mingzhe Wang and Yihe Tang and Jian Wang and Jia Deng",

note = "Publisher Copyright: {\textcopyright} 2017 Neural information processing systems foundation. All rights reserved.; 31st Annual Conference on Neural Information Processing Systems, NIPS 2017 ; Conference date: 04-12-2017 Through 09-12-2017",

year = "2017",

language = "English (US)",

volume = "2017-December",

pages = "2787--2797",

journal = "Advances in Neural Information Processing Systems",

issn = "1049-5258",

publisher = "Neural information processing systems foundation",

}

TY - JOUR

T1 - Premise selection for theorem proving by deep graph embedding

AU - Wang, Mingzhe

AU - Tang, Yihe

AU - Wang, Jian

AU - Deng, Jia

PY - 2017

Y1 - 2017

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

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

UR - https://www.scopus.com/pages/publications/85047009600

UR - https://www.scopus.com/pages/publications/85047009600#tab=citedBy

M3 - Conference article

AN - SCOPUS:85047009600

SN - 1049-5258

VL - 2017-December

SP - 2787

EP - 2797

JO - Advances in Neural Information Processing Systems

JF - Advances in Neural Information Processing Systems

T2 - 31st Annual Conference on Neural Information Processing Systems, NIPS 2017

Y2 - 4 December 2017 through 9 December 2017

ER -

Premise selection for theorem proving by deep graph embedding

Abstract

All Science Journal Classification (ASJC) codes

Other files and links

Fingerprint

Cite this