ProofCouncil: 一个解决开放数学问题的LLM智能体

# ProofCouncil：用于解决开放数学问题的LLM智能体  
来源：https://arxiv.org/html/2607.09474  

Johannes Schmitt¹, Tim Gehrunger¹, Jasper Dekoninck¹, Gergely Bérczi², Uri Kreitner¹, Liam Price³, David Holmes⁴  

¹苏黎世联邦理工学院，²奥胡斯大学，³独立研究员，⁴莱顿大学  

通讯作者：johannes\.schmitt@math\.ethz\.ch  

###### 摘要  

大型语言模型（LLM）在解决数学开放问题方面展现出日益增长的前景。然而，通过针对真实数学实践定制的智能体工作流，其性能可进一步提升。为此，我们提出了ProofCouncil，一个采用作者-评论家架构设计、旨在解决开放问题的数学智能体。ProofCouncil参与了FirstProof挑战赛第二批次，该挑战包含10个必须由智能体自主解决的现实数学问题。经评审判定，其对10个问题中的6个提交的解答最多只需小幅修改即可视为正确，在参赛团队中表现最佳。我们还在从数学研究人员处收集的30个开放问题上评估了ProofCouncil。在收到人工反馈的21个解答中，5个被判定完全正确，另有2个被认为有望通过最终验证，还有8个包含有用的部分进展。在这篇短文中，我们描述了ProofCouncil的开发过程以及用于创建它的智能体构建库，该库已作为开源资源发布给社区。  

## 1 引言  

大型语言模型（LLM）近期在数学领域展示了卓越的能力，解决了不同受关注程度的开放问题（Alon et al., 2026; Schmitt, 2025; Dixit et al., 2026）。这一进展伴随着专为数学问题求解设计的高级智能体的开发（Dixit et al., 2026; Zhao et al., 2026; Zheng et al., 2026; Ju et al., 2026），进一步突显了LLM在该领域的潜力。在此背景下，Second Proof挑战赛（Abouzaid et al., 2026a; b）启动，旨在评估AI系统在一组固定的10个尚无公开解答的问题上的表现。参赛者需提交一个能在24小时内自主尝试所有10个问题的智能体，且仅能使用公开可用的模型和工具。  

在本工作中，我们提出了ProofCouncil，一个提交至FirstProof挑战赛的数学智能体。如图1所示，ProofCouncil采用作者-评论家架构：作者智能体迭代编写和修订证明，而评论家智能体评估每个版本并提供反馈。在每一轮中，作者还可以从两个辅助来源请求针对性帮助：一个由主作者-评论家循环之外的额外LLM组成的顾问团，以及一个用于计算机代数系统（CAS）计算的计算机智能体。它们的响应将在下一轮提供给作者。为保持一致性并让评论家能够跟踪进展，评论家通常跨轮保留其对话历史，但每k轮会重置该历史以提供更独立的审查。如果新初始化的评论家接受该证明，则将该证明返回给用户。  

我们开源了解ProofCouncil和用于构建它的底层智能体构建库。该库将智能体系统表示为条件有向无环图（DAG），支持不同智能体和模型之间灵活的结构化调用。它还提供了一个简单的接口用于实现新的智能体和工作流，使未来的研究人员能够基于我们的工作构建自己的智能体系统。  

在FirstProof挑战赛中，ProofCouncil解决了10个问题中的6个（最多只需小幅修改即可视为正确），在参赛团队中表现最佳。作为二次评估，我们还联系了数学研究人员，收集了涵盖数学不同领域的30个开放问题。解答尝试被发送给问题作者以获取反馈。在收到的21份回复中，5个被判定为正确解答，2个被认为有望通过最终验证，另有8个包含有助于解决问题的不分进展。值得注意的是，没有专家报告称声称解决了所提问题的输出在数学上是不正确的。然而，有两份输出被判定为解决所提交问题的简化版本，这突显了问题解读是一个关键失败模式。我们不会发布这些研究者提供的问题的解答，因为它们是分享给我们的研究人员的知识产权，可由他们自行决定使用。  

我们的主要贡献如下：  

- •我们提出了ProofCouncil，一个通过作者-评论家架构设计用于解决复杂问题的数学智能体（第2.1节）。  
- •我们开发并发布了一个开源智能体构建库，支持将智能体系统灵活高效地构建为条件DAG（第2.2节）。  
- •我们通过解决FirstProof挑战赛中10个问题中的6个（最多只需小幅修改）以及为从数学研究人员处收集的5个开放问题生成正确解答，展示了ProofCouncil的有效性（第3节）。  

问题陈述  
作者编辑证明  
有状态评论家  
同一对话  
新评论家  
新对话  
LLM 顾问团  
其他LLM  
计算节点  
CAS工作者  
返回  
其他轮  
每k轮  
新鲜审计  
拒绝证明  
拒绝证明  

图 1: ProofCouncil 概览。作者智能体根据评论家的反馈迭代编辑证明。每 k 轮，有状态评论家被重置。作者可以选择性地请求其他 LLM 或计算节点的帮助。  

## 2 ProofCouncil  

在本节中，我们首先概述 ProofCouncil 的系统架构，然后讨论我们开发的用于将 ProofCouncil 构建为智能体调用的条件 DAG 的库。提示词见附录 C。  

### 2.1 ProofCouncil 工作流  

ProofCouncil 的整体工作流如图 1 所示。系统迭代进行，直到满足四个停止条件之一：解答被接受，达到最大轮数，总成本预算耗尽，或超时。我们依次描述每个组件。  

##### 作者  
作者负责生成和修订证明。它使用 GPT-5.5-Pro (xhigh)¹，并配备内置代码执行和网络搜索工具。通过代码执行，作者维护和编辑三个文件：  

- • answer.tex：包含证明的主要 LaTeX 文件。  
- • research_notes.tex：用于记录想法、失败尝试和不属于主要证明但可能帮助作者或评论家跟踪进展的部分结果的草稿本。  
- • references.bib：包含证明中引用的参考文献的 BibTeX 文件。  

在每次迭代中，作者接收最新的评论家反馈、顾问团或计算节点产生的任何辅助信息，以及所有文件的当前状态。然后它更新证明，并在有用时更新其研究笔记和参考文献。作者还可以通过在其输出中发出结构化的 XML 标签来请求辅助帮助。`<council></council>` 标签包含一个给 LLM 顾问团的具体问题，而 `<compute></compute>` 标签包含一个给计算节点的问题。生成的响应将在下一次迭代中传回给作者。最后，作者必须发出一个 `<ready></ready>` 标签，表明它是否认为已经找到了一个完整且正确的解决方案。  

##### 评论家  
评论家负责评估当前证明的正确性。它接收作者编写的文件，并就差距、错误或缺失的论证提供反馈。与作者一样，它使用 GPT-5.5-Pro (xhigh) 并配备相同的工具。默认情况下，评论家是有状态的。每个新版本的证明都会被附加到评论家的对话历史中，使评论家能够提供一致的反馈。为了减少路径依赖并获得更独立的反馈，我们每 k 轮重置评论家。在我们的实验中，我们使用 k=3。评论家还会发出一个 `<accept></accept>` 标签，表明它是否认为证明是完整且正确的。如果状态评论家接受了证明，则会调用一个新评论家进行额外审计。只有当新评论家也接受该证明，并且作者已将解答标记为就绪时，该证明才会作为解决方案返回。  

##### LLM 顾问团  
LLM 顾问团是一个可选的辅助组件，在主作者-评论家循环之外提供额外反馈。当被调用时，每个顾问团成员接收作者编写的所有文件，以及作者提出的具体问题。顾问团目前包括 Gemini 3.1 Pro (high)、Claude Opus 4.7 (max) 和 GPT-5.5-Pro (xhigh)。模型独立回答，不看彼此的回答。然后它们的回答作为额外上下文在下一轮提供给作者。  

##### 计算节点  
计算节点是一个可选的辅助组件，用于代码执行和计算机代数系统（CAS）计算。它被实现为一个使用 GPT-5.5 (xhigh) 的 Codex 智能体，并配备专门的数学软件，包括 SageMath (The SageMath Developers, 2026)、GAP (The GAP Group, 2026)、Singular (Decker et al., 2024) 和 Pari (The PARI Group, 2023)。计算节点接收作者编写的所有文件，以及作者的具体问题，并返回一个可能包含代码、CAS 输出或解释性分析的响应。该响应在下一轮提供给作者。此外，编辑过的代码仓库被添加到作者可用的文件系统中，使其能够在后续推理中检查或重用计算节点的输出。  

### 2.2 智能体作为 DAG  

为了创建 ProofCouncil，我们开发了一个开源库，用于将智能体系统构建为条件有向无环图（DAG）。我们在此简要描述其主要特性。  

##### DAG 表示  
在我们的库中，一个智能体被表示为一个 DAG，其节点可以是 LLM 调用、自定义 Python 块、基于 CLI 的计算智能体、确定性门（如编译检查）或控制流块，边编码了它们之间的依赖关系。节点本身也可以是智能体，支持模型和工作流的分层组合。例如，一个 LLM 节点由提示模板、模型名称和一组输出等参数定义。提示在运行时使用上游节点的输出进行渲染，节点产生的输出又可以作为下游节点的输入。这种抽象支持复杂的信息流，同时保持系统结构的显式性。  

##### 条件执行  
简单的 DAG 对于许多智能体工作流来说表达能力不足，因为要执行的调用集可能取决于中间输出。例如，在 ProofCouncil 中，LLM 顾问团仅在作者发出相应标签时才被调用。为了支持这种行为，边可以配备条件，这些条件根据其父节点的输出确定是否应执行下游节点。尽管图 1 中的工作流包含从评论家到作者的反馈循环，但可以通过将循环展开为固定轮数来表示为条件 DAG。为了提高可读性，该库支持代表循环的有界重复块，产生更易读和编辑的结构，同时仍作为有限条件 DAG 执行。  

##### 智能体执行  
为了执行一个智能体，该库计算 DAG 中节点的拓扑顺序。一旦某个节点的所有依赖项完成且其边条件满足，该节点就会运行。这使得独立节点能够并行执行，从而提高具有多个辅助调用或独立分支的工作流的效率。  

##### 用户界面  
我们还构建了一个自定义用户界面，用于编辑和运行智能体，灵感来自 Blender 节点 (Blender Online Community, 2026)。该界面允许用户可视地构造和修改 DAG 结构，编辑提示模板，添加或移除输出，以及监控每个节点的执行。输出通过要求模型发出结构化的 YAML 标签来指定。自定义组件可以作为节点添加，控制流构造（如条件语句和重复块）可以可视地创建。截图见附录 B。  

##### 人机交互工作流  
该库还支持人机交互工作流：人可以充当 DAG 中的一个节点，可与任何模型节点互换。当到达这样的节点时，运行暂停，任务显示在用户界面中，执行在提交答案后恢复。这使得数学家等能够审查中间证明或在运行过程中回答作者的问题。  

## 3 评估  

我们在两组问题上评估 ProofCouncil：一组是从数学研究人员（主要来自苏黎世联邦理工学院）处收集的开放问题，另一组是来自 FirstProof 的 10 个问题。收集前一组是为了在更广泛和多样化的研究问题上测试系统。我们还利用这些运行的反馈来改进 ProofCouncil。  

表 1：开放问题评估中的人工反馈摘要。  

### 3.1 开放问题结果  

参见图注  

图 2：所有 33 个尝试问题的进度面板：行 R1–R3 显示三个 10 问题运行，行 S 显示三个单问题预测试运行。曲线显示 GPT-5.5-Pro 后期筛选进度估计。颜色表示最终状态，根据收到的人工反馈；反馈类别与表 1 匹配。  

为了准备 FirstProof 挑战赛的提交，我们进行了几次初步评估：三个关于研究者提交问题的单问题预测试运行，然后是三个更大的各包含 10 个问题的运行，最后一个运行还包括三个 Erdős 问题。在本节中，我们报告这些运行的结果，并总结从人类数学家那里收到的关于 ProofCouncil 产生的解决方案的反馈。  

##### 问题收集  
我们联系了苏黎世联邦理工学院数学系的所有成员，请他们分享他们有兴趣让 AI 系统尝试的开放问题。通过私人通信，其他一些机构的研究人员也提供了问题。每个问题都使用 GPT-5.5-Pro 进行筛选，以检查其是否自成体系且陈述准确。必要时，与提交问题的研究人员合作进行编辑。筛选提示见附录 C。在所有运行中，我们在 33 个不同问题上评估了 ProofCouncil：30 个从研究人员处收集的问题和 3 个