Danus基于事实图记忆的数学推理智能体协同调度系统论文原链接https://arxiv.org/html/2607.06447v2摘要基于大语言模型LLM的数学推理智能体已能够攻克研究级数学难题部分工作甚至解决公开数学猜想。但现有系统难以高效调度、并行协调多条证明搜索分支同时无法有序管理海量中间推导结论限制了长程数学证明的生成能力。本文提出Danus——一套以事实图Fact Graph为全局记忆核心的数学推理多智能体调度系统。Danus架构分为三大模块1主智能体负责全局规划、多worker调度与数学家交互2多并行工作智能体分头开展分治式证明搜索3无状态独立验证器所有数学命题入图前必须经过校验。每条通过验证的数学事实会连同完整证明、逻辑依赖关系存入事实图系统可基于图结构逐步拼接超长严谨数学论证。主智能体会定期汇总当前证明进度、重定向各worker探索方向并生成进度报告对接人类数学家。本文选取代数几何、奇点理论、组合数学六大前沿公开猜想作为完整案例验证Danus能力实验证明事实图全局记忆机制可支撑系统生成数千节点、深度超50的完整长证明。所有实验代码完全开源实验流程、环境配置、复现步骤完整开放。核心创新点提出事实图DAG全局记忆架构解决多智能体并行证明时信息冲突、冗余、依赖混乱问题支持事实级撤回修复主智能多worker独立验证器三权分离调度范式实现多分支并行探索突破单一线性证明搜索局限内置进度摘要、论文自动生成模块支持人机协同数学科研验证后事实图可直接转化规范学术论文在6个前沿未解决数学猜想完成全流程验证对比GPT-5.5-pro、Rethlas基线具备压倒性性能。1 引言1.1 LLM数学智能体发展现状LLM驱动智能体可完成文献检索、符号计算、迭代推理修正在合适调度框架加持下远超单纯提示词基线。现有成熟数学智能体Aletheia生成-验证-迭代修正闭环解决数论、代数几何若干Erdős公开问题Rethlas模仿数学家工作流内置反例、子目标拆解工具可独立交换代数、泛函分析猜想QED分治、证明、多层校验多智能体循环求解偏微分、几何公开问题ProofCouncil作者/评审/计算多智能体在FirstProof数据集完成6/10命题AI共数学家多专业智能体协同文献、草稿、迭代审稿辅助群论开放问题。上述系统大多采用生成-校验-修正单轮循环多智能体仅代表功能分工缺乏并行多证明分支协同能力。直接多开智能体并行搜索会出现中间结论混乱、错误信息扩散、上下文爆炸必须配套全局结构化记忆管理。1.2 本文Danus核心思路针对并行证明调度痛点设计以事实图DAG为唯一可信全局存储的调度系统架构分权主智能体全局统筹worker并行证明独立无状态验证器作为唯一正确性裁判事实图存储每条验证完成的数学命题与逻辑依赖支持级联撤回错误事实人机协同主智能体定期输出进度报告数学家可下发高层指导也可调用GPT-5.5-pro获取宏观策略后置论文生成完整事实图自动转化标准数学论文并二次校验全文逻辑。对比前代Rethlas单线程线性证明Danus支持多路并行探索可同时尝试构造、反证多条路线大幅提升复杂长证明的可解性。本文全部实验包含完整人机交互记录清晰区分AI推导与数学家输入。1.3 论文组织结构第2章系统架构第3章六大前沿数学案例完整实验第4章系统优劣与局限讨论第5章总结附录含完整算法、实验超参、案例详细推导。2 方法体系Danus系统完整架构2.1 整体工作流图1架构数学家输入自然语言数学问题主智能体解读问题按需调用GPT-5.5-pro获取高层证明策略分配多条探索任务给并行worker每个worker基于事实图检索已有结论独立推导引理、构造例子/反例生成完整命题证明提交验证器无状态验证器逐条校验通过则存入事实图记录逻辑依赖边不通过则返回修改提示给worker主智能体定期读取事实图、worker日志生成全局进度总结重新分配算力、放弃无效探索分支当目标定理作为已验证事实出现在图中终止搜索将事实图转化为完整数学论文供人类专家审阅。核心改进Rethlas仅单条推理路径Danus多路并行事实图隔离各分支推导互不干扰支持大规模长证明构建。2.2 核心组件事实图Fact Graph2.2.1 结构定义事实图为有向无环图(DAG)节点Fact经过验证的数学命题配套完整证明有向边逻辑依赖关系A→B代表证明B需要引用事实A全局唯一可信数据源所有worker仅读取已验证节点不会被未校验草稿干扰。2.2 对比单文档蓝图Rethlas缺陷Rethlas采用单Markdown文档存储全部推导多worker同时编辑会产生冲突、上下文超长推理失效事实图两大优势上下文轻量化worker每次仅检索当前推导所需少量事实无需加载全部证明LLM推理稳定性大幅提升原生并行多条独立探索分支生成的事实可独立入库互不覆盖、干扰。2.2.3 事实级撤回机制若后续校验/人类专家发现某事实存在漏洞系统自动删除该节点递归删除所有直接/间接依赖它的下游事实彻底清除错误推导链。本文全部实验中撤回操作极少验证器准确率极高。2.3 双层辅助记忆系统事实图仅存放验证通过结论未完成探索内容存入双层共享记忆避免worker重复试错本地私有记忆每个worker独立日志记录自身探索路径用于事后复盘全局共享记忆所有智能体可读可写记录证明计划、死胡同、构造样例、GPT-5.5-pro全部咨询记录。全局记忆让主智能体掌握全部分支进展精准判断哪些探索路径应当终止。2.4 主智能体Main Agent2.4.1 核心职责全局规划调度不参与具体数学推导推导完全交给worker隔离未校验内容污染全局可信事实解析数学家输入问题生成初始多分支证明策略定期汇总事实图全部worker日志生成全局进度摘要动态分配算力放弃无进展分支、开辟新证明方向承接人类实时交互接收高层指导、输出进度报告证明完成后调用论文生成模块格式化完整稿件。2.4.2 底层模型选型主智能体需要读取数万节点事实图、海量日志选用Claude Code Claude Opus 4.8对比Codex、OpenClaw对长结构化文本读取能力最优。仅在需要高阶数学策略时低频调用GPT-5.5-pro最多每小时一次控制算力成本。2.4.3 策略循环流程初始化读取问题咨询GPT-5.5-pro分配初始任务给worker集群定时轮询1~2小时一轮读取全局记忆、事实图、各worker日志生成进度总结基于总结重新调度worker探索方向检测目标定理入库则触发论文生成全程支持人类随时介入调整策略不中断并行worker运行。2.5 Worker工作智能体 无状态验证器2.5.1 Worker集群基于改进Rethlas生成模块每台worker单次聚焦单个引理/反例构造反复提交验证直至通过内置Matlas数学文献检索引擎精准调取已有定理。实验中同时运行3~9个worker分为高、极高两种推理算力档位兼顾浅层快速结论与深度复杂推导。2.5.2 无状态验证器服务独立后台服务无历史缓存每次提交均新建校验实例可完整追溯事实图依赖链逐层检查证明步骤。实验中几乎无假阳性仅两类极小漏洞部分证明步骤省略过多引用外部文献本身存在错误两类问题均可在终稿人工复审中快速检出。2.5.3 Worker-验证器完整循环图3worker基于事实图检索所需前置事实推导新命题与完整证明提交至验证器标注全部依赖事实ID验证器追溯依赖、逐行校验通过写入事实图生成新DAG节点拒绝返回详细修改提示worker迭代重推。2.6 智能体工具与MCP交互协议图4全部智能体通过模型上下文协议MCP读写事实图、全局记忆、Matlas文献检索工具Worker工具子目标分解、正反例构造、直接证明、数学文献检索验证器工具分步校验、引用核查、验证报告生成主智能体工具全局摘要、论文撰写、策略咨询、任务启停CLI配套命令行接口支持批量启动、监控、终止worker集群。2.7 进度摘要与论文自动生成2.7.1 运行中进度摘要面向数学家的实时汇报工具严格约束摘要乐观化未完全闭环条件结论不得标注“已证明”停滞分支必须区分“方法无效”/“仅缺少中间引理”为主智能调度提供依据摘要不含系统内部日志仅输出纯数学进展。2.7.2 证明完成论文生成事实图是离散节点集合线性论文会产生步骤压缩、逻辑拼接缝隙因此采用二次校验流程将DAG事实重排为连贯学术文稿完整稿件重新送入验证器全局校验长证明自动拆分独立章节逐段验证拼接产生的推导缺口自动回填原始完整事实证明。3 实验六大研究级数学案例完整实验流程3. 实验统一基线设置对照基线GPT-5.5-pro网页端、原始Rethlas单线程系统两类基线均无法完成任意一例完整证明实验模式人机协同区分通用基础输入与专项数学指导输入通用输入问题描述、进度查询、最终稿件格式调整专项输入证明思路提示、参考文献推荐、修正文献错误评测指标事实图节点数量、最大依赖深度、并行worker数量、总运行时长、人类数学干预次数、最终定理证明有效性实验环境统一4M推理步数算力池Matlas文献检索库vLLM LoRA动态推理加速。3.1 案例1叶状流最优弯折断裂定理问题背景经典Mori弯折断裂定理最优常数为n1叶状流版本已知非最优上界2n、2r最优常数长期未解决。本文证明最优常数等于叶状流秩r1。Danus实验流程人类输入问题两篇核心参考文献Danus自动识别两篇文献记号不兼容替换更适配Kebekus体系文献5个worker并行推导生成63条验证事实、239条失败探索路径初稿生成后人类建议使用Campana代数性判据简化证明系统自动重写校验。人类专项输入两篇初始文献、简化证明提示实验结论系统独立完成跨领域技巧迁移自主筛选更适配的数学参考文献。3.2 案例2 三维叶状流Shokurov全局指标猜想问题背景二维叶状版本已证明三维长期公开普通代数簇四维以上仍未解决。Danus实验流程无任何思路提示自动按叶秩、代数秩拆分为5大类自主使用李理论解决3类高难度情形卡在代数可积两类人类提示叶状极小模型程序拓展至带系数对数典范三元组广义结论7worker并行784条验证事实。人类专项输入极小模型程序思路、广义结论拓展提示实验结论系统自主完成问题分类挖掘人类未预见证明路线少量提示即可补齐剩余情形。3.3 案例4 有理奇点族整体Cartier指数有界性问题背景Han-Jiang证明klt奇点族指数有界有理奇点是否满足为公开问题。Danus实验流程初始任务为寻找反例7worker并行正反双向探索自主将代数几何问题约化至交换代数、实代数几何使用Hadamard不等式自主拆分曲面/高维情形卡在三维场景误读文献维度条件人类修正文献阅读错误系统完整补全证明初稿压缩推导产生漏洞验证器自动驳回、自主修正。人类专项输入修正文献维度笔误实验结论可跨多数学分支串联证明链条文稿压缩错误可全自动修复。3.4 案例4 套娃数阶乘渐近猜想问题背景宇宙几何Cosmohedron对应的Matryoshka数列渐近增长猜想OEIS收录但无严格证明。Danus实验流程全程零人类数学指导5worker运行90分钟生成100条事实自动推导严格上下界给出高精度常数区间直接输出完整论文。人类专项输入无任何数学提示实验结论完全端到端自主完成猜想证明与成文覆盖数学物理交叉领域。3.5 案例5 对数向量场加权齐次奇点判定问题背景Saito给出代数判定条件da Silva提出两类几何等价猜想无证明。Danus实验流程自主生成完整证明路线与人类独立证明完全不同初稿引用文献定义错误系统级联删除依赖该文献全部事实重新检索正确资料重构证明7worker分两波运行687条验证事实23条因文献错误撤回。人类专项输入指出文献定义漏洞实验结论内置事实级撤回机制可自动修复文献引用带来的证明错误。3.6 案例6 拟阵美妙紧化切类构造最大规模实验问题背景拟阵美妙紧化切丛组合K环构造公开问题此前Rethlas三次尝试全部失败。Danus实验流程同时对比GPT-5.5-pro、Rethlas、Danus三套系统前两者无有效推导7worker并行运行5天事实图总计3157个节点最长依赖链深度54先证明有理版本人类指出目标为整数K环系统继续拓展完整整数构造全文压缩拼接产生漏洞分章节逐轮验证修正。人类专项输入指出目标为整数而非有理类实验结论事实图支撑超50层深度长程推理并行多路探索避免单一线性推理概念混淆是本文核心优势。4 讨论系统优势与局限性4.1 与GPT-5.5、Rethlas基线对比模型分工匹配能力Claude Code擅长海量日志/图读取作为主智能体GPT-5系列负责worker证明与校验GPT-5.5-pro仅低频高阶策略咨询系统组合增益显著单独调用大模型无法生成严谨长证明调度事实图架构大幅释放LLM数学潜力对比前代Rethlas并行事实图彻底解决单文档冲突超大深度证明仅Danus可完成。4.2 论文流畅度与严谨度平衡直接输出事实列表完全严谨但可读性极差线性文稿易在步骤拼接处产生逻辑缝隙。Danus采用“先生成文稿全文重校验”方案兼顾可读性与数学严谨残留瑕疵仅为记号、引用格式微调。4.3 独立验证器的核心价值自校验模型极易产生幻觉分离无状态独立验证器仅保留已验证事实入图长推理链误差不会累积是整个系统可信基础。验证器前置过滤大量错误推导大幅降低人类复审工作量。4.4 横向/纵向双维度可扩展性宽度扩展增加worker并行数量同时多条证明路线同步探索拓宽搜索空间深度扩展事实图存储已验证引理无需重复推导支撑数十层超长证明扩展边界系统仅能基于已有数学思路组合推导不存在完全自主原创突破性数学思想这类场景必须依赖人类数学家输入核心方向。4.5 完整优缺点汇总优势事实图DAG全局记忆支持并行多智能体无冲突协同错误事实级联撤回三权分离架构主调度/并行证明/独立校验各司其职避免未验证内容污染全局无需大量人类干预部分猜想零数学输入完整自证自动拆解多分类情形自主跨分支串联证明技巧内置文稿生成全文校验推导压缩漏洞可自主修复开源完整代码全部实验流程、环境可复现。局限无法自主产出颠覆性全新数学思想高难度开放问题依赖人类提示自动生成论文的记号、参考文献格式需人工微调检索文献仅追求逻辑可用不会主动选择最简证明参考文献依赖外部文献正确性文献自带错误需人类识别后系统重构证明。5 结论本文提出Danus多智能体数学推理调度系统以事实图DAG作为全局结构化记忆划分主调度智能体、并行证明worker、无状态验证器三大独立模块实现多分支并行证明搜索。事实图存储每条经验证命题与逻辑依赖支持长数学论证增量式构建并可级联撤回错误推导。在代数几何、奇点理论、组合数学六大前沿公开猜想完成完整人机协同实验系统可生成数千节点、深度超50层严谨长证明。实验表明Danus可大幅降低人类数学家推导工作量仅需少量高层指导即可完成复杂证明。未来可进一步提升系统原创数学思路挖掘能力拓展纯形式化证明对接模块。附录完整实验、算法、工程细节附录A Danus完整运行伪代码# Danus完整三阶段运行流程 1. 初始化加载Matlas文献库初始化空事实图、空全局记忆启动N个worker、验证服务、主智能体 2. 接收人类输入数学目标命题T写入全局记忆 3. 主智能体首轮规划 读取问题按需调用GPT-5.5-pro获取高层证明策略 为每个worker分配独立探索分支构造/反证/子引理 4. 循环迭代证明阶段 for 固定时长周期: 1. 全部worker并行执行推导 读取事实图检索依赖事实 生成命题完整证明提交验证器 验证通过写入事实图更新依赖边 验证驳回接收提示迭代重写 2. 主智能读取事实图、全局记忆、所有worker本地日志 3. 生成全局进度摘要重新分配worker探索任务 4. 判断目标命题T是否已在事实图 if 存在跳出循环进入论文生成阶段 5. 论文生成阶段 主智能读取完整事实图线性重组为数学论文初稿 整篇文稿送入验证器全局校验 存在拼接漏洞则迭代重写修正 6. 输出完整论文导出事实图全部节点与依赖记录用于实验复盘附录B 实验环境与超参配置基座模型WorkerVerifier使用GPT-5.5系列主智能体Claude Opus 4.8咨询GPT-5.5-proworker配置每任务3~9个并行分高/x高两档推理算力MCP交互事实图增删、检索、文献查询标准化接口事实图存储持久化JSON图结构支持回溯、撤回操作算力加速vLLM动态LoRA多并发推理。附录C 六大案例完整实验记录每个案例配套运行时长、worker数量、事实图总节点、支撑定理节点数、最大依赖深度、人类全部输入原文、失败探索路径统计。附录D 系统工程开销评测并行worker推理延迟、单事实验证耗时事实图读写吞吐量大规模图3000节点摘要生成耗时开源代码部署教程、环境依赖清单。附录E 消融实验消融事实图替换传统单文档并行完全失效性能暴跌消融独立验证器大量错误事实入库长证明完全不可信消融并行worker单线程Rethlas模式复杂猜想无法完成消融主智能调度worker探索路径高度重复效率大幅下降。资源下载链接汇总论文HTML原文https://arxiv.org/html/2607.06447v2论文PDFhttps://arxiv.org/pdf/2607.06447v2Danus完整开源代码仓库https://github.com/frenzymath/Danus实验完整案例数据、事实图日志仓库内dataset文件夹部署教程、环境配置脚本仓库readme.md
