How hard is WL?

0:00Weisfeiler–Leman refinement

Are two graphs the same up to relabelling? A classic first test is colour refinement. Give every vertex the same colour, then repeatedly recolour each vertex by its old colour and the multiset of its neighbours’ colours. If the colour counts ever differ, the graphs are not isomorphic. It can fail: in a six-cycle and in two triangles, every vertex has two neighbours, so refinement never separates them. The k-dimensional Weisfeiler–Leman method colours k-tuples of vertices instead. It starts from which entries are equal or adjacent, and updates each tuple from the tuples made by putting any vertex into any one position. In the joint form, which keeps the swaps for each new vertex together, two dimensions already separate these graphs. In our check, in the cycle 6 non-adjacent pairs share a neighbour, and in the triangles none do. Weisfeiler and Leman introduced the method in 1968. Cai, Fürer and Immerman built pairs of non-isomorphic coloured graphs of maximum degree three that need dimension linear in their size. For a fixed dimension k, refinement decides equivalence in time n^O(k). The known hardness was much weaker. Deciding whether refinement identifies a graph was P-hard for every fixed dimension. With the dimension as part of the input, equivalence was coNP-hard, and Berkholz asked whether it is EXPTIME-complete. And some coloured graph pairs need on the order of n^(k/2) rounds of refinement, which still does not rule out a faster algorithm that decides the outcome another way.

1:37The claims

Result 133 is four OpenAI preprints, 107 pages in all, dated September 25. The first claims an unconditional lower bound: for every sufficiently large fixed k, any deterministic algorithm deciding k-dimensional equivalence needs time at least n^(ck), for one absolute constant c, at every large graph size, even on connected graphs of diameter at most two. The second: with the dimension given in binary, equivalence is EXPTIME-complete, even for connected graphs of maximum degree three. The third: deciding whether refinement of a given dimension identifies a graph, separating it from every non-isomorphic graph, is EXPTIME-complete too. The fourth turns finite choice problems into graph pairs and, assuming the exponential time hypothesis, rules out fast algorithms even for the first round or two. The fine print matters. The papers use two update rules, joint and separate; the second and third results cover only the joint one. The lower bound is for deterministic sequential machines reading adjacency matrices, and for small dimensions like two or three it gives nothing beyond the cost of reading the input. Sufficiently large is very large: with the paper’s constant, 10⁻⁹, the bound only beats the n² cost of reading the input once k passes 2 billion. The Lean version uses 1/2000, from k of 100 million. OpenAI published Lean formalizations of all four. For the parity lifts, the catalogued statement is the reduction theorem, and a further file that the catalog does not link proves the conditional time bounds, with the exponential time hypothesis as an explicit assumption. In all, about 290 files and 80,000 lines, not counting Mathlib. We have not run the Lean check.

3:33How the proofs go

The building block is a parity lift, adapted from Roberson’s parity graphs, in the spirit of Cai, Fürer and Immerman. Take a base graph. Replace each vertex by bit vectors, one bit per neighbouring vertex type, with a prescribed parity. Join two of them when their base vertices are adjacent and the bits facing each other agree. Flipping the parity at one vertex twists the graph. On the complete graph on four vertices, both versions have 16 vertices, 48 edges and 32 triangles, but the untwisted one contains 8 copies of the complete graph and the twisted one none. In our check, colour refinement and joint two-dimensional refinement could not tell them apart; joint three-dimensional refinement could, after one round. The fourth paper builds the base graph from a choice system: a few domains, and for each pair of domains, labels that the chosen elements must agree on. For dimension four and up, with k plus one domains under the joint rule, or k under the separate rule, the two lifts are equivalent exactly when no consistent choice exists. A consistent choice changes the number of ways to map one small template graph into the lift, and that shows up within two rounds. Conversely, refinement only sees counts of patterns of small treewidth, and if one of them separated the lifts, following the odd parity through its tree decomposition would end at a bag whose vertices form a consistent choice. In our check, a toy system with four two-valued domains, which is dimension four under the separate rule, where three must pairwise differ, gave lifts of 16,456 vertices with equal template map counts. Turning one constraint into an equality made a choice possible, and the counts differed by about 17 trillion. The unconditional bound needs no hypothesis because it diagonalizes. First, a compressed consistency problem, on addresses written with r digits in base m, becomes two connected graphs of diameter at most two that are equivalent exactly when the problem is consistent. Second, the run of a one-tape machine, with its time and tape position written in those digits, is such a problem, so the graphs are equivalent exactly when the machine rejects. Third, a padded diagonal language simulates the machine named by the input’s prefix and flips its answer, so no one-tape machine decides it in m^s steps at any large length, though it is decidable in time polynomial in m^s. Hard pairs exist at every graph size in a window, so a decider beating n^(ck) at even one size in any late window would decide that language too fast. With the dimension as input, the same idea scales up. An exponential-time machine has exponentially many tableau cells, but each cell has a short binary address of time and position bits. The construction describes the tableau by polynomially many product rules on those addresses, sets the dimension equal to the address length, and builds graphs of polynomial size whose equivalence encodes the machine’s answer. Buffers make information flow one way, and the subcubic version rebuilds high-degree parts from paths and trees, then replaces each vertex by a triangle, with paths whose lengths encode its colour. Identification needs more. The third paper shows that every graph equivalent to its construction is a twisted copy, isomorphic exactly when the twist can be undone. If the machine accepts, every twist that refinement misses can be undone, so refinement identifies the graph; if it rejects, one twist survives.

7:14Where it stands

The four preprints are not peer reviewed and have not been revised. The Lean formalizations cover the unconditional lower bound, both EXPTIME-completeness results and the parity-lift reduction, and a file the catalog does not link covers the conditional time bounds; we have not run them. None of these papers is among those OSVerify reviewed, and we have seen no expert review. If they hold, deciding the outcome of Weisfeiler–Leman refinement is provably hard. For large fixed dimensions no deterministic algorithm beats n^(ck), with no unproved hypothesis, and with the dimension as input, both equivalence and identification are EXPTIME-complete, which by the time hierarchy theorem rules out polynomial time.