发表机构
ETH Zurich; Aarhus University; Leiden University（苏黎世联邦理工学院; 奥胡斯大学; 莱顿大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究旨在提升大型语言模型解决数学开放性问题的性能，介绍了ProofCouncil智能体，它采用作者-评论家架构，在FirstProof挑战及其他问题测试中表现出色，还介绍了其开发及相关构建库并开源。
AI 中文摘要
大型语言模型（LLMs）在解决数学开放性问题方面展现出越来越大的潜力。然而，通过针对实际数学实践定制的智能体工作流程，其性能可进一步提升。为此，我们引入了ProofCouncil，这是一个旨在使用作者-评论家架构解决开放性问题的数学智能体。ProofCouncil参与了第二批FirstProof挑战，该挑战包含10个现实世界数学问题，智能体必须自主解决。在10个问题中，其针对6个问题的提交内容经评审至多只需进行小的修订即为正确，在参赛团队中表现最佳。我们还在从数学研究人员处收集的30个开放性问题上评估了ProofCouncil。在收到人类反馈的21个解决方案中，5个被判定完全正确，2个被判定有希望待最终验证，另有8个包含有用的部分进展。在本文中，我们描述了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.
Comments25 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
