Natural Language Premise Selection: Finding Supporting Statements for Mathematical Text

Proceedings of the 12th Conference on Language Resources and Evaluation (LREC 2020), pages 2175–2182 Marseille, 11–16 May 2020 c⃝ European Language Resources Association (ELRA), licensed under CC-BY-NC 2175 Natural Language Premise Selection: Finding Supporting Statements for Mathematical Text Deborah Ferreira and Andre Freitas Department of Computer Science University of Manchester {deborah.ferreira, andre.freitas}@manchester.ac.uk Abstract Mathematical text is written using a combination of words and mathematical expressions. This combination, along with a specific way of structuring sentences makes it challenging for state-of-art NLP tools to understand and reason on top of mathematical discourse. In this work, we propose a new NLP task, the natural premise selection, which is used to retrieve supporting definitions and supporting propositions that are useful for generating an informal mathematical proof for a particular statement. We also make available a dataset, NL-PS, which can be used to evaluate different approaches for the natural premise selection task. Using different baselines, we demonstrate the underlying interpretation challenges associated with the task. Keywords: mathematical text, mathematical language processing, mathematical text analysis 1. Introduction Comprehending mathematical text requires evaluating the semantics of its mathematical structures (such as expres- sions) and connecting its internal components with the respective definitions or premises (Greiner-Petter et al., 2019). State-of-the-art models for natural language processing, such as BERT (Devlin et al., 2019), have high scores for several tasks, such as entity recognition, textual entailment and machine translation, but they do not encode the intri- cate mathematical background knowledge needed to reason over mathematical discourse. The language of mathematics is composed of a combina- tion of words and symbols, where symbols follow a dif- ferent set of rules and have a specific alphabet. Nonethe- less, word and symbols are interdependent in the context of mathematical discourse. This phenomenon is exclusive to mathematical language, not found in any other natural, or artificial, language (Ganesalingam, 2013), providing a unique and challenging application for semantic evaluation and natural language processing. Understanding mathematical discourse has been ex- plored before as a Mathematical Knowledge Extraction task (Aizawa et al., 2014); however, several aspects of the mathematical discourse related to deeper and more granu- lar reasoning over mathematical discourse has not yet been investigated. There is a lack of datasets in the literature needed for exploring and studying mathematical discourse and its associated interpretation and reasoning. We propose the task of natural premise selection, inspired by the field of automated theorem processing. Premise se- lection appeared initially as a task of selecting a (useful) part of an extensive formal library in order to limit the search space for an Automated Theorem Proving (ATP) sys- tem, increasing the chance of finding a proof for a given conjecture (Blanchette et al., 2016). Premises considered relevant are the ones that ATPs use for the automatic de- duction process of finding a proof for a conjecture. The premise selection task is defined as: Given a collection of premises P, an ATP system A with given resource limits, and a new conjecture c, predict those premises from P that …

Content truncated to 500 words