LLM智能体ProofCouncil攻克开放数学难题
速览
开源数学智能体ProofCouncil采用作者-评审架构，在FirstProof挑战的10个开放数学问题中，6个提交被评审认为仅需少量修改即可正确，在所有参赛团队中表现最佳。在30个来自数学研究者的开放问题上，21个获得人工反馈，其中5个完全正确，2个有望通过最终验证，8个提供了有用进展。该智能体及其构建库已开源。
AI 深度解读
背景
大型语言模型（LLM）在解决开放数学问题方面展现出越来越大的潜力。然而，其性能可以通过针对真实数学实践定制的 agentic 工作流进一步提升。为此，研究者提出了 ProofCouncil，一个专门设计用于利用 author-critic 架构解决开放问题的数学 agent。ProofCouncil 作为参赛作品参与了 FirstProof 挑战赛的第二批，该挑战包含 10 个真实世界的数学问题，agent 必须自主解决。该工作在 arXiv 上以计算机科学 > 人工智能类别提交，发布于 2026 年 7 月 10 日。
核心内容
ProofCouncil 是一个基于 LLM 的数学 agent，其核心架构为 author-critic 模式。在 FirstProof 挑战的第二批中，针对 10 个问题，ProofCouncil 提交的解答中有 6 个被评委判定为正确，仅需微小修订，这一表现在所有参赛队伍中最佳。此外，研究团队在从数学研究人员收集的 30 个开放问题上对 ProofCouncil 进行了评估。在收到人工反馈的 21 个解决方案中，有 5 个被判定为完全正确，另有 2 个被认为有希望但需最终验证，还有 8 个包含了有用的部分进展。本文简要描述了 ProofCouncil 的开发过程以及用于创建它的 agent 构建库，该库已作为开源项目发布给社区。
关键要点
- ProofCouncil 采用 author-critic 架构，结合 LLM 能力进行数学问题求解。
- 在 FirstProof 挑战（第二批）的 10 个问题中，ProofCouncil 有 6 个解答被评委认为正确（只需微小修订），表现最佳。
- 在 30 个来自数学研究人员的开放问题中，21 个获得人工反馈，其中 5 个完全正确，2 个有希望但需最终验证，8 个包含部分有用进展。
- 研究团队开源了用于构建 ProofCouncil 的 agent 构建库，以促进社区发展。
- 论文发表于 arXiv（cs.AI），提交时间为 2026 年 7 月 10 日。
意义与影响
ProofCouncil 展示了 LLM agent 在解决开放数学问题上的实际能力，尤其是在真实挑战中的优越表现。其 author-critic 架构为数学推理的 agentic 工作流提供了新范式。通过开源构建库，该工作为后续研究提供了可复用的基础设施，有望推动更多数学发现自动化的探索。同时，评估结果（部分完全正确、部分提供有用进展）表明，LLM agent 虽未达到完全自主解决所有开放问题的水平，但已能作为有价值的辅助工具，缩短数学研究的探索周期。