From Expert-Guided Proof Search to Automated Open-Problem Solving
作者: Adrián Zámečník, Matěj Kripner, Martin Koutecký, Martin Balko, Jan Grebík, Pavel Hubáček, Robert Šámal, Václav Rozhoň
分类: cs.AI, cs.CL
发布日期: 2026-10-07
备注: Accepted at the 6th Workshop on Mathematical Reasoning and AI (MATH-AI), NeurIPS 2026
💡 一句话要点
提出Bolzano系统以实现自动化开放问题求解
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 开放问题求解 多代理系统 自动化证明 数学研究 理论计算机科学
📋 核心要点
- 现有方法在处理开放数学问题时，往往依赖于专家的手动指导，效率低下且难以扩展。
- 论文提出的Bolzano系统通过并行代理和验证机制，实现了开放问题的自动求解，减少了对人类专家的依赖。
- 实验结果显示，Bolzano在处理3800个开放问题时，成功解决了约200个问题，验证了其有效性和实用性。
📝 摘要（中文）
大型语言模型在数学研究中日益发挥重要作用，尤其是在高效证明搜索、逐步改进和仔细验证方面。本文介绍了Bolzano，一个开源的多代理系统，利用并行证明代理和验证代理，维护可读的研究状态。在专家选择的问题上进行的初步手动使用产生了8个结果，这些证明经过领域专家的检查。随后，我们在没有问题特定人类指导的情况下，使用Bolzano解决了约3800个开放问题，成功解决了约200个开放问题。实验中还使用了STOC 2026会议接受的论文，确认了我们对论文中提出的四个问题的回答。
🔬 方法详解
问题定义：本文旨在解决开放数学问题的自动求解难题，现有方法往往需要专家的手动干预，导致效率低下和可扩展性不足。
核心思路：Bolzano系统通过引入多个并行的证明代理和一个验证代理，能够在没有人类指导的情况下自动处理开放问题，提升了求解的效率和准确性。
技术框架：Bolzano的整体架构包括多个并行的证明代理，这些代理负责生成证明，而验证代理则负责检查这些证明的正确性。此外，系统维护一个可读的研究状态，以便于人类研究者理解和跟踪进展。
关键创新：Bolzano的主要创新在于其多代理系统的设计，使得开放问题的求解过程能够并行化，显著提高了求解效率。这一设计与传统依赖单一专家指导的方法形成了鲜明对比。
关键设计：系统的关键设计包括并行代理的数量和配置、验证机制的准确性，以及人类可读状态的维护方式。这些设计确保了系统在处理复杂问题时的高效性和可靠性。
🖼️ 关键图片
📊 实验亮点
在实验中，Bolzano成功解决了约200个开放问题，验证了其在没有人类指导的情况下的有效性。这一成果表明，Bolzano在处理复杂数学问题时的自动化能力显著优于传统方法，具有较高的实用价值。
🎯 应用场景
Bolzano系统的潜在应用领域包括数学研究、理论计算机科学以及其他需要高效问题求解的领域。其自动化求解能力能够大幅提升研究效率，减少人类专家的工作负担，未来可能在教育和科研中发挥重要作用。
📄 摘要（原文）
Large language models are increasingly contributing to mathematical research, where progress often depends on efficient proof search, incremental improvements and careful verification. We describe Bolzano, a multi-agent open-source system that uses parallel prover agents with a verifier agent and maintains a human-readable research state. Initial manual use on expert-selected problems yielded 8 results whose proofs were checked by domain experts. Motivated by these case studies, we ran Bolzano without problem-specific human guidance on about 3,800 open problems extracted from four sets of papers, solving about 200 open problems. One experiment used papers accepted to STOC 2026, a top conference in theoretical computer science. There, we answered four questions raised in the papers, as confirmed by their authors.