Premise Selection in Natural Language Mathematical Texts (2020)

Abstract: The discovery of supporting evidence for addressing complex mathematical problems is a semantically challenging task, which is still unexplored in the field of natural language processing for mathematical text. The natural language premise selection task consists in using conjectures written in both natural language and mathematical formulae to recommend premises that most likely will be useful to prove a particular statement. We propose an approach to solve this task as a link prediction problem, using Deep Convolutional Graph Neural Networks. This paper also analyses how different baselines perform in this task and shows that a graph structure can provide higher F1-score, especially when considering multi-hop premise selection.

## introduction mathematical proofs are used to establish the truth value of a mathematical claim. the act of creating a new proof contributes to the development of mathematics, being one of its central components. premise selection is a well-defined task in the field of automated theorem proving (atp), where proofs are encoded using a formal logical representation. given a set of premises p , and a new conjecture c, premise selection aims to predict those premises from p that will most likely lead to an automatically constructed proof of c, where p and c are both written using a formal language @xcite . the issue with using formal mathematics is that only a small portion of the known mathematical statements is available in a formalised dataset, and formal statements are usually hard for humans to interpret and write. in this paper, we focus on natural language mathematical text (mathematical statements as they are present in scientific papers and textbooks), since it is more accessible for mathematicians to write/read mathematical statements using natural language. the mathematical discourse is composed of a particular combination of words and mathematical terms, where terms follow a different set of syntactic rules and entail a specific lexicon. nonetheless, words and mathematical terms are interdependent in the context of mathematical discourse. this phenomenon is exclusive to mathematical language, not found in any other natural, or artificial, language @xcite , providing a unique and challenging application for semantic evaluation and natural language processing. the natural language premise selection @xcite task is defined as: definition (natural language premise selection): given a set of premises (or supporting facts) p in a mathematical corpus (containing both natural language and formulae) and a new conjecture c proposed by a user, predict those premises from p that will most likely be useful for generating a proof for c (i.e. partially entails c). a premise is considered relevant if the knowledge it provides can be reused for generating a proof for a given conjecture. we propose an approach to solve the natural premise selection task, representing all conjectures and premises as nodes and the dependencies as edges, formulating the problem as a link prediction problem. we hypothesise that graph-based embeddings are suitable structures for representing and detecting the dependencies between different mathematical statements. we then use deep convolutional graph neural networks @xcite over a structural and content-based encoding of proofs in order to obtain the set of useful premises for proving a statement. in order to evaluate this task, we use the dataset ps-proofwiki. this dataset opens possibilities of applications not only for the premise selection task but also for evaluating different equational embeddings, textual entailment for mathematics and natural language inference in the context of mathematical texts. the performance of the proposed model is compared to a set of baselines. the contributions of this paper can be summarised as follows: (i) proposal of a novel representation for the natural language premise selection problem. (ii) proposal of an approach for addressing the natural language premise selection task using link prediction under a deep convolutional graph neural network representation. (iii) quantitative and qualitative evaluation against existing baselines. ## related work latent and explicit representation models have seen a substantial advance in the past years, with the introduction of neural embeddings such as bert @xcite , which are able to capture discourse-level relations and semantic abstractions. however, the development of representation models and their evaluation in the context of mathematical discourse is still an open problem. in this section, we present some of the research in nlp applied to mathematics. we also describe existing works that apply premise selection in the domain of atps. ## the natural language premise selection task figure 1 depicts an example of a theorem and its proof, where it can be observed that the proof is based upon two other supporting facts (premises): the theorem for factors of composition series for prime power group and the definition for solvable group. in order to evaluate the premise selection, we used a corpus extracted from proofwiki foot_0 . proofwiki is an online compendium of mathematical proofs, with a goal to collect and classify mathematical proofs. proofwiki contains links between theorems, definitions and axioms in the context of a mathematical proof, determining which dependencies are present. definitions and axioms are statements accepted without formal proof, while theorems, lemmas and corollaries require one @xcite . all entries are composed by a statement written in a combination of natural language and mathematical latex notation. the extracted corpus, which is named ps-proofwiki, contains more than 18, 000 entries. we also computed how many times each statement is used as a premise, and we observed that most of the statements are used as dependencies for only a small subset of premises. a total of 6, 866 statements has between one and three dependants. on average, statements contain a total length of 289 symbols (characters and mathematical symbols). the specific number of tokens will depend on the type of tokenisation used for the mathematical symbols. a complete analysis of this corpus is made available in @xcite . in the next sections, we describe the proposed model for addressing the premise selection task. the proposed model uses a deep graph convolutional neural network (dgcnn) for solving the premise selection task as a link prediction task @xcite ). the proposed model aims to encode the natural language and the formu-4 encoding mathematical propositions and supporting facts ## evaluation this section evaluates the performance of the proposed model using ps-proofwiki. we introduce initial baselines using two basic approaches, tf-idf and pv-dbow. these are further expanded using a transformer-based architecture (bert), due to its state-of-art results for the encoding of sentence-level embeddings and their use in tasks such as natural language inference. for the experiments using bert and the proposed approach, we split the dataset using a 50/20/30 (train/dev/test) split. we run all experiments ten times, evaluating on the test set, and report the average precision, recall and f1-score. all evaluation data, as well as the experimental pipeline, can be found online foot_1 for reproducibility purposes. ## conclusion & future work in this work, we introduced an approach for natural language premise selection (finding relevant theorems, axioms and definitions) in large natural language mathematical texts. the proposed approach, which uses deep graph convolutional neural networks (dgcnns) combines both structural and content elements of mathematical statements for addressing the premise selection problem as a link prediction classification problem. results show that the approach outperforms a bert-based baseline by 41% in f1-score. moreover, the proposed model shows significantly lower f1-score degradation concerning class imbalance, a fundamental desirable scalability property for the problem of premise selection. our approach is also able to obtain better performance when we consider the transitivity of premises. the qualitative analysis indicates that there is the demand to design principled embeddings for better capturing the semantics of proofs which are denser in mathematical formulae. as future work, we will explore different heuristics for navigating in the premises graph, as researched before for textual entailment @xcite and selective reasoning @xcite .