IJS at T ext G raphs-16 Natural Language Premise Selection Task: Will Contextual Information Improve Natural Language Premise Selection? (2022)

Abstract: Natural Language Premise Selection (NLPS) is a mathematical Natural Language Processing (NLP) task that retrieves a set of applicable relevant premises to support the end-user finding the proof for a particular statement. In this research, we evaluate the impact of Transformer-based contextual information and different fundamental similarity scores toward NLPS. The results demonstrate that the contextual representation is better at capturing meaningful information despite not being pretrained in the mathematical background compared to the statistical approach (e.g., the TF-IDF) with a boost of around 3.00% MAP@500.

## introduction natural language premise selection (nlps) @xcite , inspired by the field of automated theorem proving, is a mathematical nlp task that retrieves a set of useful relevant premises. given a mathematical statement written in natural language as the input, nlps systems predict the relevant premises that could support an end-user finding a proof for that mathematical statement. mathematically, nlps task can be defined as: definition 1.1. given a new mathematical statement s, that requires a mathematical proof, and a collection (or a knowledge base) of premises @xmath0, p 2 ,. . . , p n p , with size n p, retrieve the premises in p that are most likely to be useful for proving s. the premises often include supporting definitions and propositions, which can act as explanations for the proof process. figure 1 presents examples of 2 premises that support a given mathematical statement or theorem. figure 1 : example premises supporting a given theorem @xcite . most of the existing systems focus on manual feature engineering or statistical approaches to extract meaningful mathematical knowledge, with one exception being the study by ferreira and freitas (2020b), where they tackle the task by employing deep convolutional graph neural networks (dcgnn) on graph representations. the state of the art models for nlp such as bert @xcite are not fully explored under the assumption that they do not encode the intricate mathematical background knowledge needed to reason over mathematical discourse. the 1 st shared task on natural language premise selection @xcite , organized as part of the textgraphs 2022 workshop, presented one of the first opportunities to systematically compare different approaches towards a nlps task in an information retrieval setting, by adopting ps-proofwiki (premise selection-proofwiki) dataset @xcite . this dataset can be considered as the baseline corpus for our specific shared task. the contributions of this paper can be summarised as follows: this paper is organised as follows: section 2 presents the related work in premise selection. next, we introduce our methodology, experimental setup and evaluation metrics in section 3. the corresponding results are presented in section 4. finally, we conclude our work and suggest future directions in section 5. ## related work in this section, we present the related research in nlp applied to the nlps task in the domain of automated theorem proving. the research was first introduced by @xcite , who employed corpus analysis and kernelbased methods, in order to showcase the usefulness of automatic premise selection systems for proving the conjectures in the field of automated theorem proving (atp). few years later, @xcite proposed a neural deepmath-deep sequence architecture for premise selection using formal statements from the mizar corpus, which solved 67.90% of the conjectures present in the mathematical mizar library. other machine learning based approaches have also been investigated for the task at hand (e.g. knn @xcite , random forest @xcite , to mention a few). similar to the previous research, @xcite formulate this problem as a pairwise relevance classification problem and present star, a cross-modal representation for mathematical statements with two layers of self-attention, one for each language modality present in the mathematical text. recently, ferreira and freitas (2020a) introduced a new systematic formulation of the task under the name natural language premise selection (nlps) and published a new evaluation corpus called nl-ps. they propose two baseline approaches, using tf-idf and pv-dbow @xcite . additionally, they also suggested to model the task as a pairwise relevance classification problem and tackled it by employing neural contextual representations, namely bert and scibert @xcite . while the previous work focused on capturing either content (local) or structural dependencies (global) across natural language mathematical statements, @xcite were the first to consider nlps as a link prediction problem using deep convolutional graph neural networks (dcgnn), with the aim of capturing both local and global information. their study demonstrates the capability of graph embeddings to capture structural and content elements of mathematical statements. ## results in this section, we evaluate the suitability of different contextual representations of premises from the knowledge base for retrieving the top relevant premises for a given statement in the test set. we also compare the obtained results with the results of the shared task baseline @xcite . ## conclusion in this paper, we have investigated the performance of contextual representations towards the task of natural language premise selection. we also evaluated the impact of different similarity scores. by using the contextual information obtained from the pretrained transformer-based models in order to obtain premise and statement representations, we manage to outperform the baseline statistical approach using tf-idf (the baseline) by a decent margin of around 3 percentage points in terms of map@500. these findings serve as a good initiative to explore the potential of using language models' for the nlps task further. we also showed that by using the manhattan distance for measuring similarity between representations, we can improve the performance by a small margin. there remains a lot of room for improvement. in the future, we would like to investigate the effect of different mathematical representations on the performance of the model, e.g., by feeding the model graph representations. combinations of contextual and graph representations will also be explored.