🤖 AI

ProofCouncil: An LLM Agent for Solving Open Mathematical Problems

本文介绍了 ProofCouncil，这是一个采用作者-评论者（author-critic）架构的开源大语言模型智能体，该智能体在 FirstProof 挑战赛中通过自主解决十个真实数学问题中的六个，并在更广泛的开放性问题上展示了显著进展，从而取得了最先进的性能表现。

原作者： Johannes Schmitt, Tim Gehrunger, Jasper Dekoninck, Gergely Bérczi, Uri Kreitner, Liam Price, David Holmes

发布于 2026-07-13

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Johannes Schmitt, Tim Gehrunger, Jasper Dekoninck, Gergely Bérczi, Uri Kreitner, Liam Price, David Holmes

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你交给一个全新的、超级聪明的机器人一叠世界上最令人困惑的数学谜题。这些可不是那种标准的“寻找缺失数字”的谜题；它们是现实中的数学家们已经苦思冥想多年、至今仍无人知晓答案的开放性问题。

欢迎来到 ProofCouncil。请不要把它仅仅看作是一个单一的机器人，而是一个微型的、高规格的数学工作坊。

工作坊团队：作者、评论家与小队

这个系统的核心是一场由两个主要角色进行的巧妙“传热豆”游戏：作者（Author）与评论家（Critic）。

作者是梦想家。它是一个试图编写完美证明（即循序渐进的数学论证过程）的 AI。它拥有一本神奇的笔记本，可以在其中涂鸦想法、尝试代码，甚至在网上搜索线索。
评论家是严厉的编辑。它阅读作者写下的内容，并指出：“等等，这一步逻辑不通，”或者“你忘了证明这个部分了！”它不仅仅是说“错了”，还会给出具体的反馈，告诉作者如何填补漏洞。

这里的转折在于，作者并不仅仅写一次。它写作、接受批评、重写、再次接受批评，并不断循环。这就像一位作家和一位编辑被锁在一个房间里，通过不断打磨故事直到其趋于完美。

但有时，作者会陷入僵局。这时，它们会召唤 委员会（Council） 和 计算节点（Compute Node）。

委员会是一个由其他超智能 AI 模型组成的专家小组（就像是一个特邀专家团队）。作者会向他们求助：“嘿，我在这个特定部分卡住了；有没有不同的观察角度？”
计算节点是重体力劳动者。如果问题需要大规模计算或作者无法独立运行的专业数学软件工具，该节点就会承担繁重的任务，运行代码并进行数值运算，以验证某种直觉是否成立。

每隔几个回合，评论家会进行一次“精神休息”，并以全新的状态重新开始。这至关重要，因为如果评论家过于习惯作者的错误，它可能会变得视而不见。一双全新的眼睛能确保证明过程确实是稳固的。

大考：FirstProof 挑战赛

团队将 ProofCouncil 置于终极测试之下：一场名为 FirstProof 的挑战。规则简单却残酷：在 24 小时内，仅使用公开工具解决 10 个真实的未解数学问题。

结果如何？ProofCouncil 成为了全场的明星。在 10 个问题中，它成功为其中的 6 个 问题产出了解决方案，经人类评审判定这些方案是正确的（仅需进行极小的、微调式的修改）。这是所有参赛队伍中的最佳表现。

他们还将该系统应用于由真实数学家提交的 30 个其他开放性问题。在收到的 21 个反馈结果中：

5 个 被判定为完全正确的解决方案。
2 个 被认为非常有前景，只需进行最后的检查。
8 个 取得了实质性的进展，尽管并未最终完成任务。
4 个 虽然没有错误，但并未产生实质性的推动作用。
2 个 误解了问题，转而解决了版本更简单的题目。

重要的是，没有任何专家指出其输出在逻辑上存在破坏性的数学错误。主要的失败并非源于错误的数学逻辑，而是有时误读了题目要求。

天才的代价

问题的关键在于：拥有如此高的智慧是有代价的。运行 ProofCouncil 处理单个问题的计算时间及模型调用成本约为 350 美元。相比之下，一个更简单的、单次尝试的 AI 尝试仅需 12 美元，但解决的问题较少。论文指出，虽然“团队协作模式”效果更好，但目前它还是一种奢侈品。作者承认他们尚未尝试降低成本，这留作了未来研究人员的工作。

它没做到的事（以及它并未声称做到的事）

必须了解这个机器人没有做到的事情。

它并没有解决挑战中的全部 10 个问题（它漏掉了 4 个）。
它并没有产出一篇精炼、可直接发表的研究论文。评审这些工作的数学家指出，其写作风格晦涩难懂，需要人工编辑才能使其易于被非专业人士理解。
它并没有“证明”AI 可以解决任何数学问题。它展示的是，对于某些难题，一组 AI 协同工作比单个 AI 独立作战更为有效。

核心结论

ProofCouncil 表明，如果你想解决一个极其困难的开放性数学问题，你不应该只是要求一个 AI “去搞定它”。相反，你需要一个系统：其中一个 AI 负责撰写，另一个负责拆解质疑，第三个提供全新的视角，而第四个则负责进行繁重的数学计算。

在 FirstProof 挑战赛的世界里，这种“作者-评论家-委员会”式的团队是目前为止测试过的最成功的策略。它并没有征服整座大山，但它攀爬的高度比任何人都高，证明了当 AI 代理像人类研究团队一样协作时，它们可以应对那些此前被认为遥不可及的问题。

技术摘要：ProofCouncil

问题陈述
大型语言模型（LLMs）在解决开放性数学问题方面展现出了日益增强的能力，但其表现往往缺乏现实世界数学实践中所具有的严谨性和迭代优化特性。挑战在于如何创建能够处理开放性问题（特别是那些没有公开解的问题）的自主智能体，且这些问题需在受限环境（例如 24 小时窗口、固定预算）内仅使用公开工具进行解决。FirstProof 挑战赛——一个由 10 个此类未解问题组成的基准测试——是这项工作的首要评估平台。此外，作者还试图在直接从数学研究人员处收集的 30 个更广泛的开放问题集上评估性能。

方法论：ProofCouncil 架构
作者引入了 ProofCouncil，这是一个围绕**作者-评论家架构（author-critic architecture）**设计的智能体系统，旨在模拟数学研究的迭代过程。该系统通过以下组件运行：

作者智能体（Author Agent）： 负责生成和修订证明。它利用具备代码执行和网络搜索能力的 GPT-5.5-Pro (xhigh)。作者维护三个规范文件：
- answer.tex：主要的 LaTeX 证明文档。
- research notes.tex：用于记录想法、失败尝试和部分结果的持久化草稿本。
- references.bib：用于引用的 BibTeX 文件。
  作者根据反馈迭代更新这些文件，并可以发出结构化的 XML 标签来请求辅助帮助。
评论家智能体（Critic Agent）： 同样使用 GPT-5.5-Pro (xhigh)，负责评估当前证明的正确性，识别其中的漏洞、错误或缺失的论证。
- 有状态 vs. 新鲜（Stateful vs. Fresh）： 评论家通常是有状态的，保留对话历史以提供一致的反馈。然而，为了减少路径依赖，评论家的历史记录会在每 $k$ 轮（实验中 $k=3$ ）后重置。
- 验证协议： 如果有状态的评论家接受了一个证明，则由一个“新鲜”的评论家（以新的对话初始化）进行独立的审计。只有当作者标记为就绪且新鲜评论家也接受时，才会返回解决方案。
辅助组件：
- LLM Council（LLM 理事会）： 一个可选的独立模型组（Gemini 3.1 Pro, Claude Opus 4.7, GPT-5.5-Pro），当作者发出特定请求时，针对特定的子问题提供针对性的反馈。
- 计算节点（Compute Node）： 一个专门的智能体（配备 GPT-5.5 的 Codex），拥有访问计算机代数系统（CAS）的能力，如 SageMath、GAP、Singular 和 Pari。它处理繁重的计算、文献检索以及对命题的独立验证。
底层库（将智能体视为 DAG）：
ProofCouncil 构建于一个开源库之上，该库将智能体系统表示为条件有向无环图（Conditional Directed Acyclic Graphs, DAGs）。
- 结构： 节点代表 LLM 调用、Python 代码块、CLI 智能体或控制流门控。边编码了依赖关系。
- 条件性： 边可以带有条件，允许下游节点的执行取决于中间输出（例如，仅当作者发出特定标签时才调用 Council）。
- 循环展开： 虽然工作流包含反馈循环，但该库将其表示为有界重复块，实际上将其展开为一个有限的条件 DAG 以供执行。
- 人机协同（Human-in-the-Loop）： 该库支持在 DAG 中插入人类节点，允许研究人员在中途审查中间证明或回答问题。

核心贡献

ProofCouncil 系统： 一个旨在通过带有辅助支持的作者-评论家循环来解决复杂开放问题的数学智能体。
开源库： 一个用于将智能体系统构建为条件 DAG 的库，为定义工作流、提示词和执行逻辑提供了灵活的接口。
实证评估： 在 FirstProof 挑战赛和自定义的研究人员提供的题目数据集上对系统进行了全面的评估。

结果

FirstProof 挑战赛：
- ProofCouncil 被提交至第二批 FirstProof 挑战赛（10 个问题）。
- 性能： 在 10 个问题中的 6 个（P1, P2, P3, P5, P7, P9） 被评审员判定为在至多经过微调后是正确的。这代表了参与团队中的最佳表现。
- 成本： 运行成本约为 每个问题 350 美元（分析的 9 个问题总计约 3,186 美元），显著高于单次查询基准（约 12 美元/问题），但获得了更高的解决率（6/9 对比 4/9）。
- 失败模式： 其中一个问题（P6）由于 API 超时而失败。P4 和 P8 被拒绝；P8 是由于一个不支持的技术断言导致的，而 P4 则因其他原因被拒绝。
研究人员提供的题目：
- 系统在从数学研究人员处收集的 30 个开放问题（外加 3 个公开的 Erdős 问题）上进行了测试。
- 反馈： 在收到的 21 份人类评审中：
  - 5 个 被判定为完整、正确的解。
  - 2 个 被认为是极具前景的，尚待最终验证。
  - 8 个 包含了有用的阶段性进展。
  - 4 个 没有错误，但提供的实质性进展很少。
  - 2 个 被判定为解决了所述问题的较简单版本（误解）。
- 显著观察： 没有专家报告说输出声称解决问题的结论在数学上是错误的。主要的失败模式被确定为问题理解，即智能体解决了另一个更简单的版本的问题。
- 成本： 每次尝试问题的成本约为 213 美元。
组件效用：
- 计算节点在验证具体命题和寻找反例方面最为有用。
- LLM Council 提供了多元化的视角，其中 GPT-5.5-Pro 是最具决定性的贡献者。
- 评论家对于防止错误解被接受至关重要，尽管它偶尔会出现假阳性（接受了错误的解）或假阴性（拒绝了正确的解）的情况。

意义与局限性
论文声称 ProofCouncil 展示了智能体工作流提高 LLM 在开放性数学问题上表现的潜力，并在 FirstProof 挑战赛中取得了领先水平。发布底层的基于 DAG 的库旨在促进未来构建复杂智能体系统的研究。

然而，作者对其系统的能力保持谦逊：

成本： 该系统非常昂贵，这是由对前沿模型和辅助智能体的重复调用驱动的。
理解： 系统在处理歧义问题陈述时表现挣扎，经常在未检测到的情况下解决较简单的解释版本。
可读性： 生成的证明内容密集，是为正确性而非人类可读性而优化的，通常需要为非专业人士进行扩展说明。
评估： 结果高度依赖于人类判断而非形式化验证，且在研究人员题目上的评估涉及自适应开发（基于早期运行进行提示词微调），而非冻结配置。

该工作总结道，虽然 ProofCouncil 代表了自主数学推理的一个重要进步，但在成本效率、问题理解和输出润色方面仍存在待解决的挑战。