ProofCouncil: An LLM Agent for Solving Open Mathematical Problems

📄 arXiv: 2607.09474v1 📥 PDF

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

分类: cs.AI

发布日期: 2026-07-10

备注: 25 pages, 7 figures. ProofCouncil appears as System A (IMProofBench ProofCouncil) in the official FirstProof second-batch report (arXiv:2606.18119). Code and agent-building library: https://github.com/eth-sri/proof-council

💡 一句话要点

提出ProofCouncil以解决开放数学问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 数学问题 代理工作流程 作者-评论家架构 自动化定理证明 开放问题解决 人类反馈

📋 核心要点

  1. 现有大型语言模型在解决开放数学问题时，往往缺乏针对性的工作流程，导致性能不尽如人意。
  2. ProofCouncil通过引入作者-评论家架构，设计了一种新的代理工作流程，以更好地适应数学问题的解决过程。
  3. 在参与的10个问题中，ProofCouncil成功解决了6个，并在30个开放问题中获得了显著的反馈，显示出其有效性。

📝 摘要（中文）

大型语言模型（LLMs）在解决开放数学问题方面展现出越来越大的潜力。然而，通过针对现实数学实践的代理工作流程，可以进一步提升其性能。为此，我们提出了ProofCouncil，一个旨在利用作者-评论家架构解决开放问题的数学代理。ProofCouncil作为第二批FirstProof挑战的提交，成功解决了10个真实数学问题中的6个，表现优于其他参与团队。我们还在30个来自数学研究者的开放问题上评估了ProofCouncil，21个解决方案中有5个被评为完全正确，2个被认为有前景，8个则包含有用的部分进展。本文简要描述了ProofCouncil的开发及其构建库，并将其作为开源项目发布给社区。

🔬 方法详解

问题定义：论文旨在解决大型语言模型在处理开放数学问题时的性能不足，现有方法缺乏有效的代理机制，导致解决方案的质量不高。

核心思路：ProofCouncil的核心思路是采用作者-评论家架构，通过模拟数学研究的实际流程，提升模型的推理能力和解决问题的效率。

技术框架：整体架构包括问题理解、解决方案生成和反馈评估三个主要模块。首先，模型理解问题背景，然后生成解决方案，最后通过人类反馈进行评估和改进。

关键创新：最重要的技术创新在于引入了代理工作流程，使得模型能够在解决问题时进行自我评估和调整，这与传统的单一生成模型有本质区别。

关键设计：在设计上，ProofCouncil使用了特定的损失函数来优化生成的解决方案，并通过多轮反馈机制来逐步提高答案的准确性。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

在实验中，ProofCouncil在10个真实数学问题中成功解决了6个，表现优于其他参与团队。此外，在30个开放问题的评估中，21个解决方案中有5个被评为完全正确，显示出其在数学问题解决中的有效性和潜力。

🎯 应用场景

该研究的潜在应用领域包括数学研究、教育和自动化定理证明等。ProofCouncil能够帮助研究人员快速找到问题的解决方案，并为教育工作者提供辅助工具，提升学生的数学理解能力。未来，该技术可能在更广泛的科学研究和工程领域中发挥重要作用。

📄 摘要（原文）

Large language models (LLMs) have shown increasing promise in solving open problems in mathematics. However, their performance can be further improved through agentic workflows tailored to real-world mathematical practice. To this end, we introduce ProofCouncil, a mathematical agent that is designed to tackle open problems using an author-critic architecture. ProofCouncil served as a submission to the second batch of FirstProof, a challenge consisting of 10 real-world mathematical problems that agents must solve autonomously. Its submissions for 6 of the 10 problems were judged by the referees to be correct up to at most minor revisions, showing the best performance among participating teams. We also evaluate ProofCouncil on 30 open problems collected from mathematical researchers. Among the 21 solutions that received human feedback, 5 were judged completely correct, 2 more were judged promising pending final verification, and a further 8 contained useful partial progress. In this short paper, we describe the development of ProofCouncil and the agent-building library used to create it, which we release as open source to the community.