The complexity of Weisfeiler–Leman refinement

Source and verification

This article explains family 133 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

🏷️ Tuple colors and graph comparison

Weisfeiler–Leman refinement assigns colors to ordered tuples of graph vertices. A color is a finite record of structural information, not an arbitrary label chosen independently in each graph. Two graphs must use the same names for equal records.

For dimension $k\ge 2$, the initial color of $\mathbf{v}=(v_1,\dots ,v_k)$ records every equality and adjacency among its entries. Write $\mathbf{v}[i\leftarrow z]$ for replacement of coordinate $i$ by $z$. In the joint convention, define the replacement vector

$$B_r(\mathbf{v},z)=(C_r(\mathbf{v}[i\leftarrow z]){)}_{i=1}^k.$$

The next color consists of the old color and the multiset of these vectors as $z$ ranges over the vertices. In the separate convention, it instead records one replacement-color multiset for each coordinate. Joint refinement retains which replacement colors arose from the same $z$; separate refinement forgets that correlation.

Write $G{\equiv }_{k}H$ when the tuple-color histograms agree at every round under the specified convention. Keeping the old color makes the common partitions successively finer. Once a round makes no split, future rounds only rename the same classes, so stable histograms suffice.

Dimension one uses ordinary neighbor color refinement in the identification manuscript: a vertex records its old color and the multiset of its neighbors’ colors. Starting with one color, all vertices of a regular graph remain equally colored. Thus a six-cycle and two disjoint triangles have the same dimension-one histograms. Joint dimension two separates them: an adjacent pair in a triangle has a common neighbor, whereas an adjacent pair in the six-cycle does not. The joint replacement vector records adjacency to both entries of the pair. (OpenAI, 2026) (OpenAI, 2026b)

🏷️ Equivalence, identification, and time

Pair equivalence asks about supplied graphs $G,H$. Identification asks whether

$$G{\equiv }_{k}H⟹G\cong H$$

for every graph $H$. The least identifying dimension is denoted $\mathrm{WLdim}(G)$. This quantification over all possible alternatives is not supplied by a reduction that constructs just one difficult pair.

All final graphs in this family are finite, simple, undirected, and uncolored. Inputs to the complexity statements are explicit adjacency matrices. EXPTIME is the class of decision problems solvable in deterministic time $2^{p(L)}$ for some polynomial $p$ in input length $L$. Completeness here uses deterministic polynomial-time many-one reductions.

Manuscript result	Input parameter	Scope
Parity-lift construction	Fixed $k\ge 4$	Compatible finite choices correspond exactly to inequivalence; both update conventions
Unconditional time lower bound	Fixed sufficiently large $k$	Every deterministic equivalence decider has worst-case time $n^{\Omega (k)}$ at every sufficiently large order
Pair-equivalence completeness	Supplied $k\ge 2$	Joint updates; general graphs and connected graphs of maximum degree at most three
Identification completeness	Supplied positive $k$	Joint updates above dimension one; ordinary refinement at dimension one

The last two problems are EXPTIME-complete even with unary dimension encoding. The subcubic condition means degree at most three, not regular degree three. It does not make graph isomorphism EXPTIME-hard: deciding whether a specified refinement dimension distinguishes a pair is a different query. (OpenAI, 2026a) (OpenAI, 2026b)

The unconditional fixed-dimension theorem has precise quantifiers. There are absolute $c>0$ and $k_0$ such that, for every fixed $k\ge k_0$ and every correct deterministic decider $A$, some threshold $n_0(A,k)$ satisfies

$$T_A(n)\ge n^{ck}(n\ge n_0(A,k)).$$

The program may depend arbitrarily on $k$. The models are multitape Turing machines and sequential RAMs with logarithmic-size words and addresses, boundedly many memory accesses per instruction, and fixed polynomial-bit-time instructions. The theorem also holds when correctness is required only on connected graphs of diameter at most two. It asserts neither a randomized lower bound nor a bound for machines with unbounded unit-cost integers. (OpenAI, 2026b)

🏷️ A finite-choice reduction

The parity paper starts from domains $D_1,\dots ,D_t$. For each pair $i<j$, maps from $D_i$ and $D_j$ to a common label set describe their compatibility: the chosen elements must produce the same label. For example, domain elements may be allowed assignments on different variable scopes; labels record restrictions to their intersections.

Take $t=k+1$ for joint refinement and $t=k$ for separate refinement. The paper constructs two equal-order graphs such that

$$\begin{array}{c}{X}_0{\equiv }_k{X}_{\star }⟺\\ \text{no compatible choice exists}.\end{array}$$

If all domains and label sets have size at most $A\ge 1$, each output has at most $A{M}_t$ vertices, where

$$M_t=t{2}^{t-2+3\left(\genfrac{}{}{0ex}{}{t-1}{2}\right)}+12\left(\genfrac{}{}{0ex}{}{t}{3}\right).$$

A successful choice is detected after at most two joint rounds or one separate round. The theorem also covers running refinement on the disjoint union and comparing its two pure tuple sets. This variant involves mixed tuples during refinement, so it is an additional assertion rather than a change of notation. (OpenAI, 2026a)

The base template contains a clique of $t$ main types. For every pair of main types and every third type, add a helper adjacent to those three. Replace main types by domains and helpers by label sets. Edges to the first two main types enforce matching labels; the third incidence is unrestricted. These types organize the construction but are not colors supplied to the final comparison algorithm.

A parity lift replaces a base vertex by binary tags indexed by its neighboring template types. The sum of the tag bits has prescribed parity, and tags across a base edge must agree in their facing coordinates. The two lifts differ by changing the parity at one main type.

🏷️ Noncancellation and bounded-width witnesses

A graph homomorphism $F\to X$ preserves adjacency; let $\mathrm{hom}(F,X)$ count such maps. Fix a projected map $\varphi :F\to G$ into the base graph. Its lifts satisfy a binary linear system. For $X_0$ this system is homogeneous, while for $X_{\star }$ it has the same coefficient matrix with a shifted right-hand side.

A homogeneous system has its kernel as solution set. A shifted system has either no solutions or a translate of that kernel. Therefore every projection contributes a nonnegative difference, giving

$$\mathrm{hom}(F,X_0)\ge \mathrm{hom}(F,X_{\star }).$$

One inconsistent shifted system makes the inequality strict, and other projections cannot cancel its contribution. This includes projections that fail to preserve the intended interpretation of the types. A successful compatible choice supplies a distinguishing map from the template itself. (OpenAI, 2026a)

For the converse, a tree decomposition covers a test graph by vertex bags arranged on a tree, with each edge contained in a bag and the bags containing any one vertex forming a connected subtree. Its width is the largest bag size minus one. The source uses the correspondence between WL information and homomorphism counts from graphs with bags of size at most $t$.

An inconsistent shifted system has a parity certificate: a sum of its equations with zero left side and right side one. The resulting vertex and edge weights orient decomposition-tree edges toward a side of odd weight. A sink bag must contain representatives of all main types. But a bag need not form a clique, and its representatives need not have nonzero individual weight. The helper incidences supply the further boundary identities needed to force pairwise label compatibility. This extraction, rather than the mere existence of a full bag, is the substantive converse theorem.

The construction also gives conditional running-time exclusions from satisfiability. The paper distinguishes a positive exponential-rate ETH assumption, which controls even independently chosen fixed-$k$ solvers, from a weaker uniform subexponential-time exclusion, which supports a uniform parameterized conclusion. Its early-round consequences remain useful; for stable equivalence, the unconditional companion gives the stronger time theorem. (OpenAI, 2026a) (OpenAI, 2026c)

🏷️ Why an announced bijection needs exact extension

The computational reductions use an equivalent finite game. With $k+1$ pair slots for joint $k$-WL, a move proceeds as follows: discard any chosen pairs, request a vacant slot, have Duplicator announce a bijection of the entire vertex sets, then let Spoiler choose a vertex and place it with its image. All occupied pairs must preserve equality and adjacency. Separate $k$-WL uses $k$ slots in the corresponding convention. (OpenAI, 2026c) (OpenAI, 2026d)

The order matters. A response to an already selected vertex is weaker than a full bijection announced beforehand.

To encode a computation, the manuscripts use small binary-valued constraints at addresses with many coordinates. One local block records only two adjacent address coordinates. A ring of blocks reveals a full address, while one spare pair transfers a scalar value along a constraint. This hides a large addressed computation inside a much smaller graph.

The witnesses are nonempty sets of possible vectors, compared through images of individual scalar forms. Equal scalar images do not assert one simultaneous global vector assignment. Two-dimensional buffers permit forward propagation of a singleton image without imposing unwanted restrictions backward through a false predecessor.

For the game strategy, the construction needs compatible local translation offsets with exact projection: every retained offset list extends when one further block is activated, up to the allowed number of blocks. Existence of some locally consistent list on each block set would not suffice, because a play has already committed to particular values.

With exact extension, Duplicator can choose an extension separately for every inactive block and use it to biject that whole block’s vertices. These choices need not agree with each other: Spoiler’s next vertex activates only one new block. The converse reads scalar images by moving a ring through the construction, preserving old values until copied. The subcubic realization additionally replaces high-degree incidence pieces by paths and trees and proves that their readouts remain recognizable with the same slot budget. (OpenAI, 2026d)

🏷️ Fixed dimension and every sufficiently large order

In the fixed-dimension paper, an address has $r$ coordinates from $[m]$. With $r$ fixed, there are only $O(m^2)$ local blocks up to parameter-dependent constants; removing auxiliary colors produces $O(m^6)$ vertices. These bounds do not themselves give a polynomial compiler when $r$ grows. The variable-dimension paper separately proves uniform polynomial bounds using binary addresses. (OpenAI, 2026c) (OpenAI, 2026d)

The unconditional time argument starts with a diagonal language hard at every sufficiently large word length $m$. It builds equivalent or inequivalent graphs encoding the computation and pads them to any order in

$$I_m=[m^{20},(m+1{)}^{20})\cap \mathbb{Z}.$$

To turn an isolated fast graph order into a contradiction, a simulator tries every padded order in $I_m$, with time cutoffs, before using a correct fallback. If one order were fast for all graph pairs of that order, every length-$m$ source word would finish before fallback. The source tracks construction and simulation costs and chooses exponent gaps so that this contradicts the diagonal lower bound.

The intervals cover all sufficiently large orders. This establishes the eventual bound without assuming that $T_A(n)$ is monotone in $n$. A universal hub supplies connectedness and diameter two, but has unbounded degree; this promise is distinct from the subcubic variable-dimension theorem. (OpenAI, 2026c)

🏷️ Upper bounds and the all-mates condition

Binary-encoded $k$ might be enormous. It must be capped before allocating an $n^k$ tuple table. For $k\ge n$, a tuple containing every vertex has an initial equality-and-adjacency type that specifies the graph up to isomorphism. Matching that type in another $n$-vertex graph produces an isomorphism. Thus joint equivalence at $k\ge n$ is already equivalent to isomorphism, and $k$ may be replaced by $\min (k,n)$ for $n\ge 2$.

At most $2n^k$ common color classes can arise across the two tuple tables, so stabilization takes at most that many rounds. Explicit refinement then costs $2^{O(n\log n)}{L}^{O(1)}$. This establishes EXPTIME membership for supplied-pair equivalence. (OpenAI, 2026d)

For identification, enumerate all graphs of order $n$, test equivalence, and reject if an equivalent nonisomorphic graph is found. Other orders have different tuple counts. There are at most $2^{\left(\genfrac{}{}{0ex}{}{n}{2}\right)}$ candidate graphs, and even enumerating all vertex bijections to test isomorphism remains within exponential time in the explicit input length. Dimension one is handled by its ordinary refinement rule. (OpenAI, 2026b)

Hardness of identification needs an additional reconstruction theorem. The source encodes binary constraints in a graph $G(0)$ and shows that every equivalent mate is some shifted graph $G(\beta )$. Local game conditions describe allowable shifts; a global solution describes an actual isomorphism. On accepting computations, the construction forces all relevant witness sets to singletons and then forces the global compatibility needed for an isomorphism. On rejecting computations, a shift remains locally admissible but has no global solution, supplying a nonisomorphic mate. This closes the all-mates quantifier that pair-equivalence hardness leaves open. (OpenAI, 2026b)

🏷️ Key steps and proof outlines

A sink bag must also pass a compatibility test

The parity paper’s converse needs more than finding all main types in one tree-decomposition bag. Here is the additional argument from “Extracting a choice from a bounded-bag witness.” Work with binary arithmetic. An inconsistent lift system supplies vertex weights $s(x)$ and edge weights $r(xy)$ such that the total weighted mass of every type is one. At each vertex, summing the edge weights toward any adjacent type gives its vertex weight.

Contract decomposition edges whose bags are equal. Every remaining separator has at most $t-1$ vertices, so it misses some main type. For two absent main types, the edge equations force equal mass on either side of the separator. The two sides’ masses sum to one. Orient the decomposition edge toward the side of mass one, and choose a sink bag $B$. Every outer component then has mass zero in every main type absent from its separator. A main type missing from $B$ would have zero mass everywhere, a contradiction. Therefore $B$ contains exactly one representative $x_i$ of every main type.

The representatives need not be adjacent, and their individual weights need not equal one. To prove compatibility, suppose representatives of types $i,j$ carry different labels and let $\alpha$ be the first representative’s label. On vertices of type $i$ use the predicate “label is different from $\alpha$”; on type $j$ use “label equals $\alpha$.” Both predicates vanish at their bag representatives. On every actual $ij$ edge, the two endpoint labels agree, so the predicates sum to one. Their weighted sum $P$ therefore satisfies

$$P(B)=0,P(V(F))=1.$$

For an outer component $A$, choose a main type $\ell$ absent from its separator. If $\ell =i$ or $j$, the edge equations give $P(A)=m_{\ell }(A)=0$ directly, with boundary terms vanishing because the bag predicate is zero. Otherwise use the helper type $h_{ij;\ell }$. Its stored label couples the two predicates; summing its equations gives $P(A)=m_h(A)=m_{\ell }(A)=0$. Neither $h$ nor $\ell$ occurs on the separator, so these sums have no uncontrolled outgoing contribution. The disjoint partition into the bag and outer components now contradicts $P(V(F))=1$. Thus the bag representatives form a compatible choice. This weighted mismatch test is what makes the extra helper incidences necessary. (OpenAI, 2026a)

Exact extension matches the order of the game

For the computational companions, let $\mathcal{A}(S)$ denote the allowed lists of translation offsets on a set $S$ of active blocks. The required invariant is stronger than $\mathcal{A}(S)\ne \varnothing$:

$${\mathrm{proj}}_S\mathcal{A}(S\cup \{b\})=\mathcal{A}(S)$$

for every permitted next block $b$. Equality says that every already chosen list extends, not only that some list does. At a game position, Duplicator has committed to one element of $\mathcal{A}(S)$. For each inactive block, choose an extension and use its new offset to translate all vertices in that block. The union of these blockwise translations is a full bijection announced before Spoiler chooses a vertex. The extensions for different inactive blocks need not agree jointly, because the move activates only one of them. This proves why exact projection is the correct local invariant and why a global assignment is unnecessary for survival of the bounded-slot game. (OpenAI, 2026d)

Two separate closures of quantifiers

The fixed-dimension time paper turns an infinitely-often hardness argument into an eventual lower bound by testing every padded order in $[m^{20},(m+1{)}^{20})$. This interval contains only polynomially many orders in $m$. If even one order admitted uniformly fast decisions on all graph pairs, trying the orders with suitable cutoffs would solve every source word of length $m$ quickly. The diagonal source language rules this out for every sufficiently large $m$. No monotonicity of the graph algorithm’s running time is needed. (OpenAI, 2026c)

Identification has a different missing quantifier: all equivalent mates. Its reconstruction theorem first proves that every mate is a shifted realization $G(\beta )$. The local offset invariant characterizes shifts invisible to the game, while a global compatible offset assignment characterizes actual isomorphisms. Accepting computations force the local witness images to singletons and make them globally compatible; rejecting computations retain a locally admissible shift without a global solution. Thus the reduction proves identification or nonidentification against every mate, rather than only against its one deliberately constructed comparison graph. (OpenAI, 2026b)

🏷️ Reading connections

Two-way automata studies another distinction between a concrete computation and the complexity of all possible deciders in a fixed resource model. Depth-three circuit lower bounds likewise depends on keeping a lower bound’s computational model and quantifiers explicit.

🏷️ Manuscripts and verification scope

• Parity lifts and bounded-treewidth witnesses for Weisfeiler–Leman equivalence — pinned manuscript and companion source.
• The complexity of identifying a graph by Weisfeiler–Leman refinement — pinned manuscript and companion source.
• Unconditional time lower bounds for Weisfeiler–Leman equivalence — pinned manuscript and companion source.
• Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs — pinned manuscript and companion source.

The family scope page describes selected formalization coverage. It lists comparators for the parity construction, identification completeness, unconditional sequential lower bound, and variable-dimension pair equivalence. The parity construction selection excludes its conditional time consequences. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026a. Parity lifts and bounded-treewidth witnesses for Weisfeiler–Leman equivalence.

🐻  OpenAI 2026b. The complexity of identifying a graph by Weisfeiler–Leman refinement.

🐻  OpenAI 2026c. Unconditional time lower bounds for Weisfeiler–Leman equivalence.

🐻  OpenAI 2026d. Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs.