本文的共同第一作者包括北京大学信息科学技术学院图灵班本科生柯绎思、疏彦凯、数学科学学院本科生黄天域；共同通讯作者为北京大学王立威老师、卡内基梅隆大学博士生盖景初；其他作者还包括北京大学贺笛老师。

近期，LLM 已经在 IMO 上取得了很好的成绩，在一些研究级数学上（如短程证明、组合构造）也有所进展。但如果真正让 LLM 去处理提出数十年的数学猜想，结果会是如何？在本工作中，北大王立威教授团队构建了一套基于 LLM 的框架，聚焦Gilbert-Pollak 猜想（斯坦纳比猜想），成功将二维平面的斯坦纳比从 1985 年证明的 0.824 改进到了，距离猜想目标仅差 0.01，一步之遥！

该进展已被陶哲轩 Terence Tao收录组合数学优化中的常数列表中！问题编号 43。

仓库链接：https://github.com/teorth/optimizationproblems

这个问题有多大影响力？在上个世纪，该问题由贝尔实验室科学家 Gilbert 和 Pollak 提出。著名数学家、美国数学学会（AMS）前主席 Ronald Graham（葛立恒）、美国国家科学院院士 Fan Chung（金芳蓉）都对该问题进行过系统深入的研究。1990 年，堵丁柱教授和 Frank Hwang（黄光明）研究员进行了一系列相关研究，曾被誉为 1989 年 - 1990 年度美国离散数学界和理论计算机科学界重大成果。围绕该问题的研究论文众多，是一个饱受数学家关注的猜想。

目前该工作已被 ICML 2026 接收，相关代码和数学证明均已开源。

论文标题：Towards Solving the Gilbert-Pollak Conjecture via Large Language Models论文地址：https://arxiv.org/abs/2601.22365项目仓库：https://github.com/keyisi2006/Steiner-Ratio

困扰人类 60 年的 Gilbert-Pollak 猜想

形象点说：给定平面上 n 个城市，最小生成树（MST）就是修建 n - 1 条铁路将它们连起来。最小斯坦纳树（SMT）就是可以额外修建若干个中转站，再修建铁路将它们连起来。可以看出，合适地建立中转站会让路程变短，但猜想指出：并不会短太多。

问题 1：直接写成 prompt 问 LLM，行不行？

之前一系列 AI4Math 的工作，要么是数学证明的长度较短（如 IMO 问题），要么是针对构造性的、非严谨证明性的组合构造问题。

让 LLM 直接去写几十页的严谨数学证明，还要有创新性，对于目前 LLM 能力来说为时过早。为了解决斯坦纳比猜想，必须减少证明长度，或者向构造性的方向转换。

步骤 1.1：看看人类数学家怎么做？

回顾人类数学家的工作，发现大家都是采取了归纳法：对于一棵很大的斯坦纳树，只去考虑一个局部，从中摘除（prune）掉一小部分的点，并将剩下的点重连成斯坦纳树。

那么，只要剩下的部分满足比例（归纳假设）+ 摘除过程的变化量满足比例，就可以合并得到原问题满足比例！写成一行公式就是：

从而，问题的关键就是找到更好的摘除 / 分割树的方式。

步骤 1.2：整理一下？这就是 Max-Min 问题！

本工作中提出了一个叫做验证函数（verification functions）的数学工具，一个验证函数就代表了一种分割树的方式。归纳法就是要求：任意的树形态，存在一种分割，使得比例成立。其实这就是一个max-min 问题：最大的树形态 w ——最小的验证函数 F。

人类数学家尝试了 10 种不同的 F，可以得到 0.824 的下界。如果 LLM 能帮助人类尝试 1000 种不同的 F，就有机会得到更好的下界！

本工作设计了一个Reward Model，自动化了这一 max-min 问题的求解过程，通过证明单调性，并配合分治法，为所有树形态 w 找到一个验证函数 F 进行覆盖。以前人类数学家需要手动进行启发式的参数空间划分，现在一个代码自动搞定。下图是假设参数空间是 2 维的一个例子：

至此，LLM 不再需要证明完整的猜想，它只需要找到更多的验证函数 F，再与 reward model 交互就可以了！

问题 2：找来的这么多 F，正确性怎么保证？

想要生成 1000+ 个 F，只需要反复调用 LLM 即可。但基于自然语言推理的 LLM，你能相信它的严谨性吗？如果让人类一个一个检查，时间开销不可估量，难以 scale up。

因此，我们必须让 LLM 在正确性可验证的框架中运行。

步骤 2.1：给 LLM 一个引理模板

本工作通过数学变换，证明了一个事实：找更多的 F 函数，可以通过找两类引理的方式实现：一类是 Trapped Regular Point Lemma，另一类是 4-Point Steiner Tree Lemma。

LLM 只需要负责填入结构化的参数，通过代码片段进行表达，系统就可以通过翻译（嵌入代码片段）的方式产生一系列合法的 F。以第 1 类为例，这个翻译过程可以是构造分段函数：

步骤 2.2：光有模板还不够，让 LLM 彻底「搭积木」

生成结构化的代码片段仍然可能会出错。必须要让 LLM 像「搭积木」一样，拼凑人类提供的规则（rules），让数学软件 Mathematica「合成」保对的引理，才能从根本上保证正确性。

以第 1 类引理为例，本工作提出了 A、B 两类规则，分别代表斯坦纳树必须满足的性质，和确保点存在性的条件。LLM 要做的，就是去选择 2 - 3 个规则，调用 Mathematica 去化简「什么条件下，若干个 A 能推出一个 B」。

通过这种方法，LLM 能在多轮的 tools 调用中，充分探索这个推理空间。而且这是保对的——任何的创意搭建，都不会产生逻辑的错误。

问题 3：正确的 F 就能提升下界吗，有没有「浑水摸鱼」？

目前为止，系统看似很完美，实则还有一个隐藏的大问题：只是重复运行，生成 1000+ 个 F，很可能其中很多是平凡的甚至重复的，根本对斯坦纳比没有提升！

如何让 LLM 真正生成有效的 F？必须给它针对性的迭代引导信号

步骤 3：针对问题的瓶颈反省机制

本工作提出了瓶颈（bottleneck）的概念：在 reward model 运行完成后，把得到的提升一个小量 δ（比如 0.0001），再让 reward model 运行——此时必然反馈失败，未被 F 覆盖的部分的 bounding box，就是瓶颈区域。

换言之，瓶颈就是让 ρ += δ 必须克服的参数区域。在下一轮生成 F 时，LLM 必须确保能够覆盖瓶颈区域。从而为每一轮的高效提升提供了保障。

迭代系统框架和成果

通过「重复生成 Reward → 确定瓶颈 → LLM Agent 提出引理 → 翻译并开始下一轮」这个迭代范式，系统成功在 ~10 轮迭代中，将斯坦纳比改进到了 0.8559。最终的成果通过了人类的检查。

本文基于 GPT-5 系列构建了系统，并验证了模型鲁棒性：其余模型如 Gemini 3 和 Claude 4.6 均可得到类似的结果。下图展示了迭代轮次和斯坦纳比的关系。

结语

本工作证明了 LLM 有能力为研究级数学提供帮助，但要设计合适的运作框架。

在这个过程中，人类的 insight 仍然是必要的。同时，人类检查也是必不可少的部分。

如果要用 LLM 去处理其他数学问题，可以参考的内容包括，设计一个「搭积木」式的结构化推理空间，以及设计瓶颈反省机制。