COMPOSE 数据集

COMPOSE数据集是由耶路撒冷希伯来大学研究团队构建的大规模数学研究资源，旨在支持基于科学引文和形式定理依赖的接地未来数学生成任务。该数据集包含108,000个配对样本，每个样本由科学图（基于arXiv论文的引文网络和定理提取）和形式图（基于Mathlib定理依赖结构）组成，数据来源涵盖2000年至2023年的50万篇数学论文，并通过FrenzyMath进行非形式化对齐处理。数据创建过程涉及从S2ORC收集数学论文、构建引文图、提取定理节点，并与Mathlib形式定理库进行对齐，形成双图结构。该数据集主要应用于人工智能驱动的数学研究预测领域，旨在解决如何结合科学语境和形式逻辑约束来生成合理未来数学命题的核心问题，为机器学习模型提供多源知识融合的训练基础。

The COMPOSE dataset is a large-scale mathematical research resource constructed by a research team from the Hebrew University of Jerusalem, aiming to support grounded future mathematical generation tasks based on scientific citations and formal theorem dependencies. It contains 108,000 paired samples, each consisting of a scientific graph (based on the citation network and theorem extraction from arXiv papers) and a formal graph (based on the Mathlib theorem dependency structure). The data sources cover 500,000 mathematical papers published between 2000 and 2023, and the dataset undergoes informal alignment processing via FrenzyMath. The data creation process involves collecting mathematical papers from S2ORC, constructing citation graphs, extracting theorem nodes, and aligning with the Mathlib formal theorem library to form a dual-graph structure. This dataset is mainly applied in the field of AI-driven mathematical research prediction, aiming to solve the core problem of how to combine scientific context and formal logical constraints to generate plausible future mathematical propositions, and provide a training foundation for machine learning models to fuse multi-source knowledge.

搜集汇总

数据集介绍

构建方式

COMPOSE 数据集通过系统性地整合科学论文中的引文图与基于 Mathlib 的形式定理依赖图构建而成。具体而言，从 arXiv 数学论文中提取锚定论文及其引文子图，同时利用 FrenzyMath 语料库以非正式到非正式的相似度检索策略，将论文中提取的非正式定理与 Mathlib 中的形式定理进行对齐。随后，以对齐的形式定理为根节点，从 Mathlib 中扩展其局部依赖关系形成形式图，最终整合得到约 108K 个配对样本，并额外构建了涵盖 47K 篇未来论文的评估基准。

特点

该数据集的核心特色在于其双图（dual-graph）结构，同时融合了科学引文上下文与形式定理依赖关系。科学图继承了论文之间思想演变的脉络，而形式图则捕获了数学定理之间严格的逻辑依赖。通过非正式到非正式的对齐策略，有效克服了非正式数学文本与形式语法之间的语义鸿沟。数据集规模庞大，涵盖多种数学子领域，且包含时间上独立的未来论文评估集，支持对模型时间泛化能力的可靠评估。

使用方法

使用 COMPOSE 数据集时，采用双图编码器架构：分别用图神经网络对科学引文图与形式定理依赖图进行编码，再通过交叉注意力机制将两者融合为统一的图表示。该表示随后作为条件输入至数学专用的大语言模型解码器（如 DeepSeek-Math），从而生成立足先前工作且符合形式逻辑依赖的未来数学定理。模型训练分为两阶段：第一阶段通过对比学习与对齐目标优化图编码器与融合模块，第二阶段微化解码器以生成图条件化文本。在推理时，仅需给定锚定论文的标题，系统自动构建其双图并生成预测。

背景与挑战

背景概述

COMPOSE数据集由希伯来大学的David Busbib与Michael Werman于2026年构建，旨在填补数学未来研究生成领域中科学与形式知识融合的空白。现有方法或仅关注科学文献中的引文脉络，或仅局限于形式定理库的逻辑依赖，未能将二者有机结合，导致生成的未来数学命题缺乏扎实的双重根基。该数据集包含从arXiv与Mathlib中提取的约10.8万对科学-形式图样本，以及来自2024至2025年间的4.7万篇未来论文作为评测基准，开创性地提出了“有根基的未来数学生成”任务。其核心研究问题在于：如何同时建模科学引文图所指示的研究趋势与形式定理依赖图所约束的逻辑可行性，从而生成既符合学术方向又具备形式有效性的未来数学猜想。该数据集深刻影响了数学自动化推理、科学预言生成以及人机协同数学发现等前沿领域，为智能数学研究开辟了崭新路径。

当前挑战

该数据集面临的核心挑战在于双重异质性：科学引文图与形式定理依赖图虽共享数学内容，但其结构范式截然不同，前者以论文为节点表征思想演化，后者以定理为单元体现逻辑脉络，如何实现跨模态的有效对齐与融合是一大难题。其次，构建过程中面临非形式化数学表述与形式化定理库之间的语义鸿沟，采用非形式到非形式的对齐策略虽优于自动形式化方法，但高置信匹配率仍仅达16.9%，引入了显著噪声。此外，生成的未来数学主张缺乏形式证明验证器的直接验证，目前只能依赖检索评估与语言模型评判等代理信号，而非严格的逻辑正确性测试。数据集还需应对未来论文中主定理自动提取的噪声问题，尤其当论文包含多个并列结果时，这一过程更为脆弱。

常用场景

经典使用场景

COMPOSE数据集的核心价值在于其为未来数学定理生成任务提供了首个融合科学引文语境与形式化定理依赖结构的双图框架。该数据集将108K对来自arXiv的论文摘要、引文网络与Mathlib形式化定理库中的依赖图进行配对对齐，构建了从非正式数学文本到形式化证明结构的桥梁。其最经典的用法是作为双图编码-解码模型的基础训练资源，用于生成既符合学界研究演化方向、又受限于形式化逻辑依赖的合理未来数学断言，从而模拟数学家在已有文献和已知定理逻辑约束下提出新推论的认知过程。

衍生相关工作

该数据集直接催生了一系列跨学科的前沿工作，涵盖未来科学研究生成、形式化数学推理以及非正式-形式化对齐三大方向。在生成方向，它启发了结合引文图与时序监督的未来论文摘要与主张预测方法；在形式推理方向，其双图编码思想被借鉴以改进定理前提选择与蓝图自动生成系统，使探针搜索能同时被文献语境和形式依赖所引导；在对齐方向，其非正式到非正式的检索策略（FrenzyMath）为跨表示空间的高覆盖率匹配提供了高效范式，后续工作在此基础之上发展了更强的联合嵌入与交错训练方案，推动自动形式化在真实论文层面的可用性迈上新台阶。

数据集最近研究

最新研究方向

当前，COMPOSE数据集的前沿研究聚焦于将科学引文语境与形式化定理依赖结构深度融合，以生成具有数学严谨性和逻辑合理性的未来数学定理。这一方向突破了传统方法仅依赖单一语境（如文本或形式化证明）的局限，通过构建双图编码框架，同时捕捉学术论文中隐含的研究演化路径与形式化数学库中定理间的推理约束，使得生成结果不仅在内容上延续先前的科学趋势，更在逻辑上严格遵循已有的定义与引理。该工作发表的论文还配套构建了包含10.8万对科学-形式图样本的大规模基准，并设立了基于2024-2025年未来论文的评估集，为自动数学推导与定理猜想提供了可验证的数据基础与评测标准，有望加速人工智能辅助数学发现的过程。

相关研究论文

• COMPOSE: Composing Future Theorems from Citations and Formal Structure

  耶路撒冷希伯来大学 · 2026年