arXiv cs.CL· Adri\'an Z\'ame\v{c}n\'ik, Mat\v{e}j Kripner, Martin Kouteck\'y, Martin Balko, Jan Greb\'ik, Pavel Hub\'a\v{c}ek, Robert \v{S}\'amal, V\'aclav Rozho\v{n}·· 10 天前AI 评分71
Bolzano：多智能体系统自动求解约 200 个开放数学问题
Bolzano: From Expert-Guided Proof Search to Automated Open-Problem Solving
AI 导读
论文提出 Bolzano，一个开源多智能体系统，由并行证明智能体配合验证智能体，并维护人类可读的研究状态。在专家选定问题上的初步人工使用产出 8 个经领域专家核验的证明；随后在无问题特定人工引导下，对从四组论文中提取的约 3800 个开放问题运行，解出约 200 个。
正文 · AI 翻译
摘要：大语言模型正越来越多地为数学研究做出贡献，而数学研究的进展往往依赖于高效的证明搜索、渐进式改进和仔细验证。我们描述了 Bolzano，一个多智能体开源系统，它使用并行证明智能体和一个验证智能体，并维护人类可读的研究状态。在专家选定的问题上进行初步人工使用，得到了 8 个结果，其证明由领域专家检查。受这些案例研究的启发，我们在没有针对具体问题的人工指导下运行 Bolzano，处理从四组论文中提取的约 3,800 个开放问题，解决了约 200 个开放问题。其中一项实验使用了被 STOC 2026 接收的论文，STOC 是理论计算机科学领域的顶级会议。在那里，我们回答了论文中提出的四个问题，并得到了其作者的确认。
| 评论： | 被第 6 届数学推理与人工智能研讨会（MATH-AI），NeurIPS 2026 接收 |
| 主题： | 人工智能（cs.AI）；计算与语言（cs.CL） |
| 引用为： | arXiv:2610.09769 [cs.AI] |
| （或 arXiv:2610.09769v1 [cs.AI] 为此版本） | |
| https://doi.org/10.48550/arXiv.2610.09769 arXiv 颁发的 DOI 通过 DataCite（待注册） |
提交历史
来自：Matěj Kripner [查看电子邮件]
[v1]
2026年10月7日星期三 09:52:46 UTC（13 KB）
来源：arXiv cs.CL · arxiv.org