# Premise Selection for Theorem Proving by Deep Graph Embedding

arXiv: https://arxiv.org/abs/1709.09994 · HTML: https://mlsanity.com/paper/1709.09994/

## Key facts

- Cited by 44 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Sep 2017.

## Built on by (most cited first, 30 of 44)

- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [Premise Order Matters in Reasoning with Large Language Models](https://mlsanity.com/paper/2402.08939/) (2024)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning](https://mlsanity.com/paper/2101.06223/) (2021)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [Embedding Symbolic Temporal Knowledge into Deep Sequential Models](https://mlsanity.com/paper/2101.11981/) (2021)
- [Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving](https://mlsanity.com/paper/2404.07382/) (2024)
- [ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis](https://mlsanity.com/paper/2501.18310/) (2025)
- [Vampire With a Brain Is a Good ITP Hammer](https://mlsanity.com/paper/2102.03529/) (2021)
- [MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation](https://mlsanity.com/paper/2505.10962/) (2025)
- [A Survey in Mathematical Language Processing](https://mlsanity.com/paper/2205.15231/) (2022)
- [SyGNS: A Systematic Generalization Testbed Based on Natural Language Semantics](https://mlsanity.com/paper/2106.01077/) (2021)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [ATG: Benchmarking Automated Theorem Generation for Generative Language Models](https://mlsanity.com/paper/2405.06677/) (2024)
- [CoProver: A Recommender System for Proof Construction](https://mlsanity.com/paper/2304.10486/) (2023)
- [Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification](https://mlsanity.com/paper/2504.17017/) (2025)
- [A Study of Continuous Vector Representationsfor Theorem Proving](https://mlsanity.com/paper/2101.09142/) (2021)
- [An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations](https://mlsanity.com/paper/2305.08676/) (2023)
- [Graph Contrastive Pre-training for Effective Theorem Reasoning](https://mlsanity.com/paper/2108.10821/) (2021)
- [Lemmas: Generation, Selection, Application](https://mlsanity.com/paper/2303.05854/) (2023)
- [Exploring the Limits of Fine-grained LLM-based Physics Inference via Premise Removal Interventions](https://mlsanity.com/paper/2404.18384/) (2024)
- [COMPOSE: Composing Future Theorems from Citations and Formal Structure](https://mlsanity.com/paper/2605.30333/) (2026)
- [Learning Structure-Aware Representations of Dependent Types](https://mlsanity.com/paper/2402.02104/) (2024)
- [BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving](https://mlsanity.com/paper/2403.03401/) (2024)
- [Exploring Representation of Horn Clauses using GNNs (Extended Technical Report)](https://mlsanity.com/paper/2206.06986/) (2022)

## Abstract (arXiv)

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