# Graph Sequence Learning for Premise Selection

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 Mar 2023.

## Built on by (most cited first, 5 of 5)

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [Solving Hard Mizar Problems with Instantiation and Strategy Invention](https://mlsanity.com/paper/2406.17762/) (2024)
- [Hierarchical Attention Generates Better Proofs](https://mlsanity.com/paper/2504.19188/) (2025)
- [Machine Learning for Quantifier Selection in cvc5](https://mlsanity.com/paper/2408.14338/) (2024)

## Abstract (arXiv)

Premise selection is crucial for large theory reasoning as the sheer size of the problems quickly leads to resource starvation. This paper proposes a premise selection approach inspired by the domain of image captioning, where language models automatically generate a suitable caption for a given image. Likewise, we attempt to generate the sequence of axioms required to construct the proof of a given problem. This is achieved by combining a pre-trained graph neural network with a language model. We evaluated different configurations of our method and experience a 17.7% improvement gain over the baseline.