Danus系统用事实图内存编排数学推理智能体

背景

近年来，基于大型语言模型（LLM）的数学推理智能体已开始涉足研究级问题，甚至在多个案例中为开放问题的解决做出了贡献。然而，有效扩展和协调这类智能体仍然面临挑战：难点在于协调并行的证明搜索，同时保持中间主张的组织性和可靠性。现有方法通常缺乏全局的内存管理机制，导致多个推理分支之间难以共享中间结果，且不易验证和追踪依赖关系。针对这一瓶颈，本文提出了一种名为 Danus 的编排系统，以共享的事实图（fact graph）作为核心内存管理机制，旨在实现研究级数学推理智能体的规模化协同工作。

核心内容

Danus 是一个面向研究级数学推理的编排系统，其核心创新在于围绕一个共享的**事实图（fact graph）**作为全局内存管理机制。系统包含以下组件：

• 主智能体（main agent）：负责规划与协调。它周期性地总结不断演化的证明状态，将工人智能体重定向到有希望的方向，并通过进度报告支持与人类数学家的交互。
• 多个工人智能体（worker agents）：并行执行证明搜索，各自在事实图基础上探索不同分支。
• 无状态验证器（stateless verifier）：在数学主张被纳入事实图之前，对它们进行检验。只有通过验证的事实才会被存储。

每个通过验证的事实都会连同其证明和逻辑依赖关系一起被保存，使得系统能够逐步构建长篇论证，同时保持共享证明状态的条理清晰。

论文通过六个研究级案例研究对 Danus 进行了评估，这些案例涵盖代数几何、奇点理论和组合学。案例表明，事实图内存机制使 Danus 能够构造出长篇幅、细节详尽的数学证明。实验结果暗示，基于事实图的编排为解决长期研究问题的数学推理智能体的规模化提供了一条有效路径。

Danus 已开源。

关键要点

• 核心机制：Danus 采用共享的事实图作为全局内存，每个事实存储其证明和逻辑依赖关系，支持增量式长篇证明构建。
• 系统架构：由主智能体（规划与协调）、多个工人智能体（并行证明搜索）和无状态验证器（准入控制）三部分组成。
• 验证流程：任何数学主张必须先经过无状态验证器检验，才能被加入到事实图中，确保全局证明状态的可信性。
• 人类协作：主智能体可通过进度报告与人类数学家交互，允许人类介入或引导搜索方向。
• 评估结果：在代数几何、奇点理论、组合学等六个研究级案例中，Danus 成功生成了长而详细的数学证明，验证了其有效性。
• 开源可用：Danus 已开放源代码，便于社区复现和进一步开发。

意义与影响

Danus 的提出标志着数学推理智能体从简单题目解答向研究级问题求解迈出了重要一步。通过将事实图作为全局内存，Danus 解决了大规模并行证明搜索中的两个关键问题：中间结果的可靠性和组织性。这种“主-从-验证”的编排模式不仅提升了证明构建的规模与深度，还保留了与人类数学家协同的可能性——主智能体可以主动汇报进展，人类则可以提供方向性建议。这为未来将 LLM 智能体作为数学研究辅助工具铺平了道路。事实上，论文暗示了事实图编排对于长期、开放研究问题的可扩展性，可能为自动定理证明、形式化验证以及数学发现等领域的系统设计提供新的参考范式。开源发布进一步降低了使用门槛，有望催生更多基于事实图内存的推理系统。