当AI开始啃数十年的老骨头：北大团队用LLM攻克60年数学猜想，将斯坦纳比推向极限

导语：北大王立威团队利用崭新工具，一举改写尘封60年的几何猜想纪录，让AI以全新姿态深入前沿数学腹地。

在科技圈，大语言模型在标准化数学竞赛中考出好成绩已经算不上太新鲜的头条了。公众对AI的认知正在逐渐产生脱敏反应。但如果我们将目光移向真实的学术前沿，让AI去解一解那些尘封了半个多世纪、让几代数学家一筹莫展的纯数学猜想，结果会怎样？

最近，来自北京大学的王立威教授团队给出了一个令人振奋的答案。他们利用一套极其精巧的LLM协同推理框架，直接把起源于1968年的知名几何难题——吉尔伯特-波雷克猜想（Gilbert-Pollak Conjecture，即斯坦纳比猜想）的二维平面下界，从沿用了近四十年的 0.824 大幅提升到了 0.8559。

这已经不仅仅是常规意义上的学术微调，这个数字距离该猜想的终极目标 $\sqrt{3}/2 \approx 0.8660$ 仅剩不到 0.01 的距离，几乎是探手可得。更有说服力的是，这一研究进展已经被著名数学大师、菲尔兹奖得主陶哲轩（Terence Tao）正式收录到他维护的“组合数学优化中的常数列表”中（编号为 Problem 43）。目前，这项突破性工作已被 ICML 2026 接收，相关的算法和数学证明均已开源。

这项研究的背后是一支年轻且极具朝气的队伍。共同第一作者包括北京大学信息科学技术学院图灵班本科生柯绎思、疏彦凯，以及数学科学学院本科生黄天域；共同通讯作者为北京大学王立威教授与卡内基梅隆大学博士生盖景初；合作者还包括北京大学贺笛老师。

什么是吉尔伯特-波雷克猜想？一个“修铁路”的最优解游戏

吉尔伯特-波雷克猜想由贝尔实验室的科学家 Edgar Gilbert 和 Henry Pollak 在 1968 年正式提出。尽管听上去名字高深，但它的物理模型却相当接地气，可以被通俗地理解为一类“铁路线网规划”的最优解问题。

想象一下，我们需要在平原上修建铁路，连接已知的 $n$ 个城市。你有两种规划方案：第一种是只能在城市之间建路，把所有城市连通且总里程最短，这在数学上叫做最小生成树（MST）；第二种是允许我们在田野间任意位置额外修几个“转运中心”（中转站），通过这些中转站来进行铁路线的交叉和重连，从而让整体路程缩短，这种做法被称为最小斯坦纳树（SMT）。

显然，因为有了转运中心这一维度的变量，最小斯坦纳树的长度在大多数情况下都会比最小生成树更短。但吉尔伯特和波雷克在1968年大胆猜测：不管这群城市怎么摆放，最小斯坦纳树的长度再怎么缩水，也绝不可能低于最小生成树长度的 $\sqrt{3}/2$（约为 0.8660）倍。这个临界比例就是著名的“斯坦纳比”。

半个多世纪里，包括美国数学学会（AMS）前主席 Ronald Graham 以及多名顶尖科学家都曾对该猜想发起过冲击。然而，自上世纪80年代人类将斯坦纳比的下界证明推进到 0.824 之后，这个领域便陷入了长达近 40 年的死寂。前人留下的理论大厦停滞于此，再无实质性突破。

AI4Math的破局点：为什么不能让大型语言模型硬写证明？

目前的AI在解决这类顶级学术难题上面临一个尴尬的瓶颈。对于像IMO竞赛这样长度较短、逻辑紧凑的证明，模型尚可应付；而对于长达数十页甚至上百页、充满新颖数学概念的系统性证明，LLM一旦长篇大论，逻辑幻觉的缺陷就会被成倍放大。

让AI直接去硬写几十页的严密数学推导显然是不现实的。北大王立威团队敏锐地意识到，必须找到一种数学上的转换方法，为LLM搭建一个“结构上可验证”的推理空间。

回顾前人的思路，数学家们在解决类似问题时普遍采用了归纳法：对于一棵错综复杂的斯坦纳树，如果可以每次从中摘除（prune）一小部分局部点，并把剩下的点重连，那么只要“剩下部分符合比例（归纳假设）”+“摘除动作产生的前后差量符合比例”，就能合并推进最终的证明。写成具体的数学表达就是：

$$SMT(V) \ge \rho \cdot MST(V) + F(P)$$

在这里，核心的数学工具被称为验证函数（Verification Functions, $F$）。不同的分裂和摘除树的方式，就对应着不同的验证函数 $F$。如果能够找到足够好的验证函数 $F$，使之能完美覆盖所有可能的树形态，我们就能把下界 $\rho$ 推得更高。

在此之前，人类数学家绞尽脑汁也只手动构建了 10 种不同的验证函数，从而锁定了 0.824 的下界。那么，如果用LLM作为计算和创意的杠杆，去搜索 1000 种、乃至上万种验证函数，是否就能冲上新的理论高峰？答案是肯定的。

巧妙的破局方案：“搭积木”防错与“靶向靶心”的瓶颈反馈机制

为了让这个设想落地，北大团队并没有直接放任LLM胡乱生成公式，而是精心编排了一套自动化的工业级交互系统。核心步骤如下：

1. 引入 Reward Model 与自动化分治

如何快速知道当前生成的验证函数能不能包住所有的树形态？这其实可以归结为一个 max-min 问题。以前人类数学家需要用脑力进行复杂的启发式参数空间划分，而团队设计了一个 Reward Model，配合分治算法，用代码实现了全自动化的参数拓扑覆盖判定，彻底解放了双手。

2. 建立“搭积木”式的引理合成机制

语言模型天然存在严谨度缺陷，如何确保它寻找到的每一个验证函数在数学上都是100%正确的？研究人员做出了一个绝顶聪明的设定：把寻找函数的过程，转化为寻找两类特征引理（Trapped Regular Point Lemma 与 4-Point Steiner Tree Lemma）。

他们将几何性质拆解为好几种“原子规则”（A类规则代表斯坦纳树的一些本质几何定理，B类规则代表节点合理存在的物理边界条件）。LLM的任务类似于玩积木——它只需要挑选两三个合适的规则拼在一起，去询问专业的数学符号计算软件 Mathematica：“在什么条件下，这些 A 规则能推演出 B 规则？”由 Mathematica 在底层执行符号化简和保对推理。这样一来，无论LLM怎么“异想天开”，其产出的引理都在公式逻辑上坚如磐石。

3. 首创“瓶颈（Bottleneck）”反省反馈机制

在海量尝试中，LLM极易重复生成那些毫无用处或者已经重复的低价值函数。为了避免这种无意义的计算浪费，研究团队提出了一个极富洞察力的机制——瓶颈区域检测。

• 每当一轮迭代结束，系统会强行把预期的下界 $\rho$ 向上微调一个小量 $\delta$ ；
• 此时旧的函数群必然无法完全支持这套新标准，Reward Model 在计算中会显式地反馈出“哪些几何参数区间没有被妥善覆盖”；
• 系统将这些具体的几何参数区域打包作为“瓶颈信号”，投喂给下一轮的 LLM Agent；
• AI 带着极为明确的“补天”靶向，精准构思新的引力结构来填补漏洞。

通过这套闭环机制，整个系统仿佛拥有了敏锐的自我审视能力，只用了大约 10 轮的大模型调用迭代，就势如破竹般地完成了海量函数的发掘与收敛，成功将二维斯坦纳比下界稳定印刻在了 0.8559 这一历史性高位。

人机协同展现出的未来范式

这项令人振奋的工作不仅在数学上突破了近40年的坚冰，更重要的是，它为AI4Math的研磨提供了一个全新的标本：

面对极其复杂、高难度的科学猜想，我们不应该奢求AI像人类天才一样，灵光一闪凭空写出一整本完美的推导手稿。更可行、也更有威力的做法，是由人类构建出坚实好用的“数学积木和保对容器”，把纯粹的发散性创意和地毯式搜索留给AI，再让符号计算软件与反馈闭环来做无情的审查官。

这种人机智慧的有机咬合，或许正是我们在迈向通用人工智能（AGI）的漫长道路上，探寻真理最自然、也最强大的姿态。