结果族 133：The computational complexity of Weisfeiler–Leman refinement · 学科：Theoretical computer science · 验证状态：暂无形式化证明，请以社区核验为准
判断两张图能否被 @@M@@k@@ 维 WL”对话”分开，照流程走一遍需要 @@M@@n^{O(k)}@@ 步。可万一有聪明算法根本不走这套流程呢？本文证明：没有——任何确定性算法最坏都得花 @@M@@n^{\Omega(k)}@@ 步，而且不借助任何未证明假设（不需要 ETH、P≠NP），是彻底无条件的结果，就连直径至多 2 的稀疏简单图上也不例外。
关键词卡片
@@M@@k@@-WL 等价判定（@@M@@k@@-WL equivalence）：判断两张 @@M@@n@@ 顶点图经 @@M@@k@@ 维对话后是否仍不可区分。看个具体例子
数字版定理：存在绝对常数 @@M@@c>0@@ 与 @@M@@k_0@@，使得对每个正确的确定性判定器 @@M@@A@@，
@@M@@DT_A(n)\ \ge\ n^{ck}\qquad\text{（每个固定 } k\ge k_0\text{，且每个足够大的 } n\text{ 都成立）}.@@
两个细节让这个下界格外”硬”：指数里的 @@M@@c@@ 与程序和 @@M@@k@@ 都无关；下界在每个足够大的图阶上成立，而不是只在无穷多个阶上——连”算法偶尔在某个大阶上特别快”的漏洞也堵上了。于是任何形如 @@M@@f(k)\,n^{g(k)}@@、@@M@@g(k)=o(k)@@ 的运行时间（例如 @@M@@n^{\sqrt{k}}@@）对足够大的 @@M@@k@@ 都不可能。
为什么值得关心
此前的 WL 难度结果要么只约束细化流程本身，要么依赖 ETH 这类假设；本文给出对一切算法无条件成立的硬下界，把姊妹篇的条件性结论变成了定理。
暂无形式化证明（AI 结果待核验）
第一级台阶
导读里的”聪明算法根本不走对话流程”可译成：对象是一个是/否问题——两张图在 @@M@@k@@ 维”染颜色、对答案”的对话后是否仍不可区分；照流程走一遍需要约 @@M@@n^k@@ 步，而真正要问的是：任何确定性方法，哪怕完全绕开这套流程，是否也逃不开随 @@M@@k@@ 线性增长的指数开销？本文的答案是”逃不开”，且不借助任何未证明假设。
第二级台阶
本科术语化：@@M@@k@@-WL 等价指两图稳定元组颜色直方图相同；判定器 @@M@@A@@ 对输入规模一致、但可任意依赖固定的 @@M@@k@@，@@M@@T_A(n)@@ 记其在 @@M@@n@@ 顶点图对上的最坏时间；计算模型为多带图灵机与对数字长 RAM。”无条件下界”意为不假设 ETH 或 P@@M@@\ne@@NP，仅凭对角化与显式归约成立。
第三级台阶
定理的语境：存在绝对常数 @@M@@c>0@@ 与 @@M@@k_0@@，使每个固定 @@M@@k\ge k_0@@、每个正确的确定性判定器都有 @@M@@T_A(n)\ge n^{ck}@@ 对每个足够大的 @@M@@n@@ 成立。”显式邻接矩阵输入”挡住了隐式表示转移难度的质疑；”确定性串行模型”挡住了随机化与非一致建议的越界；结论甚至在直径至多 2 的简单连通无色图上成立，joint 与 separate 两种约定通吃，从而排除一切 @@M@@f(k)n^{g(k)}@@、@@M@@g(k)=o(k)@@ 型运行时间。
本文无条件证明：对每个足够大的固定 @@M@@k@@，任何判定两张 @@M@@n@@ 顶点图是否 @@M@@k@@ 维 Weisfeiler–Leman 等价的确定性串行算法，最坏情形需要 @@M@@n^{\Omega(k)}@@ 时间；不依赖 ETH 等任何复杂性假设，且在直径至多 2 的简单连通无色图上已成立。
固定 @@M@@k@@ 时，@@M@@k@@-WL 等价的朴素判定耗时 @@M@@n^{O(k)}@@。要证明任何算法——哪怕根本不执行细化——都逃不开随 @@M@@k@@ 线性增长的指数，现有工具都不够用：Cai–Fürer–Immerman 的奇偶构造及 Grohe–Lichter–Neuen–Schweitzer 的压缩版本给出的是”需要多少轮细化”的下界，只约束细化过程本身；变维数下的 coNP 艰难与 EXPTIME 完全结果（Seppelt；Lichter–Raßmann–Schweitzer 等）量词不同，推不出固定维数的时间指数；Berkholz 关于存在博弈（existential pebble game）的无条件下界对应的是另一种博弈规则。因此本文自足地证明所需的博弈对应与完整归约。
定理：存在绝对常数 @@M@@c>0@@ 与 @@M@@k_0@@，使得对每个固定整数 @@M@@k\ge k_0@@ 与每个正确的确定性判定器 @@M@@A@@，存在 @@M@@n_0(A,k)@@，使 @@M@@T_A(n)\ge n^{ck}@@ 对每个整数 @@M@@n\ge n_0@@ 成立。要点：指数常数 @@M@@c@@ 与程序和 @@M@@k@@ 都无关；下界在每个足够大的图阶上都成立，而非只在无穷多个阶上——这排除了算法在稀疏的任意大阶上异常快的可能；模型覆盖多带图灵机与顺序对数字长 RAM（地址与字长 @@M@@O(\log(n+2))@@ 位，每条指令可在字长多项式时间内实现）；输入为显式邻接矩阵；即使算法只被要求在直径至多 2 的简单连通无色图上正确、且最坏时间只按该类输入计，下界依旧成立。joint 与 separate 两种替换约定都在结论之内。由此排除任何形如 @@M@@f(k)n^{g(k)}@@、@@M@@g(k)=o(k)@@ 的运行时间界。
证明按五级接口展开。第一步固定双射博弈（bijective game）对应：joint 约定的 @@M@@k@@-WL 等价恰对应 Duplicator 在 @@M@@k+1@@ 个对槽的双射博弈中获胜，separate 约定对应 @@M@@k@@ 个对槽。第二步是压缩一致性归约：考虑变量按地址 @@M@@\mathbf a\in[m]^r@@ 下标、取值于 @@M@@\mathbb F_2^{d_P}@@ 的实例，逐边弧一致（individual-edge arc consistency）指存在非空集合 @@M@@Q_{P,\mathbf a}@@ 使每条比较 @@M@@\phi_{e,0}(Q_{P,\mathbf a})=\phi_{e,1}(Q_{R,\boldsymbol\sigma_e(\mathbf a)})@@ 逐条成立；定理把这类实例转成两张同阶、连通、直径至多 2、阶为 @@M@@O(m^6)@@ 的无色图，使 Duplicator 获胜当且仅当弧一致成立。技术核心：位点块与方块只记录两个相邻坐标，只有凑满一整圈 @@M@@r@@ 个块的”缠绕”子集才暴露一个完整地址；Duplicator 的策略用”组件位移+角势”表示平移，非缠绕组件上的位移改变可被角势吸收而读出值不变，精确投影引理 @@M@@\mathcal H_U|_V=\mathcal H_V@@ 保证保留块逐块延拓。
第三步编码计算：单调电路用私有两坐标缓冲 @@M@@\{(z,z'):z+z'\in D\}@@ 实现单向传播——目的地被压成单点不会反向限制假源；再用 Cook 式局部更新规则把单带图灵机的时空表编码为按 @@M@@m@@ 进制数字寻址的电路，时间与位置的移位通过进位/借位分解写成有界多个乘积模式，得到”机器接受当且仅当两图不等价”，且图可从 @@M@@O(m)@@ 条一坐标表在 @@M@@O(n^4)@@ 时间内构造，无需枚举完整地址。
第四步是对角语言：沿 Hennie–Stearns 的填充对角化构造显式语言 @@M@@H_s@@，它有固定的单带判定器在 @@M@@O(m^{20s})@@ 步内可解，而任何正确的单带判定器在每个足够大的长度上最坏时间严格大于 @@M@@m^s@@。第五步是截断迁移：对长度 @@M@@m@@ 的词尝试区间 @@M@@[m^{20},(m+1)^{20})@@ 内的一切图阶，每阶给候选算法 @@M@@m^p@@ 步截断；若某个阶 @@M@@n@@ 上 @@M@@T_A(n)<n^{c_0k}@@，则所有长度 @@M@@m@@ 的词都能在截断内完成，拼出一个 @@M@@m^{D+50p}<m^s@@ 时间的 @@M@@H_s@@ 单带判定器，与第四步矛盾。参数取 @@M@@s=\lfloor r/1000\rfloor@@、@@M@@p=\lfloor s/1000\rfloor@@、@@M@@c_0=10^{-9}@@，两个严格缝隙恰好容纳全部构造与模拟开销。
本文为无条件结果，但未经形式化验证，请以社区核验为准。作者明确指出局限：为达到直径 2 而引入的通用枢纽顶点度数无界，本文不主张有界度数承诺；当 @@M@@r@@ 随输入增长时压缩构造不给出多项式编译。它与族 133 的姊妹篇互补：本文主定理取代 ETH 条件下界篇的条件性结论，而识别篇处理的是另一量词（识别）的 EXPTIME 完全性。按 OpenAI 官方声明，未经形式化的结果可能有问题。
问 1：证明中最脆弱的一步是什么？
答：压缩构造的反方向（第 2 节）：位移族须”精确投影”到更小块族的位移族上，每个已保留的赋值都可延拓。非缠绕组件上的位移变化可被角势吸收而读出值不变，凑满一圈 @@M@@r@@ 个块才恢复完整地址。若投影只”近似”而非精确，Duplicator 策略与弧一致的等价性即出现缝隙，全链断裂。
问 2：为什么必须强调”每个足够大的图阶”而不是”无穷多个阶”？
答：若下界只在稀疏的阶序列上成立，算法可以在这些阶之外异常快而仍逃过结论。论文用截断迁移补洞：在区间 @@M@@[m^{20},(m+1)^{20})@@ 内逐一尝试所有图阶并给 @@M@@m^p@@ 步截断，任何一个阶上的快算法都能拼出全长度上的快判定器，与对角语言矛盾。
问 3：与已有工作相比真正的新意是什么？
答：CFI 及其压缩版（GLNS）约束的是细化轮数，Berkholz 的无条件下界针对存在博弈——规则不同；变维数的 coNP/EXPTIME 结果量词不同。本文对固定维数、对一切确定性判定器给出无条件的线性于 @@M@@k@@ 的指数下界，且博弈对应是自足证明、不当黑盒。
问 4：无条件怎么做到的？大多数下界都要假设。
答：这里不用 NP 艰难性，而用时间层级式的对角化：沿 Hennie–Stearns 填充机器索引构造显式语言 @@M@@H_s@@，它在每个足够大长度上让一切单带判定器超过 @@M@@m^s@@ 步，再把每个长度硬度迁移到每个图阶。这是对”所有机器”的构造性否定，天然不需要假设。
问 5：AI 生成证明最可能出错的模式？
答：五级接口的常数簿记：@@M@@s=\lfloor r/1000\rfloor@@、@@M@@p=\lfloor s/1000\rfloor@@、@@M@@c_0=10^{-9}@@，两个”严格缝隙”要容纳全部构造与模拟开销；模拟成本若被低估一处，@@M@@m^{D+50p}<m^s@@ 即不成立。本文未经形式化，此类算术最怕静默错位。
问 6：论文自己承认了哪些局限？
答：为压到直径 2 引入的通用枢纽顶点度数无界，文中明言不作有界度数承诺；@@M@@r@@ 随输入增长时压缩构造不给出多项式编译；结论只覆盖确定性算法，随机化与非一致模型不在内。
总评
它把 WL 等价的难度从”流程贵”提升为”本质上贵”，无假设、全阶成立，是同族三篇里最硬的一根梁柱；最大风险在未经形式化的多层接口常数与投影引理的精确性，引用前值得独立复核第 2 节。