BERT Is Not The Count: Learning to Match Mathematical Statements with Proofs (2023)

Abstract: We introduce a task consisting in matching a proof to a given mathematical statement. The task fits well within current research on Mathematical Information Retrieval and, more generally, mathematical article analysis (Mathematical Sciences, 2014). We present a dataset for the task (the MATcH dataset) consisting of over 180k statement-proof pairs extracted from modern mathematical research articles. We find this dataset highly representative of our task, as it consists of relatively new findings useful to mathematicians. We propose a bilinear similarity model and two decoding methods to match statements to proofs effectively. While the first decoding method matches a proof to a statement without being aware of other statements or proofs, the second method treats the task as a global matching problem. Through a symbol replacement procedure, we analyze the “insights” that pre-trained language models have in such mathematical article analysis and show that while these models perform well on this task with the best performing mean reciprocal rank of 73.7, they follow a relatively shallow symbolic analysis and matching to achieve that performance.

## introduction research-level mathematical discourse is a challenging domain for natural language processing (nlp). mathematical articles frequently switch between natural language and mathematical formulae, and a semantic analysis of mathematical text needs to solve relationships (e.g. coreference) between mathematical symbols and concepts. moreover, mathematical writing follows many conventions, statement. when @xmath0, and when m ̸ = 0 we have e 0 however, mathematical research can benefit from nlp @xcite , in particular as concerns bibliographical research: researchers need tools to find work relevant to their research. indeed, prior nlp work on mathematical research articles focused on mathematical information retrieval (mir) and related tools or data @xcite @xcite . we introduce a task aimed at improving the processing of research-level mathematical articles and make a step towards the modeling of mathematical reasoning. given a collection of mathematical statements and a collection of mathematical proofs of the same size, the task consists in finding and assigning a proof to each mathematical statement. we construct and release a dataset for the task (match), by collecting over 180k statementproof pairs from mathematical research articles (an example is given in figure 1 ). related datasets, such as leanstep @xcite and the synthetic dataset of @xcite do not include natural language. naturalproofs @xcite , another related dataset, only consists of 32k theorem-proof pairs from proofwiki, 3 some sub-topics in algebraic geometry and two textbooks. our dataset is over five times larger and contains pairs extracted from advanced academic mathematical papers. there are multiple motivations for the design of the task and our dataset. we believe it may help mir by serving as a proxy for the search for the existence of a mathematical result, or for theorems and proofs related to one another (e.g. using the same proof technique), an important search tool for any digital mathematical library @xcite . learning to match statements and proofs would also benefit computer-assisted theorem proving, as it is akin to tasks such as premise selection, also recently addressed with nlp methods @xcite . we provide first results on our proposed task with an array of neural models, aimed at scoring the likelihood of relationship between a statement and its proof. an analysis through a symbol replacement procedure provides insight on what such neural models are capable of learning about mathematical equations and text. we provide two methods for decoding, one is local decoding, matching a proof to a theorem in a greedy way, and one that provides a global bipartite matching based on a structured max-margin objective. such an architecture may have applications to other nlp problems that can be cast as maximum bipartite matching problems (for a recent similar use in a different context, see @xcite . our analysis shows that pre-trained language models do not obtain significant "mathematical insight" for performing this matching, but rather rely on shallow matching. however, this does not prevent them from performing the matching relatively well in several carefully crafted scenarios, reaching an mrr of 73.7. ## related work most nlp work on mathematical discourse focuses on improving mathematical information retrieval @xcite by establishing connections between mathematical formulae and natural language text in order to improve the representation of formulae. the interpretation of variables is highly dependent on the context. for example, the symbol e could denote an expectation in a statistics article, or the energy in a physics article. some studies use the surrounding context of a formula to assign a definition or a type to the whole formula, or to specific variables. nghiem @xcite focus on identifying coreferences between mathematical formulae and mathematical concepts in wikipedia articles. @xcite extract definitions of mathematical expressions. @xcite , @xcite and @xcite disambiguate mathematical identifiers, such as variables, using the surrounding textual context. @xcite infer the type of a variable in a formula from the textual context of the formula. another line of work focused on identifying specialized terms or concepts to improve mir @xcite . some work adapts standard nlp tools to the specificity of mathematical discourse, e.g. pos taggers @xcite , with the objective of using linguistic features to improve the search for definitions of mathematical expressions @xcite . more recent work focuses on typing variables in mathematical articles @xcite , modeling formulae @xcite , and selecting premises @xcite . an earlier version of our work covers some of the material in this paper @xcite . the main differences between that version and the current version are the introduction of the symbol replacement evaluation ( §5) and the use of pre-trained language models rather than recurrent neural networks. ## task description given a collection of mathematical statements {s (i) } @xmath1, and a separate equal-size collection of mathematical proofs {p (i) } @xmath2, we are interested in the problem of assigning a proof to each statement. evaluation we use two evaluation metrics. assuming that a system predicts a ranking of proofs, instead of providing only a single proof, we evaluate its output with the mean reciprocal rank (mrr) measure: mrr( by construction (see §4), it is possible though unlikely that the same mathematical statement occurs several times in the dataset. it is more unlikely that ## dataset construction this section describes the construction of the match dataset of statement-proof pairs (see figure 1 for an example). source corpus we use the mrec corpus foot_1 @xcite as a source. the mrec corpus contains around 450k articles from arxmliv @xcite , an on-going project aiming at converting the arxiv foot_2 repository from l a t e x to xml, a format more suited to machine processing. in this collection, mathematical formulae are represented in the mathml foot_3 format, a markup language. statistics we extract statement-proof pairs as described in appendix a. our processing of mrec includes the identification of statement-proof pairs through meta tags and the linearization of the representation of mathematical equations. we report in statements min max @xmath3.5% 58%±20 proofs text+math 20 500 210± 127 text only 1 467 81 ± 56 math only 0 495 129 ± 96 math proportion 0% 99.6% 56%± 21 ## symbol replacements with our current dataset setup, we implicitly make the assumption that both the theorem and the proof are authored by the same authors. this assumption is incongruent with the mir-flavor of our task. first, it is not useful for researchers to match proofs they authored. second, each person has a unique writing style expressed by unique mathematical jargon and notations. to relieve of this assumption, we introduce several symbol replacement levels for changing the names of the proof variables. then, we train and test our models using these altered datasets. these replacement levels also provide insight on the ability of our models to semantically analyze the input statement-proof pairs. ## bilinear similarity model we propose a model based on an encoder ( §8) that constructs fixed-size vector representations for statements and proofs, and a similarity function that scores the relatedness of a statement-proof pair. ## local and global training we propose two training methods for the similarity model above: a local training method that only considers statements in isolation ( §7.1) and a global model trained to predict a bipartite matching ( §7.2), with a hybrid global-local objective. ## experimental setup dataset we use the dataset whose construction is described in §4. we shuffle the collection of statement-proof pairs before performing a 80%/10%/10% train-development-test split, corresponding to 147278 pairs for the training sets and 18408 pairs for the development and tests. we experiment with a default, mixed, split and a harder unmixed split (see §9.3). ## results first, we assess the task difficulty under different replacement levels using different encoders and schemes (global or local training, global or local decoding). in particular, we are interested in assessing whether global decoding improves accuracy when training is only local, and how the more complex global training method fares with respect to local training. we then measure the informativeness of different types of input: text, mathematical formulae, or both. the comparison of these settings is meant to provide insight into which type of information is crucial to the task. finally, we experiment with a cross replacement levels setup, i.e., when a model is tested on a different symbol replacement level from the one that was used during training. we hope this experiment will shed some light on the importance of training models on real-world datasets. ## conclusion we developed a bilinear similarity model and a large dataset (match) for a task focusing on the domain of mathematical research articles. the task consists in matching a proof to a mathematical statement. we proposed two ways to train and inference with our model and dataset: local matching and global matching. we assessed the difficulty of the task with several pre-trained encoders, demonstrating the importance of the vocabulary support for these models. further assessment relies on using a symbol replacement procedure, which helps test the type of mathematical reasoning the encoders can perform. while our model performs well on this task, we observe through the symbol replacement procedure that the model makes a relatively shallow use of the text and formulae to obtain this performance.