我的嵌入是否反映了 $A = B$？评估嵌入模型中的数学等价性

因为数学是高度抽象的，所以一个陈述可以采取非常不同的形式，具体取决于它所在的子领域。有很多例子表明，研究人员发现某个问题已经在不同领域得到了答案后，就出现了突破。与此同时，与形式化相关的新资源的增长增加了对能够在数学“语言”（例如，从精益语言到自然语言）之间进行高效可靠导航的工具的需求。在本文中，我们研究了当前的嵌入模型是否捕获了数学等价性。为此，我们引入了数学等效但词汇不同的对 (MELD) 数据集，这是用非常不同的语言表达的数学等效语句的集合。我们表明，当前最先进的嵌入模型倾向于按用于表达它们的术语而不是底层数学对语句进行分组。受此启发，我们提出了一种学习数学文本嵌入的对比方法，该方法侧重于将非正式陈述与不同的形式化相结合。我们的实验表明，这不仅可以改进非正式-正式检索任务，还可以改进仅包含自然语言语句的 MELD。