Cogentic: Multi-Agent Orchestration for Automated Proof Discovery
Yang Cai, Vineet Gupta, Yanchen Jiang, Christopher Liaw, Aranyak Mehta, Grigoris Velegkas, Di Wang
cs.AI, cs.GT
2026-10-01
Google 多智能体框架 Cogentic 让 Gemini 自主跑证明,解出在线学习与拍卖理论五个开放问题,多数仅用数百次模型调用,全部经专家核验。
前沿 LLM 一次调用就能给出不错的数学点子,开放研究问题是另一回事:要同时押注多个互相竞争的猜想,要翻越隐蔽的技术障碍,还要把长周期工作里的中间进展留住。单次生成这三件事都做不到,多采样几次也只是同一深度上的重复。
已有自动化路线各有前提。Lean 这类交互式定理证明器给出机器可查的保证,代价是先把问题形式化;FunSearch、AlphaEvolve 一类程序搜索在极值组合学上找到过新构造,前提是存在便宜、可机器计算的打分器。Cogentic 对准没有打分器的场景:STOC、FOCS 级别的开放理论问题,产出自然语言证明,交领域专家核验。
系统按研究组分工:orchestrator 决定做什么,prover 并行写草稿,verifier 挑毛病。一轮流程是规划方向、逐人 briefing、并行起草、双重验证,所得写入账本,下一轮接着用,循环到某份草稿通过全部验证为止。
终止时 comparator 选出最强证明,formal writer 扩写成完整论文,再做一轮对照审计,确认阐述过程没引入新错误。多数问题整趟只花 O(100) 次 Gemini 调用,最难的一个 O(1000)。
五个开放问题全部解出,每个都经领域专家独立核验,并以伴随论文形式完整发表。
| 问题 | 此前最好 | Cogentic 结果 |
| 在线逆线性优化 regret | O(d ln T) 且高效;O(d) 只有非 proper、需 T^Θ(d) 次测试的规则 | 首个高效且 proper 的 O(d) 界,每轮 O(d²) 运算,距最优 √d 还差 O(√d) 因子 |
| 双边市场 competition complexity | 双侧招募,每侧至少 20000 人 | 小侧加 2 人即够;加 1 人对任何 DSIC、IR、弱预算平衡机制都不够 |
| n 专家 anytime regret | √(t ln n),比固定 horizon 差 2 倍 | (1+O(√(ln ln n/ln n)))·√(t ln n/2),领头常数零代价 |
| 单加性买家简单机制 | 5.2·max(SRev,BRev) ≥ OPT | 3.52·max(SRev,BRev) ≥ OPT |
| autobidding 拍卖 PoA | 2 人 1.8;n 人紧机制开放 | 2 人 1.5 且为紧界;n 人 2−1/(4n+1) |
两处细节信息量最大。2 人 PoA 一题,作者原本就猜想比例第一价格拍卖能到 1.5,只是没有证明,Cogentic 把上界和下界都补齐;n 人那一半作者从未研究过、没给任何提示,机制和分析由系统独立提出。逆线性优化的伴随论文发表后,Sakaue 又证出紧的 O(√d) 界,但算法非高效,高效 O(√d) 仍是开放问题。
这五个结果是能过同行评议的数学贡献,不是玩具 benchmark。对从业者更有用的是配方本身:ledger 加尝试记录解决了长程任务的进展持久化,双通道对抗验证把输出可信度压到人类可复核的粒度,过程与内容分离避免调度层污染探索方向。这套骨架不绑定数学,换成任何有可验证中间产物的长程任务,原理上都成立。
预算也低:百次量级的调用解 STOC/FOCS 级问题,按当前 test-time compute 的标准相当省。
作者自认的:问题全选在自己的研究领域内,因为只有这样才能人工核验自然语言证明;部分伴随论文的合作者原本就在做相应问题;人类补写了文献定位与阐述,有些论证被推得比系统更远。产出端仍需专家后处理。
读下来的疑点:论文明确不与其他 agentic 数学系统做对照,也不报失败率,多少个问题跑了没出结果无从得知,能看到的都是成功案例。验证靠人不靠机器,作者在讨论里自己担心,系统产出候选证明的速度会超过人类阅读速度,缺口随算力预算扩大;形式化到 Lean 能机械定案,但人类理解可能滞后。n 人 PoA 的上界还额外假设 bid 是 undominated 的。