智能体
x.com ·
@omarsar0
Google Research 多智能体证明发现系统 Cogentic：对抗验证与共享账本
该研究提出基于 Gemini 的多智能体证明发现系统 Cogentic，从问题陈述出发、无需专家提示。系统按轮次运行，编排器决定 prover 数量，每个 prover 负责一个方向，summarizer 独立撰写历史简报；每份草稿须通过两个对抗式验证器（独立检查与同轮横向比对）才被接受。智能体通过记录与账本两份磁盘文档共享状态，auditor 从被拒证明中提取并复核正确引理，process advisor 依据验证日志更新指令。据称在在线学习、拍卖理论与机制设计的五个开放问题上取得新结果，多数问题约 100 次 Gemini 调用，最难约 1000 次。
AI推荐理由 转述 Google Research 关于多智能体数学证明发现的研究（Cogentic，基于 Gemini）。正文给出较具体的机制：编排器按轮次决定 prover 数量，每个 prover 负责一个方向并由 summarizer 独立撰写简报；每份草稿需通过两个对抗式验证器（一个独立检查、一个横向比对同轮草稿）；通过磁盘文档共享状态，记录失败尝试与已验证引理；另有 process advisor 依据验证日志更新指令。据称在在线学习、拍卖理论和机制设计五个开放问题上取得新结果，多数问题约 100 次 Gemini 调用，最难约 1000 次，并附 arXiv 链接。机制描述具体、可追溯，但“新结果”与专家核验仍属转述，需以论文为准。
82
浏览 5,788
点赞 53
评论 10
转发 8
正文
Banger paper from Google Research on multi-agent proof discovery.
(bookmark it)
It's really interesting to see this emerging multi-agent pattern: not enforcing too much execution structure and pairing it with dedicated agents for advising and verification.
I think it is generally applicable as well. Great read.
Here is how it works:
Cogentic runs on Gemini and works on open problems in theoretical computer science, starting from the problem statement with no expert hints.
The system works in rounds, and the orchestrator decides how many provers to run in each round. Every prover gets one direction to work on, such as a specific bound or a counterexample search, plus a short briefing that a summarizer agent writes from earlier attempts and verifier feedback. Each summarizer writes its briefing independently, so provers in the same round read different summaries of the same history.
Each draft goes through two adversarial verifiers. One checks the draft on its own, and the other reads all of the round's drafts side by side to catch shared mistakes. A draft is accepted only if both pass it.
The agents share state through two disk documents. A record logs every attempt with the objection it failed on, and a ledger stores verified lemmas and ruled-out directions. An auditor extracts correct lemmas from rejected proofs, verifies them again independently, and adds them to the ledger.
A separate process advisor reads the verification logs across rounds and updates the instructions given to provers and verifiers. The orchestrator and the advisor can't give mathematical opinions, so the provers provide all the math.
It produced new results on five open problems in online learning, auction theory, and mechanism design, each checked by domain experts. Most problems took around 100 Gemini calls, and the hardest took around 1,000.
Paper: [arxiv.org/abs/2609.40324](https://arxiv.org/abs/2609.40324)
Chat with Paper: [academy.dair.ai/papers/cogenti…](https://academy.dair.ai/papers/cogentic-multi-agent-orchestration-for-automated-proof-discovery-2609.40324)
