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.

翻译：我们提出了一项任务，即匹配证明与给定的数学陈述。该任务很好地契合了当前关于数学信息检索及更广泛的数学文章分析的研究（《数学科学》，2014年）。我们为此任务构建了一个数据集（MATcH数据集），包含从现代数学研究论文中提取的超过18万个陈述-证明对。我们发现该数据集高度代表我们的任务，因其包含对数学家有用的较新研究成果。我们提出了一种双线性相似度模型和两种解码方法，以有效匹配陈述与证明。第一种解码方法在匹配证明与陈述时独立于其他陈述或证明，而第二种方法将该任务视为全局匹配问题。通过符号替换过程，我们分析了预训练语言模型在此类数学文章分析中的“洞察力”，并表明尽管这些模型在此任务上表现良好（最佳平均倒数排名为73.7），但它们是通过相对浅层的符号分析和匹配来实现这一性能的。