结果族 133：The computational complexity of Weisfeiler–Leman refinement · 学科：Theoretical computer science · 验证状态：暂无形式化证明，请以社区核验为准
WL 对话的”维数 @@M@@k@@“以前都被当成固定的小常数；这篇论文让 @@M@@k@@ 成为输入的一部分，用二进制写在数据里——30 个比特就能写下十亿维，而熟悉的 @@M@@n^{O(k)}@@ 算法随之变成货真价实的指数时间。论文证明：此时判定两图是否 @@M@@k@@-WL 等价恰好是 EXPTIME 完全，哪怕图限制到每个点至多 3 条边，正面回答了 Berkholz 的公开问题。
关键词卡片
@@M@@k@@ 随输入给出、用二进制编码。@@M@@k@@-WL 等价的等价刻画——Dup 必须先亮出整张双射表，Spo 再选点考验。看个具体例子
归约的骨架是把一台指数时间机器的计算，压进一对多项式规模的小图：
代入数字：@@M@@d=20@@（机器跑约一百万步）时 @@M@@k=40@@，图对约有 @@M@@41^{12}\approx 2\times10^{19}@@ 个顶点。两头夹起来，判定问题恰好落在 EXPTIME 完全的位置上。
为什么值得关心
Luks 已证明固定最大度图的同构测试是多项式的，而本文说明”按指定维数做 WL”即使在同样的图上也指数时间完全——这是与同构测试本质不同的问题。
暂无形式化证明（AI 结果待核验）
第一级台阶
导读里”30 个比特写下十亿维”的比喻落到地上：对象是两张图外加一个用二进制写在输入里的维数 @@M@@k@@，操作仍是那套 @@M@@k@@ 维”染颜色、对答案”的对话，问题是对这个写下来的 @@M@@k@@ 问”两图是否仍不可区分”。@@M@@k@@ 从固定小常数变成输入数据，熟悉的 @@M@@n^{O(k)}@@ 流程一下子变成货真价实的指数时间——这个判定问题到底有多难，正是本文要钉死的。
第二级台阶
本科术语化：联合更新约定的 @@M@@k@@-WL 对元组逐轮精化，@@M@@G\equiv_kH@@ 指稳定直方图相同；判定语言 @@M@@\WL@@ 的输入是显式邻接矩阵与二进制 @@M@@k\ge2@@。等价的博弈刻画是双射博弈：Duplicator 须先宣布整张顶点双射、Spoiler 再选点考验，@@M@@k@@ 维对话对应 @@M@@k+1@@ 个对槽。子立方图指最大度至多 3 的图；@@M@@\EXPTIME@@ 是指数时间可解问题类，”完全”意为其中最难。
第三级台阶
定理的语境：@@M@@\WL@@ 在确定性多项式时间多一归约下 @@M@@\EXPTIME@@ 完全，且限制到连通、无色、同阶、最大度至多 3 的图（@@M@@\SubWL@@）仍完全。上界一侧”维数封顶”挡住浪费：@@M@@k\ge n@@ 时等价即同构，换 @@M@@\min\{k,n\}@@ 后标准细化只需 @@M@@2^{O(n\log n)}@@；艰难度一侧把指数时间机器的计算压进多项式规模的图对，维数取 @@M@@k=r=2d@@。”显式邻接矩阵”挡住隐式表示的质疑，正面回答 Berkholz 的公开问题。
证明当维数 @@M@@k@@ 以二进制编码作为输入时，判定联合更新 @@M@@k@@ 维 Weisfeiler–Leman 等价（@@M@@G\equiv_k H@@）是 @@M@@\mathsf{EXPTIME}@@-完全的，即使在连通、无色、最大度至多 3 的简单图上亦然，正面回答了 Berkholz 的公开问题。
Weisfeiler–Leman 精炼源自 1968 年 Weisfeiler 与 Leman 关于图标号（graph canonization）的工作：对有序顶点元组反复染色并比较两图的直方图，固定维数 @@M@@k@@ 时可在多项式时间完成。可一旦 @@M@@k@@ 本身是输入的一部分（二进制给出），熟悉的 @@M@@n^{O(k)}@@ 元组算法就不再是多项式时间的，该判定问题的复杂度长期悬而未决。经典的 Cai–Fürer–Immerman 构造只给出维数下界——区分某些非同构图需要线性多个变量——并非求解判定问题的时间下界。2024 年 Seppelt 证明了配对等价问题的 coNP-困难性，并记录下 Berkholz 提出的是否 @@M@@\mathsf{EXPTIME}@@-完全之问；Lichter–Raßmann–Schweitzer 随后对简单无色图独立得到 coNP-困难性。本文彻底解决此问题，并额外攻克最大度至多 3 的连通图这一受限情形——鉴于 Luks 已证明固定最大度图的同构测试属多项式时间，该限制恰恰说明”按指定维数做精炼”问的是另一回事：不同构的图仍可能等价。
定义语言 @@M@@\WL@@：输入为两张以显式邻接矩阵给出的有限简单无色无向图 @@M@@G,H@@ 与二进制整数 @@M@@k\ge2@@，判定是否 @@M@@G\equiv_k H@@；受限版 @@M@@\SubWL@@ 额外要求两图连通、阶相同且最大度至多 3。主定理断言：两者在确定性多项式时间多一归约（many-one reduction）下均为 @@M@@\mathsf{EXPTIME}@@-完全。上界来自”维数封顶”引理——同阶两图当 @@M@@k\ge n@@ 时 @@M@@G\equiv_k H@@ 当且仅当二者同构，故可把 @@M@@k@@ 替换为 @@M@@\min\{k,n\}@@ 后运行标准精炼，耗时 @@M@@2^{O(n\log n)}L^{O(1)}@@。归约输出的维数 @@M@@k=r@@ 是源输入长度的多项式，故即使改用一进制编码 @@M@@k@@，完全性仍成立。文中还给出显式规模：一般实现的图阶为 @@M@@O_M((r+1)^{12})@@、亚三次实现为 @@M@@O_M((r+2)^{16})@@（@@M@@r@@ 为地址坐标数），邻接矩阵均可在 @@M@@r@@ 的多项式时间内写出。
整体策略是把一台指数时间图灵机的计算压入一对多项式规模的小图，使 Duplicator 获胜当且仅当机器拒绝该输入；对目标语言取补判定器即得所需归约极性。先证游戏刻画：@@M@@G\equiv_k H@@ 当且仅当 Duplicator 在 @@M@@k+1@@ 个对槽的双射博弈（bijective game）中获胜，而 Duplicator 必须在 Spoiler 选点之前宣布整个顶点集双射——这一时序是全部构造必须满足的强约束。归约链分四步。第一步把时间与带头位置各记为 @@M@@d@@ 位二进制数，地址长 @@M@@r=2d@@，输出维数 @@M@@k=r@@；借助进位/借位表，用多项式多条连接模式（connection schema）描述指数规模的门电路，单带机在长 @@M@@4T@@ 环上的局部更新给出无环电路，某测试门为真当且仅当机器接受。第二步把电路翻译成 @@M@@\F_2@@ 上的标量像一致性（scalar-image consistency）：每个变量取非空的 1–2 位向量集合，每条比较只要求两端仿射形式的像集相等；私有的二坐标缓冲器 @@M@@(z,z')@@ 实现定向传播——真信号被迫把像缩为 @@M@@\{0\}@@，假信号保留全集，故一致当且仅当所有测试为假。第三步把每条比较细分为长导线、将 @@M@@r@@ 个地址坐标排成环，得到位点（site）与方块（square）两类块，其合法赋值构成 @@M@@\F_2@@ 上的仿射纤维；核心的精确投影命题为至多 @@M@@K=r+1@@ 个块构造相容偏移列表族且限制恰等于小族——围绕坐标环闭合的”包裹”分支至少需 @@M@@r@@ 个块、恰为 @@M@@r@@ 个时恢复唯一完整地址并受见证集约束，非包裹分支则靠调整角势（corner potential）吸收偏移改变。第四步实现成图：一般实现把合法赋值直接当作顶点、用私有叶子标记块；亚三次实现改用估值路径、前缀树、锚点链与共享读出上的相等匹配，再以”三角形＋连接器＋长度等于色号的私有路径”小配件消除颜色，得到连通、简单、最大度至多 3 的图对。最后读出博弈：Duplicator 对每个未激活块预先选定扩展列表，因 Spoiler 一步至多激活一个新块，各块选择无须彼此相容；反向用零查询历史，把环上 @@M@@r@@ 个位点的解码向量求和得到被寻址变量处的值，用仅剩的空槽将环沿导线逐格搬运（先放新再弃旧），对方块方程求和使竖直读出两两抵消，双向搬运恰好凑出见证集所需的像集等式。
本文与两篇姊妹篇同属结果族 133：固定维数篇对足够大的固定 @@M@@k@@ 证明 @@M@@n^{\Omega(k)}@@ 的确定性时间下界，识别维数篇证明”判定给定维数能否识别一张图”亦 @@M@@\mathsf{EXPTIME}@@-完全并直接复用本文的一致计算接口，三篇共享乘积地址、标量像与角势方法而互相支撑。本文主结果暂无 Lean 形式化证明；按 OpenAI 官方声明，未经形式化的结果可能有问题，请以社区核验为准。
问 1：证明中最脆弱的一步是什么？
答：精确投影命题（第 4 节）：为至多 @@M@@K=r+1@@ 个块构造相容偏移列表族，其限制恰等于小族——包裹分支至少需 @@M@@r@@ 个块、恰为 @@M@@r@@ 个时恢复唯一完整地址，非包裹分支靠角势吸收偏移改变。若投影有半点多余的自由度，Duplicator 的预选扩展策略即不闭合，”获胜当且仅当机器拒绝”的等价便脱钩。
问 2：难度会不会只是”@@M@@k@@ 用二进制写得短”的记法戏法？
答：不会。归约输出的维数 @@M@@k=r@@ 是源输入长度的多项式，改一进制编码问题仍 @@M@@\EXPTIME@@ 完全（论文明确指出）；上界一侧还靠 @@M@@\min\{k,n\}@@ 封顶排除了”维数巨大却轻松”的假象。难度是组合的，不是编码的。
问 3：与已有工作相比真正的新意是什么？
答：Seppelt 与 Lichter–Raßmann–Schweitzer 只证到 coNP 困难；本文给出完整 @@M@@\EXPTIME@@ 完全性，正面回答 Berkholz 的公开问题。与 Luks 多项式同构算法的对照更有意味：固定最大度图上同构易、指定维数的 WL 等价却指数时间完全——因为等价的图不必同构，这是另一个问题。
问 4：亚三次实现为什么值得单独啃？
答：把合法赋值当顶点的一般实现度数无界；压到最大度 3 需要估值路径、前缀树、锚点链、”三角形＋连接器＋长度等于色号的私有路径”等小配件逐层改写并消色，任何一处度数或色号簿记出错，连通性与度界即破。这也是全文工程量最大、最易藏错的部分。
问 5：AI 生成证明最可能出错的模式？
答：极性与时序：Duplicator 获胜对应机器”拒绝”，归约须取补判定器；且双射博弈要求 Duplicator 先亮整张双射表——构造必须在此强时序下仍可预选扩展列表。方向接反或”先选后答”的顺序违规，是这类归约最典型的静默错误。本文未经形式化，尤需逐条核对第 7 节的博弈读出。
问 6：谁会用到它？
答：它补全了变维数配对等价的分类格点；识别篇直接复用本文的一致计算接口，三姊妹篇共享乘积地址、标量像与角势方法，互相支撑成族 133 的骨架。
总评
这是 Berkholz 公开问题的干净了结，且把难度钉死在最受限的子立方图上，对照 Luks 结果颇具冲击力；最大风险在未经形式化的长归约中投影命题与亚三次配件的精细簿记。