💬 NLP

DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems

本文提出了 DRIFT 框架，通过“分解、检索、举例、形式化”的新范式解决大语言模型在数学定理形式化中难以识别前提和映射形式语言的难题，在多个基准测试中显著提升了前提检索与形式化性能。

原作者： Meiru Zhang, Philipp Borchert, Milan Gritta, Gerasimos Lampouras

发布于 2026-04-08

📖 1 分钟阅读☕ 轻松阅读

原作者： Meiru Zhang, Philipp Borchert, Milan Gritta, Gerasimos Lampouras

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文介绍了一个名为 DRIFT 的新框架，旨在帮助人工智能（大语言模型）更好地完成一项高难度任务：将人类写的数学定理“翻译”成计算机能验证的严格代码（这个过程叫“自动形式化”）。

想象一下，你是一位天才数学家，你能用优美的自然语言写出复杂的定理，但计算机只懂一种极其严格、像法律条文一样死板的“数学编程语言”（比如 Lean）。让 AI 做这个翻译工作，就像让一个只会说中文的人去写一本完全符合英国法律格式的合同，还要求每一个词都不能有歧义。

目前的 AI 在这个任务上经常“翻车”，原因主要有两个：

看不懂“行话”：AI 不知道去哪里找定义好的数学概念（比如“素数”在代码里具体叫什么）。
只会背字典，不会造句：即使 AI 查到了定义，它也不知道怎么把这些定义像搭积木一样正确地拼成一个完整的定理。

DRIFT 就是为了解决这两个问题而设计的，它的名字代表了一个四步走的策略：分解 (Decompose) -> 检索 (Retrieve) -> 举例 (Illustrate) -> 形式化 (Formalize)。

我们可以用一个生动的**“高级翻译团队”**的比喻来理解 DRIFT 是如何工作的：

1. 分解 (Decompose)：把大任务拆成小任务

现状：以前的 AI 拿到一个复杂的数学句子（比如“证明对于形如 4t+3 的素数 p..."），会把它当成一个整体去查资料。这就像让一个翻译员直接去查整本百科全书，结果往往抓不住重点，或者查到了不相关的信息。
DRIFT 的做法：它先派出一位**“拆解专家”**（一个 AI 模型），把那个复杂的长句子拆成几个简单的、原子化的小问题。
- 比喻：就像你要做一道复杂的“佛跳墙”，拆解专家不会直接让你去查“佛跳墙怎么做”，而是先列出清单：“我们需要查‘鲍鱼’的定义”、“查‘海参’的处理方法”、“查‘高汤’的配方”。
- 效果：把一个大而模糊的问题，变成了几个精准的小问题，让后续的搜索更准确。

2. 检索 (Retrieve)：精准查找“零件”

现状：以前的方法是用整个句子去搜，容易搜到一堆看起来像但实际没用的“零件”。
DRIFT 的做法：利用上面拆解出来的小问题，去数学图书馆（Mathlib）里精准地找对应的“零件”（定义、引理）。
- 比喻：既然知道了需要“鲍鱼”和“海参”，我们就直接去海鲜市场分别找这两种东西，而不是拿着整张菜单去问摊主。这样找到的“零件”（数学定义）非常精准。

3. 举例 (Illustrate)：提供“使用说明书”

现状：这是 DRIFT 最精彩的一步。以前的方法只给 AI 提供“零件”（比如告诉你“素数”的代码定义是什么），但没告诉 AI 怎么用这个零件。就像给你一把螺丝刀，却不告诉你怎么拧螺丝。
DRIFT 的做法：它会在找到“零件”后，再去找几个**“示范案例”**。这些案例展示了别人是如何在类似的定理中正确使用这些“零件”的。
- 比喻：这就像在给你螺丝刀的同时，还递给你一本**“乐高搭建说明书”**，上面画着别人是怎么用同样的螺丝刀和积木搭出城堡的。AI 看了这些例子，就知道该怎么把刚才找到的定义正确地“组装”起来，而不是胡乱拼凑。

4. 形式化 (Formalize)：最终组装

做法：最后，AI 综合了所有信息：拆解后的问题、找到的精准零件、以及参考的搭建说明书，最终写出完美的计算机代码。
- 比喻：现在，这位翻译员手里有清单、有材料、有说明书，他就能自信地写出那份完美的法律合同了。

实验结果：它有多强？

研究人员在三个不同的数学测试集上测试了 DRIFT：

ProofNet（大学水平的数学）：DRIFT 的表现大幅领先，几乎把找对“零件”的准确率翻了一倍。
ConNF（非常生僻、从未见过的数学领域）：这是最难的“出考题”。DRIFT 在这里表现惊人，比之前的最好方法提升了 40% 以上。这说明它真的学会了“举一反三”，而不是死记硬背。
MiniF2F（奥林匹克数学题）：对于这种本身就不需要太多外部知识的题目，DRIFT 也能保持不错的水平，没有因为加了太多信息而“画蛇添足”。

总结

这篇论文的核心思想是：不要试图让 AI 一次性解决所有问题，也不要只给它冷冰冰的定义。

DRIFT 就像是一个聪明的项目经理：

它先拆解复杂任务；
然后精准采购所需材料；
接着提供施工案例作为参考；
最后让 AI 完成高质量交付。

这种方法不仅让 AI 在数学翻译上更准确，也为未来让 AI 处理其他复杂、需要大量外部知识的任务（比如写代码、做法律分析）提供了新的思路。

DRIFT 框架技术总结：分解、检索、示例化与定理形式化

本文介绍了一种名为 DRIFT (Decompose, Retrieve, Illustrate, Then Formalize Theorems) 的新框架，旨在解决大型语言模型 (LLM) 在数学定理自动形式化（Autoformalization）中面临的核心挑战。该论文发表于 ICLR 2026。

1. 研究背景与问题定义

自动形式化是指将自然语言描述的数学陈述翻译成机器可验证的形式语言（如 Lean 4）的过程。尽管 LLM 在非形式化数学推理上取得了进展，但在形式化任务中仍面临两大主要障碍：

查询复杂性与粒度不匹配：现有的检索增强生成（RAG）方法通常直接将完整的非形式化陈述作为查询去检索外部库（如 Mathlib）。然而，非形式化陈述往往密集且多维，直接作为查询会导致检索器难以精准定位到形式化所需的原子级定义（如 IsPrimitiveRoot, ZMod 等），因为非形式化文本与形式化定义之间缺乏直接的映射关系。
缺乏上下文用法指导：即使检索到了正确的形式化定义，LLM 往往缺乏如何将这些定义在特定上下文中正确组合和使用的知识（即语法结构和应用模式），导致生成的形式化语句存在句法错误或逻辑结构错误。

现有的依赖检索（Dependency Retrieval）方法虽然能识别所需的定义，但往往忽略了定义在实际定理中的具体用法示例，导致模型在整合信息时表现不佳。

2. 方法论：DRIFT 框架

DRIFT 框架通过四个阶段来解决上述问题，将单调的检索过程转化为一个符合形式数学依赖结构的分解与增强过程（如图 1 所示）：

2.1 分解 (Decompose)

目标：将复杂的非形式化陈述拆解为更小、更易于处理的原子级子查询。
机制：利用 LLM 将输入的非形式化陈述（IF）分解为一组结构化的子查询 $Q = \{(q_i, \hat{l}_i)\}$ $Q={(qi,l^i)}$ 。
- $q_i$ ：描述单一数学概念的自然语言短语。
- $\hat{l}_i$ ：LLM 基于其参数知识预测的该概念的形式化表示（如 Lean 中的类型或定义名）。
优势：这种分解将多维的检索问题转化为针对单一概念的精确搜索，避免了将整句语义压缩进单一向量导致的细节丢失。预测的形式化名称作为“锚点”，辅助检索器更精准地定位。

2.2 检索 (Retrieve)

目标：针对每个子查询，从形式化库（如 Mathlib）中检索对应的依赖前提（Premises）。
机制：使用在依赖检索任务上微调的密集段落检索器（Dense Passage Retriever, DPR，基于 BGE-M3 编码器）。
- 将每个子查询编码为向量，并在预计算的嵌入空间中寻找余弦相似度最高的形式化对象。
- 最终聚合所有子查询的 Top-1 结果，去重后形成依赖前提集 $R_{DRIFT}$ 。
优势：相比直接检索整句，基于分解的检索显著提高了召回率和精确率，能够更准确地捕捉分散在陈述中的不同数学概念。

2.3 示例化 (Illustrate)

目标：为检索到的定义提供具体的使用示例，填补“定义”与“用法”之间的鸿沟。
机制：采用贪心算法从库中选择少量（ $m=3$ $m = 3$ ）具有代表性的定理。
- 候选集：所有使用了至少一个检索前提的定理。
- 选择策略：优先选择能覆盖最多未覆盖前提的定理，同时按语义相似度排序以确保相关性。
优势：这些示例定理展示了检索到的定义在实际代码中的语法结构、类型转换和参数绑定方式，充当了模型生成正确代码的“脚手架”。

2.4 定理形式化 (Formalize Theorems)

目标：生成最终的形式化语句。
机制：LLM 接收包含以下内容的上下文 $C$ $C$ 进行生成：
- 形式化指令 ( $I$ )
- 原始非形式化陈述 ($IF$)
- 检索到的依赖前提集 ( $R_{DRIFT}$ )
- 示例定理集 ( $T$ )
输出：生成符合 Lean 4 语法的定理语句。

3. 关键贡献

提出 DRIFT 框架：首次将查询分解（Query Decomposition）和上下文增强（Context Augmentation）系统性地应用于数学定理的自动形式化。它通过原子化分解解决了查询复杂性，并通过示例定理解决了用法缺失问题。
建立新的 SOTA 性能：在 ProofNet（分布内）、MiniF2F-test（自包含）和 ConNF（分布外）三个基准测试中，DRIFT 在前沿 LLM（GPT-4.1, DeepSeek-V3.1）和专用开源模型（Goedel-V2-8B）上均取得了最先进的性能。
揭示检索有效性的边界：研究发现，检索增强在数学形式化中的效用高度依赖于模型自身的参数知识边界。对于分布外（OOD）任务，检索带来的提升尤为显著；而对于简单的自包含任务，过多的检索上下文可能成为干扰。这强调了自适应检索策略的必要性。

4. 实验结果

实验在三个基准上进行，主要指标包括类型检查通过率 (TC) 和语义等价性 (BEq+)。

依赖检索性能：
- 在 ProofNet 上，DRIFT 的 F1 分数比基线（直接检索整句）提高了 13.34%。
- 在 ConNF（分布外）上，F1 分数提高了 7.74%。
- 分解模块显著提升了检索的精确度和召回率。
形式化性能：
- ProofNet：DRIFT 使 GPT-4.1 的 BEq+@10 提升了 8.56%，超越了现有的检索增强基线 (DPR/RAuto)。
- ConNF (OOD)：表现最为显著。DRIFT 使 GPT-4.1 的 BEq+@10 提升了 55.57%，甚至超越了不完美的 Oracle*（提供真实依赖但无用法示例）基线。这表明示例定理对于处理未知领域的形式化至关重要。
- MiniF2F-test：由于该基准依赖较少，检索有时会成为干扰。DRIFT 在此基准上表现稳健，但在某些情况下，过多的上下文可能导致句法正确性（TC）略有波动，验证了自适应策略的需求。
消融实验：
- 移除“示例化”模块会导致 BEq+ 显著下降，证明用法示例对逻辑正确性至关重要。
- 移除“分解”模块在某些情况下性能未进一步下降甚至略有回升（在 ConNF 上），这揭示了“分解带来的多样性检索”与“示例化提供的脚手架”之间存在协同效应：示例化帮助模型导航分解带来的多样化信息。

5. 意义与展望

方法论创新：DRIFT 证明了将复杂的自然语言任务分解为原子子任务，并结合具体示例进行上下文增强，是提升 LLM 在严格形式化领域表现的有效途径。
对 RAG 的启示：在专业领域（如数学证明），简单的语义相似检索是不够的。必须结合依赖结构分析（分解）和用法模式学习（示例化）。
未来方向：
- 自适应检索：开发能够判断何时需要检索、何时应依赖模型内部知识的智能代理（Agentic）框架。
- 迭代优化：结合编译器反馈（如 Lean 的类型检查错误）进行迭代修正。
- 更广泛的库支持：将检索范围扩展到用户自定义的代码库和局部项目。

综上所述，DRIFT 通过结构化的分解和示例化的上下文增强，显著缩小了非形式化数学陈述与机器可验证形式语言之间的差距，为自动化定理证明系统的进一步发展提供了强有力的工具。