Semantic Search over 9 Million Mathematical Theorems¶

会议: NeurIPS 2026
arXiv: 2602.05216
OpenReview: https://openreview.net/forum?id=GcmwQESSmp
论文: https://arxiv.org/abs/2602.05216
代码: https://github.com/uw-math-ai/theorem-search
领域: 信息检索/RAG
关键词: 语义检索, 数学信息检索, 定理检索, 文本嵌入, 大语言模型

一句话总结¶

针对现有学术检索工具仅停留在论文级而无法定位具体数学命题的痛点，构建了涵盖 920 万条定理语句的最大规模非形式化数学定理库，提出利用 LLM 生成自然语言标语（slogan）表征并结合两阶段向量检索架构，在专业数学家评测集上将定理级 Hit@20 提升至 45.0%。

研究背景与动机¶

数学知识天然以离散命题为核心组织架构，包括定理（Theorems）、引理（Lemmas）、命题（Propositions）和推论（Corollaries）。无论人类数学家在推演新成果以避免重复劳动，还是自动化定理证明智能体在推导过程中寻找辅助前提，实际检索的粒度往往都是一个具体的数学命题而非整篇论文。据 arXiv 撤稿统计，超过 2.5% 的撤回预印本是因为核心结论早已被前人证明；与此同时，先进数学推理模型在探索时也频频陷入因无法获知文献既有引理而重复证明已知结果的困境。然而，现有的学术检索基础设施（如 Google Scholar、arXiv 原生检索乃至挂载通用网页搜索的商业 LLM）均停留在整篇论文维度，迫使研究人员在海量候选论文中耗费大量精力人工通读与翻查。

导致定理级检索长期难以落地的核心矛盾在于：数学定理在源码中以高度符号化、自定义宏密布的 LaTeX 形式呈现，其符号表示与人类数学家在文献翻查或提问时所用的非形式化自然语言之间存在巨大的语义鸿沟。通用稠密检索器在符号密集型文本上极易失效，而现存的形式化数学检索库（如针对 Lean Mathlib4 的工具）所涵盖的定理量级极度有限，仅占全人类数学文献的九牛一毛；要跨越到数百万篇非形式化 arXiv 与经典专著定理，面临极其繁复的 LaTeX 环境鲁棒解析、长上下文非对称语义表示以及超大规模向量低延迟检索三重工程与算法挑战。

本文的切入角度是打破直接对 LaTeX 符号公式做对称匹配的固有思维，引入大语言模型为定理抽取并提炼出高度概括的自然语言“标语”（slogan），将困难的形式化符号匹配转化为成熟的非对称自然语言语义检索。核心 idea：通过三层渐进回退解析管线从 arXiv 及经典数学专著中提取 9.2M 定理级语句，利用结合上下文的 LLM 生成紧凑的自然语言 slogan 作为定理语义检索表征，并基于 HNSW 汉明距离粗筛与余弦精排两阶段架构实现网页级低延迟定理检索。

方法详解¶

整体框架¶

定理检索系统由离线语料构建与标语表征管线、在线多阶段检索索引服务两大部分构成。在离线构建阶段，系统首先采用包含 AST 解析、TeX 编译钩子和正则匹配的三层回退机制，从 arXiv 和 7 个经典开源数学专著源中鲁棒提取出 9.2M 条独立的定理陈述；接着利用大语言模型在引入论文引言/摘要上下文的前提下生成纯 ASCII 的自然语言 slogan 消除符号壁垒；最后使用 Qwen3-Embedding-8B 将标语编码为 4096 维向量并进行二值量化（Binary Quantization）。在线检索阶段，用户输入的自然语言查询在经过短文本重复增强后编码为向量，经由 HNSW 索引在汉明距离空间完成毫秒级粗筛，再在原高维向量空间计算余弦相似度并融合文献引用权重完成重排序。

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    A["多源数学文献库<br/>arXiv + 7个开源数学专著"] --> B["多策略级联解析管线<br/>plasTeX AST → TeX Logging → 正则回退"]
    B --> C["上下文感知标语生成<br/>定理主体 + 论文引言生成自然语言 Slogan"]
    C --> D["两阶段混合检索与排序<br/>二值量化 HNSW 汉明粗筛 + 余弦引用融合精排"]
    D --> E["定理级精准结果输出<br/>定理名称/源码/元数据/双向验证链接"]

关键设计¶

1. 多策略级联解析管线：解决大规模多风格 LaTeX 源码中定理环境的鲁棒抽取 数学文献作者定义定理类环境（Theorem, Lemma, Proposition, Corollary）的宏和宏包五花八门，单一解析器无法兼顾高准确率与全量覆盖。本文设计了由深到浅的三级渐进式回退架构：首先采用 Python 库 plasTeX 将 LaTeX 源码编译转换为抽象语法树（AST），遍历命令与环境节点，精准抽取定理类型、编号、附加备注（note，如“Theorem 3.9 (Shokurov reduction)”）与主体（body），并自动展开作者在导言区定义的诸如 \R \to \mathbb{R} 的简单宏；对于因未识别宏包而失败的文档，无缝回退至定制的 TeX Logging 宏包方案，在论文 TeX 编译时通过底层日志钩子拦截并记录所有定理环境；若编译依然失败，则最后回退至轻量正则表达式解析器，通过 \begin{...}、\proclaim 等分隔符兜底。整套管线从 arXiv 成功解析出 920 万条定理，并拓展至 Stacks Project、ProofWiki、HoTT Book 等开源专著，结合启发式规则过滤截断残缺语句，保证了语料的纯度与完整度。

2. 上下文感知标语生成：消除符号语义鸿沟与非对称信息检索建模 直接对包含大量 LaTeX 命令和紧凑符号的定理陈述计算嵌入向量已被证实效果极差，因为现存预训练嵌入模型主要在自然语言上训练，难以对齐符号推导；且人类科研人员在检索定理时通常采用概括性的非形式化自然语言描述（如“有理代数簇是单连通的”）。为此，本文引入大语言模型（DeepSeek-V3 / Claude 3.5 Sonnet 等）为每条定理生成不超过 4 句话、纯 ASCII、去除复杂符号和证明细节的自然语言“标语”（slogan），将定理检索重构为非对称检索任务。更为关键的是，数学定理往往高度依赖前文引入的概念符号与上下文定义，脱离上下文的定理主体极易导致生成的 slogan 语义断层。系统在提示词中不仅输入定理主体，还系统引入论文的第一节（引言），利用引言中阐述的全局动机、核心贡献与定义背景辅助 LLM 准确理解局部引理的技术定位，从而显著提升了标语的判别力。

3. 两阶段混合检索与排序：兼顾海量定理级向量的秒级响应与精细语义分辨 在 920 万规模的高维稠密向量空间中实现交互式检索，直接计算 4096 维浮点向量的余弦相似度会导致不可接受的延迟。本文在 PostgreSQL 中部署 pgvector 扩展与层次化可导航小世界图（HNSW）索引，并结合二值量化（Binary Quantization）技术将 4096 维浮点向量压缩为 4096 比特二进制签名。在线查询时，系统首先在比特流上通过汉明距离快速粗筛出候选池： $$\text{pool\_size} = \text{clamp}(\max(200, 12 \times k), 200, 800)$$ 随后基于原始未量化浮点向量计算精确余弦相似度完成重排序。当用户启用学术权重模式时，系统采用复合打分公式平衡语义匹配度与经典文献权威度： $$\text{score} = \cos(\mathbf{q}, \mathbf{d}) + \lambda \cdot \log(\max(\text{citations}, 1))$$ 其中 $\lambda$ 为用户可调节的权重超参数。此外，针对用户短关键词查询与多句型标语嵌入长度失配的问题，设计了自动检测并复制短查询（Query Duplication）机制，有效强化关键术语在嵌入表示中的信号强度。

一个完整示例：代数几何定理端到端检索¶

以数学家查询“over an algebraically closed field, any abelian p-Lie algebra splits as a torus and a sum of nilpotent cyclic Lie algebras”为例： 1. 查询预处理：查询文本被注入指令提示词 Instruct: Given a math search query, retrieve theorems mathematically equivalent to the query.\nQuery: ...，通过 Qwen3-Embedding-8B 映射为 4096 维向量 $\mathbf{q}$ 并量化为 4096-bit 签名。 2. HNSW 粗筛：在 9.2M 的 pgvector 二进制索引中计算汉明距离，在 50ms 内从 920 万条定理标语中筛选出排名前 200 个候选定理。 3. 高维余弦精排：加载这 200 个候选标语的原始浮点向量，计算精确余弦相似度并结合引用量对数奖励项重新排序。 4. 结果命中与溯源：系统排在第 1 位的检索结果精准命中 Usefi (2009) 论文中的 Theorem 2.7，前端界面同时展示该定理的纯文本标语、完整编译的 LaTeX 渲染公式及 arXiv 原文直达链接，全流程耗时约 3 秒（远快于传统 LLM 联网检索的 60+ 秒）。

实验关键数据¶

主实验：验证集检索性能评测¶

评测基于 3 位资深研究数学家在不接触语料标语的情况下独立盲写出的 111 个专业数学定理检索查询（覆盖代数几何、偏微分方程、经典分析等 14 个领域）。基线方法包括通用论文检索工具（Google Search 约束 site:arxiv.org、arXiv 原生高级检索）以及具备联网搜索能力的先进大模型（ChatGPT 5.2 w/ Search、Gemini 3 Pro）。结果指标以“定理级命中率 / 论文级命中率”汇报（Google 与 arXiv 仅支持论文级检索）。

检索模型 / 系统	Hit@1	Hit@10	Hit@20	MRR@20
Google Search (site:arxiv.org)†	– / 0.162	– / 0.378	– / 0.378	– / 0.237
arXiv Advanced Search†	– / 0.009	– / 0.018	– / 0.027	– / 0.011
ChatGPT 5.2 w/ Search	0.117 / 0.117	0.180 / 0.180	0.198 / 0.198	0.139 / 0.139
Gemini 3 Pro	0.171 / 0.171	0.252 / 0.252	0.270 / 0.270	0.196 / 0.196
Gemma 0.3B (原始 LaTeX)	0.027 / 0.054	0.090 / 0.117	0.090 / 0.135	0.041 / 0.070
Gemma 0.3B (Slogan)	0.081 / 0.108	0.189 / 0.225	0.252 / 0.306	0.118 / 0.154
Qwen3 0.6B (Slogan)	0.081 / 0.153	0.234 / 0.342	0.270 / 0.351	0.132 / 0.215
Qwen3 8B (Slogan)	0.171 / 0.243	0.387 / 0.505	0.450 / 0.568	0.243 / 0.328
Qwen3 8B w/ Reranker (0.6B)	0.189 / 0.324	0.432 / 0.613	0.450 / 0.631	0.270 / 0.416

注：† 表示仅能返回论文级结果，无法直接定位定理。

消融实验：Slogan 上下文窗口与生成模型对比¶

在包含 7,356 条代数几何陈述的高精度子集上，固定 Qwen3-8B 嵌入模型，系统对比了不同上下文注入方案以及不同生成基座模型对检索召回的影响。

上下文配置 / 生成模型	Hit@1	Hit@10	Hit@20	MRR@20
上下文消融 (DeepSeek-V3)
仅定理主体 (Body Only)	0.342	0.658	0.737	0.451
定理主体 + 摘要 (w/ Abstract)	0.316	0.645	0.737	0.429
定理主体 + 第一节引言 (w/ First Section)	0.368	0.737	0.763	0.496
Slogan 生成器消融 (Body+Abstract)
DeepSeek-V3.1	0.316	0.645	0.737	0.429
DeepSeek-R1	0.276	0.671	0.697	0.388
Gemini 3 Pro	0.368	0.750	0.816	0.507
Claude Opus 4.5	0.395	0.776	0.842	0.536

关键发现¶

Slogan 化是突破符号壁垒的决定性因素：直接对 LaTeX 源码做嵌入时，Gemma 0.3B 的定理级 Hit@20 仅有 9.0%，而转为自然语言 slogan 后暴增至 25.2%（提升近 3 倍），证明了非对称口语化表示在数学 IR 中的基石作用。
引入引言上下文带来显著增益：将论文第 1 节（引言）引入 Slogan 生成 prompt 后，Hit@10 从 65.8% 提升至 73.7%，MRR@20 从 0.451 提升至 0.496；而仅加摘要反而略有波动，表明只有详细阐述定义与背景的引言才能有效消除引理的上下文孤岛效应。
前沿闭源 LLM 生成的标语质量更高：Claude Opus 4.5 生成的标语取得了 84.2% 的 Hit@20 和 0.536 的 MRR@20，明显优于开源模型，展现了更精准提炼抽象数学内涵的能力。
通用 LLM 搜索的“论文聚集效应”压低了检索多样性：ChatGPT 与 Gemini 在联网搜索时倾向于连续返回同一篇论文中的多个条款，其平均返回独立论文数仅为 10.98 篇，而 Qwen3 8B 检索结果覆盖 16.89 篇独立论文，更擅长挖掘深藏于论文腹地的关键辅助引理。

亮点与洞察¶

将定理确立为信息检索的第一等公民：改变了学术搜索数十年以文档为颗粒度的范式，建立起全球最大（9.2M+）的定理级非形式化数学索引数据库。
低成本高质量的数据生产管线：整个 920 万条定理的解析与 slogan 生成仅耗费约 6,000 美元（4,000 美元 LLM API + 2,000 美元算力存储），验证了用中等尺寸/前沿 API 进行超大规模学术资产重构的可行性。
即插即用的 AI 智能体 RAG 工具：系统不仅上线了 Web 前端，更提供了标准 REST API 与 MCP（Model Context Protocol）服务器，使得 Claude 等外部推理 Agent 能够直接调用定理搜索，有效根治数学前沿推导中的“幻觉定理”问题。

局限与展望¶

作者承认的局限：语料解析仍存在少量长公式截断和宏展开失效现象；依赖单向量密集检索在极端冷门的代数记号上可能不如稀疏精确词匹配敏感。
深层局限与假设：当前的验证集仅有 111 个查询且偏重代数几何与分析，虽然契合 MathIR 小而精的基准惯例，但对于离散数学、概率统计等大类的覆盖仍待扩充；对于包含复杂交换图表、长证明构造的定理，纯文本标语依然会丢失结构化拓扑信息。
后续演进方向：引入 ColBERT 类晚期交互（Late Interaction）模型或稀疏稠密混合检索（BM25+Dense），探索与形式化证明辅助器（Lean 4 / Isabelle）的深度端到端前提选择（Premise Selection）协同。

评分¶

新颖性: ⭐⭐⭐⭐ [首次在近千万级非形式化数学定理上实现低延迟、高召回的语义级检索]
实验充分度: ⭐⭐⭐⭐ [包含了 111 个专家盲测真实验证集、细致的消融实验与 RAG 推理落地展示]
写作质量: ⭐⭐⭐⭐⭐ [逻辑架构清晰严密，工程实现与学术洞察并重]
价值: ⭐⭐⭐⭐⭐ [极大便利了数学研究人员避免重复发明轮子，并为数学 Agent 提供了急需的基石检索工具]