Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure

Tobias Ladner, Michael Eichelbeck, Matthias Althoff

TL;DR

This work tackles the problem of formally verifying graph convolutional networks under joint uncertainty in node features and graph structure across multiple message-passing steps. It introduces matrix polynomial zonotopes to preserve non-convex dependencies and enable sound, scalable verification, including exact enclosure of graph layers and handling of uncertain edges through a matrix-zonotope framework. The approach achieves polynomial-time complexity in the number of uncertain inputs and edges and is validated on Enzymes, Proteins, and Cora, with subgraph verification significantly boosting scalability. The results demonstrate robust verification capabilities in safety-critical contexts and offer a path toward broader applicability and hardware-accelerated implementations.

Abstract

Graph neural networks are becoming increasingly popular in the field of machine learning due to their unique ability to process data structured in graphs. They have also been applied in safety-critical environments where perturbations inherently occur. However, these perturbations require us to formally verify neural networks before their deployment in safety-critical environments as neural networks are prone to adversarial attacks. While there exists research on the formal verification of neural networks, there is no work verifying the robustness of generic graph convolutional network architectures with uncertainty in the node features and in the graph structure over multiple message-passing steps. This work addresses this research gap by explicitly preserving the non-convex dependencies of all elements in the underlying computations through reachability analysis with (matrix) polynomial zonotopes. We demonstrate our approach on three popular benchmark datasets.

Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure

TL;DR

This work tackles the problem of formally verifying graph convolutional networks under joint uncertainty in node features and graph structure across multiple message-passing steps. It introduces matrix polynomial zonotopes to preserve non-convex dependencies and enable sound, scalable verification, including exact enclosure of graph layers and handling of uncertain edges through a matrix-zonotope framework. The approach achieves polynomial-time complexity in the number of uncertain inputs and edges and is validated on Enzymes, Proteins, and Cora, with subgraph verification significantly boosting scalability. The results demonstrate robust verification capabilities in safety-critical contexts and offer a path toward broader applicability and hardware-accelerated implementations.

Abstract

Graph neural networks are becoming increasingly popular in the field of machine learning due to their unique ability to process data structured in graphs. They have also been applied in safety-critical environments where perturbations inherently occur. However, these perturbations require us to formally verify neural networks before their deployment in safety-critical environments as neural networks are prone to adversarial attacks. While there exists research on the formal verification of neural networks, there is no work verifying the robustness of generic graph convolutional network architectures with uncertainty in the node features and in the graph structure over multiple message-passing steps. This work addresses this research gap by explicitly preserving the non-convex dependencies of all elements in the underlying computations through reachability analysis with (matrix) polynomial zonotopes. We demonstrate our approach on three popular benchmark datasets.
Paper Structure (27 sections, 19 theorems, 61 equations, 12 figures, 3 tables, 1 algorithm)

This paper contains 27 sections, 19 theorems, 61 equations, 12 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Contributions
  4. Background
  5. Notation
  6. Neural Networks
  7. Set-Based Computing
  8. Verification of Feedforward Neural Networks
  9. Problem Statement
  10. Matrix Polynomial Zonotopes
  11. Formal Verification of Graph Convolutional Networks
  12. Verification with Uncertain Node Features
  13. Verification with Uncertain Graph Structure
  14. Subgraph Verification
  15. Experimental Results
  16. ...and 12 more sections

Key Result

Proposition 1

[proposition]prop:image-enclosure Let $\mathcal{H}_{k-1} \supseteq \mathcal{H}^*_{k-1} \subset\mathbb{R}^{n_{k-1}}$ be an input set to layer $k$, then computes an outer-approximative output set. If the layer $k$ is nonlinear (def:act_layer), the output $\mathcal{H}_{k}$ has at most $n_k$ more generators than $\mathcal{H}_{k-1}$.

Figures (12)

  • Figure 1: Graph $\boldsymbol{\mathcal{G}}$ with uncertain node features and uncertain graph structure.
  • Figure 2: Example architecture of a graph neural network.
  • Figure 3: Main steps of enclosing a nonlinear layer. Step 1: Evaluate nonlinear function element-wise. Step 2: Find bounds of the input set. Step 3: Find an approximating polynomial. Step 4: Find the approximation error. Step 5: Evaluate polynomial over the input set. Step 6: Add the approximation error.
  • Figure 4: Enclosure of the inverse square root function. The x-axis corresponds to the degree of a node in $\tilde{D}_\text{diag}$\ref{['eq:degree-matrix']}, and the y-axis to the respective entry in $\tilde{D}_\text{diag}^{-\frac{1}{2}}$\ref{['eq:enclosure-degMat-diag']}.
  • Figure 5: Visualization of \ref{['ex:gnn-simple-example']}. Our approach allows a tight enclosure of the output with uncertain input graph $\boldsymbol{\mathcal{G}}$.
  • ...and 7 more figures

Theorems & Definitions (35)

  • Definition 1: Neural Networks bishop2006pattern
  • Definition 2: Linear Layer
  • Definition 3: Activation Layer
  • Definition 4: Graph Convolutional Layer kipf2017semisupervised
  • Definition 5: Global Pooling Layer
  • Definition 6: Polynomial Zonotope kochdumper2020sparse
  • Proposition 1: Image Enclosure kochdumper2022open
  • Definition 7: Matrix Polynomial Zonotope
  • Lemma 1: Multiplication of Matrix Polynomial Zonotopes
  • Proposition 2: Enclosure of Graph Convolutional Layer
  • ...and 25 more