Cogentic：面向自动定理发现的多智能体编排框架

Cogentic：面向自动定理发现的多智能体编排框架

arXiv编号：arXiv:2609.40324v1 [cs.AI]

摘要
本文提出Cogentic，一套用于开放研究问题自动定理发现的多智能体执行框架。前沿大模型可以单次生成高质量数学思路，但对于开放研究问题，仅靠单次生成往往不足以完成证明：需要探索多条互相竞争的猜想、攻克微妙的技术障碍，并且在长视界流程中保留中间推导进展。
Cogentic通过迭代式「证明‑验证」循环解决上述挑战：编排器将一批独立证明智能体分配到不同证明方向；多个专用组件对输出开展对抗式验证；经过确认的中间结果会被提升进入持久化已验证账本，供后续迭代轮次复用。该框架目标是求解研究级数学与理论计算机科学问题。基于Gemini基座，Cogentic在线性学习、拍卖理论、机制设计五大开放问题上产出全新研究结果；每一项结果均由领域专家独立核验，配套专题论文完整阐述。全部结果以及后续新增验证成果公开在项目网站：https://sites.google.com/view/cogentic。

关键词
多智能体编排；自动定理发现；大语言模型推理；对抗式验证；推理算力调度

目录

1. 引言
2. Cogentic系统框架
   • 2.1 组件介绍
   • 2.2 一轮完整工作流
   • 2.3 方向分配与任务简报生成
   • 2.4 双重对抗验证机制
   • 2.5 跨轮次通信：尝试记录与已验证账本
   • 2.6 流程级自适应调整
   • 2.7 终止条件与输出文稿生成
3. 实验结果：五大开放问题的求解
   • 3.1 高效在线逆线性优化
   • 3.2 双边市场的Bulow‑Klemperer竞争复杂度
   • 3.3 多专家预测下的任意时刻遗憾界
   • 3.4 单可加买家场景下简单机制与最优收益
   • 3.5 自动竞价拍卖的无政府代价
4. 讨论
5. 参考文献
6. 附录A 问题原始Prompt

1 引言

本文介绍Cogentic，面向开放数学研究问题自动定理发现的多智能体执行框架。该系统的设计灵感来源于理论计算机科学与数学领域真实科研团队协作模式：编排器决定研究任务分配，多个证明智能体并行起草证明，验证智能体审阅草稿、查找漏洞。
系统具备较高推理效率：本论文报告的实验，大部分问题仅需要KaTeX parse error: Can't use function '\(' in math mode at position 1: \̲(̲O(100)\)次Gemini模型调用；难度最高问题约KaTeX parse error: Can't use function '\(' in math mode at position 1: \̲(̲O(1000)\)次调用。系统还有进一步降低调用量的优化空间，同时也可以横向扩展以攻克更难的问题。
Cogentic一个核心特点：仅输入问题描述，不需要专家提示，就可以自主运行直到产出论文形式的结果。
本研究聚焦作者团队熟悉的研究领域，产出人类可读自然语言证明，方便领域专家直接核验推理，并且生成配套背景介绍、新技术阐释文本。

现有相关工作分为几类：

1. 交互式定理证明器：Lean、Isabelle/HOL、Coq，可以提供机器可校验的形式化保证；大量工作使用大模型降低形式证明门槛。但Cogentic工作在自然语言层面，输出可供领域专家直接审阅的数学文本。
2. 数学对象搜索类系统：通过程序搜索、进化智能体寻找极值构造；该类方案依赖廉价可计算的评价函数，并非全部数学问题都可以转化为此类形式。
3. 测试时推理扩展方案：思维链、自一致性、多智能体辩论；Cogentic建立在证明‑验证迭代交互之上，验证器采用对抗式预设怀疑视角。
4. 其它科研级数学智能体框架：近期涌现多个面向数学研究的智能体 harness，本文不做全面横向对比。

本文主要贡献

1. 设计Cogentic多智能体编排框架，实现迭代式证明‑验证闭环，维护持久化已验证中间结果账本；
2. 无需人工数学干预，仅输入原始问题，在5个理论计算机科学开放研究问题得到新定理结果，全部经过领域专家独立核验；
3. 验证多智能体对抗式验证+可复用中间账本，能够在有限大模型调用预算下完成高难度开放数学研究。

2 Cogentic系统框架

整套系统由一组智能体协同求解同一个数学问题；全部智能体共享磁盘工作区，由**编排器（orchestrator）**做集中调度，决定运行哪些智能体、执行时机、分配任务。

2.1 组件介绍

1. 编排器Orchestrator：全局控制器；维护全局状态，将证明智能体插槽分配到不同研究方向；生成摘要器，为每一个证明智能体生成定制简报；评估验证器的共识输出；管理两份核心存储：尝试记录、已验证账本。编排器本身不执行数学推导。
2. 文献审阅智能体Literature reviewers：检索相关工作，获取定义、已有定理；运行中途遇到技术障碍时，可以再次发起定向文献检索。
3. 证明智能体Provers：读取分配的定制简报，并行独立生成候选证明草稿。
4. 验证智能体Verifiers：从互补角度对候选证明做对抗式批判。
5. 尝试记录Record：保存证明智能体全部尝试，以及验证器对应的批判意见。
6. 已验证账本Verified ledger：存储从证明草稿中提取、并且独立复验证通过的中间引理；是智能体之间传递进展的核心载体。
7. 流程顾问Advisor：审阅多轮全部日志，协助编排器调整后续轮次的任务分配、调整各智能体提示指令。顾问本身不能输出数学猜想、不能推荐技术路线。
8. 结果整合阶段Consolidation：比较器、形式写作者、论文验证器，最终输出完整可独立阅读的已核验手稿。

2.2 一轮完整工作流

每一轮执行完整流程：

1. 编排器做规划，分配多个证明智能体到不同研究方向；流程顾问调整全局指令；
2. 摘要器为每一个证明智能体生成专属任务简报Briefing；
3. 多个证明智能体并行起草候选证明；
4. 双重对抗验证：每个草稿独立验证，同时将本轮全部草稿横向对比联合验证；
5. 将本轮产出写入「尝试记录」、「已验证账本」；
6. 判断：如果存在草稿全部通过验证，进入整合输出；否则开启新一轮迭代。

系统流程图：
问题陈述 + 文献审阅 → 规划 → 简报生成 → 并行证明智能体 → 双重对抗验证 → 更新尝试记录 + 已验证账本；循环直到出现通过验证的草稿；最终执行结果整合，产出已验证完整手稿。

2.3 方向分配与任务简报生成

一轮开始编排器规划：确定启用多少证明智能体，每个智能体负责哪一条研究方向。方向可以是：证明某条界、寻找反例、修复已有有希望的证明草稿等。
随着迭代轮次增加，历史材料不断膨胀；不会直接把全部历史上下文喂给证明智能体。编排器生成摘要器Summarizer，读取全部历史尝试与验证反馈，筛选高价值上下文，生成该智能体专属简报，给出下一步可行建议。长文档仅传入文件路径，由证明智能体按需读取，避免上下文窗口爆炸。

2.4 双重对抗验证机制

每一份证明草稿执行两级验证：

1. 独立单草稿验证：验证器审阅单份草稿；预设对抗怀疑假设：每一步推导都是错的，每一条文献引用都可能错误，需要推导充分证明才予以采信。
2. 本轮全部草稿横向联合验证：同轮所有草稿放在一起对比，识别集体共有的思维盲区，对比不同证明的优劣。

一份草稿必须两级验证全部通过，才视为本轮合格输出。

2.5 跨轮次通信：尝试记录与已验证账本

每一轮结束产出两份持久化产物：

1. 尝试记录Record：按研究方向归类所有证明尝试，记录使用方法、失败对应的反驳理由；编排器与顾问读取记录，指导下一轮任务规划。
2. 已验证账本Verified ledger：提取证明草稿中被验证通过的中间引理，剥离原始草稿上下文，改写为自包含引理，再次独立验证；验证通过写入账本，后续所有证明智能体可以直接复用，无需重复证明。账本同时记录死胡同结论（例如被反例排除的界），避免后续重复踩坑。

关键点：即便某一份完整证明整体失败，其中部分中间引理如果核验成立，依旧会被提取进入账本复用。

2.6 流程级自适应调整

每一轮结束，流程Advisor顾问审阅本轮以及全部历史验证日志，识别反复出现的错误、论证的共性缺口、验证器的遗漏盲区。基于观测，调整证明智能体、验证智能体的提示指令。例如增加对高频错误的警告，对经常跳步的推导提升证明严谨性要求。

约束：Advisor仅做流程层面调优，禁止输出任何数学观点，不能猜想答案，不能评判方向是否有前景。

2.7 终止条件与输出文稿生成

当某候选证明全部验证通过，编排器可以选择继续探索其它潜在更优结果；穷尽有价值方向之后终止。
终止后执行整合流水线：

1. 比较器Comparator：挑选最优已验证证明；
2. 形式写作者Formal writer：扩充为完整学术手稿，补齐定理、引理、符号、背景知识，做到完全自包含；
3. 论文验证器Paper verifier：审计扩充后的文稿，确认扩充过程没有引入新错误。
   输出一份不需要了解系统运行过程，领域专家就可以直接阅读审核的完整文档。

3 实验结果：五大开放问题的求解

基于Gemini基座运行Cogentic，全部实验仅输入问题陈述，无人工数学干预；全部输出结果由领域专家独立核验，配套专题论文。汇总表如下：

3.1 高效在线逆线性优化

在线逆线性优化：学习者观察专家决策，在不知道专家优化目标w ∗ w^*w∗前提下模仿专家选择。历史工作：高效算法得到O ( d ln ⁡ T ) O(d\ln T)O(dlnT)；KaTeX parse error: Can't use function '\(' in math mode at position 1: \̲(̲O(d)\)界已有结果但是算法既不proper也不高效。
Cogentic产出定理：存在确定性、proper、任意时刻算法，累积短fallKaTeX parse error: Can't use function '\(' in math mode at position 5: R_T=\̲(̲O(d)\)，该界对任意视界T TT一致；每轮仅O ( d 2 ) O(d^2)O(d2)算术运算加一次线性优化。
证明改造变量度量框架，替换掉带来ln ⁡ T \ln TlnT项的log‑det势能，改用迹幂势能，消除对数因子。同时拓展得到抗损坏版本、秩自适应变体、凸极小化拓展结论。

3.2 双边市场的Bulow‑Klemperer竞争复杂度

经典Bulow‑Klemperer定理：单边拍卖增加1个竞拍者即可达到最优机制收益；双边市场此前结果需要每一侧至少增加20000个参与者。
Cogentic证明：当买家分布一阶随机占优于卖家，m ≥ n m\ge nm≥n，仅向规模更小的卖家侧增加2名交易者，STR机制即可达到原市场的一阶最优贸易增益；并且该结果是紧的，仅增加1名不存在满足条件的DSIC、个体理性、弱预算平衡机制。

3.3 多专家预测下的任意时刻遗憾界

专家建议预测：固定视界下最优遗憾界t ln ⁡ n / 2 \sqrt{t\ln n/2}tlnn/2​；历史任意时刻算法会引入2 \sqrt{2}2​的主阶开销，该开销是否不可避免长期开放。
Cogentic构造算法，证明：存在无需预知视界T TT的算法，满足
R t ≤ ( 1 + O ( ln ⁡ ln ⁡ n ln ⁡ n ) ) t ln ⁡ n 2 R_{t} \leq\left(1+O\left(\sqrt{\frac{\ln \ln n}{\ln n}}\right)\right) \sqrt{\frac{t \ln n}{2}}Rt​≤(1+O(lnnlnlnn​​))2tlnn​​
主阶常数渐近和固定视界完全对齐。证明思路：在几何网格维护多组乘权算法，通过受控唤醒与退役策略，保证同时运行实例数量与t tt无关。

3.4 单可加买家场景下简单机制与最优收益

单可加买家，物品价值独立；SRev单卖收益，BRev捆绑销售收益，OPT最优机制收益。历史最好界OPT ≤ 5.2 ⋅ max ⁡ ( SRev , BRev ) \text{OPT} \le 5.2\cdot \max(\text{SRev},\text{BRev})OPT≤5.2⋅max(SRev,BRev)，下界为2。
Cogentic改进得到：
3.52 ⋅ max ⁡ ( SRev , BRev ) ≥ OPT 3.52 \cdot \max(\text{SRev},\text{BRev}) \ge \text{OPT}3.52⋅max(SRev,BRev)≥OPT
证明改造对偶框架，将截断阈值改为max ⁡ ( SRev , BRev ) \max(\text{SRev},\text{BRev})max(SRev,BRev)，直接合并Core与Tail分析，通过极值分布对二阶矩做界约束。

3.5 自动竞价拍卖的无政府代价

自动竞价广告拍卖，无政府代价PoA衡量均衡相对最优社会福利的损失。2投标人历史上界1.8；n投标人紧上界长期开放。
Cogentic研究r‑比例首价拍卖pFPA_r，得到：

1. KaTeX parse error: Can't use function '\(' in math mode at position 1: \̲(̲n=2\)，取KaTeX parse error: Can't use function '\(' in math mode at position 1: \̲(̲r=1\)标准PFPA，PoA ≤ 1.5 \text{PoA}\le 1.5PoA≤1.5，该界是紧的，任何匿名机制都无法优于1.5；
2. 对通用n nn，取KaTeX parse error: Can't use function '\(' in math mode at position 1: \̲(̲r=2n\)，PoA ≤ 2 − 1 4 n + 1 \text{PoA} \le 2-\frac{1}{4n+1}PoA≤2−4n+11​，匹配已知下界2 − 4 n + 4 2-\frac{4}{n+4}2−n+44​。

重要背景：对于第二个结论，人类研究者事先并没有想到该机制；Cogentic独立提出该机制并且完成全部分析证明。

4 讨论

Cogentic输出自然语言证明，后续全部由领域专家人工核验。系统产出候选结果的速度可以远超人类阅读、核验的速度；随着算力提升这个差距会进一步拉大。
未来一个重要方向：将自然语言输出转译为Lean等形式化证明助手，得到机器可验证的正确性；但即便机器可以校验，人类对证明思路的理解、衍生出新研究方向依旧无法被完全替代。平衡AI产出吞吐量和人类的理解消化，是该领域的重要开放问题。

5 参考文献

完整参考文献查阅原始arXiv网页：https://arxiv.org/html/2609.40324v1

附录简要说明

• 附录A：五大开放问题给Cogentic使用的原始完整Prompt；包含问题描述、参考论文指引。