💻 computer science

Towards Solving the Gilbert-Pollak Conjecture via Large Language Models

本文提出了一种利用大语言模型生成并优化可执行几何引理的 AI 系统，该系统的成果将斯坦纳比率的已认证下界提升至 0.8559，并在解决长期悬而未决的吉尔伯特 - 波拉卡猜想方面取得了重大进展。

原作者： Yisi Ke, Tianyu Huang, Yankai Shu, Di He, Jingchu Gai, Liwei Wang

发布于 2026-05-22

📖 1 分钟阅读☕ 轻松阅读

原作者： Yisi Ke, Tianyu Huang, Yankai Shu, Di He, Jingchu Gai, Liwei Wang

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象你是一名城市规划师，试图用道路连接一组房屋。你有两种方法可以实现这一目标：

直接方式（最小生成树）：你直接将房屋彼此连接。你不能建造任何新的交叉口；你只是在现有的房屋之间画线。
智能方式（斯坦纳最小树）：你被允许在城市中任何位置建造新的、不可见的交叉口（称为斯坦纳点）。通过添加这些额外的枢纽，你通常可以创建一个比直接方式更短、使用更少沥青的网络。

核心问题：
“智能”方式比“直接”方式能短多少？

1968 年，数学家吉尔伯特（Gilbert）和波拉克（Pollak）提出了一个著名的猜想。他们说：“无论房屋如何排列，‘智能’方式的长度永远不会低于‘直接’方式长度的86.6%（具体为 $\sqrt{3}/2$ ）。”

几十年来，数学家们试图证明这一点。他们设法证明了其长度至少为直接方式的82.4%，但在此处陷入了困境。这个数学问题就像一个巨大的、纠缠不清的绳结，人类的大脑无法解开，因为需要检查的形状和角度太多了。

新方法：AI“引理工厂”
这篇论文描述了一个新系统，其中人工智能（大型语言模型）帮助解开这个绳结。但人工智能并不试图一次性解决整个问题——那就像要求机器人在一秒钟内写完一本小说。相反，研究人员为人工智能建立了一个专门的工厂。

以下是该系统的工作原理，使用一个简单的类比：

1. “证明”是一个巨大的拼图

为了证明 86.6% 的规则，你必须检查道路网络可能呈现的每一种形状。逐一检查是不可能的。
相反，数学家使用一种称为归纳法的策略。他们说：“如果我们能证明，每当我们从网络中切掉一块，剩余部分仍然遵循规则，那么整体就遵循规则。”

为了做到这一点，他们需要称为引理的微小、特定规则。将引理想象为一个完美的拼图碎片，它说：“如果道路看起来像这样，那么我们可以肯定长度至少是那样。”

2. 人工智能的工作：制作拼图碎片

研究人员没有要求人工智能解决整个拼图。他们要求它做一件小得多的事情：编写生成这些拼图碎片的代码。

约束：人工智能被告知：“你只能编写描述特定几何形状（如‘被困规则点’或'4 点树’）的代码。”
输出：人工智能编写了一个小程序（一个“引理”），内容是：“如果道路长度为 $X, Y, Z$ ，那么总长度受 $W$ 限制。”
安全网：人工智能的代码不会被盲目信任。它被输入到一个严格的数学计算器中（像 Mathematica 这样超精密的计算器）。如果计算器说代码有误，人工智能会重试。如果它说“正确”，该碎片就会被添加到集合中。

3. “反思”循环：寻找薄弱环节

这是巧妙之处。该系统并非随机猜测。

系统尝试使用当前的拼图碎片集合来证明 86.6% 的规则。
它失败了。它发现了一个特定的“瓶颈”——一种奇怪的形状，当前的碎片无法适应。
系统告诉人工智能：“嘿，你在这里失败了。看看这个特定的形状。去写一个新的拼图碎片，正好适合这个位置。”
人工智能生成一个新的引理，计算器对其进行检查，如果有效，系统再次尝试。

这就像一款电子游戏，你不断撞墙，而游戏会确切地告诉你在哪里建桥才能通过。

结果

经过大约 10 轮这种“尝试、失败、反思、改进”的循环后，系统建立了一个极其强大的拼图碎片集合，最终证明了一个新的、更严格的规则：

智能方式的长度至少是直接方式长度的 85.59%。

这比保持了近 40 年的 82.4% 的旧纪录有了巨大的提升。

为什么这很重要（根据论文）

成本低廉：整个研究项目仅花费了数百美元的计算机时间。
速度快：人工智能仅用了几天时间的“思考”（以及数千次模型调用）就完成了人类几十年无法完成的工作。
严谨性：人工智能并没有仅仅“猜测”。它生成了经过数学验证、100% 正确的代码。最终的证明是一个标准的数学证明，独立于人工智能而成立。

简而言之：研究人员没有要求人工智能成为一名天才数学家。他们要求它成为一名聪明、不知疲倦的助手，构建微小的、经过验证的工具（引理），以帮助人类解决一个此前被认为过于庞大而无法攻克的难题。他们将一个“黑盒”人工智能转变为一个透明的、逐步推进的发现引擎。

技术摘要：迈向通过大语言模型解决吉尔伯特 - 波拉卡猜想

1. 问题陈述

本文探讨了吉尔伯特 - 波拉卡猜想（Gilbert-Pollak Conjecture，1968 年），这是组合优化与计算几何领域的一个开创性未解难题。该猜想断言，对于欧几里得平面中的任意有限点集，斯坦纳最小树（SMT）长度与欧几里得最小生成树（MST）长度之比的下界为 $\sqrt{3}/2 \approx 0.866$ 。该比率被称为斯坦纳比。

尽管该猜想已针对少量点（ $n \le 6$ ）的情况得到验证，但针对任意 $n$ 的通用下界自 1985 年以来一直停滞不前。此前的最先进下界由 Chung 和 Graham（1985 年）确立，数值为 0.824。由于分析所需的拓扑结构组合爆炸，以及人工推导中涉及的几何验证难以处理，研究进展陷入停滞。

作者探讨了大语言模型（LLM）——这些模型已在竞赛级数学中展现出能力——能否被扩展用于解决此类开放的研究级猜想。他们指出，由于搜索空间巨大且不受约束，以及训练数据中缺乏研究级概念，直接提示 LLM 求解该猜想往往会导致幻觉和逻辑漏洞。

2. 方法论

作者提出了一种新颖的 AI 系统，该系统避免了直接端到端的证明生成。相反，该系统将问题分解为由验证函数和反思驱动的结构化、迭代发现过程。

2.1. 验证框架

核心数学策略依赖于基于归纳的归约论证（Du & Hwang, 1983）。要证明下界 $\rho$ ，必须证明对于任何几何构型 $w$ ，都存在一种树的“分割”，使得特定的分割函数 $F_\tau(w, \rho) \le 0$ 。

验证函数：为了使连续极小极大问题变得可处理，系统引入了验证函数。这些是满足特定结构约束（沿坐标轴的单峰性）的分割函数的上界。
顶点最大性质：一个关键的理论贡献是证明了对于这些验证函数，其在有界超矩形上的全局最大值是在其某个顶点处取得的。这将无限连续域上的验证简化为有限个顶点的检查。
分支定界：系统采用分支定界算法递归地划分参数空间，在顶点处验证条件，并检查无界区域的单调性。

2.2. LLM 代理与引理生成

系统并非要求 LLM 证明猜想，而是 tasked 其生成作为可执行代码实现的规则约束几何引理。搜索空间被缩小到两种特定类型的引理：

受限正则点引理：证明在特定线性约束下，一个隐式正则点被限制在一个有界多边形区域内，从而允许进行距离界定。
有效 4 点斯坦纳树引理：证明在特定正交凸条件下，特定的 4 点斯坦纳树拓扑是有效的，从而允许进行精确的长度计算。

LLM 代理在一个循环中运行：

选择：它从预定义集合中选择相关的几何谓词（A 类：内在性质；B 类：充分受限条件）。
推导：它使用符号工具（Mathematica）推导这些谓词的含义。
简化：它将复杂的代数区域简化为适合奖励模型的线性或正交凸约束。
编码：它将推导出的条件输出为 C++ 函数（如 X_cond、AX_upper_bound 等），这些函数充当验证函数。

2.3. 迭代反思机制

系统利用有针对性的反思机制来克服瓶颈：

评估：奖励模型尝试认证一个候选下界 $\rho$ 。
瓶颈识别：如果验证失败，系统会识别出特定的“瓶颈区域”（一组未认证的超矩形），即当前引理不足以覆盖的区域。
反馈：该区域被转换为结构化提示，指示 LLM 生成专门针对该瓶颈几何约束的新引理。
细化：新引理经过验证并被添加到验证函数集中，随后过程重复。

3. 主要贡献

用于理论发现的新颖 AI 系统：本文展示了一个系统，成功自动化了针对数十年未解难题的中间几何引理的发现，超越了标准的竞赛级问题解决。
验证函数与顶点性质：作者正式定义了验证函数，并证明了“顶点最大性质”，这使得在连续域上对下界进行严格且计算上可处理的验证成为可能。
分解策略：通过将猜想分解为生成特定的、规则约束的引理（受限点和有效 4 点树），而非完整的证明，该系统有效地管理了搜索空间并最大限度地减少了幻觉。
瓶颈驱动的反思：引入了一种反思机制，明确识别并针对阻碍进一步改进的几何区域，而不是依赖通用的自我修正。

4. 结果

新的下界：该系统成功将斯坦纳比的认证下界从 0.824（Chung & Graham, 1985）提升至 0.8559。
效率：整个研究工作仅需约 10 次 细化循环迭代。
资源使用：该过程涉及约 数千次 LLM 调用，在 4.6 小时的推理时间内消耗了约 50 万 token（每轮约 3.5 万）。总计算成本仅为数百美元。
鲁棒性：使用不同 LLM 骨干（GPT-5 和 Gemini 3 Pro）的实验得出了收敛至相同下界的一致结果，证明了该框架对模型选择的鲁棒性。
验证：所有生成的引理均经过人工检查以确保正确性，最终下界使用符号工具（柱形代数分解）在整个参数空间上得到了严格验证。

5. 意义与主张

本文声称展示了基于 LLM 的系统在高级数学研究中的巨大潜力，特别是在需要深刻几何直觉和组合搜索的领域。

可扩展性：作者认为，他们的方法提供了一种可扩展的范式，即 LLM 负责创造性搜索和引理生成，而符号工具负责形式化验证。这种分工利用了双方的优势。
可及性：总成本仅为数百美元，这项工作表明，LLM 辅助的理论研究对于没有巨额计算预算的研究人员来说也是可及的。
可推广性：作者提出了他们认为可推广到其他数学发现问题的两个设计原则：
1. 通过将问题分解为参数化引理而非端到端证明，来构建结构化的推理空间。
2. 通过将特定的瓶颈区域反馈给模型以指导针对性细化，来反思局部验证器的失败。

本文对最终结果保持了谦逊，指出虽然下界得到了显著改进，但猜想本身（0.866）仍未被证明。此外，作者承认了当前的局限性，例如依赖人工验证引理的正确性，以及符号验证（CAD）在更高维度或更复杂拓扑结构上的可扩展性问题。他们建议未来的工作可以涉及形式化证明助手（如 Lean），以实现完全自主的发现。