# Premise Selection for Theorem Proving by Deep Graph Embedding

Source: [Premise Selection for Theorem Proving by Deep Graph Embedding](<https://www.sota2.com/research/paper/68fa63ba1e209131cea00732>)

Collection index: [llms.txt](<https://www.sota2.com/research/llms.txt>)

Data updated: 2026-01-04T02:54:35.447Z

Authors: Mingzhe Wang, Yihe Tang, Jian Wang, Jia Deng

Published: 2017-09-28T14:44:40.000Z

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

## Recorded benchmark results

A research result applies to its stated dataset, split, metric and evaluation configuration. Compare like-for-like settings, preserve the metric's unit and direction, and distinguish paper-reported results from independent reproduction. The best result recorded here is not a claim of exhaustive, current global coverage.

- [Premise Selection on HolStep (test)](<https://www.sota2.com/research/sota/premise-selection-on-holstep-test.md>): Premise Selection; HolStep (test); Accuracy: 90.3.

- [Proof step classification on Holstep (test)](<https://www.sota2.com/research/sota/proof-step-classification-on-holstep-test.md>): Proof step classification; HolStep (test); Accuracy: 90.3.

## Original sources and implementation

[Original paper](<https://arxiv.org/abs/1709.09994>)

[PDF](<https://arxiv.org/pdf/1709.09994.pdf>)