PaperlayerView exact revision on arXiv

Source-linked AI summary

The Logic of Graph Neural Networks

Martin Grohe

arXiv:2104.14624v2cs.LGcs.AIcs.LO

TL;DR

The paper addresses which graph functions GNNs can express, a question that can guide architecture choice. It explains precise correspondences between GNN expressiveness, Weisfeiler-Leman algorithms, and finite-variable counting logics; these include characterisations of node distinguishability and definable node properties.

  • Problem

    Which functions on graphs can GNNs express, and how can that understanding guide architecture choice?

    Source: §I · p. 1

  • Method

    The paper explains and proves characterisations connecting GNN expressiveness with colour refinement, Weisfeiler-Leman algorithms, and finite-variable counting logics.

    Source: §I · p. 1, §VIII · p. 9

  • Results

    GNNs distinguish vertices exactly as colour refinement does, while every node property definable in GC2 is expressible by a GNN uniformly over graphs.

    Source: §I · p. 1

  • Takeaways & Limitations

    Expressiveness characterisations can help choose an appropriate architecture and compare learning approaches, though they do not address generalisation or computational efficiency.

    Source: §XII · p. 13

    The paper does not consider generalisation from data or the computational efficiency of learning and inference.

    Source: §XII · p. 13

Abstract

from arXiv · show

Graph neural networks (GNNs) are deep learning architectures for machine learning problems on graphs. It has recently been shown that the expressiveness of GNNs can be characterised precisely by the combinatorial Weisfeiler-Leman algorithms and by finite variable counting logics. The correspondence has even led to new, higher-order GNNs corresponding to the WL algorithm in higher dimensions. The purpose of this paper is to explain these descriptive characterisations of GNNs.

I. INTRODUCTION

The introduction frames GNN expressiveness as a way to guide architecture choice and explains its precise characterisation through Weisfeiler-Leman algorithms and finite-variable counting logics. The preliminaries and logic background establish the graph setting and the logical notions used in that account.

I. INTRODUCTION

  • The k-dimensional WL algorithm iteratively colours vertex tuples using local isomorphism and current-colour information, but may not distinguish all structurally different tuples.For graph classes excluding a fixed minor, some dimension fully characterises graphs in the class and their automorphism orbits; planar graphs need only k = 3.Source: §I · p. 1
  • GNNs pass local information along graph edges and update vertex states using shared neural-network message and state functions.Shared parameters guarantee isomorphism invariance or equivariance, which is essential for learning functions on graphs.Source: §I · p. 1
  • Colour refinement and GNNs distinguish the same pairs of vertices, and node properties definable in GC2 are expressible by GNNs uniformly over graphs.Corresponding characterisations also hold for GNNs with global aggregate information, 1-dimensional WL, and C2.Source: §I · p. 1

II. PRELIMINARIES

  • The paper focuses on finite, undirected, simple, vertex-labelled graphs, while noting that results extend to directed graphs with edge labels and that weighted-label extensions are not discussed.The number of vertex labels is treated as fixed, not part of the computational input.Source: §II · p. 2

III. FINITE VARIABLE COUNTING LOGIC

  • Counting logic interprets formulas over graph vertices, and the k-dimensional WL algorithm corresponds to the (k + 1)-variable counting logic Ck+1.The guarded two-variable fragment GC2 is also known as graded modal logic.Source: §I · p. 1, §III · pp. 2–3

IV. INVARIANTS AND COLOURINGS

This section develops isomorphism-invariant colourings as a framework for describing graph and tuple properties, presenting Weisfeiler–Leman algorithms for distinguishing graphs and characterizing their limits, computational tradeoffs, and connections to finite-variable counting logics. It also relates k-dimensional owl colors to 1-dimensional WL colors on an associated structure using relations that encode tuple-coordinate differences and atomic types.

IV. INVARIANTS AND COLOURINGS

  • An invariant respects graph isomorphisms; it is complete when equal outputs imply an isomorphism, and collecting its tuple values as a multiset yields a graph invariant.A complete invariant induces a complete graph invariant, though the converse need not hold.Source: §IV · p. 3
  • Colourings partition vertex tuples into colour classes, and atomic types encode tuple equalities, adjacencies, and labels to identify isomorphic induced subgraphs.Atomic types are invariant, and their outputs agree exactly when the tuple-wise mapping is an isomorphism between the induced subgraphs.Source: §IV · pp. 3–4

V. THE WEISFEILER-LEMAN ALGORITHM

  • Colour refinement repeatedly counts each vertex’s neighbours by current colour, stabilizes in fewer than n rounds, and computes in O((n + m) log n) time, yet can miss non-isomorphic graphs.Its stable colouring fails to distinguish the Figure 1 pair and a 6-cycle from two triangles.Source: §V · p. 4
  • Neither 1-WL nor 2-WL is complete, and colour refinement and 1-WL distinguish the same pairs of graphs at every round.1-WL fails on regular graphs of the same degree, while 2-WL fails on strongly regular graphs with the same parameters.Source: §V · p. 5
  • Oblivious k-WL trades simpler context-free updates for higher memory use: k-WL distinction implies owl^{k+1} distinction, while the reverse requires one extra k-WL round.Matching k-WL’s expressive power requires oblivious WL on (k + 1)-tuples, with memory Ω(n^{k+1}) rather than O(n^k).Source: §V · p. 5
  • WL indistinguishability corresponds to agreement in finite-variable counting logic, while vertex colour refinement is characterized by the guarded fragment; these results also extend to relational structures.For graph-level distinction, colour refinement corresponds to C2, but at the vertex level the relevant logic is GC2.Source: §V · p. 6
  • The excerpts state an observation interpreting owl(t)_k over a graph (or binary structure) G as wl(t)_1 over a structure A_G; they do not establish universal-round or infinite-round scope.Source: §V · p. 6
  • The associated structure encodes tuple-coordinate differences with binary relations and atomic types with unary relations.Each binary relation marks pairs of tuples that differ in exactly one coordinate; each unary relation groups tuples by atomic type.Source: §V · p. 6
  • This observation goes back to.Source: §V · p. 6

VI. THE EXPRESSIVENESS OF FEED-FORWARD NEURAL NETWORKS

Feed-forward neural networks are parameterized compositions of layers, and this section examines which functions their architectures can express. Universal approximation applies to continuous functions on compact domains, while VC dimension and circuit complexity characterize limits under specified conditions.

VI. THE EXPRESSIVENESS OF FEED-FORWARD NEURAL NETWORKS

  • An FNN architecture specifies layer dimensions and activation functions, while instantiating weights and biases yields a function trained to approximate a target from labelled examples.The section distinguishes architecture, parameterized network, and computed function; it focuses on expressiveness rather than learning.Source: §VI · pp. 6–7
  • Depth-2 FNNs with a continuous non-polynomial activation can approximate any continuous function on a compact domain to arbitrary accuracy.The first-layer width is unrestricted and may depend on the target function, potentially growing exponentially with its description.Source: §VI · p. 7
  • For FNN architectures using Pfaffian activations, the VC dimension is polynomial in network size, with the polynomial depending on the activations.The paper notes that this bound also limits expressiveness and bounds the number of labelled examples needed for PAC guarantees linearly in VC dimension.Source: §VI · p. 7
  • Bounded-depth, polynomial-size FNN families with piecewise polynomial activations decide properties in TC0.TC0 is the class of properties decidable by bounded-depth, polynomial-size Boolean threshold-circuit families.Source: §VI · p. 7

VII. GRAPH NEURAL NETWORKS

The section frames GNNs as models for learning invariant functions on graphs, vertices, or vertex tuples. Their architecture guarantees invariance, unlike directly applying an FNN to adjacency matrices.

VII. GRAPH NEURAL NETWORKS

  • Graph learning may target functions on graphs, vertices, or vertex tuples in supervised learning or representation learning.In either setting, the functions of interest are invariants.Source: §VII · p. 7
  • GNNs guarantee invariance by design, whereas ensuring invariance for FNNs applied to adjacency matrices would be difficult.Source: §VII · p. 7
  • The paper focuses on a core GNN model also called a message passing neural network or aggregate-combine graph neural network.The passage cites [19] for the former name and for the latter.Source: §VII · p. 7

A. GNNs as a Computation Model

GNN layers transform vertex feature maps by aggregating neighbor features and combining them with each vertex’s current features. Readouts turn final features into vertex- or graph-level outputs, while the transformations preserve isomorphism invariance.

A. GNNs as a Computation Model

  • A GNN layer aggregates a multiset of neighbor feature vectors and combines the aggregate with the current feature to produce a new feature.The layer maps one feature map to another; its computation can be viewed as vertices exchanging states along graph edges.Source: A. GNNs as a Computation Model · pp. 7–8
  • GNN feature transformations preserve isomorphism invariance when corresponding vertices begin with matching features.Composing layers preserves that invariance at each intermediate stage.Source: A. GNNs as a Computation Model · p. 8
  • A recurrent GNN repeatedly applies one layer to produce an infinite sequence of feature maps, without requiring that the sequence converge.Source: A. GNNs as a Computation Model · p. 8
  • Initial vertex features represent the input graph’s labels, with the GNN input dimension at least the number of labels.The paper later discusses padding those initial features with random values.Source: A. GNNs as a Computation Model · p. 8
  • A vertex-level output applies a readout to each final vertex feature, while a graph-level output aggregates the multiset of final vertex features.Recurrent GNNs also specify an iteration count, which may depend on the input graph.Source: A. GNNs as a Computation Model · p. 8

B. Learning GNNs

GNNs become neural network models when their aggregation, combination, and readout functions are learned. The section specifies assumptions and choices that make these functions suitable for the paper’s expressiveness analysis.

B. Learning GNNs

  • The paper treats aggregation, combination, and readout functions as learned neural-network functions, but focuses on expressiveness rather than training.The theoretical analysis assumes depth-2 FNNs with a non-polynomial activation for combination and readout, enabling approximation of arbitrary continuous functions.Source: B. Learning GNNs · pp. 8–9
  • The aggregation function handles multisets of vectors, so it can be separated conceptually into message, aggregation, and post-processing functions.The aggregation component is typically fixed, while message and post-processing functions can be learned.Source: B. Learning GNNs · p. 8
  • Summation is the aggregation used in the analysis and is stated to be more expressive than max or mean, sufficient for full GNN expressiveness in this analysis.The message and post-processing functions can be merged into neighboring combination functions, so the analysis assumes aggregation is simply summation.Source: B. Learning GNNs · pp. 8–9
  • In practice, a learned linear messaging function is typically used, and aggregate readout can sum feature vectors before FNN post-processing.Source: B. Learning GNNs · p. 9

C. Variants

The section surveys GNN variants and establishes colour refinement as the boundary of ordinary GNN expressiveness, with recurrent GNNs recovering its distinguishing power on bounded-size graphs. It also extends the correspondence to GNNs with global readout and notes a proof tradeoff between generality and efficiency.

C. Variants

  • Variants include edge-type- and direction-aware messages for relational structures, plus global readout that distributes graph-wide information, equivalently implementable with a virtual node.Ordinary updates are local, so a node cannot directly receive information from another connected component.Source: C. Variants · p. 9

VIII. WEISFEILER AND LEMAN GO NEURAL

  • GNNs and colour refinement have equal distinguishing power on bounded-size graphs: colour refinement bounds every GNN, and a recurrent GNN recovers its iterations.The converse construction works through n rounds for graphs of order at most n.Source: §VIII · p. 9
  • The upper bound holds regardless of the aggregation and combination functions; the converse also holds with sum aggregation.The converse constructs a recurrent GNN matching colour refinement through n iterations on graphs of order at most n.Source: §VIII · pp. 9–10
  • For recurrent GNNs, colour refinement refines every computed vertex invariant, and any graph distinction made by a GNN is also made by colour refinement.The converse direction holds for graphs of order at most n with a recurrent GNN run for n iterations.Source: §VIII · pp. 9, 11
  • The converse is non-uniform: its GNN depends on input graph size, and the presented proof does not establish polynomial-size networks.The alternative proof in [43] gives polynomial-size GNNs, while the proof in uses two-layer networks that may be exponentially large in n.Source: §VIII · pp. 9–10
  • The two converse proofs trade generality for efficiency: handles more activation functions, while [43] controls network size and encoding length.The [43] construction uses polynomial-size, single-layer FNNs and integer encodings; the presented proof may yield exponentially large, two-layer FNNs and exponential-bit rational encodings.Source: §VIII · p. 10
  • With global readout, a recurrent GNN can refine colour refinement at every iteration on graphs of order at most n.Global readout distributes aggregate graph-wide information to each node, addressing the locality of ordinary updates.Source: C. Variants · p. 9, §VIII · p. 11

IX. THE LOGICAL EXPRESSIVENESS OF GNNS

The section characterizes logical queries expressible by GNNs, relating them to graded modal logic and counting logic. It shows that GNNs with global readout express all C2 queries, while the stated graded-modal result is proved for a restricted activation setting.

IX. THE LOGICAL EXPRESSIVENESS OF GNNS

  • Every unary query expressible in GC2 is expressible by a GNN, and any query expressible by both a GNN and first-order logic is expressible in GC2.The latter is a partial converse, not a claim that every GNN-expressible query is first-order expressible.Source: §IX · p. 11
  • The cited proof of GC2-query expressibility uses linearised sigmoid; adapting it to relu is straightforward, but adapting it to sig or tanh is not obvious.The non-uniform setting provides no obvious compact domain for applying the FNN universal approximation property.Source: §IX · p. 11
  • The graded-modal construction encodes subformula truth values in vertex features, with updates handling counting thresholds.For a guarded counting quantifier, the update tests whether at least p neighbors satisfy the relevant subformula.Source: §IX · p. 11
  • A GNN with global readout expresses every Boolean or unary query expressible in C2.This corresponds to the transition from colour refinement to 1-WL enabled by global readout.Source: §IX · p. 12

X. HIGHER ORDER GNNS

Higher-order GNNs operate on vertex tuples and correspond in expressiveness to higher-dimensional Weisfeiler-Leman refinement. Random node initialisation offers another route to greater expressiveness, with bounded-size universality but an open complexity analysis.

X. HIGHER ORDER GNNS

  • A k-GNN operates on k-tuples and corresponds to k-dimensional oblivious WL, hence to (k −1)-dimensional WL.Its distinguishing power is bounded by that WL procedure, and recurrent k-GNNs can refine its iterations on bounded-size graphs.Source: §X · p. 12
  • n-GNNs can approximate all invariant and equivariant functions on graphs of order at most n; 4-GNNs express all planar graph invariants.The planar result follows because 3-WL characterises planar graphs up to isomorphism.Source: §X · p. 12

XI. RANDOM INITIALISATION

  • Random initialisation is presented as an alternative to higher-order networks, which have substantial computational cost, without a steep computational cost.With high probability, random initialisation provides each node a unique identifier, which can help GNNs detect message paths that ordinary GNNs cannot distinguish.Source: §XI · p. 12
  • Random node initialisation assigns random values to extra feature coordinates, and the resulting computation is a random variable that remains isomorphism invariant.For query expression, the paper quantifies the error probability; it assumes these GNNs admit global readout.Source: §XI · p. 12
  • For every unary query and every input-size bound n, some GNN with random node initialisation expresses that query on graphs of order at most n.The paper also reports the cited result that all invariant functions on graphs can be expressed using GNNs with random initialisation [1].Source: §XI · p. 12
  • The universality theorem is non-uniform and does not analyze computational efficiency in input size; a complexity-theoretic analysis remains future work.Experiments [1] [49] have shown increased expressiveness, but do not replace that analysis.Source: §XI · p. 13

XII. CONCLUSIONS AND OPEN PROBLEMS

The paper characterizes GNN expressiveness using Weisfeiler-Leman algorithms and 2-variable counting logic, a characterization that can guide architecture choice. It distinguishes expressiveness from learnability, generalization, and computational efficiency, and identifies several open questions.

XII. CONCLUSIONS AND OPEN PROBLEMS

  • GNN expressiveness can guide architecture choice, but the paper does not address generalization or the computational efficiency of learning and inference.The paper presents expressiveness as one aspect of a machine-learning algorithm.Source: §XII · p. 13
  • The logical correspondence may support neuro-symbolic integration, but whether GNNs can learn models for logical queries remains an empirical question.Examples of learnable GNNs for logical queries are reported, alongside a call for more systematic empirical investigation.Source: §XII · p. 13
  • Theorems VIII.4, VIII.8, X.1(2), and XI.1 are non-uniform, whereas Theorem IX.1 is uniform.The non-uniform results require GNNs that depend on input graph size.Source: §XII · p. 13
  • Theorem IX.1 has only been proved with the linearised sigmoid activation, leaving its validity for other activation functions open.The paper asks whether a general condition, such as non-polynomiality, suffices.Source: §XII · p. 13
  • Open questions include whether GNNs with global readout capture first-order unary queries expressible in C2 and whether recurrent GNNs capture queries in modal two-variable fixed-point logic with counting.Theorem IX.2 gives a partial converse, while a similar result for C2 and GNNs with global readout remains open.Source: §XII · p. 13
  • Open questions ask whether GNNs with random node initialisation express order-invariant C2 or fixed-point queries, polynomial-time queries, and queries computed by polynomial-size threshold-circuit families.The paper also asks whether such GNNs can express every Boolean query, and whether the threshold-circuit question has a positive answer for polynomial-size GNN families.Source: §XII · p. 13

PROOF OF THEOREM V.6

The proof of Theorem V.6 proceeds by induction on the iteration count and uses bijections between tuple sets to relate the colorings across graphs.

PROOF OF THEOREM V.6

  • The proof fixes two graphs and proceeds by induction on t, with a trivial base case at t = 0.The inductive step considers tuples from the two graphs.Source: PROOF OF THEOREM V.6 · p. 16
  • The construction defines g as a bijection from V(G)^k to V(G′)^k, setting v+ = (v1, ..., vk, vk) for each v = (v1, ..., vk).Source: PROOF OF THEOREM V.6 · p. 17
  • For each k-tuple, the proof uses a bijection between vertices to match extended tuples and their WL colors, then assembles these maps into a bijection on (k+1)-tuples.The local vertex bijections are used to show that the assembled map preserves the coloring at iteration t.Source: PROOF OF THEOREM V.6 · p. 17

PROOF OF THEOREM V.10

The proof of Theorem V.10 uses induction on color-refinement rounds to relate vertex colors to formulas in two-variable counting logic. Its inductive step matches neighbor counts by color.

PROOF OF THEOREM V.10

  • At round 0, the coloring captures label information, represented by atomic Label formulas.The proof states that other atomic formulas are unnecessary for this base case.Source: PROOF OF THEOREM V.10 · p. 17
  • In the inductive step, equality of colors at round t + 1 implies agreement on formulas built from label atoms and counting quantifiers over neighbors.The argument compares the number of neighbors satisfying a formula across each color class from round t.Source: PROOF OF THEOREM V.10 · p. 17
  • Conversely, the proof assumes agreement on all GC2 formulas at round t + 1 and uses formulas distinguishing colors from the previous round.It introduces formulas for pairs of distinct colors, using the induction hypothesis.Source: PROOF OF THEOREM V.10 · p. 17
Loading 2104.14624v2…