Bolzano：LLM辅助数学研究的案例研究

# Bolzano：LLM辅助数学研究的案例研究 来源：https://arxiv.org/html/2604.16989

Jan Grebík¹, Pavel Hubáček¹,², Martin Koutecký¹, Matěj Kripner³, Václav Rozhoň¹, Robert Šámal¹, Adrián Zámečník¹
¹查理大学计算机科学研究所；²捷克科学院数学研究所；³查理大学形式与应用语言研究所。

###### 摘要
我们报告了在 Bolzano（一个开源的多智能体大语言模型系统）协助下，在数学和理论计算机科学领域的六个问题上取得的新成果。Bolzano 在并行证明者智能体和验证者智能体之间协调多轮交互，同时维护跨轮次持续存在的基础知识库。按照 Feng 等人 \[F+26b (https://arxiv.org/html/2604.16989#bib.bibx21)\] 的重要性-自主性分类法进行分类，六项成果中有四项达到了可发表研究的水准，其中三项基本上是由 Bolzano 自主完成的。我们的结果为“大语言模型能够为数学研究做出实质性贡献”提供了证据，补充了 Bubeck 等人 \[BCE+25 (https://arxiv.org/html/2604.16989#bib.bibx3)\]、Woodruff 等人 \[WCAJ+26 (https://arxiv.org/html/2604.16989#bib.bibx52)\] 等人的近期报告。

## 1 引言

将大型语言模型整合到数学研究中，已从推测阶段快速迈向有据可查的实践阶段。我们重点提及两份近期报告，确立了这一现象的真实性（更多相关成果见“相关工作”部分）：
- • Woodruff、Mirrokni 等人 \[WCAJ+26 (https://arxiv.org/html/2604.16989#bib.bibx52)\] 呈现了一系列案例研究，其中 Google 的 Gemini Deep Think 解决了数学、理论计算机科学与物理学领域的开放性问题。
- • Bubeck 等人 \[BCE+25 (https://arxiv.org/html/2604.16989#bib.bibx3)\] 记录了实验过程，其中 OpenAI 的 GPT-5 参与了数学、物理和计算机科学研究。

本文进一步提供了该方向的佐证。Bolzano \[Bol25b (https://arxiv.org/html/2604.16989#bib.bibx10)\] 是一个面向数学研究的开源 AI 系统，已向有兴趣的研究人员开放。该系统通过多轮交互（涉及多个证明者与一个验证者）开展问题研究。每个证明者和验证者均由最先进的 LLM（如 GPT、Gemini、Claude 或其他模型）实现。其架构详见第 2 节。我们利用 Bolzano 为数学和理论计算机科学中的六个问题提供了新结果。

#### Bolzano 的优势
在我们的案例研究中，Bolzano 作为生成具有数学意义的中间研究步骤的工具最为有效：它尤其擅长寻找反例和障碍结构，提出具体的构造与组件（gadgets），或将已知的基例或较简单的证明模板推广至更一般的命题。这与 \[WCAJ+26 (https://arxiv.org/html/2604.16989#bib.bibx52), BCE+25 (https://arxiv.org/html/2604.16989#bib.bibx3)\] 的发现一致。在其中一种情形下，Bolzano 自主提供了一个硬度（hardness）证明及针对受限类问题的多项式时间算法，并纠正了人类提供的原始问题陈述中的一处小错误。

#### 局限性
本工作存在几点局限。首先，我们没有提供 Bolzano 与单会话聊天机器人交互之间的全面对比；虽然原则上可行，但在包含六个问题的案例研究中难以严谨执行，且多智能体架构相对于直接使用底层模型的优势尚未量化。其次，很难清晰剥离人类与 AI 的贡献；即便选择正确的研究方向也是一项非平凡的人类输入。

#### 已解决的问题
我们记录了 Bolzano 解决或取得进展的六个数学与理论计算机科学问题。这些成果要么由 AI 独立完成，要么由领域专家数学家与计算机科学家协作完成。对每个问题均附有讨论。相应的正式结果证明于本文附录或独立论文中。

表1：根据 Feng 等人 \[F+26b (https://arxiv.org/html/2604.16989#bib.bibx21)\] 提出的分类法，按重要性和自主性对我们的成果进行分类，范围涵盖至里程碑式的突破（landmark breakthrough）。自主性等级从 H（以人类为主，AI 为辅）经 C（人机协作）至 A（基本自主）。
1. **复杂性理论：** 我们构造了一个黑盒分离结果，表明 PWPP 对自适应图灵归约不封闭（第 3.1 节）。人类输入提出了该问题，Bolzano 返回证明后，人类研究者建议保持主要结构（展示 PWPP 不封闭的相同问题选取）但尝试不同的分析策略，随后 Bolzano 基本完成了证明。
2. **加性组合数学：** 我们给出了一个用单一瓦片平铺 $\mathbb{R}^2$ 的例子，展示了即将发表的一篇论文 \[dDGGM26 (https://arxiv.org/html/2604.16989#bib.bibx17)\] 中所述技术的局限性（第 3.2 节）。
3. **密码学：** 我们在标准模型下证明了多多项式、多点 KZG 批量处理的特殊有效性（special soundness）（第 3.3 节）。人类研究者提出了协议变体并提供了一个更简单的基例证明作为背景。Bolzano 在六轮交互内找到了完整证明，生成了长篇但基本完整的正式论证。
4. **数据结构：** 我们证明了堆的两个“最坏情况之外”（beyond worst-case）性质是等价的（第 3.4 节）。这最初由一位人类研究者在一项未公开项目中证明。Bolzano 独立重新证明了该等价性，并独立提出了更强的命题及其证明。
5. **组合数学：** 我们驳回了来自 KAMAK 2020 研讨会 \[Krá20 (https://arxiv.org/html/2604.16989#bib.bibx38)\] 的一个关于函数原像划分的猜想。此外，Bolzano 建立了修正后的假设并为其证明了若干边界界限（第 3.5 节）。
6. **计算复杂性：** 我们确定了基于 KKOS 文化动力学模型 \[KKOS16 (https://arxiv.org/html/2604.16989#bib.bibx37)\] 的优化问题的复杂度（第 3.6 节）。一般图上的判定问题是 NP 完全的；对于森林（forests），我们给出了一种多项式时间算法。Bolzano 在此过程中完全自主工作，还纠正了原始问题陈述中的一处小错误。

总体而言，我们的经验在几个方面与 \[WCAJ+26 (https://arxiv.org/html/2604.16989#bib.bibx52)\] 和 \[BCE+25 (https://arxiv.org/html/2604.16989#bib.bibx3)\] 的发现平行。LLM 在生成候选证明、构造反例以及建立跨领域联系方面表现卓越。截至 2026 年初，人类的指导在问题筛选、高层战略制定和验证方面仍然不可或缺。

#### 相关工作
近期研究开始记录 LLM 在数学与科学研究中的应用。GPT-5 已被证实可参与数学、物理及其他科学领域的研究，包括解决开放性问题与改进常数界限 \[BCE+25 (https://arxiv.org/html/2604.16989#bib.bibx3)\]。类似结果也在 Gemini 上有所报道 \[WCAJ+26 (https://arxiv.org/html/2604.16989#bib.bibx52)\]。Aletheia \[F+26b (https://arxiv.org/html/2604.16989#bib.bibx21)\] 是一种基于“生成器-验证者-修订者”循环的数学研究智能体，曾自主解决过一系列研究级问题，其中包括在首次证明挑战（First Proof challenge）\[FJhK+26 (https://arxiv.org/html/2604.16989#bib.bibx24)\] 的 10 道题目中成功解答了 6 道。First Proof \[ABH+26 (https://arxiv.org/html/2604.16989#bib.bibx1)\] 是一项包含 10 道来自 11 位数学家未发表论文中研究级问题的基准测试；OpenAI \[Ope26 (https://arxiv.org/html/2604.16989#bib.bibx45)\] 报告至少产生了 5 个高度可信的解。AlphaEvolve \[N+25 (https://arxiv.org/html/2604.16989#bib.bibx44)\] 已应用于 67 个问题 \[GGSTW25 (https://arxiv.org/html/2604.16989#bib.bibx26)\]，主要集中在常数优化与构造搜索领域，专家提示提升了效率但未显著提升性能上限。FunSearch \[RPBN+24 (https://arxiv.org/html/2604.16989#bib.bibx48)\] 将 LLM 与评估器配对形成进化循环，已在组合数学与算法领域产出新成果。许多系统致力于自动化定理证明与形式化验证。AlphaGeometry \[TWL+24 (https://arxiv.org/html/2604.16989#bib.bibx49)\] 通过神经符号引擎解决奥林匹克几何题。众多近期系统聚焦于 Lean 定理证明助手，包括 AlphaProof \[HMS+25 (https://arxiv.org/html/2604.16989#bib.bibx31)\]（通过强化学习达到 IMO 奖牌级水平）、Hilbert \[V+25 (https://arxiv.org/html/2604.16989#bib.bibx51)\]（结合非正式证明草稿与形式化验证）、Aleph Prover \[Log25 (https://arxiv.org/html/2604.16989#bib.bibx40)\]（形式化定理证明器，在 PutnamBench 中领先）、Ax-Prover \[B+25 (https://arxiv.org/html/2604.16989#bib.bibx2)\]（面向量子物理与抽象代数），以及低成本自动形式化一本 13 万行拓扑教材 \[Urb26 (https://arxiv.org/html/2604.16989#bib.bibx50)\]。我们将形式化验证视为对我们方法的补充：Bolzano 依赖非正式证明生成后再经专家验证，该方法目前覆盖范围更广但保证较弱。一项针对 1000 个问题上超过 5000 份 LLM 生成证明的大规模评估 \[D+25 (https://arxiv.org/html/2604.16989#bib.bibx16)\] 发现，非正式证明生成的性能显著强于形式化证明生成。数学推理的多智能体架构已在多个方向得到探索，包括多智能体辩论、逐步验证、迭代自我完善以及用于问题求解的 LLM 脚手架 \[DLT+23 (https://arxiv.org/html/2604.16989#bib.bibx18), G+25 (https://arxiv.org/html/2604.16989#bib.bibx25), HY25 (https://arxiv.org/html/2604.16989#bib.bibx33), MTG+23 (https://arxiv.org/html/2604.16989#bib.bibx43)\]。2025 年底，开放的 Erdős 问题成为测试 LLM 数学能力的试验场，各模型产出了先前未解决问题的一些原创证明 \[PSV26 (https://arxiv.org/html/2604.16989#bib.bibx47), F+26a (https://arxiv.org/html/2604.16989#bib.bibx20)\]；然而，迄今解决的难题通常仍易于采用直接技巧处理 \[F+26a (https://arxiv.org/html/2604.16989#bib.bibx20)\]。

#### 文章结构
第 2 节描述了 Bolzano 的架构与设计。第 3 节呈现每个已解决的问题，包括问题陈述、背景、人机协作讨论及 Bolzano 对话记录链接。证明不在独立论文中的，完整版见附录。所有证明均已获领域专家验证。

## 2 Bolzano

Bolzano 是一款研究工具，可在 https://bolzano.app/ 获取。它提供了一套自动化流水线，包含*证明者（prover）*、*验证者（verifier）*和*总结者（summarizer）*智能体，旨在迭代性地调查数学研究问题。在本节中，“智能体”指代一个可调用函数，它会向 LLM 发起预配置请求，附带指定研究身份、任务与目标的自定义提示词。

#### 整体架构
我们将 Bolzano 流水线的一次迭代称为一个*研究回合（research round）*。它涉及并行运行 $n$ 个*证明者智能体*，随后由一个*验证者智能体*进行审核，最后由一个*总结者智能体*收尾。研究回合并行执行；回合之间，调查状态会保存在三个人类可读的文件中。

#### 智能体
*证明者智能体*的任务是构思证明思路、寻找反例、证明特殊情况、识别错误并撰写证明。*验证者智能体*负责检查证明者的工作——识别错误与缺乏依据的步骤，将思路整合为可行的解决方案——并且是唯一被允许决定哪些内容写入知识库文件的智能体。*总结者智能体*为后续使用者和其他智能体生成每个研究回合的精简摘要。

#### 知识库文件
在研究回合之间，我们维护三个充当持久知识库的文件。*笔记（notes）*文件聚合洞见、失败的尝试、猜想及简化证明。*证明（proofs）*文件维护严格且细节完整的正式证明。*输出（output）*文件为人类研究者提供当前状态的简短摘要。所有智能体均读取这些文件，但仅有验证者拥有写入权限。

#### 模型多样性
Bolzano 允许用户为每个证明者智能体选择不同的 LLM。由于各模型的训练数据存在差异，这似乎能激发更多样化的解题路径。该策略也被报道有助于缓解“自我偏好偏差”（self-preference bias）\[PBF24 (https://arxiv.org/html/2604.16989#bib.bibx46)\]。

#### 人类引导
在研究回合之间，用户可提供额外指令以引导调查方向。我们的经验表明，人类引导往往能带来更强的研究成果——例如，PWPP 的成果（第 3.1 节）就是在专家建议 Bolzano 尝试不同策略后获得的。

## 3 已解决的问题

本章收录由 Bolzano 解决的六个选定问题。对于每个问题，我们会讨论研究流水线中哪些部分由人类完成，哪些由 Bolzano 完成。我们始终附上包含该证明的 Bolzano 系统链接。但需注意，Bolzano 生成的证明并非直接可用于发表。因此，我们要么在相应附录中添加经专家验证的正式证明，要么链接至包含该证明的独立论文。

### 3.1 PWPP 自适应与非自适应的黑盒分离 – Pavel Hubáček

复杂性类 PWPP（多项式弱鸽笼原理）\[Jeř16 (https://arxiv.org/html/2604.16989#bib.bibx35)\] 刻画了 TFNP 中的碰撞查找问题。其典范完备问题 Collision 要求：给定一个压缩电路 $C: \{0,1\}^n \to \{0,1\}^{n-1}$，寻找不同的 $x_1, x_2 \in \{0,1\}^n$ 使得 $C(x_1)=C(x_2)$。PWPP 包含所有可通过多对一归约归约至 Collision 的全总搜索问题。Jeřábek \[Jeř16 (https://arxiv.org/html/2604.16989#bib.bibx35)\] 证明了 PWPP 在非自适应图灵归约下是封闭的，即 $P^\parallel_{\mathrm{PWPP}} = \mathrm{PWPP}$：求解 $k$ 个独立准备的 PWPP 实例可归约为单次碰撞查询。TFNP 子类的一个基本结构性问题是：它们是否在自适应图灵归约下保持封闭？在自适应归约中，后续的预言机查询可能依赖于之前的回答 \[BJ12 (https://arxiv.org/html/2604.16989#bib.bibx8)\]。对于多个类（例如 PLS、PPA、PPAD），自适应与非自适应预言机访问是一致的 \[BJ12 (https://arxiv.org/html/2604.16989#bib.bibx8)\]，而与之相关的类 PPP（多项式强鸽笼原理），Fleming 等人 \[FGPR24 (https://arxiv.org/html/2604.16989#bib.bibx23)\] 证明了黑盒分离结果，表明其对图灵归约不封闭。结合 Bolzano，我们在 \[Hub26 (https://arxiv.org/html/2604.16989#bib.bibx32)\] 中通过引入 Bolzano 建议的一个自然自适应任务 NestedCollision，解决了黑盒设定下 PWPP 的类比问题，该任务要求