T ext G raphs-16 Natural Language Premise Selection Task: Zero-Shot Premise Selection with Prompting Generative Language Models (2022)

Abstract: Automated theorem proving can benefit a lot from methods employed in natural language processing, knowledge graphs and information retrieval: this non-trivial task combines formal languages understanding, reasoning, similarity search. We tackle this task by enhancing semantic similarity ranking with prompt engineering, which has become a new paradigm in natural language understanding. None of our approaches requires additional training. Despite encouraging results reported by prompt engineering approaches for a range of NLP tasks, for the premise selection task vanilla re-ranking by prompting GPT-3 doesn’t outperform semantic similarity ranking with SBERT, but merging of the both rankings shows better results.

## introduction the recently proposed task of natural language premise selection for mathematical statements @xcite follows in line with tasks such as mathematical information retrieval @xcite and mathematical formula understanding (e.g. @xcite ). those tasks share the common objective to improve the processing and understanding of mathematical statements, which are a significant part of scientific information. on the other hand, with the advent of the attention mechanism @xcite pretrained and fine-tuned transformers, such as bert (see @xcite ), gpt-3 ( @xcite ) etc. were able to improve state of the art results for many natural language task. in this short paper we investigate the use of transformers for the natural language premise selection in the context of mathematical statements within the 1st shared task natural language premise selection at textgraphs2022 workshop @xcite . we propose embedding the knowledge base with a bert style transformer to obtain dense embedding of the statement in the knowledge base. by computing similarity of a given statement with the knowledge base we then obtain relevant candidates from the knowledge base that can be fed into a large language model, such as gpt-3, to rank the candidates according to their importance to the given statement. we look at two structurally different transformers to compute the embeddings. 1. sentence bert @xcite and 2. mathbert @xcite . the final ranking of the premises is done with gpt-3 using the openai playground. as this approach does not require further training of the transformer models and only uses the inherent knowledge it falls under the regime of zero-shot learning. ## related work transformer models are large and deep neural network based on the attention mechanism (see @xcite ) that where pretrained originally with general language processing and understanding tasks in mind (see @xcite , @xcite , @xcite , @xcite ). recently transformers have been applied to tasks apart from natural language processing and generation. models designed specifically for mathematical task can be found in @xcite and @xcite . premise selection @xcite ) can be viewed as a precursor for automated theorem proving @xcite . automated theorem proving has a long history @xcite and is recently being tackled with approaches using deep neural networks (e.g. @xcite , @xcite and also @xcite ). the approach in this paper is inspired by retro @xcite -a model that is able to reference a large knowledge base to solve general language tasks, by using a transformer on top of a frozen bert retriever -and recent successes in prompt engineering for very large language mod-els @xcite . ## dataset description the organizers provide a dataset foot_0 with a tf-idf baseline @xcite . provided data consist of training, validation and test sets and a knowledge base. each sample in the training and development sets includes id, theorem text and list of relevant premise id's. texts of theorems and premises are represented in l a t e x markup. dataset statistics are shown in ## approach description the central approach, which we have designed and evaluated for the premise selection task is leveraging prompting methods for re-ranking. overall idea of it is to generate a primary ranking and further improve it by prompting generative language model with an instruction and top-k candidates from the primary ranking. prompt-based learning in a new paradigm in natural language processing. "unlike traditional supervised learning, which trains a model to take in an input x and predict an output y as p (y|x), promptbased learning is based on language models that model the probability of text directly" @xcite . during prompt-based learning the original input x is modified using a template into a textual string prompt x ′ that has some unfilled slots (i.e., for model's answer), and then the language model is used for generating sequence completing the template. due to multitasking abilities of generative language models to perform well on a wide range of tasks, there has appeared a bunch of prompt engineering approaches (prompt sharing, decomposition, noising, etc.), i.e. authors of the survey in @xcite propose a typology including above 50 approaches. for the primary ranking we have implemented two unsupervised approaches without model finetuning on train or validation sets: first uses sentence transformers (see section 4.1) and second one uses mathbert foot_1 (see section 4.2) for embedding premise and theorems. both approaches score premises by computing cosine similarity between the text of premise and text of theorem. for re-ranking with prompt engineering we create prompts containing top-10 candidates from primary ranking and feed them to the gpt-3 model @xcite via openai playground foot_2 , model text-davinci-002. details of the approach are provided in sec. 4.3 and appendix. ## experiments gpt-like models, despite impressive performance on many nlp tasks under the zero-shot and fewshot setup, are not capable of long-term memory. during re-ranking, the model may favor last seen premises and "forget" the relevant ones, that were presented (ranked) first in the original ranking. we have implemented three simple experiments to estimate how the order of the premises in the prompt influences the gpt-3 generated ranking. results are provided in table2. experiment 1. favoring the "last seen premise". in this experiment, we checked, whether gpt-3 favours "last seen" (and, probably, irrelevant) premise in the end of the prompt to more relevant ones in the middle of the prompt. for this reason, premises with ranks 1 and 2 were swapped in the ranking obtained from gpt-3. since the mean average precision (map) decreased, it is possible to say, that gpt-3 at least relies on the meaning of premises while re-ranking. experiment 2a. "forgetting" a relevant premise. in this experiment, the premise id with rank 1 in ranking-sbert was moved closer to the ranking head in gpt-3 ranking (to rank 3). it slightly improved the gpt-3 ranking, but hasn't outperformed ranking-sbert approach. experiment 2b. "forgetting" a relevant premise. in this experiment, a merged ranking was created by inserting the premise with rank 1 from ranking-sbert, to the re-ranked results from gpt-3. this has resulted in major improvement and has shown, that gpt-3 struggles with memorizing relevant information and tends to increase the rank of relevant premises, if they appear at the beginning of a long sequence. ## results and error analysis results of approaches, described in section 4, are summarized in the results in the table steer towards the actively discussed question, have large language models (not only gpt-like) actually learned to do reasoning, or have they only memorized training examples @xcite , see also 6 , 7 . despite its game-changing performance for many nlp tasks, gpt-3 doesn't outperform sbert for the natural language premise selection task, where reasoning based on a large knowledge base is required. approach /accuracy train validation test phase ranking-sbert n/a n/a 0,1460 evaluation ranking-mathbert-edu n/a n/a 0.0609 post-competition re-ranking sbert with prompting gpt-3 n/a n/a 0,1423 evaluation experiment 1. favouring last seen item n/a n/a 0,1262 post-competition experiment 2a. merged ranking n/a n/a 0,1450 post-competition experiment 2b. merged ranking n/a n/a 0,1497 post-competition moreover, analysis of the gpt-3 generation output shows that the model occasionally repeated premise ids, omitted premise ids or "hallucinated" ids with comparable length during generation (total 16,5% of all premises). this erroneous output was not taken into account during re-ranking: it means, that for each sample there is a different portion of premises, re-ranked by gpt-3. prompt design should be implemented carefully, because gpt-3 tends to rely on the order of premises in the prompt, as well as on its meaning. although the model doesn't really favor the last seen information in the prompt, it suffers from forgetting relevant information, if it was presented at the beginning of the prompt. this can be handled, for example by randomly shuffling elements subjected to re-ranking by gpt-3. overall, re-ranking by prompting generative language models, in a vanilla setup, does not improve similarity-based ranking, although merging these two rankings brings a better result. ## limitations and future work while the approach presented here requires conceptually low resources compared to fine-tuning to the given training data, the use of gpt-3 comes with a significant cost (with the most capable model costing up to $0.02 for 1000 tokens). furthermore, mathematical formulas are non-typical input for training general language models and hence tokenization might be less accurate thus also reducing the capability of the transformer models used for pre-ranking as they come with a maximum sequence length (512 for sbert, mathbert-edu and mathbert). performance of the proposed similarity ranking and prompt engineering approach, and available results from the shared task leaderboard show, that automated theorem proving is a hard task for nlu methods. l a t e xmarkup remains a hard type of input for encoders, that could possibly be overcome by using language models that have been pre-trained on l a t e x(e.g. mathbert) or inputagnostic models, such as perceiver. furthermore, transformation of formulas into typesetting invariant representations should be investigated. especially the representation of formulas as operator trees or translation to natural language might be beneficial in combination with general language models.