结果族 133：The computational complexity of Weisfeiler–Leman refinement　·　学科：Theoretical computer science　·　验证状态：暂无形式化证明，请以社区核验为准

入门导读 🐣

@@M@@k@@ 维 WL”对话”分不出两张图，只说明这两张像；本文问一个更强的问题：多大的 @@M@@k@@ 才能让一张图 @@M@@G@@ 从所有非同构的图里被单独认出来？论文证明：判定”认出来所需维数 @@M@@\le k@@“是 EXPTIME 完全的——指数时间世界里的最难一档，比 NP 难题还要再高一层。

关键词卡片

WL 维数（Weisfeiler–Leman dimension, @@M@@\mathrm{WLdim}(G)@@）：能把 @@M@@G@@ 与所有非同构图区分开的最小维数 @@M@@k@@。
识别问题（identification）：判定 @@M@@\mathrm{WLdim}(G)\le k@@，要对一切比较图 @@M@@H@@ 全称量化。
联合更新（joint update）：@@M@@k@@ 维颜色细化的一种标准约定。
EXPTIME 完全（EXPTIME-complete）：指数时间可解，且一切指数时间问题都能归约到它。

看个具体例子

比如输入一张 20 个顶点的图和 @@M@@k=5@@，问”5-WL 认得出它吗”：

上界一侧很朴素：@@M@@k\ge n@@ 时必能识别，故枚举全部 @@M@@2^{\binom n2}@@ 张 @@M@@n@@ 顶点图逐一检验，耗时对 @@M@@n@@ 指数；下界一侧把任意图灵机的指数长计算压进多项式规模的图与维数 @@M@@r@@。结论：即使 @@M@@k@@ 改用一进制编码，问题仍 EXPTIME 完全——难，不靠 @@M@@k@@ 的数字写得长。

为什么值得关心

它补全了 WL 框架下”识别”这一量词形态的复杂度分类（此前只知 P 艰难与 NP 艰难），说明只差一个”对所有图”的量词，问题就从多项式可解跳到指数时间完全。

暂无形式化证明（AI 结果待核验）

由浅入深：从类比走向定理

第一级台阶

导读里”赢下所有对手”的比喻展开：对象是一张图 @@M@@G@@ 和一个维数 @@M@@k@@，操作是那套”染颜色、对答案”的对话，问题从”分不分得开指定的一对图”升级为”@@M@@k@@ 维对话能否把 @@M@@G@@ 从所有与它不同构的图里单独认出来”。配对等价只需打平一位对手，识别要赢下全体对手——多出的恰是一个全称量词。

第二级台阶

本科术语化：联合更新约定的 @@M@@k@@-WL 每轮把元组旧色与”同一替换顶点在 @@M@@k@@ 个坐标上的旧色向量”的多重集合并；@@M@@G\equiv_kH@@ 指两图元组颜色直方图逐轮相同。若 @@M@@G\equiv_kH@@ 蕴含 @@M@@G\cong H@@ 对每个比较图 @@M@@H@@ 成立，称 @@M@@k@@-WL 识别 @@M@@G@@；最小这样的 @@M@@k@@ 记为 WL 维数 @@M@@\mathrm{WLdim}(G)@@。判定问题是：输入 @@M@@G@@ 的二进制邻接矩阵与二进制编码的 @@M@@k@@，问 @@M@@\mathrm{WLdim}(G)\le k@@ 是否成立。

第三级台阶

定理的语境：该问题在确定型多项式时间多一归约下 EXPTIME 完全。成员性一侧很朴素：@@M@@k\ge n@@ 时必能识别，枚举全部 @@M@@2^{\binom n2}@@ 张 @@M@@n@@ 顶点图逐对检验即得指数算法；艰难度一侧把任意指数时间机器的计算编码进多项式规模的图与多项式有界的维数。”无色、简单图、显式邻接矩阵”挡住了靠顶点着色传递信息的取巧；”识别专用论证不把配对艰难性当黑盒”挡住了循环论证的质疑。推论：@@M@@k@@ 改一进制编码仍完全——难，不靠数字写得长。

一句话结论

本文证明：给定无色图 @@M@@G@@ 的邻接矩阵和二进制编码的正整数 @@M@@k@@，判定”Weisfeiler–Leman 维数 @@M@@\mathrm{WLdim}(G)\le k@@“是 EXPTIME 完全的；即使 @@M@@k@@ 改为一进制编码仍然完全，从而完成了输入维数下识别问题的复杂度分类。

问题背景

@@M@@k@@ 维 Weisfeiler–Leman 细化是图同构检测的核心工具。与”给定一对图在细化后是否仍不可区分”不同，识别（identification）问题问：@@M@@k@@-WL 是否把 @@M@@G@@ 从所有非同构图中单独区分出来，即是否 @@M@@G\equiv_k H@@ 蕴含 @@M@@G\cong H@@ 对每个比较图 @@M@@H@@ 都成立；最小的这样的 @@M@@k@@ 称为 @@M@@G@@ 的 WL 维数（Weisfeiler–Leman dimension）。此前 Arvind–Köbler–Rattan–Verbitsky 证明维数一的识别是 P 艰难的，Lichter–Raßmann–Schweitzer 把固定维数的 P 艰难性推广到一切 @@M@@k\ge 2@@，并在维数作为输入时证明 NP 艰难性；变维数的配对等价已知 coNP 艰难。识别带有”对所有比较图”的全称量词，此前没有完整的复杂度刻画，本文补上最后一格：EXPTIME 完全。

主要结果

约定 @@M@@k\ge 2@@ 采用联合更新（joint update）：每轮记录”同一个替换顶点 @@M@@z@@ 在 @@M@@k@@ 个坐标上的旧色向量”的多重集；@@M@@k=1@@ 用普通邻居颜色细化。主定理：判定 @@M@@\mathrm{WLdim}(G)\le k@@——输入为非空有限简单无色图的二进制邻接矩阵与二进制正整数 @@M@@k@@——在确定型多项式时间多一归约下 EXPTIME 完全；推论：@@M@@k@@ 用一进制编码仍是 EXPTIME 完全，故艰难性并不依赖 @@M@@k@@ 的数值指数级大于其编码长度。成员性来自朴素指数算法：先比较 @@M@@k@@ 与 @@M@@n@@（@@M@@k\ge n@@ 时直接接受），否则枚举全部 @@M@@2^{\binom n2}@@ 个 @@M@@n@@ 顶点图，逐个检验等价与同构，耗时指数于 @@M@@n@@ 的多项式。艰难度来自把任意指数时间机器 @@M@@M@@ 与输入 @@M@@w@@ 编码成图 @@M@@G(0)@@ 和多项式有界的维数 @@M@@r=2p(m)+4@@。

证明思路

归约把 @@M@@\mathbb F_2@@ 上的线性约束编码成”局部可重构”的图：每个变量比特对应一对顶点，每个小约束的每个合法赋值对应一个顶点并连向它指定的比特值；用互不相交的度数区间加私有悬挂叶子的办法抹去颜色，得到 @@M@@G(\beta)@@，其中 @@M@@\beta@@ 是各方块约束的右端比特。关键压缩在于：地址 @@M@@a\in\{0,1\}^r@@ 处的向量值不逐个存储，而写成相邻坐标之和 @@M@@h(a)=\sum_{i=1}^r h_i(a_i,a_{i+1})@@（@@M@@a_{r+1}=a_1@@），于是指数多的地址只需多项式大的短表即可描述。先证配偶结构：由双射博弈（bijective game，joint 约定恰对应 @@M@@k+1@@ 个对槽），任何满足 @@M@@H\equiv_r G(0)@@ 的图都同构于某个 @@M@@G(\beta)@@——度数区间先恢复颜色类与私有叶子，再用不超过 @@M@@K\ge 33@@ 个槽做小尺寸关联测试逐块重构同一约束模式；且 @@M@@G(\beta)\cong G(0)@@ 当且仅当移位后的约束组有全局偏移解。其次，博弈等价给出各地址处非空的向量值集合 @@M@@Q_{P,a}@@，每条比较在移位下恰好等同一个标量像（像一致性），而对一类特殊移位该条件也是充分的。计算编码采用单调电路与私有两坐标缓冲：集合 @@M@@\{(0,0),(1,1)\}@@ 的两个坐标像都是全 @@M@@\mathbb F@@ 而和像为 @@M@@\{0\}@@，因此缓冲既能保持源端的完整像，又能把和限制成单点；反之两坐标像都是单点时整个缓冲被逼成单点——这正是”真值单向传播”。若 @@M@@M@@ 接受 @@M@@w@@：广播类型 @@M@@A@@ 经翻转单坐标的自连接把单点性传遍所有 @@M@@2^r@@ 个地址，再连到每个门的坐标；每个坐标的自连接取两份，第三次比较中两份相加抵消该坐标本身，迫使值恰具相邻坐标和的形式，于是全局偏移存在，一切等价配偶都同构，@@M@@\mathrm{WLdim}\le r@@。若不接受：在某条广播自连接的第三次比较上放常数 1 的特殊扭转，两条自连接分别强制 @@M@@h_A(a)=0@@ 与 @@M@@h_A(a)=1@@，无全局解，但仍可对每个门按真值取 @@M@@\{0\}@@ 或 @@M@@\mathbb F@@ 构造满足像一致性的非空集合，得到等价而非同构的配偶，@@M@@\mathrm{WLdim}>r@@。图阶为 @@M@@O_M((r+1)^{12})@@，多项式时间可构造。

可信度与备注

本文未经形式化验证，请以社区核验为准。它与族 133 的姊妹结果互相支撑：变维数配对等价篇提供压缩计算构造的短表与势能延拓技术，本文的识别专用论证（全称量词下的局部到全局重构）独立完成，并不把配对艰难性当黑盒；无条件下界篇则处理固定维数的时间指数。按 OpenAI 官方声明，未经形式化的结果可能有问题。

深入探讨：像审稿人一样追问 🔍

问 1：证明中最脆弱的一步是什么？

答：接受情形下的”每个移位都提升为一个全局同构”。论文须证：与 @@M@@G(0)@@ 在维数 @@M@@r@@ 等价的任何图都同构于某个 @@M@@G(\beta)@@，且当机器接受时一切等价配偶都与 @@M@@G(0)@@ 同构——这远超逐块识别约束模式，靠偏移延拓定理把局部选择拼成全局解（第 4、5 节）。拼接若有一处不闭合，接受与拒绝两种情形的界线即模糊。

问 2：为什么”全称量词”会把复杂度从 NP 一路抬到 EXPTIME？

答：量词本身不是全部原因——LRS 对彩色 CFI 图也分析过全体配偶。真正的原因是编码方式：指数长的计算表被压缩成多项式规模的图，靠相邻坐标和 @@M@@h(a)=\sum_i h_i(a_i,a_{i+1})@@ 用短表描述指数多地址；识别的全称量词与这种压缩相乘，才够到 EXPTIME。

问 3：一进制编码的推论为什么值得一提？

答：它排除了最廉价的”难度”来源：若艰难性只靠 @@M@@k@@ 的数值远大于其编码长度，二进制的指数膨胀就是全部戏法。一进制下仍完全，说明难度是组合的，不是记法的。

问 4：与已有工作相比真正的新意是什么？

答：此前只有固定维数的 P 艰难与变维数的 NP 艰难（LRS）；本文补全输入维数下识别问题的完整分类。技术上，引入可整体移位的约束族并把”博弈可赢的选择”与”定义一个同构的相容选择”分开处理，再在抽象比较族上先证二者等价，是识别专用的局部到全局重构。

问 5：AI 生成证明最可能出错的模式？

答：这类归约的典型风险是”接受情形证多了、拒绝情形证少了”：私有两坐标缓冲的真值单向传播、第三次比较中两份相加抵消坐标自身等环节，任何一处单调性判断失误都可能让拒绝实例也被迫全局可解，归约失效。本文未经形式化，只能靠人工逐条复核。

问 6：谁会用到它？

答：WL 维数作为单图参数的算法研究就此画上复杂度句号：最坏情形下计算它不可行；图同构与有限模型论的工具箱多了一个完整的分类格点，GNN 表达力的理论刻画也多了一块对照基准。

总评

它以一个干净的 EXPTIME 完全性收束了 WL 识别问题的分类，压缩编码与局部到全局重构的技术组合颇有分量；最大风险是未经形式化的长归约链条中缓冲与移位环节的簿记错误。

解读 | The complexity of identifying a graph by Weisfeiler–Leman refinement

入门导读 🐣

由浅入深：从类比走向定理