摘要
最近，基于大型语言模型（LLM）的数学推理代理开始处理研究级问题，并在一些案例中为解决开放性问题做出了贡献。然而，如何有效地扩展和协调这些代理仍然是一项挑战，主要因为在保持中间声明有序和可靠的同时，协调并行证明搜索的难度较大。
在本文中，我们提出了 Danus，一个针对研究级数学推理的协调系统，中心是一个共享的事实图作为全局记忆管理机制。Danus 由一个主要代理和多个工作代理组成，主要代理负责规划和协调，工作代理则并行进行证明搜索，同时还有一个无状态的验证器在提议的数学声明被纳入事实图之前进行检查。
每个经过验证的事实都与其证明和逻辑依赖关系一起存储，使系统能够在保持共享证明状态有序的同时，逐步构建长的论证。主要代理会定期总结演变中的证明状态，重新引导工作代理朝有前景的方向发展，并通过进度报告支持与人类数学家的互动。我们通过六个在代数几何、奇点理论和组合学中的研究案例对 Danus 进行了评估，展示了事实图记忆机制如何使 Danus 能够构建长而详细的数学证明。我们的结果表明，基于事实图的协调为扩展数学推理代理以应对长远研究问题提供了一条有效的途径。Danus 的开源地址为 GitHub。
博主点评： Danus 系统通过共享的事实图显著提高了数学推理的效率和可靠性，展示了如何通过分层代理机制有效管理复杂的数学推理过程。这一方法为未来的数学研究提供了新的视角，尤其是在处理开放性问题时的潜力值得关注。