A Logical View of GNN-Style Computation and the Role of Activation Functions

TL;DR

The paper develops MPLang as a rigorous framework to analyze GNN-style computation on graphs, separating the roles of linear aggregation and activation functions in shaping numerical and Boolean expressivity. It shows A-MPLang is tied to walk-count features, and that for bounded asymptotically constant activations all such variants collapse to the same numerical power with Boolean closure, while linear layers elevate expressive power. A central achievement is proving that ReLU-based MPLang strictly outperforms any eventually constant activation in numerical queries on coloured graphs, a separation established via red-blue symmetric trees and Liouville-type arguments. The work connects MPLang to established logics for GNNs, demonstrates a Booleanisation approach with a canonical bool activation, and highlights that activation choices are a critical design factor for the expressive capabilities of GNN-like models, offering a roadmap for future investigations into unbounded activations and visualization of their logical power.

Abstract

We study the numerical and Boolean expressiveness of MPLang, a declarative language that captures the computation of graph neural networks (GNNs) through linear message passing and activation functions. We begin with A-MPLang, the fragment without activation functions, and give a characterization of its expressive power in terms of walk-summed features. For bounded activation functions, we show that (under mild conditions) all eventually constant activations yield the same expressive power - numerical and Boolean - and that it subsumes previously established logics for GNNs with eventually constant activation functions but without linear layers. Finally, we prove the first expressive separation between unbounded and bounded activations in the presence of linear layers: MPLang with ReLU is strictly more powerful for numerical queries than MPLang with eventually constant activation functions, e.g., truncated ReLU. This hinges on subtle interactions between linear aggregation and eventually constant non-linearities, and it establishes that GNNs using ReLU are more expressive than those restricted to eventually constant activations and linear layers.

Figures (3)

• Figure 1: Graphs and Boolean queries used to show non-closure of $\textsf{A-MPLang}\xspace_\mathbb{B}$ in the proof of \ref{['prop:nonclosure']}.
• Figure 2: Simulation of $\sigma(e)$ by a $\textsf{bool}\xspace$-MPLang expression $e'$ as described in the proof of \ref{['thm:eventually-constant-activation-functions']}.
• Figure 3: The red--blue symmetric tree $T[r,b,3]$.

Theorems & Definitions (50)

• Proposition 3.1
• Remark 3.2
• Theorem 3.3
• Example 4.1
• Theorem 4.2
• Corollary 4.3
• Example 4.4
• Proposition 4.5
• proof
• Proposition 4.5