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.

翻译：前提选择对于大型理论推理至关重要，因为问题的庞大规模会迅速导致资源匮乏。本文提出了一种受图像描述领域启发的前提选择方法，在该领域中，语言模型会自动为给定图像生成合适的描述。类似地，我们尝试生成构建给定问题证明所需的公理序列。这是通过结合预训练图神经网络和语言模型实现的。我们评估了该方法的不同配置，并实现了比基线提升17.7%的改进。