💻 computer science

COMPOSE: Composing Future Theorems from Citations and Formal Structure

本文介绍了 COMPOSE，这是一种双图框架，通过联合利用科学引用上下文和形式化定理依赖关系来生成合理的未来数学定理，并通过新构建的数据集和基准测试证明了其卓越性能。

原作者： David Busbib, Michael Werman

发布于 2026-05-29

📖 1 分钟阅读☕ 轻松阅读

原作者： David Busbib, Michael Werman

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

想象一下，你正试图预测数学某个特定领域的下一个重大突破。你想猜测未来的一篇论文会说什么，但你不希望只是胡乱编造一些数学词汇。你希望你的猜测是合理的——这意味着它既要符合当前的学术对话，又要遵循数学所要求的严格逻辑规则。

本文介绍了一个名为COMPOSE（从引用和形式结构中构建未来定理）的新系统，旨在实现这一目标。

以下是其工作原理，分解为简单的概念：

问题：两张不同的地图

要预测数学的未来，你通常需要两样东西，但现有的工具只关注其中一样：

“社会”地图（引用）： 这就像观察派对上谁在和谁交谈。如果论文 A 引用了论文 B，它们就在进行对话。这告诉你哪些主题很流行，以及研究正朝着什么方向发展。
“逻辑”地图（形式结构）： 这就像游戏规则手册。在数学中，你不能随意说话；你必须用之前的步骤来证明它。这张地图展示了严格的依赖关系：“只有在你已经知道引理 Y 的情况下，你才能证明定理 X。”

问题所在：

如果你只看社会地图，你可能会猜出一个很流行但在逻辑上不可能的话题（就像试图在没有地基的情况下盖房子）。
如果你只看逻辑地图，你可能会找到一个逻辑完美的证明，但它可能关于一个没人再关心的主题，或者它可能错过了该领域发展方向的“大局”。

解决方案：COMPOSE

作者构建了一个系统，它既像一位双语翻译，又像一名侦探。它同时查看这两张地图。

输入： 你向系统提供一篇“锚定论文”（一篇当前的数学论文）。
双重图：
- 它构建一个科学图：它查看锚定论文及其引用的论文，形成一个思想和对话的网络。
- 它构建一个形式图：它提取这些论文内部的数学定理，并在一个名为Mathlib的巨大数字图书馆中找到它们的“官方”版本（Mathlib 就像一个经过验证的数学证明百科全书）。然后，它追踪这些官方版本之间的逻辑依赖关系。
融合： 系统使用一种特殊的“神经网络”（一种人工智能）来合并这两张地图。它学习对话（引用）如何与规则（形式逻辑）相连接。
输出： 系统生成一个新的、合理的数学主张（一个“未来定理”），它既符合当前的学术对话，又遵守逻辑规则。

类比：预测国际象棋的下一步

想象一下，你正试图预测一场复杂国际象棋比赛中的下一步棋。

旧方法就像查看一份流行的国际象棋开局列表（“社会地图”）。它们能猜到你可能会走“王翼弃兵”，但它们不知道这步棋是否合法，或者是否会导致你立即被将死。
COMPOSE就像一位特级大师，它既查看比赛历史（以前谁走了什么棋），又查看国际象棋的严格规则（棋子如何移动）。它预测的一步棋不仅是一个流行的策略，而且是一步合法、稳健且符合当前棋盘局势的棋。

他们如何测试它

研究人员没有只是猜测；他们构建了一个巨大的测试集。

他们收集了 108,000 个论文及其对应形式逻辑结构的示例。
他们利用 2024 年末和 2025 年发表的论文创建了一个“未来测试”（模型尚未见过这些论文）。
他们问模型：“基于这篇旧论文，下一篇论文会说什么？”

结果：

更准确的猜测： 与其他人工智能模型相比，COMPOSE 在猜测未来论文的确切主题方面表现更好。
更扎实： 当人类评委（以及其他人工智能）审查输出结果时，COMPOSE 的猜测在数学深度、具体性和准确性方面获得了更高的评分。
秘密武器： 当他们关闭“社会地图”或“逻辑地图”中的任何一个时，系统的表现都会变差。这证明了要做出良好的预测，你确实需要两者兼备。

一个局限性（“盲点”）

该论文承认一个弱点：系统依赖“形式地图”（Mathlib）来运作。如果一个数学主题非常新或非常小众，尚未被写入形式化图书馆中，系统可能会感到困惑，并试图将这个新主题强行归入旧的、不相关的类别中（就像试图用另一种乐器的规则来解释一种新类型的音乐）。

总结

COMPOSE是一个工具，它通过结合数学家们在讨论什么与他们的逻辑实际如何运作，来帮助预测数学的未来。它确保未来的预测不仅仅是听起来流畅的胡言乱语，而是既扎根于该领域的历史，又遵循数学的严格规则。

技术摘要：COMPOSE——基于引用与形式结构构建未来定理

问题定义

本文探讨了有依据的未来数学生成这一挑战：即为给定的“锚点”论文预测一个合理的未来数学主张（类定理陈述）。作者认为，有效的预测必须同时满足两个约束条件：

科学轨迹：它必须延伸科学引用图所指示的研究方向以及文献中思想的演变。
形式依据：它必须尊重形式数学中固有的逻辑依赖关系，确保该主张能从现有的定义、引理和定理中有效推导出来。

现有方法通常仅建模这两种来源之一。仅基于科学文本训练的模型可能生成流畅但缺乏逻辑依据的主张，而定理证明系统虽能基于形式结构进行推理，却缺乏识别有前景研究方向的科学背景。本文指出，由于科学论文与形式库（如 Mathlib）在组织知识方面的根本差异，将这两种互补来源相结合并非易事。

方法论：COMPOSE 框架

作者提出了COMPOSE，这是一个双图框架，使语言模型能够同时基于科学引用上下文和形式定理结构进行条件生成。该方法包含三个主要组成部分：

1. 数据构建

作者构建了一个包含108,000 个成对科学 - 形式图示例的数据集，源自 arXiv 数学论文（2000–2023 年）和 Lean Mathlib 库。

科学图（ $G_s$ ）：基于锚点论文及其引用上下文（最多两跳）构建。它包含论文的摘要节点和从文本中提取的定理节点。边代表引用链接和论文内部的依赖关系。
形式图（ $G_f$ ）：通过将提取的非形式定理与 Mathlib 中的相应定理对齐来构建。这种对齐使用FrenzyMath（一个为 Mathlib 定理编写的人工非形式描述语料库）执行非形式到非形式的检索，从而避免直接自动形式化带来的噪声。形式图利用通过 LeanDojo 提取的依赖边，从匹配的定理根节点向外扩展。
基准测试：一个时间上留出的测试集，包含 2024 年末至 2025 年的47,000 篇未来论文，用于评估模型预测实际已发表结果的能力。

2. 模型架构

COMPOSE 采用双编码器架构，后接一个以图为条件的解码器：

双编码器：两个专用的图神经网络（GNN）分别处理 $G_s$ $G_{s}$ 和 $G_f$ $G_{f}$ 。
- $G_s$ 节点使用 E5 嵌入（科学文本）初始化。
- $G_f$ 节点使用 DeepSeek-Math 嵌入（形式签名）初始化。
- 两者均采用带有门控残差连接的有向、边类型特定的消息传递机制。
融合模块：来自两个图的表示被投影到共享的潜在空间，并通过双向交叉注意力机制进行融合。这使得模型能够将科学方向与形式约束相结合。
解码器：一个经过预训练的数学专用大语言模型（DeepSeek-Math-7B 或 Mistral-7B），并采用 LoRA 进行适配。交叉注意力层被插入解码器中，使生成过程以融合后的图嵌入为条件，允许模型在生成 token 时关注完整的图结构。

3. 两阶段训练

阶段 1（表示学习）：在不使用解码器的情况下，使用三个目标训练图编码器和融合模块：
- 链接预测：确保编码器捕捉图结构。
- 对比对齐：将融合后的图表示与目标论文的摘要及主要主张对齐。
- 交叉对齐：显式地将非形式定理节点与其匹配的形式对应项对齐。
阶段 2（生成）：添加解码器并使用以下方法进行微调：
- 自回归损失：标准的下一个 token 预测。
- 图边界损失：一项正则化项，如果模型为不匹配的图对生成相同的文本，则对其进行惩罚，迫使模型依赖特定的图上下文。

关键结果

实验在 47K 未来论文基准上进行了，将 COMPOSE 与强基线模型（包括 GIANTS、FutureGen、GoAI 以及各种仅文本或仅提示变体）进行了比较。

检索性能：COMPOSE 取得了最高的Gap（0.240），定义为生成文本与真实未来论文之间的余弦相似度与与无关论文之间余弦相似度的差值。它在H@10（50.8%）和H@100（80.8%）方面显著优于基线，表明其生成的主张更有可能从池中检索到正确的未来论文。
新颖数学主张预测（NMCP）：COMPOSE 在精确率（0.560）和匹配度（0.730）方面领先，表明其输出不仅在主题上，而且在形式和非形式层面上都与未来定理相一致。
LLM 裁判评估：LLM 裁判（GPT-4.0）从内容、深度、新颖性、精确性和具体性等方面评估了输出。COMPOSE 获得了最高的总体得分（3.36/5），特别是在技术深度（3.52）和具体性（3.52）方面，其生成的输出比基线（通常生成模糊的摘要）更加具体且数学内容更丰富。
消融研究：移除科学图编码器或形式图编码器均导致性能显著下降，证实了两种模态提供了互补的信号。形式图对于提供依据至关重要，而科学图对于识别正确的研究方向必不可少。

意义与主张

本文主张，未来数学生成受益于科学背景与形式结构的结合。

有依据的生成：作者证明，仅依赖科学文本会导致主张在主题上相关但缺乏逻辑依据，而仅依赖形式结构则会将模型限制在已知定理范围内，无法预见新方向。COMPOSE 成功弥合了这一差距。
数据贡献：108K 成对数据集和 47K 未来论文基准的构建为评估有依据的数学生成提供了新资源，解决了该领域缺乏时间基准的问题。
方法进步：带有交叉注意力融合的双图框架为将异构知识来源（非形式文献与形式逻辑）整合到生成任务中提供了一种新颖的方法。

作者指出了局限性，具体而言，该方法依赖于近似的非形式 - 形式对齐（这在 Mathlib 覆盖稀疏的领域可能会引入噪声），并且生成的主张未经过证明助手验证，而是依赖检索和基于 LLM 的评估作为代理信号。他们建议未来的工作可以纳入证明感知的验证，以直接检查生成主张的形式正确性。