QED用多智能体系统自动生成数学难题的完整证明。
QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems
- 分三阶段：拆解问题、生成论证、验证正确性
- 在18个课题中产出5项原创成果，3项达期刊发表水平
- 开源系统，适合数学研究者探索自动化证明
我们提出 QED，一个开源的多智能体系统，可将人类提出的科研问题自动转化为无需进一步人工干预的完整数学证明。其流程通过分离规划、证明与验证三个环节来克服单次查询生成证明的常见失败：分解代理负责结构化证明搜索，证明代理生成候选论证，验证代理检查逻辑正确性。在与领域专家协作下，我们在18个难度各异的研究级项目上评估了QED的表现，成功生成了5项原创成果，涵盖代数几何、流体偏微分方程、概率论和反问题等领域。专家评估认为这些成果为扎实的专业研究贡献，其中三项在难度与范围上可比肩主流专业数学期刊的常规发表论文。QED 已开源，地址为 https://github.com/proofQED/QED。
原文摘要 · Abstract (English)
We present QED, an open-source multi-agent system that turns human-provided research questions into complete mathematical proofs without further human guidance. Its pipeline is designed to overcome common failures of single-query proof generation by separating planning, proving, and verification: a decomposition agent structures the proof search, prover agents generate candidate arguments, and verifier agents check correctness. In collaboration with domain experts, we evaluated QED on 18 research-level projects of varying difficulty. QED produced five original works across algebraic geometry, fluid PDEs, probability, and inverse problems. Expert assessments regard these works as solid specialized research contributions, with three comparable in difficulty and scope to work commonly published in established specialist mathematics venues. QED is released at https://github.com/proofQED/QED.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。