On the Expressive Power of Implicit Line-Graph Higher-Order Weisfeiler–Leman
Fan Yang
cs.SI
Sep 14, 2026 · v1
cs.AI cs.LG
TL;DR
The backward-transfer theorems, WL refinements, line graphs, ILG definitions, and the neural expressivity model are formalized in Lean 4, with a public repository.
Abstract
Whitney's theorem allows isomorphism testing for connected simple graphs, apart from $K_3$ and $K_{1,3}$, to be formulated as distinguishing their line graphs. However, the relation between fixed-dimensional Weisfeiler–Leman (WL) expressivity on line graphs and on their roots remains unresolved. We study this relation through Implicit Line-Graph WL (ILG-$k$-WL), which is exactly $k$-WL on $L(G)$, executed over the edges of $G$ with line-graph relations derived from endpoint incidence and without explicitly constructing $L(G)$. On the Whitney-general class, the relation between root-domain and line-graph WL depends on $k$. For $k=1,2$, ILG-$k$-WL adds no distinguishing power beyond root-domain $1$-WL and misses some pairs that $1$-WL separates. For $k=3$, we prove the backward containment $L(G)\equiv_{3\text{-WL}}L(H)\Rightarrow G\equiv_{3\text{-WL}}H$. Strongly regular witness pairs, including the Shrikhande/rook pair, show that ILG-$3$-WL is strictly more expressive than $3$-WL. The backward containment also extends to disconnected graphs with no isolated vertices when every connected component is Whitney-general. Deterministic ILG-$3$-WL separates all three substructure-counting witness pairs, all $105$ pairs in SR25, and $359$ of $400$ BREC pairs. An untrained dense ILG-$3$-GNN gives the same pairwise verdicts on these evaluations.
Problem
Whitney's theorem lets isomorphism testing of connected simple graphs be phrased as distinguishing their line graphs. How fixed-dimensional Weisfeiler–Leman expressivity on line graphs relates to WL expressivity on the root graphs was unresolved.
Approach
The paper defines Implicit Line-Graph WL (ILG-k-WL), which is k-WL on L(G) run over the root edges using endpoint-derived relation codes, without building L(G). It proves expressivity relations for k=1,2,3 on Whitney-general graphs and derives a higher-order GNN realization. The backward-transfer theorems and supporting lemmas are machine-checked in Lean 4.
Results
ILG-k-WL is strictly weaker than root k-WL for k=1,2. For k=3 it is strictly stronger: L(G)≡3-WL L(H) implies G≡3-WL H, and the Shrikhande/rook pair is a separating witness. ILG-3-WL separates all 105 SR25 pairs and 359 of 400 BREC pairs, and an untrained dense ILG-3-GNN gives the same pairwise verdicts.