QED：一个用于生成开放问题数学证明的开源多智能体系统

我们探讨数学人工智能的一个核心问题：人工智能系统能否为开放研究问题提供原始的、重要的证明？尽管基准测试表现强劲，但对于大语言模型来说，制作真正新颖的证明仍然是一个巨大的挑战。通过与前沿大语言模型在研究级证明任务上的系统实验，我们确定了七种阻碍可靠证明生成的故障模式，包括上下文污染、引用幻觉、关键步骤上的挥手和证明工作的错误分配、不稳定的证明计划、不集中的验证、问题修改和单一模型瓶颈。我们认为，由于这些失败模式，基准测试成功与研究水平证明之间的差距主要是系统设计方面的差距。我们提出了 QED，一个开源多代理证明系统，其中每个架构决策都直接解决特定的故障模式。通过对领域专家贡献的应用分析和偏微分方程中的五个开放问题进行评估，QED 为三个问题提供了正确的证明，每个问题都由贡献专家验证为原始且重要的。 QED 作为开源软件发布于 https://github.com/proofQED/QED。