Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Lecture Notes on Verifying Graph Neural Networks

François Schwarzentruber

TL;DR

The notes establish a formal bridge between graph neural networks and logical formalisms by linking GNN computation to WL tests and modal logics with counting. They introduce a counting modal logic K# and its extension K# with global readout to model GNN verification tasks, and provide a PSPACE tableau method for satisfiability. They then show how to encode GNNs as logical expressions and reduce GNN verification to satisfiability problems, including handling of ReLU and quantized activations via truncReLU and existential Presburger arithmetic with star. The work analyzes the expressive limits of color refinement relative to GNNs, details higher-order extensions (k-FWL, k-OWL), and outlines the computational complexity landscape, including NP and PSPACE results, with undecidability results for broad settings. Overall, it offers a rigorous logical toolkit for reasoning about GNN behavior, verification, and equivalence against formal specifications, with practical implications for safety-critical graph-based systems.

Abstract

In these lecture notes, we first recall the connection between graph neural networks, Weisfeiler-Lehman tests and logics such as first-order logic and graded modal logic. We then present a modal logic in which counting modalities appear in linear inequalities in order to solve verification tasks on graph neural networks. We describe an algorithm for the satisfiability problem of that logic. It is inspired from the tableau method of vanilla modal logic, extended with reasoning in quantifier-free fragment Boolean algebra with Presburger arithmetic.

Lecture Notes on Verifying Graph Neural Networks

TL;DR

The notes establish a formal bridge between graph neural networks and logical formalisms by linking GNN computation to WL tests and modal logics with counting. They introduce a counting modal logic K# and its extension K# with global readout to model GNN verification tasks, and provide a PSPACE tableau method for satisfiability. They then show how to encode GNNs as logical expressions and reduce GNN verification to satisfiability problems, including handling of ReLU and quantized activations via truncReLU and existential Presburger arithmetic with star. The work analyzes the expressive limits of color refinement relative to GNNs, details higher-order extensions (k-FWL, k-OWL), and outlines the computational complexity landscape, including NP and PSPACE results, with undecidability results for broad settings. Overall, it offers a rigorous logical toolkit for reasoning about GNN behavior, verification, and equivalence against formal specifications, with practical implications for safety-critical graph-based systems.

Abstract

In these lecture notes, we first recall the connection between graph neural networks, Weisfeiler-Lehman tests and logics such as first-order logic and graded modal logic. We then present a modal logic in which counting modalities appear in linear inequalities in order to solve verification tasks on graph neural networks. We describe an algorithm for the satisfiability problem of that logic. It is inspired from the tableau method of vanilla modal logic, extended with reasoning in quantifier-free fragment Boolean algebra with Presburger arithmetic.

Paper Structure

This paper contains 80 sections, 41 theorems, 70 equations, 6 figures.

Table of Contents

  1. Graph neural networks and Weisfeiler-Lehman tests
  2. Motivation
  3. Graph neural networks
  4. GNN on graphs
  5. Graph isomorphism
  6. 1-WL aka Colour refinement
  7. Description
  8. Example
  9. Implementation
  10. Indistinguishability
  11. Link with isomorphism
  12. Analysis of failure
  13. Colour refinement and GNNs
  14. Colour refinement is self-contained
  15. But GNNs are powerful
  16. ...and 65 more sections

Key Result

Proposition 2

If $G$ and $G'$ are isomorphic then$G, G'$ are cr-indistinguable.

Figures (6)

  • Figure 1: A graph neural network $N$ presented as an algorithm. The main function is $N$. It computes a sequence of labellings $\ell_1, \ell_2, \dots, \ell_L$ via functions $layer_i$. Learnt weights are $\textcolor{blue}{w}, \textcolor{blue}{b}, \textcolor{blue}{A_i}, \textcolor{blue}{B_i}, \textcolor{blue}{b_i}$.
  • Figure 2: Colour refinement algorithm.
  • Figure 3: Decaprismane and dodecahedrane. Two non isomorphic graphs that are 1-WL-indistinguishable DBLP:journals/corr/abs-2003-04078.
  • Figure 4: Model constructed by gluing models obtained from the subcall when diamond formulas are $\Diamond \psi_1, \Diamond\psi_2$ and $\Diamond \psi_3$.
  • Figure 5: Example of a pointed graph $G, u$. We indicate true propositional variables at each vertex.
  • ...and 1 more figures

Theorems & Definitions (102)

  • Definition 1: graph neural network
  • Example 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Proposition 2
  • proof
  • Proposition 3
  • Proposition 4
  • ...and 92 more