Keyword-based Natural Language Premise Selection for an Automatic Mathematical Statement Proving (2022)

Abstract: Extraction of supportive premises for a mathematical problem can contribute to profound success in improving automatic reasoning systems. One bottleneck in automated theorem proving is the lack of a proper semantic information retrieval system for mathematical texts. In this paper, we show the effect of keyword extraction in the natural language premise selection (NLPS) shared task proposed in TextGraph-16 that seeks to select the most relevant sentences supporting a given mathematical statement.

## introduction a mathematical statement requires a collection of appropriate definitions, previously proved statements, and inference rules to be proved. the automatic reasoning field deals with computing systems automating proof procedures and proof checking. one of the considerations in implementing automatic deduction and artificial intelligence approaches is restricting the proof search space and preventing the automatic prover from pursuing unfruitful reasoning paths. a dual aspect of search is looking for previous results that could be useful in proof completion @xcite . premise selection was initially introduced in @xcite as a task to select a part of a formal library that improves the chance that an automatic prover can prove a mathematical conjecture. in @xcite , neural network-based premise selectors were applied for the first time, and @xcite reformulated the problem as a pairwise relevance classification problem. similar challenges in mathematical context have been proposed, such as arqmath @xcite seeking an answers retriever and ranker for a given mathematical question. an answer retriever system mainly needs to consider mathematical text similarities. however, the premise selector task also requires a mathematical concept understanding component. in this study, we work on the shared-task introduced by the 16 th workshop on graph-based natural language processing @xcite on natural language premise selection. in this task, the teams are given a collection of mathematical statements in natural language and the goal is to retrieve supportive premises from a knowledge-base that can prove certain statements. in this study we look into the effectiveness of keyword extraction in selecting premises for proving each statement outperforms the tf-idf-based baseline. ## results the results achieved using methods described in the previous section compared to the baseline score are presented in ## conclusions in this paper, we checked the effectiveness of keyword extraction of mathematical statements for premise selection shared task nlps and considered three keyword scoring schemas. given statements, we scored the keywords extracted for each statement and selected supportive sentences. results show that keywords of statements can be effectively used in selecting relevant premises.