Danus：基于事实图谱记忆的数学推理智能体编排系统

# Danus：使用事实图记忆编排数学推理代理  
来源：https://arxiv.org/html/2607.06447  

1北京大学数学科学学院  
2北京大学北京国际数学研究中心  
3京都大学数理解析研究所  
4天津大学数学学院  
5中关村学院  
6斯坦福大学数学系  
7西湖大学西湖高等研究院  
8同济大学数学科学学院、智能计算与应用教育部重点实验室  
9北京大学北京国际数学研究中心与新基石科学实验室  
10北京大学机器学习研究中心  
11大湾区大学大湾区高等研究院智能计算中心  

\contribution\[\*\] 共同第一作者  
\contribution\[¶\] 通讯作者   Guoxiong Gao  

Zeming Sun  Bin Wu  Shurui Liu  Jiedong Jiang  Haocheng Ju  Leheng Chen  Ronnie Cheng  Xiping Zhang  Bin Dong [[email protected]](https://arxiv.org/html/2607.06447v1/mailto:[email protected]) (2026年7月7日)  

###### 摘要  

近年来，基于大语言模型（LLM）的数学推理代理已开始处理研究级别的问题，并在多个案例中为开放问题的解决做出了贡献。然而，有效扩展和编排此类代理仍然具有挑战性，这主要是由于难以协调并行的证明搜索，同时保持中间声明的组织和可靠性。在本文中，我们提出Danus，一个以共享事实图（fact graph）作为全局内存管理机制的研究级数学推理编排系统。Danus由一个负责规划和协调的主代理、多个并行执行证明搜索的工作代理以及一个无状态验证器组成，该验证器在提议的数学声明被纳入事实图之前对其进行检验。每个经过验证的事实都与其证明和逻辑依赖关系一起存储，这使得系统能够逐步构建较长的论证，同时保持共享证明状态的有序性。主代理定期总结不断演化的证明状态，将工作代理重新引导至有前景的方向，并通过进度报告支持与人类数学家的交互。我们通过六个研究级别的案例（涵盖代数几何、奇点理论和组合学）评估Danus，展示了事实图记忆机制如何使Danus构建长而详细的数学证明。我们的结果表明，基于事实图的编排为实现长期研究问题的数学推理代理的扩展提供了一条有效途径。Danus是开源的。  

## 1 引言  

大语言模型（LLMs）越来越多地被部署为智能系统的推理核心，这些系统能够检索知识、调用工具、执行代码、与外部环境交互，并通过反馈修订其输出。在这些系统中，性能不仅取决于基础模型，还取决于控制信息、工具、状态和反馈如何暴露给模型的框架（harness）。通过适当的框架工程，基于LLM的代理在需要外部信息、迭代修正或长期执行的任务上可以超越非交互式的提示基线[27](https://arxiv.org/html/2607.06447#bib.bib27), [48](https://arxiv.org/html/2607.06447#bib.bib48)。  

已有多个代理被提出用于研究级数学推理。Aletheia代理[16](https://arxiv.org/html/2607.06447#bib.bib16)基于Gemini Deep Think的高级版本，由生成器、验证器和修订器组成，并在这三个组件之间迭代。它已自主或半自主地解决了几个Erdős问题，并已应用于代数几何[41](https://arxiv.org/html/2607.06447#bib.bib41)、组合学[26](https://arxiv.org/html/2607.06447#bib.bib26)和表示论[15](https://arxiv.org/html/2607.06447#bib.bib15)中的研究级问题。Rethlas代理[21](https://arxiv.org/html/2607.06447#bib.bib21)旨在模拟人类数学家的工作流程。它配备了为数学研究量身定制的技能和工具，并维护一个工作记忆，用于存储推理过程中产生的中间产物，例如构造的示例、反例和子目标分解计划。Rethlas已自主解决了交换代数[18](https://arxiv.org/html/2607.06447#bib.bib18)、泛函分析[13](https://arxiv.org/html/2607.06447#bib.bib13)和概率论[28](https://arxiv.org/html/2607.06447#bib.bib28)中的几个开放问题，并协助解决了代数几何[40](https://arxiv.org/html/2607.06447#bib.bib40)中的数学研究问题。QED代理[5](https://arxiv.org/html/2607.06447#bib.bib5)由分解器、证明器、结构验证器、详细验证器和调节器组成，并在循环中编排这些特定用途的代理。它已解决了代数几何、偏微分方程、概率论和反问题中的几个研究级问题。ProofCouncil系统[44](https://arxiv.org/html/2607.06447#bib.bib44)由作者代理、咨询LLM委员会、评论代理和计算代理组成，并在这些组件之间迭代。它在FirstProof第二批次中正确解决了10个问题中的6个（最多仅需少量修订）[1](https://arxiv.org/html/2607.06447#bib.bib1)。AI co-mathematician [49](https://arxiv.org/html/2607.06447#bib.bib49)是一个智能化的AI工作区，协调多个专门化的代理，以分解问题、探索想法、检索文献、运行计算、草拟非正式证明，并迭代审查和修订其输出。它已帮助人类数学家以交互方式解决了群论中的开放问题。  

上述大多数代理都显式或隐式地包含了生成-验证-修订循环，而现有“多代理”数学推理系统中的“多”通常指具有不同专业角色的代理。相比之下，很少有系统性的研究探讨如何通过增加直接参与证明生成的代理数量来扩展基于生成-验证-修订循环的数学推理系统。扩展此类代理并非简单地孵化多个代理同时处理一个问题而不加修改。它需要谨慎的内存管理和协调。如果多个代理的共享内存处理不当，可能会混淆代理，传播无关或错误的中间产物，并最终损害性能。  

为了有效扩展和编排数学推理代理，我们提出Danus，这是一种以共享事实图（fact graph）作为全局内存管理机制的编排系统。在Danus中，主代理负责规划和协调，而多个工作代理执行证明生成。共享的事实图使中间的非正式验证事实保持有序，从而使系统能够构建漫长而精细的证明。Danus与人类数学家之间的交互也得到了精心设计。主代理定期将当前证明状态总结成报告，允许人类数学家检查证明进展，并在必要时通过主代理提供高层指导。同样的报告也可由主代理用于咨询高级系统（如GPT-5.5-pro）以获取额外的数学指导。此外，Danus包含一个写作系统，一旦目标陈述被证明，它就会将完整的证明转化为论文风格的文章，使论证对人工读者更易理解。  

我们通过代数几何、奇点理论和组合学中的几个具有挑战性的研究级问题展示了Danus的有效性，并讨论了事实图记忆机制在产生长、详细且正确的证明中的作用。我们还明确报告了每个问题中提供的人工输入，以及在这些例子中数学家如何与Danus协作。  

本文的其余部分组织如下。第2节（https://arxiv.org/html/2607.06447#S2）介绍Danus系统的设计；第3节（https://arxiv.org/html/2607.06447#S3）介绍六个案例研究；第4节（https://arxiv.org/html/2607.06447#S4）讨论其优势与局限性；第5节（https://arxiv.org/html/2607.06447#S5）总结全文。  

## 2 方法  

Danus是一个面向研究级数学的自动化系统，建立在先前系统Rethlas[21](https://arxiv.org/html/2607.06447#bib.bib21)的工作-验证核心之上。它将一群证明搜索工作代理和一个无状态验证器与一个共享内存结合起来，全部由主代理协调。该设计遵循严格的分权原则：主代理执行全局规划和协调，工作代理执行详细的证明搜索，验证器是正确性的唯一权威，而单个事实图包含所有经过验证的结果，是系统唯一的真理来源（图1（https://arxiv.org/html/2607.06447#S2.F1））。本节的其余部分逐一介绍这些组件：第2.1节（https://arxiv.org/html/2607.06447#S2.SS1）描述工作流程；第2.2节（https://arxiv.org/html/2607.06447#S2.SS2）和第2.3节（https://arxiv.org/html/2607.06447#S2.SS3）介绍事实图及其之外的记忆；第2.4节（https://arxiv.org/html/2607.06447#S2.SS4）和第2.5节（https://arxiv.org/html/2607.06447#S2.SS5）介绍主代理、工作代理和验证器；第2.6节（https://arxiv.org/html/2607.06447#S2.SS6）介绍每种代理的技能和工具；第2.7节（https://arxiv.org/html/2607.06447#S2.SS7）介绍总结和论文写作。  

参见说明图1：Danus的整体架构。  

### 2.1 工作流程概述  

这些部分协同工作，从初始陈述到最终论文，处理单一问题。数学家以自然语言向主代理提出问题。主代理制定初始计划，必要时咨询GPT-5.5-pro以获得高层数学策略，并将研究方向分配给工作代理。工作代理是Rethlas生成代理，它们并行运行，从多个方向探索问题，包括建设性和反驳性路径。每个工作代理反复提出一个可验证的陈述及其支撑证明，并提交给验证器；证明通过验证的陈述将作为一个“事实”被存储。这些事实形成一个有向无环图（DAG），称为事实图，其边记录逻辑依赖关系。在工作代理进行过程中，主代理定期读取它们的进度和事实图，总结当前状态，咨询GPT-5.5-pro，并重新分配工作代理。迭代不会在预设轮数后停止；只有当主代理确认目标陈述（或其反驳）已作为已验证事实出现在事实图中时，迭代才会停止。主代理随后可以将事实图转化为论文，供人类专家检查。  

这种并行探索是与Rethlas的主要区别。Rethlas一次只追求一个推理路线，而Danus同时运行多个工作代理，每个代理探索问题的不同方面，例如要证明的不同引理、要构造的反例或要研究的简单示例。这拓宽了探索范围，并使长而多步骤的论证变得可行。这也带来了事实图旨在解决的问题：让许多工作代理为一个证明做出贡献，同时不相互干扰。  

### 2.2 事实图  

参见说明图2：第3.6节（https://arxiv.org/html/2607.06447#S3.SS6）拟阵切类案例研究背后的事实图：3,157个已验证事实，8,616条依赖边；节点随依赖深度（最多54层）变暗和变大。簇代表不同的攻击路线：底部，最终证明从未引用的条件铺垫；左侧，Chern数界的独立再推导；右上部，结果的积分提升，其最终路径进入证明。  

**结构**。事实图是整个系统唯一的真理来源，也是其核心设计要素。它是一个有向无环图（DAG），节点是事实，边记录逻辑依赖关系。事实是一个数学陈述及其经过验证器检查的证明；从一个事实指向另一个事实的边表示第二个事实的证明使用了第一个事实。工作代理可以借鉴已存在于图中的事实：原则上它可以访问整个图，实践中通过搜索图检索相关事实。当工作代理提交一个新的陈述和证明时，它记录证明所依赖的事实标识符，这些标识符将成为新事实的入边。每个通过验证的陈述都会被添加到图中，因此图不断增长，直到包含目标定理（图2（https://arxiv.org/html/2607.06447#S2.F2））。  

**为什么是图而不是单个蓝图**。这种设计使多个工作代理能够协作。在Rethlas中，整个结果由一个单一的Markdown蓝图承载，该蓝图包含所有支持性引理、定义和最终定理；工作代理反复编辑这个蓝图，并要求验证器检查并提出修订建议。与单个蓝图相比，事实图有两个优点。首先，它使每个工作代理的上下文保持小而集中。这种上下文管理很重要，因为语言模型代理在仅包含相关材料的短上下文中推理最可靠；不相关的内容既消耗其容量又干扰其推理。单个蓝图迫使每个工作代理携带整个累积证明，而事实图允许每个工作代理只根据需要的事实来论证当前声明，一次只提交一个事实，因此即使证明增长到很多页，工作上下文也能保持较小。其次，它支持并行工作：单个文件很难让多个工作代理同时编辑或用于不同的攻击路线，而事实图允许它们的贡献累积到一个共享结构中。  

**撤销**。事实图也支持撤销：如果一个事实后来被发现是错误的，那么它以及直接或间接依赖于它的所有事实都将被移除。这发生在以下两种情况之一：被引用的参考文献中存在错误（通常由代理在最终审查中发现，或由人类专家指出），或者更罕见的是存在概念混淆或有缺陷的证明。在我们的运行中，撤销很少需要，这一点在我们讨论验证的可靠性时会再次提及。  

### 2.3 事实图之外的记忆  

已经过验证的内容存在于事实图中；其他值得保留的内容则存在于记忆中。记忆不属于真理部分；它是共享上下文，帮助工作代理避免重复彼此的失败尝试，并有两个层级。每个工作代理维护一个私有的本地记忆，即自身活动的运行日志，主要用于后续分析推理路线的发展过程。在其之上是一个全局记忆，所有工作代理和主代理都可以读写。全局记忆记录搜索的中间产物，例如计划、有前景的方向、死胡同以及构建的示例和反例。它还记录每次GPT-5.5-pro咨询的提示和回复。这两个层级一起，使每个工作代理避免重复自身的本地探索，并让主代理看到每个工作代理在搜索分支上发生了什么。