SNLP at T ext G raphs 2022 Shared Task: Unsupervised Natural Language Premise Selection in Mathematical Texts Using Sentence- MPN et (2022)

Abstract: This paper describes our system for the submission to the TextGraphs 2022 shared task at COLING 2022: Natural Language Premise Selection (NLPS) from mathematical texts. The task of NLPS is about selecting mathematical statements called premises in a knowledge base written in natural language and mathematical formulae that are most likely to be used to prove a particular mathematical proof. We formulated this task as an unsupervised semantic similarity task by first obtaining contextualized embeddings of both the premises and mathematical proofs using sentence transformers. We then obtained the cosine similarity between the embeddings of premises and proofs and then selected premises with the highest cosine scores as the most probable. Our system improves over the baseline system that uses bag of words models based on term frequency inverse document frequency in terms of mean average precision (MAP) by about 23.5% (0.1516 versus 0.1228).

## introduction deep learning methods have achieved state of the art performance across several natural language processing (nlp) tasks in a wide variety of applications in several fields. despite the importance of the field of mathematics and its contribution to scientific discovery, the application of nlp to mathematical text is still under-explored @xcite . the task of natural language premise selection in mathematical text is a novel application of nlp in the field of mathematics. it involves selecting mathematical statements (premises) which are written in natural language and mathematical formulae that are most likely to be useful in proving a given conjecture or mathematical proof from a knowledge base. more formally, given a set of premises p and a new conjecture c, all written in a combination of free text and mathematical formulae, natural language premise selection (nlps) aims to select premises from p that will be helpful in proving a conjecture or proof c @xcite . this is not a trivial task since it involves comprehending mathematical text, which in turn requires understanding of distinctive structure, discourse, and dependencies within text. computational approaches have been proposed to solve this task. for example, ferreira (2021) used a graph neural network trained in a supervised learning approach to extract the most relevant premises @xcite . in this work we formulate the natural language premise selection task as an unsupervised semantic similarity task by retrieving premises that have a higher cosine similarity score with the given conjecture or proof of interest. a straightforward way to solve the task would have been to encode the premises and conjectures using word embeddings, and then perform cosine similarity to obtain the most relevant premises as those with the highest cosine score. however, this naive approach requires that both sentences are fed into the neural network, which causes a massive computational overhead. additionally, for better performance fine tuning or pretraining the models on downstream sentence pairs may be necessary @xcite , and that is computationally expensive. in this work, we propose to use smpnet (sentence masked and permuted language modeling), a computationally efficient and effective sentence transformer, which is a modification of the pre-trained mpnet @xcite ) that uses siamese and triplet network structure to derive semantically meaningful sentence embeddings that were used for this task. mpnet @xcite is a variant of transformer models @xcite that leverages the advantages of bert (bidirectional encoder representations from transformers) @xcite and xlnet @xcite (generalized autoregressive pretraining for language understanding) while avoiding their limitations. ## methodology consider a knowledge base k from which we retrieve a collection of n mathematical premises @xmath0, ..., p n } written in natural language. we would like to retrieve the premises p in k that are most likely to be useful in proving a mathematical statement or conjecture @xmath1, ...c m }. we formulate this task as a semantic similarity task by retrieving premises p in k that were semantically close to a given statement or conjecture c. ## conclusion in this work, we introduce an approach (spmnet) for natural language premise selection, which is a task that involves finding the relevant theorems, axioms and definitions in natural language mathematical texts. our proposed approach uses sentence embeddings based on the state-of-the-art transformer mpnet (masked and permuted language modeling) generating high quality embeddings that we used for retrieving the most important premises for a given mathematical conjecture. the results from our experiment show that the proposed approach (spmnet) outperforms the baseline method (tf-idf) by 0.028838 in mean average precision (map) which is a 23.5% improvement.