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

Proceedings of the 17th Conference of the European Chapter of the Association for Computational Linguistics, pages 3581–3593 May 2-6, 2023 ©2023 Association for Computational Linguistics BERT is not The Count: Learning to Match Mathematical Statements with Proofs Weixian Waylon Li1 Yftah Ziser1 Maximin Coavoux2∗ Shay B. Cohen1 1 University of Edinburgh, School of Informatics, Edinburgh 2 Univ. Grenoble Alpes, CNRS, Grenoble INP, LIG, W.Li-67@sms.ed.ac.uk yftah.ziser@ed.ac.uk Abstract We introduce a task consisting in matching a proof to a given mathematical statement. The task fits well within current research on Math- ematical Information Retrieval and, more gen- erally, mathematical article analysis (Mathe- matical 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.1 We find this dataset highly representative of our task, as it consists of relatively new find- ings useful to mathematicians. We propose a bilinear similarity model and two decoding methods to match statements to proofs effec- tively. 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 anal- ysis and show that while these models per- form well on this task with the best performing mean reciprocal rank of 73.7, they follow a rela- tively shallow symbolic analysis and matching to achieve that performance.2 1 Introduction Research-level mathematical discourse is a chal- lenging domain for Natural Language Processing (NLP). Mathematical articles frequently switch be- tween 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, ∗Work mostly done at the University of Edinburgh. 1Our dataset and code are available at https:// github.com/waylonli/MATcH. 2Like Bert, The Count (or Count von Count; ) is a character from the television show Sesame Street. The Count likes counting, and his main role in the show is to teach this skill to children. Statement. When m = 0 we have E0 rg = ∅, and when m ̸= 0 we have E0 rg = E0. Proof. Hence E0When m = 0, the image of r is {1}. rg = ∅. When m ̸= 0, the map r is a surjective proper map. Hence E0 rg = E0. Figure 1: Example of a statement-proof pair. such as variable naming or typography that are implicit, and may differ between subfields. However, mathematical research can benefit from NLP (Mathematical Sciences, 2014), in par- ticular as concerns bibliographical research: re- searchers need tools to find work relevant to their research. Indeed, prior NLP work on mathemati- cal research articles focused on Mathematical In- formation Retrieval (MIR) and related tools or data (Zanibbi et al., 2016; Stathopoulos and Teufel, 2016, 2015). We introduce a task aimed at improving the pro- cessing of research-level mathematical articles and make a …

Content truncated to 500 words