Premise Selection in Natural Language Mathematical Texts

Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pages 7365–7374 July 5 - 10, 2020. c⃝2020 Association for Computational Linguistics 7365 Premise Selection in Natural Language Mathematical Texts Deborah Ferreira and Andre Freitas Department of Computer Science University of Manchester {deborah.ferreira, andre.freitas}@manchester.ac.uk Abstract The discovery of supporting evidence for ad- dressing complex mathematical problems is a semantically challenging task, which is still unexplored in the field of natural language processing for mathematical text. The natu- ral language premise selection task consists in using conjectures written in both natural lan- guage and mathematical formulae to recom- mend premises that most likely will be use- ful to prove a particular statement. We pro- pose an approach to solve this task as a link prediction problem, using Deep Convolutional Graph Neural Networks. This paper also anal- yses how different baselines perform in this task and shows that a graph structure can pro- vide higher F1-score, especially when consid- ering multi-hop premise selection. 1 Introduction Mathematical proofs are used to establish the truth value of a mathematical claim. The act of creat- ing 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 represen- tation. Given a set of premises P, and a new con- jecture 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 (Irving et al., 2016). 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 math- ematical 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 par- ticular combination of words and mathematical terms, where terms follow a different set of syntac- tic rules and entail a specific lexicon. Nonetheless, words and mathematical terms are interdependent in the context of mathematical discourse. This phe- nomenon is exclusive to mathematical language, not found in any other natural, or artificial, lan- guage (Ganesalingam, 2013), providing a unique and challenging application for semantic evaluation and natural language processing. The natural language premise selection (Ferreira and Freitas, 2020) task is defined as: Definition (Natural language premise selec- tion): Given a set of premises (or supporting facts) P in a mathematical corpus (containing both natu- ral 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 knowl- edge it provides can be reused …

Content truncated to 500 words