STAR : Cross-modal [ STA ]tement [ R ]epresentation for selecting relevant mathematical premises (2021)

Abstract: Mathematical statements written in natural language are usually composed of two different modalities: mathematical elements and natural language. These two modalities have several distinct linguistic and semantic properties. State-of-the-art representation techniques have demonstrated an inability in capturing such an entangled style of discourse. In this work, we propose STAR, a model that uses cross-modal attention to learn how to represent mathematical text for the task of Natural Language Premise Selection. This task uses conjectures written in both natural and mathematical language to recommend premises that most likely will be relevant to prove a particular statement. We found that STAR not only outperforms baselines that do not distinguish between natural language and mathematical elements, but it also achieves better performance than state-of-the-art models.

## introduction natural language understanding has been applied to several different tasks and areas, from question answering to visual grounding. even though mathematics is a well-established field with immense importance for most areas of science, applications of nlp in this field are still limited. natural language premise selection (nlps) (ferreira and freitas, 2020a) is a task that requires the combination of natural language reasoning and mathematical reasoning. given a certain conjecture (a mathematical statement written in natural language) that needs to be proven, we attempt to recommend useful premises that can be relevant for developing that mathematical argument. mathematical statements have a particular discourse structure that makes it challenging to use traditional nlp techniques. some of its distinctive features are: (1) entangled dual lexical spaces for the mathematical elements (me) and natural language (nl); (2) distinct syntactic phenomena between me and nl. given this entangled nature of the discourse, where two very different linguistic modalities coexist in the same text, traditional information retrieval approaches are not able to capture the different semantics for each modality @xcite . for example, in the mathematical domain, variables are represented using generic symbols; this lexical layer does not necessarily ground the semantics of the variables. the context surrounding the variables is more important than the symbol itself. when interpreting mathematical discourse, such particulars need to be taken into account. in this work, we propose star, a cross-modal representation for mathematical statements for addressing the task of premise selection. in order to interpret the different modalities in the mathematical discourse (natural language and equational), star uses two different self-attention layers, one focused on the mathematical elements, such as expressions and variables, while the other attends to natural language features. star is taught to see these tokens as parts of different languages, the mathematical language and the english language, similar to what our human brain does @xcite . even though the brain interprets mathematics as a language, it requires different parts for processing it @xcite . using different attention layers, star can learn that understanding mathematics requires a different type of reasoning than natural language, approximating the behaviour of the brain when faced with mathematical tokens. the approach presented in this work is based on the hypothesis that the use of cross-modal attentionbased mechanisms provides a better encoding of the semantic content of mathematical statements for the task of premise selection. the contributions of this work can be summarised as follows: ## background: natural language premise selection in this work, we address the problem of natural language premise selection @xcite (premise selection or nlps). 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 requiring proof. on the other hand, accepted truths include statements that need 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. this network structure of known premises can be used as a foundation in order to predict new ones. given a new conjecture c, that requires a mathematical proof, and a collection of premises @xmath0, p 2 , . . . , p np }, with size n p , the nlps task aims to retrieve the premises that are most likely to be useful for proving c. premises of accepted truth statements can also have a subset of premises p ⊆ p . figure 1 presents an example of a conjecture containing two premises. both premise 1 and premise 2 can be used as part of the proof for this conjecture. figure 1 : example of a conjecture and its premises. similar to previous approaches @xcite , we formulate this problem as a pairwise relevance classification problem. given a pair (c, p i ), we classify if p i can be used for proving c. our approach is built on top of a cross-modal representation for mathematical statements, as the following section presents. ## our approach: cross-modal statement representation (star) mathematical language follows a regular pattern (in contrast to natural language) @xcite , regardless of representing a conjecture, universal truth or accepted truth. in this work, we consider mathematics written in natural language, instead of mathematics expressed in logical formal languages. the target corpus is composed of a combination of mathematical symbols and natural language words. given the set of mathematical statements m and a statement @xmath1, m is defined as a sequence of elements @xmath2, s 2 , . . . , s n }, where s @xmath3, the set of words, or s @xmath4, the set of mathematical elements present in m. these components are situated in different lexical spaces; therefore, a function to generate a representation for m should take this into account. we define an embedding model γ : @xmath5, where d is the dimension of the output vector. the complete architecture is presented in figure 2a , where part of a statement is shown as an input example. each layer is described in detail below. ## experiments this section presents the experiments performed to test our hypotheses. we use the dataset ps-proofwiki @xcite for these experiments. this dataset is composed of pairs of conjectures and premises, framing the problem as a pair classification task. each statement is written using a combination of words and l a t e xnotation. for each positive pair, where the statement is a premise to the conjecture, there can be n number of negative pairs. for testing the robustness to noise in the proposed model, we use @xmath6, 2, 5, 10}. the number of entries for train, validation and test for each value of n is shown in the negative pairs are obtained using two different methods. the first collects random examples of statements that are not premises to form a new pair (negative examples). in the second technique, we use bm-25 to retrieve statements that are lexically similar to the premises, but that are not part of positive pairs (similar examples). for these experiments, we used 512 as a the size of the hidden units layer in the lstm, embedding size and output statement vector in the embedding architecture. we used 50 epochs for each training round. as shown in figure 3 , with this number of epochs we achieve convergence for all values of n. for each epoch, the validation set was evaluated, and the best model was chosen for testing. all experiments and data can be found in our github repository foot_0 . ## related work several areas of research apply natural language processing for domain-specific tasks, mathematics being one of these areas. one crucial task in this field is solving mathematical word problems, where the goal is to provide the answer to a mathe some contributions focus on the representation of mathematical text and mathematical elements. @xcite proposes a representation for mathematical proofs using discourse representation theory. similarly, @xcite introduces a grammar for representing informal mathematical text, while @xcite presents this style of text using argumentation theory. such explicit representations are relevant for representing the reasoning process behind mathematical thinking. however, it is still not possible to accurately extract these representations at scale. representations of mathematical elements are often used in the context of mathematical information retrieval, used, for example, for obtaining a particular equation or expression, given a specific query. tangent-cft @xcite ) is an embedding model that uses the subparts an expres-sion or equation, to represent its meaning. this type of representation @xcite often removes the expression for its original discourse, losing the textual context that can help to find a semantic representation. in this work, we focus on creating a representation that can integrate both of these aspects, natural language and mathematical elements. similar to our work, @xcite uses self-attention for mathematical elements in order to generate headlines for mathematical questions. other relevant tasks for nlp applied to mathematics include typing variables according to its surrounding text @xcite , obtaining the units of mathematical elements @xcite and generating equations on a given topic @xcite . 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 conjecture premise predicted label let @xmath8, τ ) be a topological space. let a, b be subsets of s. then: ∂(a ∩ b) ⊆ ∂a ∪ ∂b where ∂a denotes the boundary of a. let s, t 1 , t 2 be sets such that t 1 , t 2 are both subsets of s. then, using the notation of the relative complement: let @xmath9, τ a,b ) be a modified fort space. then t is not a t 3 space, t 4 space or t 5 space. 1 0 in this work, we propose a new representation that distinctively captures both language modalities present in the mathematical discourse in order to solve the premise selection task. ## conclusion in this work, we introduced star, a model to represent mathematical statements for the task natural language premise selection. in this model, we used two layers of self-attention, one for each language modality present in the mathematical text. in order to test star's ability to capture the different aspects of each modality, verifying if it can interpret that expressions and words belong to different lexical spaces, we compared our performance with other baselines. we found that having one layer for each modality significantly increases the performance for premise selection. we also compared our approach with state-of-the-art models and found that star achieves the highest results for the test set. star was also tested for transfer learning, revealing that cross-modal attention improves the transportability between different mathematical areas. however, we discovered that star is still limited regarding variable modelling. there is still a gap in how to handle variable typing in latent models, considering its meaning instead of its lexi-