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

# 我的嵌入是否反映 A=B？评估嵌入模型中的数学等价性
来源：https://arxiv.org/html/2606.23959
\\theorembodyfont\\theoremheaderfont\\theorempostheader

:\\theoremsep \\jmlrvolume334\\jmlryear2026\\jmlrworkshop数据科学中的拓扑、代数与几何

\\NameJiaying Ye\\nametag\\Emailyjy0509@uw\.edu \\NameSamarth Rao\\nametag∗ \\NameLeo Carlin\\nametag∗ \\NameKedar Chintalapati \\NameSaharsh Bhargava \\NameRachit Jaiswal \\NameMichael Zhou \\NameJared Darlington \\NameJarod Alper \\addr华盛顿大学\\NameVasily Ilin \\addrAxiom Math华盛顿大学\\NameHenry Kvinge\\Emailhjk3@uw\.edu \\addr华盛顿大学太平洋西北国家实验室

###### 摘要

由于数学具有高度抽象性，同一个陈述根据其所在的不同子领域，可能呈现出截然不同的形式。许多突破性进展都发生在研究人员发现某个问题已在另一个领域得到解答之后。与此同时，与形式化相关的新资源的增长，增加了对能够在不同数学“语言”（例如，从Lean到自然语言）之间进行高效可靠导航的工具的需求。在本文中，我们研究当前的嵌入模型是否能够捕捉数学等价性。为此，我们引入了**数学等价但词汇不同对（MELD）数据集**，该数据集由一组使用截然不同语言表达的数学等价陈述组成。我们表明，当前最先进的嵌入模型倾向于根据陈述所用的术语来分组，而非根据其底层数学内容。受此启发，我们提出了一种用于学习数学文本嵌入的对比方法，该方法侧重于将非正式陈述与不同的形式化版本对齐。我们的实验表明，这种方法不仅在非正式-形式化检索任务上带来了改进，而且在仅包含自然语言陈述的MELD上也带来了改进。

###### 关键词:

人工智能数学，文本嵌入，Lean

## 1 引言

语言模型在研究级数学方面已变得越来越有能力，有多个记录案例表明，像GPT（tao2024primetime;gowers2026chatgpt;openai2026unitdistance）、Gemini（feng2026semi）和Claude（knuth2024news）这样的LLM帮助数学家们在解决开放问题上取得了进展。这些系统的一个优势是，它们能够以人类无法企及的规模，利用庞大的数学文献（通过参数知识和互联网搜索）。这包括建立超越表层词汇重叠的非平凡联系。

同时，有效导航大量数学文本的能力正变得至关重要，这不仅是因为arXiv等在线数据库中数学论文数量不断增长，还因为像mathlib（mathlib2020）这样由形式化驱动的新资源。尽管最先进的LLM可能已经具备执行此类导航的能力，但它们在计算上过于昂贵，无法扩展到许多应用。另一方面，文本嵌入模型被明确设计用于高效捕捉文本语料库中的语义关系。在本文中，我们探究当前最先进的嵌入模型是否能够捕捉数学等价性。

为了测试这一点，我们引入了一个新数据集：**数学等价、词汇不同对（MELD）**，该数据集包含270对使用不同术语表达的数学等价陈述。一个简单的例子是从集合论和范畴论角度对两个集合乘积的定义。然后，我们表明最先进的嵌入模型往往不会将这些对嵌入到彼此附近，而是根据陈述所在的数学子领域进行分组。

如果一个嵌入模型能够基于数学等价性而非词汇相似性对陈述进行分组，那将是一个强大的数学发现工具。受此启发，我们提出了一种用于训练数学嵌入模型的对比方法，该方法将陈述的形式化和非正式版本视为同一底层数学内容的不同“视图”。为了实现这一点，我们生成了`mathlib_informal_v4.16.0`数据集（frenzymath2025mathlibinformal）的增强版本，该数据集包含来自mathlib库的Lean陈述及其非正式描述。我们还添加了非正式描述的重述。我们在此设置下训练的两个模型，`MathLeap-Qwen-8B`和`MathLeap-Octen-8B`，在一系列数学检索任务上取得了强劲结果111代码可在https://github.com/uw-math-ai/math2vec找到。。支持我们的假设，即我们的训练方法鼓励模型学习反映陈述数学内容的表示，我们表明这两个模型在我们评估的所有模型中，在MELD上取得了最高分数。这一点尤其值得注意，因为MELD仅包含自然语言内容。

总之，我们的贡献包括：

1. 1.我们引入了**数学等价但词汇不同对（MELD）**，一个包含270对数学陈述的数据集，这些陈述在词汇上不相似但在数学上等价。
2. 2.观察到大多数嵌入模型优先考虑语言相似性而非数学等价性，我们提出了一种开发数学嵌入模型的对比方法，使用陈述的非正式和形式化表示作为底层数学内容的不同视图。
3. 3.我们表明，这导致了在MELD以及其他一系列数学检索任务上的显著改进。

## 2 相关工作

有效利用数学文献的能力的价值意味着检索和搜索是人工智能数学社区中的一个活跃研究领域。例如，（welleck2021naturalproofs）引入了一个数学定理数据集，将定理搜索视为引用检索任务。这表明当检索仅依赖于捕捉数学陈述之间的表层相似性时，文本嵌入模型可能是有效的，但当需要更深层次的数学联系时，效果可能较差。最近，（alexander2026semantic）使用Qwen3-Embedding-8B的嵌入对900万个定理进行了检索。另一方面，我们的工作旨在提高文本嵌入模型本身的能力，特别专注于捕捉数学等价性。

更近期，（ju2025mirb）提出了一个完整的数学检索文本嵌入基准：数学信息检索基准（MIRB）。该基准包括从较不严谨的语言（例如，搜索MathStackExchange重复项）到更正式的语言（例如，Lean前提检索）的混合任务。我们的工作与MIRB不同，因为MELD旨在针对特定的嵌入模型能力，而非一般的数学检索。

## 3 嵌入模型是否捕捉数学等价性？

参见图注图1：来自MELD的“向量空间与模论”子集的嵌入陈述的UMAP可视化。蓝色点对应使用向量空间术语表达的陈述，棕色点对应使用模论术语表达的陈述。小三角形是干扰陈述。MELD对是大的点，由线连接。嵌入的陈述按子领域而非数学等价性聚集。数学最吸引人的特点之一（也是使数学如此困难的特点之一）是，一个单一的陈述通常可以用两种截然不同的方式精确描述。这些“一件事，两个视角”的情况是许多富有成果的数学领域（例如，代数几何、代数拓扑和几何群论）的基础。

表1：用于生成MELD的子领域对受此启发，我们引入了**数学等价但词汇不同对（MELD）**222MELD可在https://huggingface.co/datasets/uw-math-ai/MELD-dataset找到，这是一个包含270对用自然语言和LaTeX编写的陈述的数据集，其中配对的陈述是等价的，但无法通过表层词汇相似性轻松匹配。示例如下：

> 恒等映射（集合论）
> 对于集合AA，映射idA:A→A\\mathrm{id}_{A}:A\to A由idA(a)=a\\mathrm{id}_{A}(a)=a定义。

> 恒等映射（范畴论）
> 对于每个对象AA，一个特殊的箭头idA:A→A\\mathrm{id}_{A}:A\to A，使得对于任何对象BB和CC以及f:A→Bf:A\rightarrow B和g:C→Ag:C\rightarrow A，有f∘idA=ff\\circ\\mathrm{id}_{A}=f和idA∘g=g\\mathrm{id}_{A}\\circ g=g。

这270对来自九个不同的领域对，这些领域对一组共同的思想提供了独特的描述（例如，表示论和傅里叶分析）。这些总结在表1（https://arxiv.org/html/2606.23959#S3.T1）中。

表2：MELD中数学等价陈述的检索召回率。每个指标的最佳分数以粗体标出。我们通过遍历九个互补领域对中的每一个，描述两个领域之间的联系，并提示Claude Opus 4.7生成30对数学等价但词汇不同的陈述来生成MELD。然后我们手动审阅这些内容，进行修改以增加不相似性，同时保持等价性。然后我们使用GPT-5.5（中）评估所有陈述，以检查（i）两个陈述是否有效，（ii）它们是否等价，以及（iii）它们是否可以被表述得更不相似。

虽然使用LLM生成的数据集存在风险，但所有内容都属于数学的基础研究生课程，因此应在当前LLM的能力范围之内。这也意味着嵌入模型在MELD上的失败不太可能归因于主题的深奥，而更可能指向这些模型表示数学文本方式的局限性。

为了理解数学文本的嵌入在多大程度上由数学等价性而非仅仅词汇相似性组织，我们使用一些当前最佳的嵌入模型嵌入所有540个陈述，并查看等价对是否彼此靠近分组。这包括`Qwen3-Embedding-4B`（qwen3embedding）、`Qwen3-Embedding-8B`（qwen3embedding）、`harrier-oss-v1-27b`（microsoft2026harrier）、`KaLM-Embedding-Gemma3-12B`（hu2025kalmembedding;zhao2025kalmembeddingv2）、`llama-embed-nemotron-8b`（babakhin2025llamaembednemotron8buniversaltextembedding）和`Octen-Embedding-8B`（octen2025rteb）。

我们发现，陈述主要按其表达所在的领域进行聚类。例如，在表2（https://arxiv.org/html/2606.23959#S3.T2）中，取得最佳结果的模型Octen-Embedding-8B的召回率@1仅为25.0。为了定性地了解原因，在图1（https://arxiv.org/html/2606.23959#S3.F1）中，我们使用UMAP（mcinnes2018umap）降低嵌入的维度，然后可视化来自30对陈述的数据，其中一个是使用向量空间语言编写的（蓝色），另一个是使用模论语言编写的（棕色）。成对的陈述由灰色线连接。该模型似乎强烈地按领域而非等价性对陈述进行聚类。

## 4 一种用于嵌入数学文本的对比方法

第3节（https://arxiv.org/html/2606.23959#S3）中的实验表明，当前的嵌入模型捕捉的是数学陈述的词汇相似性，而非它们的数学等价性。受此启发，我们考虑训练策略，引导模型生成按数学等价性而非表面语言相似性对陈述进行聚类的嵌入。虽然在MELD上进行训练有可能做到这一点，但MELD很小，并且没有简单的方法以低成本进行扩展，因为它依赖于最先进的LLM。幸运的是，形式化的发展已经开始创造解决这一需求的新资源。

mathlib对于在Lean中进行形式化证明开发至关重要，因为它提供了现代数学中核心定义和定理的形式化。mathlib被用于生成`mathlib_informal_v4.16.0`数据集（frenzymath2025mathlibinformal）。该数据集中的每个条目对应一个mathlib陈述，有三种不同的形式：Lean签名、Lean类型和自然语言摘要。我们将这些视为单个底层数学陈述的不同“视图”。我们的假设是，引导模型对齐陈述的形式化和非正式版本的结果将是更好地捕捉数学等价性的嵌入。

### 4.1 训练我们的MathLeap模型

除了继承自`mathlib_informal_v4.16.0`的自然语言、Lean签名和Lean类型视图外，我们还为训练集中的某些实例生成了自然语言重述。我们首先使用`Qwen3.5-9B`将自然语言定理分解为明确的假设和结论。然后，我们将这些提供给`gemma-4-E4B-it`以生成重述。这样做时，`gemma-4-E4B-it`被提示更改定理陈述的 superficial 方面，例如变量名称。更多细节，包括使用的提示，可以在B.1节（https://arxiv.org/html/2606.23959#A2.SS1）找到。我们的最终训练集包含118,334个实例（每个实例有三到四个视图），而测试集包含15,287个实例333https://huggingface.co/datasets/uw-math-ai/Math2Vec-embedding-dataset。大约85%的训练集附有自然语言重述。

由于我们的初步实验表明，`Qwen3-Embedding-8B`（qwen3embedding）和`Octen-Embedding-8B`（octen2025rteb）是数学检索任务中最有效的现有模型，我们选择将这些模型作为微调的基础模型。我们使用来自Sentence-BERT库（reimers-2019-sentence-bert）的缓存多负样本排序损失（Cached Multiple Negatives Ranking Loss）进行训练，这是一种对比损失函数，使用批内负样本，同时避免了将对比方法扩展到GPU训练时常见的 issues。我们使用了默认的缩放值20.0。我们使用了AdamW优化器、700个预热步骤、常数调度器、批量大小为16以及最大序列长度为128。模型训练了大约两个epoch（∼\\sim14,790步）。训练在单个H200上进行，耗时约8小时。我们将得到的模型分别命名为`MathLeap-Qwen-8B`444https://huggingface.co/uw-math-ai/MathLeap-Qwen-8B和`MathLeap-Octen-8B`555https://huggingface.co/uw-math-ai/MathLeap-Octen-8B。

### 4.2 评估

我们在一系列数学检索任务上评估了`MathLeap-Qwen-8B`和`MathLeap-Octen-8B`。总体而言，我们发现，我们用于训练数学嵌入模型的对比方法显著提高了在检索数学等价陈述至关重要的任务上的性能。

#### MELD

对`Qwen3-Embedding-8B`进行微调后，召回率@1从17.0增加到27.2，召回率@5从47.8增加到63.1（表2（https://arxiv.org/html/2606.23959#S3.T2））。同时，数学等价对在所有邻居中的平均排名从16.1下降到9.7（表5（https://arxiv.org/html/2606.23959#A0.T5））。`MathLeap-Qwen-8B`和`MathLeap-Octen-8B`各自在我们所考虑的每个指标上，在MELD上的得分都独立地高于我们评估的任何其他模型。这一点尤其值得注意，因为自然语言