核心发现
方法论
本文提出一种双图编码框架COMPOSE，利用科学引用图和形式定理依赖图两个互补的图结构，通过专门设计的图神经网络（GNN）编码器分别提取图特征，再通过交叉注意机制融合，最终条件化语言模型生成未来可能的数学定理。数据集由arXiv和Mathlib中共108K对科学-形式图组成，训练分两个阶段：第一阶段优化图编码和对齐目标，第二阶段微调生成模型。该方法显著优于单一信息源模型，在检索真实未来论文方面表现优异，获得最高的LLM评判得分。
关键结果
- 在未来论文检索任务中，COMPOSE在47K测试样本中实现Tgt-Sim 0.525，明显优于仅利用科学引用图或形式依赖图的模型（最高0.471），Gap指标达0.240，表明生成内容更贴近真实未来论文。在多项指标如H@10和H@100中也优于基线，说明模型能更准确地预测未来研究方向。
- 在生成质量评估中，COMPOSE在LLM评判中获得平均3.36/5分，特别在数学内容、深度和专业性方面表现突出，优于纯文本或单一图源模型。通过消融实验验证双图融合机制的贡献，去除任一图源或融合步骤都导致性能下降。
- 在跨场景测试中，COMPOSE在不同解码器（DeepSeek-Math 7B和Mistral 7B）上均表现优越，验证其模型架构的鲁棒性和泛化能力。该系统不仅能预测具体未来定理，还能在广义研究方向上提供有价值的科学建议。
研究意义
该研究突破了传统单一信息源的限制，首次系统性结合科学文献中的引用关系和形式化定理结构，为数学创新提供了自动化辅助工具。其深远意义在于推动自动数学推理、科学发现的自动化进程，助力科研人员快速洞察潜在研究方向，减少重复劳动，加速数学理论的发展。未来，该技术有望融入数学文献管理、自动推理系统甚至人工智能辅助科研平台，极大提高科研效率和创新能力。
技术贡献
本文提出了双图编码与融合机制，创新性地将科学引用图与形式定理依赖图结合，利用专门的GNN编码器提取结构特征，通过交叉注意机制融合信息，条件化生成模型实现了对未来定理的 grounded 生成。数据集构建采用多层次对齐策略，结合FrenzyMath和Lean的Mathlib库，丰富了学术图谱的构建方法。训练采用两阶段策略，有效优化图表示和生成能力，显著提升了模型在科学推理中的表现。该框架为未来结合多源知识进行科学推理提供了新思路。
新颖性
这是首个系统性将科学文献中的引用关系与形式定理结构融合，用于未来数学定理生成的工作。不同于以往只关注文本或单一结构的模型，COMPOSE通过双图编码实现信息互补，显著提升生成的科学深度和逻辑严密性。其创新点在于引入对齐目标和多阶段训练策略，有效解决了 informal-formal 结构映射和知识融合的难题，开辟了自动化数学推理的新路径。
局限性
- 模型依赖于高质量的图结构和对齐信息，若图构建或对齐出现偏差，可能影响生成效果，特别是在新颖或未覆盖的数学领域。
- 当前系统主要面向数学论文，尚未充分验证在其他科学领域的迁移能力，且对复杂长篇推理的处理仍有限。
- 训练和推理过程计算成本较高，尤其是在大规模图和模型条件下，实际应用中需考虑效率优化。
未来方向
未来可探索多模态知识融合，如引入图像、代码等多源信息，增强模型的推理能力。同时，结合强化学习优化生成的科学合理性，提升模型的创造性和可靠性。此外，扩展到其他科学领域，推动跨学科的自动化科学发现，逐步实现自动化数学和科学研究的智能助手。
AI 总览摘要
在当今科学研究中，数学作为基础学科，其创新性和严密性对科技进步起着关键作用。然而，随着文献数量的激增，科研人员面临着海量信息的筛选与理解难题。传统的自动化方法多依赖于单一信息源，如文本或结构化数据库，难以全面捕捉数学知识的深层联系。本文提出了COMPOSE框架，旨在通过结合科学引用图和形式定理依赖图，生成具有数学深度的未来定理，为自动数学推理开辟新路径。
COMPOSE的核心思想在于利用两个互补的图结构：一是科学引用图，反映研究的演变路径和研究方向；二是形式定理依赖图，揭示定理之间的逻辑关系。通过专门设计的图神经网络（GNN）编码器，分别提取这两种图的结构特征，再通过交叉注意机制融合，形成统一的知识表示。这一融合的表示作为条件，驱动预训练的数学专用语言模型生成未来可能的数学定理。
为了训练和评估该模型，作者构建了一个庞大的数据集，包括来自arXiv和Mathlib的108K对科学-形式图对，以及一个由2024-2025年未来论文组成的47K测试集。训练采用两阶段策略：第一阶段优化图编码和对齐目标，确保模型能有效捕获图结构和知识对齐；第二阶段微调生成模型，增强其在实际生成任务中的表现。实验结果显示，COMPOSE在未来论文检索和定理生成任务中均优于多种基线模型，特别是在保持内容深度和数学严密性方面表现突出。
此外，通过LLM评判和消融实验，验证了双图融合机制的有效性。模型不仅能准确预测未来研究方向，还能生成具有数学丰富性和逻辑严密的定理描述，为自动化数学推理提供了强有力的技术支持。这一研究不仅推动了科学知识图谱的构建，也为未来智能科研助手的实现奠定了基础。尽管如此，模型在处理极端新颖或复杂推理任务时仍存在一定局限，未来的研究将继续优化图结构构建和多模态融合策略，期待在跨学科科学研究中发挥更大作用。
深度分析
研究背景
随着人工智能技术的快速发展，自动科学推理逐渐成为研究热点。早期工作主要集中在自然语言处理和知识图谱构建，如OpenAI的GPT系列、BERT等模型在科学文本理解中的应用。近年来，图神经网络（GNN）在科学知识图谱中的表现尤为突出，特别是在捕获论文引用关系和定理结构方面。数学推理系统如Lean的Mathlib、Coq和Isabelle，提供了丰富的形式化定理库，显著提升了逻辑推理的严密性。然而，现有方法多局限于单一信息源，难以结合科学论文的演化轨迹与形式化的逻辑关系，导致生成的定理缺乏深度和逻辑一致性。近年来，尝试将非正式的自然语言描述映射到形式化语法的Autoformalization工作逐步展开，但在大规模论文层面仍面临词汇差异和结构匹配的挑战。综上，如何融合科学文献中的演化路径与形式定理的逻辑关系，成为推动自动数学推理的重要难题。
核心问题
核心问题在于如何有效结合科学论文中的演化线索与形式定理的逻辑依赖，以生成合理的未来数学定理。单一信息源模型在科学探索中表现有限：只利用引用关系的模型缺乏逻辑严密的推理基础，难以保证生成内容的数学正确性；而只依赖形式定理结构的模型则缺乏科学背景和研究动机，难以预测创新方向。这种信息孤岛式的建模方式，限制了模型在复杂推理和创新生成中的能力。实际应用中，科研人员需要一种既能理解研究演变，又能保证逻辑严密的工具，以辅助发现潜在的研究突破。解决这一问题，要求模型不仅具备强大的结构编码能力，还能实现不同知识源的有效融合，确保生成内容既科学合理，又具有创新潜力。
核心创新
本文的创新点主要体现在以下几个方面：
- �� 双图编码架构：引入科学引用图和形式定理依赖图两个结构化知识源，分别用专门的GNN编码器提取特征，突破单一信息源的限制。
- �� 图结构融合机制：设计交叉注意机制，将两个图的表示进行有效融合，形成统一的知识表示，增强模型的推理能力。
- �� 目标对齐与训练策略：采用多阶段训练，包括图对齐、知识对齐和生成微调，有效缓解信息融合中的偏差问题。
- �� 大规模数据集构建：结合arXiv和Mathlib，构建108K对科学-形式图对，丰富了学术知识图谱的表达能力。
- �� 未来定理生成：实现基于知识图谱的grounded生成，生成具有数学深度和逻辑严密性的未来定理，为自动化数学推理提供新范式。
方法详解
- �� 数据采集：从arXiv中提取数学论文，构建科学引用图，选择与目标论文相关的引用节点，构建多跳引用关系。
- �� 形式定理对齐：利用FrenzyMath和Lean Mathlib库，通过密集检索匹配非正式定理与正式定理，建立正式-非正式对应关系，扩展到多跳依赖图。
- �� 图编码：为科学引用图和形式依赖图设计专门的GNN编码器，节点类型不同，初始化方式不同，采用边类型特定的消息传递机制。
- �� 图融合：通过双向交叉注意机制，将两个图的结构化表示融合，生成统一的知识表示。
- �� 条件化生成：将融合后的图表示作为条件输入，结合预训练的数学语言模型（如LoRA微调的模型），实现未来定理的自然语言生成。
- �� 训练策略：分两个阶段，第一阶段优化图编码和对齐目标，第二阶段微调生成模型，加入图条件的生成损失和对齐损失，确保模型在结构和内容上的一致性。
实验设计
- �� 数据集：利用从arXiv和Mathlib中采集的108K科学-形式图对，构建未来论文测试集47K，确保时间上的前后关系，模拟未来预测场景。
- �� 评估指标：包括Tgt-Sim（目标相似度）、Neg-Sim（无关论文相似度）、Gap（差距指标）、H@10和H@100（检索排名），以及数学定理的精准匹配率和创新性指标。
- �� 基线模型：单一图源模型、文本微调模型、检索基线和API调用模型，比较不同信息源对生成效果的影响。
- �� 消融实验：逐步去除图编码器、融合机制和训练阶段，验证各个组件的贡献。
- �� 训练细节：采用两阶段训练策略，第一阶段优化图结构和对齐目标，第二阶段微调生成模型，使用LoRA技术提升效率。
结果分析
- �� COMPOSE在未来论文检索中实现Tgt-Sim 0.525，明显优于单一信息源模型（最高0.471），Gap达0.240，显示其生成内容更贴近真实未来论文。
- �� 在生成质量方面，LLM评判得分达3.36/5，特别在数学内容和深度方面表现优异，优于纯文本模型。
- �� 消融实验显示，去除任一图源或融合机制都导致性能显著下降，验证双图融合的必要性。
- �� 在不同解码器（DeepSeek-Math 7B和Mistral 7B）上均表现优越，证明模型架构的鲁棒性和迁移能力。
应用场景
- �� 立即应用：可用于数学研究文献的自动补充和未来研究方向预测，辅助科研人员快速定位潜在突破点。
- �� 长期愿景：未来可整合到智能科研助手平台，实现自动推理、知识发现和创新建议，推动科学研究的智能化和自动化发展。
局限与展望
- �� 依赖高质量的图结构和对齐信息，若数据偏差或缺失，可能影响生成效果。
- �� 目前主要面向数学领域，迁移到其他科学领域仍需大量适应和验证。
- �� 计算成本较高，尤其在大规模图和模型条件下，实际部署存在挑战。
通俗解读 非专业人士也能看懂
想象你在一个大型工厂里工作，工厂里有许多不同的机器，每台机器都在生产不同的零件。工厂的设计图和生产流程就像科学论文中的引用关系和定理结构。每当你要设计一台新机器（未来的定理），你需要参考之前的设计图（引用图）和逻辑关系（定理依赖图），确保新设计既符合已有的技术路线，又符合逻辑关系。这个工厂的设计师（模型）通过学习大量的设计图和流程，逐渐掌握了如何结合不同的设计元素，创造出新的机器。COMPOSE就像这个工厂的智能设计师，它能根据已有的设计图和逻辑关系，自动提出合理的新设计方案（未来定理），帮助工程师们更快地创新。它不仅理解每个零件的作用，还知道哪些零件可以组合在一起，形成更复杂、更强大的机器，从而推动整个工厂的技术进步。
简单解释 像给14岁少年讲一样
想象你在学校里学数学，老师经常让你猜测未来可能会出现什么新定理。以前，你只能靠自己猜测或者看别人的猜测，但这些猜测有时候不太靠谱。现在，有了COMPOSE这个聪明的助手，它可以帮你根据以前学过的定理和论文，预测未来可能的数学发现。它就像一个超级聪明的数学朋友，能结合你们老师讲的内容和数学书上的逻辑关系，帮你想出一些新颖又合理的定理。比如，它可以告诉你：“如果你研究这个问题，可能会发现一个新的定理，帮助你解决难题。”这样，你就能更快地找到研究方向，也能学到更多有趣的数学知识。它用的技术就像是把很多数学书和论文都放在一起，让它变得非常聪明，能帮你预测未来的数学世界会变成什么样子。
原文摘要
A plausible future mathematical claim must satisfy two constraints: it should follow the direction of prior work and respect the formal dependencies that constrain what can validly follow. Existing approaches typically model only one of these sources, producing claims that are either weakly grounded or insufficiently motivated. We introduce grounded future mathematical generation, where the goal is to generate a plausible future theorem-like claim for an anchor paper using two complementary sources of context: its scientific citation graph and aligned formal theorem dependency graph. To address this setting, we propose COMPOSE, a dual-graph framework that conditions a language model on both scientific citation context and formal theorem structure. To support this setting, we construct a dataset of 108K paired scientific-formal graph examples from arXiv and Mathlib, together with a benchmark of 47K future papers from 2024--2025. Experiments show that COMPOSE outperforms strong baselines on retrieval to real future papers and achieves the best overall performance under LLM-judge evaluation, producing more grounded and mathematically richer outputs. These results show that future mathematical generation benefits from combining scientific context with formal structure. Project page is available at https://david-busbib.github.io/COMPOSE-page/.
参考文献 (20)
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Kaiyu Yang, Aidan M. Swope, Alex Gu 等
GoAI: Enhancing AI Students'Learning Paths and Idea Generation via Graph of AI Ideas
Xian Gao, Zongyun Zhang, Ting Liu 等
ResearchAgent: Iterative Research Idea Generation over Scientific Literature with Large Language Models
Jinheon Baek, S. Jauhar, Silviu Cucerzan 等
ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization
Rafael Cabral, T. Do, Xuejun Yu 等
Enhancing Scientific Papers Summarization with Citation Graph
Chen An, Ming Zhong, Yiran Chen 等
LoRA: Low-Rank Adaptation of Large Language Models
J. Hu, Yelong Shen, Phillip Wallis 等
Representation Learning with Contrastive Predictive Coding
Aäron van den Oord, Yazhe Li, O. Vinyals
Improving Scientific Hypothesis Generation with Knowledge Grounded Large Language Models
Guangzhi Xiong, Eric Xie, Amir Hassan Shariatmadari 等
Advancing mathematics by guiding human intuition with AI
A. Davies, Petar Velickovic, L. Buesing 等
Autoformalization with Large Language Models
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li 等
Neural Message Passing for Quantum Chemistry
J. Gilmer, S. Schoenholz, Patrick F. Riley 等
The coq proof assistant reference manual
G. Huet, Christine Paulin-Mohring
GIANTS: Generative Insight Anticipation from Scientific Literature
Joy He-Yueya, Anikait Singh, Ge Gao 等
Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions
Lan Zhang, Marco Valentino, Andr'e Freitas
ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings
Prithwish Jana, Kaan Kale, Ahmet Ege Tanriverdi 等
DeepMath - Deep Sequence Models for Premise Selection
G. Irving, Christian Szegedy, Alexander A. Alemi 等
STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Kefan Dong, Tengyu Ma
Text Embeddings by Weakly-Supervised Contrastive Pre-training
Liang Wang, Nan Yang, Xiaolong Huang 等