Introduction to Mathematical Language Processing: Informal Proofs, Word Problems, and Supporting Tasks (2023)

Abstract: Automating discovery in mathematics and science will require sophisticated methods of information extraction and abstract reasoning, including models that can convincingly process relationships between mathematical elements and natural language, to produce problem solutions of real-world value. We analyze mathematical language processing methods across five strategic sub-areas (identifier-definition extraction, formula retrieval, natural language premise selection, math word problem solving, and informal theorem proving) from recent years, highlighting prevailing methodologies, existing limitations, overarching trends, and promising avenues for future research.

## introduction prove that there is no function f from the set of non-negative integers into itself such that f (f (n)) = n + 1987 for every n. ## methods we highlight key points abstracted from task approaches in bold, give an overview of methods in ## datasets various datasets have been proposed for tasks related to identifier-definition extraction and var-iable typing @xcite @xcite , with limited adoption. the symlink shared task @xcite is an emerging solution, with training data, annotations of 102 papers, and high inter-annotator agreement. formula retrieval data exists through ntcir-12 @xcite , which has been expanded in the most recent arqmath task @xcite , removing formula duplicates and balancing query complexity. premise selection datasets include ps-proofwiki @xcite , used in the nlps shared task @xcite , and naturalproofs @xcite . the latter is more inclusive, comprising proofwiki, text books, and other sources. modern consensus mwp datasets include (easy) mawps @xcite , (medium) math23k @xcite , and (hard) mathqa @xcite , comprising both chinese and english problems. gsm8k @xcite claims to resolve diversity, quality, and language @xcite issues from previous datasets, involves step-wise reasoning and natural language solutions, with balanced difficulty. math @xcite is larger and more difficult than gsm8k. informal theorem proving data includes naturalproofs @xcite , and some mwp datasets involving step-wise reasoning with mathematical language, such as math and gsm8k. however, there is no consensus data for autoformalization or theorem proving from mathematical language input involving sequence learning. proofnet @xcite aims to remedy this, by providing 297 theorem statements expressed in both natural and formal @xcite language, at undergraduate difficulty. some are accompanied by informal proofs. minif2f @xcite is a neural theorem proving benchmark of olympiad-level problems written in many formal languages. lila @xcite provides data for 23 math reasoning tasks. key datasets information is described in data scarcity. some datasets, such as math and the auxiliary mathematics problems and solutions (amps) @xcite of actual mathematicians would be invaluable. @xcite attempt to tackle this problem for a single research paper in a very limited setting.