A Logic for Reasoning About Aggregate-Combine Graph Neural Networks

TL;DR

The paper defines $K^{\#}$, a modal-logic framework that integrates counting modalities within linear inequalities to precisely capture Aggregate-Combine GNNs (AC-GNNs). It proves a bidirectional correspondence: every $K^{\#}$ formula has an equivalent AC-GNN and every AC-GNN in the studied class has an equivalent $K^{\#}$ formula, enabling formal reasoning about GNNs via logic. It establishes that satisfiability for $K^{\#}$ is PSPACE-complete and shows that essential reasoning tasks about GNNs (e.g., checking equivalence, containment, or non-emptiness of intersections with a formula) can be solved in PSPACE. These results pave the way for applying standard logical methods to GNN querying, equivalence checking, and abductive explanations, with potential for developing verification tools. The work also discusses potential extensions to broader GNN classes and graph settings, aiming to broaden the practical impact of logical reasoning in graph neural models.

Abstract

We propose a modal logic in which counting modalities appear in linear inequalities. We show that each formula can be transformed into an equivalent graph neural network (GNN). We also show that a broad class of GNNs can be transformed efficiently into a formula, thus significantly improving upon the literature about the logical expressiveness of GNNs. We also show that the satisfiability problem is PSPACE-complete. These results bring together the promise of using standard logical methods for reasoning about GNNs and their properties, particularly in applications such as GNN querying, equivalence checking, etc. We prove that such natural problems can be solved in polynomial space.

Figures (6)

• Figure 1: Expressivity of our logic $K^{\#}$ compared to modal logic (ML), graded modal logic (GML) and first-order logic (FO).
• Figure 2: A layer in a GNN transforms the state $x_{t-1}$ at step $t-1$ into the state $x_t$ at time $t$. The figure shows how $x_t(u)$ is computed. First, the function $\mathit{agg}$ is applied to the features in the successors of $u$. Then $\mathit{comb}$ is applied to that result and $x_{t-1}(u)$ to obtain $x_t(u)$.
• Figure 3: General idea of a GNN with 2 layers applied on a graph with 4 vertices.
• Figure 4: DAG representation of formulas. (a) We allow for reusing subformulas. (b) We disallow for reusing arithmetical expressions.
• Figure 5: Example of a pointed graph $G, u$. We indicate true propositional variables at each vertex.

Theorems & Definitions (33)

• Example 1
• Definition 1
• Example 2
• Example 3
• Example 4
• Example 5
• Example 6
• Definition 2
• Example 7
• Definition 3