用机制驱动方法生成精准且有价值的数学猜想
MECA: A Mechanism-Centered Agent for Constructing Well-Specified and Valuable Mathematical Conjectures

- 通过多智能体协作,同时构建猜想与支持它的数学机制
- 在100个半开放问题中生成的猜想均难被现有自动证明器攻破
- 适合从事数学发现与自动化推理的研究者参考
自动构造精确且有价值的数学猜想仍是人工智能辅助数学发现的核心挑战。许多现有开放问题或猜想过于宽泛、表述不清,难以关联可行的证明或反证路径。我们定义数学机制为连接假设与结论的结构或推理原则,如不等式、不变量、分解或归约至中间命题。提出MECA(机制中心猜想代理),一种多智能体框架,通过协同生成候选猜想及其支撑机制实现优化:探索者智能体提出机制并测试应用,据此修正猜想;批评者智能体评估其数学有效性与研究价值,并反馈以调整假设、范围和结论。该过程将宽泛研究方向转化为具有明确未解核心的精确猜想。我们在两个互补场景下评估:一是在目标条件下的盲源材料中重构已发表论文结论;二是在文献种子与现存开放问题基础上生成100个半开放问题,并由自动证明器独立尝试证明或反证。结果表明,机制中心的精炼能生成既精确又具研究价值的猜想,仍对当前自动证明器构成挑战。
原文摘要 · Abstract (English)
Automatically constructing well-specified and valuable mathematical conjectures remains a central challenge in AI-assisted mathematical discovery. Many existing open problems and conjectures are often too broad, underspecified, or difficult to connect to plausible proof or refutation strategies. We view a mathematical mechanism as a structure or reasoning principle that connects the assumptions of a candidate problem to its target conclusion, such as an inequality, invariant, decomposition, or reduction to an intermediate claim. We present MECA (MEchanism-centered Conjecture Agent), a multi-agent framework that constructs conjectures by jointly developing candidate statements and their supporting mechanisms. Explorer agents propose mechanisms, test how they apply, and revise the candidate conjecture accordingly, while critic agents assess their mathematical validity and research value. Their feedback guides changes to the assumptions, scope, and conclusion. Through this process, MECA transforms broad research directions into precise conjectures with substantive mathematical support while retaining a clearly identified unresolved core. We evaluate MECA in two complementary settings. First, we compare it with a generate-and-revise baseline on reconstructing preselected target-paper conclusions from target-conditioned but article-blind source materials. Second, we construct 100 semi-open problems from literature-derived seeds and existing open problems and evaluate them through independent proof and refutation attempts by automated provers. Our results indicate that mechanism-centered refinement produces well-specified and research-worthy conjectures that remain challenging for current automated provers.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。