T ext G raphs 2022 Shared Task on Natural Language Premise Selection (2022)

Abstract: The Shared Task on Natural Language Premise Selection (NLPS) asks participants to retrieve the set of premises that are most likely to be useful for proving a given mathematical statement from a supporting knowledge base. While previous editions of the TextGraphs shared tasks series targeted multi-hop inference for explanation regeneration in the context of science questions (Thayaparan et al., 2021; Jansen and Ustalov, 2020, 2019), NLPS aims to assess the ability of state-of-the-art approaches to operate on a mixture of natural and mathematical language and model complex multi-hop reasoning dependencies between statements. To this end, this edition of the shared task makes use of a large set of approximately 21k mathematical statements extracted from the PS-ProofWiki dataset (Ferreira and Freitas, 2020a). In this summary paper, we present the results of the 1st edition of the NLPS task, providing a description of the evaluation data, and the participating systems. Additionally, we perform a detailed analysis of the results, evaluating various aspects involved in mathematical language processing and multi-hop inference. The best-performing system achieved a MAP of 15.39, improving the performance of a TF-IDF baseline by approximately 3.0 MAP.

## introduction the articulation of mathematical language represents a core feature of human intelligence, requiring complex reasoning capabilities and abstraction as well as a correct evaluation of the semantics of mathematical structures and its internal components @xcite . moreover, mathematical language consists in a combination of words and symbols, which act following different rules and alphabets, but preserving, at the same time, mutual dependencies that are necessary figure 1 : given a mathematical statement s, that requires a mathematical proof, and a collection of premises p , the task of natural language premise selection (nlps) consists in retrieving the premises in p that are most likely to be useful for proving s @xcite . these features provide a unique set of opportunities for the evaluation of state-of-the-art models in natural language processing (nlp) @xcite . to encourage new lines of research at the intersection of natural language and mathematics, we propose the 1st shared task on natural language premise selection (nlps). the nlps task asks participants to retrieve the premises that are most likely to be useful for proving a given mathematical statement from a supporting knowledge base (see figure 1 ). specifically, nlps is designed to assess the capabilities and behaviours of state-of-the-art approaches in dealing with a mixture of natural language and mathematical text along with the modelling of complex multihop dependencies between statements. to this end, this edition of the shared task makes use of a large set of approximately 21k mathematical statements extracted from the ps-proofwiki dataset @xcite . in this summary paper, we present the results of the 1st edition of the natural language premise selection task, providing a detailed description of the evaluation data, and the participating systems. moreover, we perform a detailed analysis of the behaviour of the participating systems, evaluating various aspects involved in mathematical language processing (i.e., the ability to deal with an increasing number of mathematical elements) and multi-hop inference. the best performing system achieved a map of 15.39, improving the performance of a tf-idf baseline by approximately 3.0 map, while still leaving a large space for future improvements. ## natural language premise selection given a mathematical statement s that requires a mathematical proof, and a collection (or a knowledge base) of premises @xmath0, p 2 , . . . , p np }, with size n p , the task of natural language premise selection (nlps) consists in retrieving the premises in p that are most likely to be useful for proving s. a mathematical statement can be a definition, an axiom, a theorem, a lemma, a corollary or a conjecture. premises are composed of universal truths and accepted truths. definitions and axioms are universal truths since the mathematical community accepts them without proof. accepted truths include statements that need a proof before being adopted. theorems, lemmas and corollaries are such types of statements. these statements were, at some point, framed as a conjecture before they were proven. as such, they can be grounded on past mathematical discoveries, referencing their own supporting premises (i.e., the background knowledge that was used to prove the conjecture). this network structure of available premises can be used as a foundation in order to predict new ones. the relationship between these statements can be leveraged to build models that can better perform inference for mathematical text @xcite . the nlps task can be particularly challenging for existing information retrieval systems since it requires the ability to process both natural language and mathematical text @xcite . moreover, as shown in the example in figure 2 , the retrieval of certain premises necessitates complex multi-hop inference @xcite . statement type data split kb train dev test all (unique) definitions 7,077 0 0 0 7,077 lemmas 252 134 70 69 252 corollaries 161 113 57 57 275 theorems 8,715 5,272 2,652 2,636 14,003 total 16,205 5,519 2,778 2,763 21,746 however, definitions are often used as premises playing a fundamental role in the nlps task. there also exists an intersection between the kb and the training set. accordingly, we include the last column to account for all unique entries in the dataset. figure 3 presents a histogram with the frequency of the different number of premises. we can observe that the statements usually have a small number of premises, with 9, 640 (around 87% of the entries in the train/dev/test set) statements containing between one and five premises. the highest number of premises for one theorem is 72. similarly, the histogram in figure 4 shows the frequency of the dependencies between statements, reporting how many times each statement is used as a premise. a total of 4,236 statements is connected to between one and three dependants. on average, the statements contain a total of 289 symbols (characters and mathematical symbols). the dataset provides a specific semantic modelling challenge for natural language processing as it requires specific tokenisation and the modelling of specific discourse structures tailored towards mathematical text, such as encoding mathematical elements along with natural language, and encoding the relationship between conjectures and premises. ## system descriptions and performance following the previous editions of the textgraphs shared tasks on multi-hop inference for explanation regeneration @xcite ; jansen and ustalov, 2020, 2019), we frame natural language premise selection (nlps) as a ranking problem. to this end, the participating systems have been evaluated using mean average precision (map) at k, with @xmath1. specifically, the top 500 premises retrieved for supporting a given mathematical statement are compared against the gold premises in the corpus via map. the competition has been organised on co-dalab @xcite ), foot_1 with a total of four teams submitting their solutions to the leaderboard @xcite @xcite . here, we summarize the key features of the models proposed by the participating teams: team name map ijs (tran et al., 2022) 15.39 unlps @xcite 15.16 kamivao @xcite 14.60 langml @xcite 14.14 tf-idf baseline 12.28 ijs @xcite . the team investigates the task of nlps evaluating the impact of transformerbased contextual representations along with several similarity metrics for retrieval. specifically, the authors propose a systematic evaluation of different pre-trained sentence-transformers (reimers and gurevych, 2019) using a bi-encoder architecture. in order to rank the premises, the authors extract the contextual representation from different transformers, computing the similarity scores to rank how likely the sentences in the supporting knowledge base are to be a part of the set of premises for a given mathematical statement. the authors observe that the best performance are obtained via roberta large @xcite and manhattan distance achieving a map score of 15.39. unlps @xcite . similar to iijs, the team explore the usage of sentence-transformers @xcite , employing a bi-encoder architecture for addressing the nlps task. the team does not rely on fine-tuning techniques but, instead, adopts pre-trained transformers to retrieve the most relevant premises via a cosine similarity score. the team demonstrated that employing the sentence-transformer smpnet model, which internally adopts a pre-trained mp-net @xcite , yields a map score of 15.16. kamivao @xcite . the team proposes an approach based on a mixture of dense retrieval and prompt-based methodology. specifically, the proposed model combines a bi-encoder based on a pre-trained sentence-transformer (reimers and gurevych, 2019) (bert @xcite and mathbert @xcite ) with a gpt3 model @xcite which is instructed to re-rank a set of candidate premises. in the first stage, the model uses bi-encoders and cosine similarity to retrieve a list of potentially relevant premises, while in the re-ranking stage, the authors adopt a prompt-based methodology to construct specific instructions for gpt-3. this approach achieves a map score of 14.60. iangml @xcite . the team proposes a method that relies on keywords extraction and matching to select relevant premises. the proposed approach employs a keyword extractor @xcite to generate up to 20 keywords for each sentence. the team proposes and evaluates a range of similarity functions based on the extracted keyworkds through the generation of sparse embeddings. the embeddings are generated using the fasttext model @xcite . the scoring functions are then applied to re-rank the top 500 premises retrieved by the tf-idf baseline. their experiments show that the jacardian similarity scoring function yields the best map performance of 14.14. ## detailed analysis in order to better evaluate and characterise the behaviour of the proposed systems beyond the aggregated map score, we carried out an additional analysis by partitioning the set of mathematical statements according to different categories. specifically, we categorise the statements in the test-set according to the total number of occurring mathematical elements (e.g., equations, variables, etc.) and the total number of gold premises. in particular, these categories allow for the evaluation of the behaviour of the systems when (a) dealing with a mixture of natural language and mathematical text and (b) retrieving premises that require multihop inference. the larger the number of premises supporting a given mathematical statement, in fact, the higher the number of inference steps that are likely to be required in the nlps task. the results of this analysis are reported in ## conclusion our shared task on natural language premise selection (nlps) attracted a total of four participating teams, allowing for the evaluation of a diverse set of solutions ranging from transformers to lexical-based approaches. the participating systems have all contributed to improving the performance of a tf-idf baseline. the best-performing team, ijs, presented an approach based on pretrained sentence-transformers, which has been shown to achieve a map score of 15.39. given the challenges involved in the task, supported by the relatively low performance of state-of-the-art approaches, we hope this work will encourage future research in the field, exploring nlps as a benchmark for testing complex inference capabilities and exploring the limit of ai and nlp models.