Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure
Authors: Tobias Ladner
Michael Eichelbeck
Matthias Althoff
Venue: Accepted by TMLR ()

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.

Published in Transactions on Machine Learning Research (04/2025)
Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure
Tobias Ladner
tobias. ladner@tun.ammmmmmmooo.o.m de michael. wwwhelbecc-@uuanmn... de althoff@tum.c de
Michael Eichelbeck
Matthias Althoff
School of Computation, Information and Technology
Technical University of Munich, Germany
Reviewed on OpenReview: https: //pp://eveee.eu net/ per/fo 9 id= 16y12000cP
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 exists research the formal verification of neural networks, there is no work verifying the robustness of generic graph convolutional network architectures with uncerlainty in the node features and in the graph structure over multiple message- 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.
neural networks are prone to adversarial attacks. While there
1 Introduction
A graph neural network extends the typical notion of feedforward neural networks to graph imputs (Kipf & Welling, 2017). Each node in the graph is associated with a feature vector, which is iteratively updated by exchanging information with neighboring nodes using their feature vectors over multiple message-passin steps. They have shown to achieve state-of- taate-of-the-art the-art results in variety of fields (Wu et al. 2020), including advances drug discovery (Zhang et al. 2021), recommender systems in social networks (Ying et al.
2018
and have also been applied salety-critical environments such as power grids (Wang et al. 2022
Stock
ett al. 2022 Wu al. 2022b) and cooperative autonomous driving (Chen et al. 2021).
However, it is well known that neural networks sensitive to adversarial attacks (Goodfellow et al. 2015 where minor perturbations to the input can lead to unexpected predictions. Adversarial examples have also extensively been studied for graph neural networks (Dai et al. 2018 Günnemann, 2022) where both the node features and the graph structure can be perturbed. As graph neural networks are a generalization of many other network architectures to non-Euclidean input data [Bronstein et al. 2017). the existence of adversarial examples not surprising. Thus, neural networks need be formally verified before they can be safely deployed (Brix et al. 2023 König et al., 2024h.
This is particularly important for safety-critical cyber-physical systems. For example, accurate state es- timation is essential for the safe control of power grids, inappropriate power injections might lead to blackouts (Primadianto & Lu 2017). Graph neural networks have been demonstrated for grid parameter identification (Wang et al. 2022) and real-time state estimation (Stock el al.] 2022 Wu el al. (022b), where uncertainties come from unmodelled environment interactions (Bhattarai et al. 2017). manipulation of a few network node sensor readings or, in the extreme case, on the destruction of transmission infrastruc- ture (Liang et al. 20117 Kosut et al. 22011) Similar scenarios also occur cooperative autonomous driving when graph neural networks are applied (Chen et al. 2021h, where distances to other cars inherently

---

Published in Transactions on Machine Learning Research (04/2025)
uncertain and features can be adversarially manipulated to favor their own car. Using formally verified graph neural networks would leverage the capabilities of graph neural networks in safety-critical scenarios.
1.1 Related Work
Most state-of-the-art verifiers only consider standard, feedforward neural networks (Brix et al. 2023 König
et al. 2024]: These can generally be categorized into complete and incomplete algorithms König et al.
2024j. Complete algorithms (Huang et al. 2017 Katz et al. 2017) compute the exact output of a neural network given perturbations on the input. This allows one to either verify given specifications or to extract a counterexample. However, it has been shown that verifying a neural network with ReLU activations requires solving an exponential number of linear subproblems as this problem is NP-hard (Katz et al. 2017). Thus, many existing verifiers use incomplete but sound algorithms (Brix et al. 2023). which can verify given specifications by relaxing the problem; however, this relaxation might prevent them from extracting a counterexample when the specification could not be verified. These verifiers can again be categorized into optimization- based approaches and approaches using reachability analysis.
Optimization-basel approaches formulate relaxed constraints for the activation functions in a neural network. This relaxed problem is then solved using sat bsiisbbbiy modulo theories (SMT) or mixed integer programming
(MIP) solvers (Zhang et al. 2018 Katz et al. 2019 Müller et al. 2022 Tieng et al., 2019 Dutta et al. 2018 symbolic interval propagation (Henriksen & Lomuscio 2020; Singh et al. 2019 Brix & Noll 2020 These
algorithms can be improved using branch-and-bound strategies (Bunel et al. 2020), where the problem is
divided into simpler subproblems. For example, one can split ReLU neurons into their linear parts (Botoeva
et al.] 2020 Singh et al. 2018b). Such branch-and-bount strategies (Wang et al. 2021 Ferrari et al. 2022
Shi et al. 2023 are currently the dominant strategies in state-of-the-ar verifiers (Brix et al. 2023
On the other hand, one can use reachability analysis to verify a neural network by computing an enclosure of the output set. This is realized by propagating the perturbed input set through each layer of the neural network and bounding all approximation errors. Early approaches propagate convex set representations
through neural networks, such as intervals (Pulina & Tacchella 2010) and zonotopes (Gehr et al.) 2018 Singh
et al. 2018a). Non-convex set representations can improve the verification results as the exact output set can
be non-convex due to the nonlinearities within the network. These approaches use Taylor models [Tanov
iet al.] 2021 Bogomolov et al. 2019 Huang et al. 2022), star sets (Bak) 2021 Lopez et al. 2023 and
polynomial zonotopes (Kochdumper et al.] 2023: Ladner & Althooff 2023 to verify neural networks. Branch-
and-bound stralegies are also used in approaches using reachability analysis (iiang el. al. 2018).
To the best of our knowledge, there exist only few approaches considering the formal verification of graph neural networks. As with feodforward neural networks (Katz et al.] 2017). the theoretical limits of the graph neural networks verification problem have been discussed (Sälzer & Langee 2023). Thus, most existing methods for verifying graph neural networks again employ incomplete but sound algorithms: Some approaches (üügner& & Günnemann 2019 Bojchevski & Günnemann 2019) formulate uncertainty in the semi- supervised node classification setting as an optimization problem, where uncertain node features (Zügner & Günnemann] 2019) and uncertainty in the graph structure (Bojehevski & Günnemann, 2019) are considered scparately. The network architecture in the latter approach only has single, slightly altered messago-passe passing step. This approach is extended to restrict both the global and the local uncertainty of the graph QJin el al. 2020a). Another approach (Wu et al. 2022a) verifies uncertain node features in graph neural networks for job schedulers by unrolling them into feodforward neural networks and verifies them using reachability analysis. It also worth mentioning that probabilistic guarantees can be achieved using randomized smoothing (Jia) ett al.] 2020 Bojchevski al., 2020), and one can try to defend adversarial attacks (Jin et al.] (020b): however, these approaches do not provide formal guarantees. Thus, such approaches are not directly usable in safety-critical environments where one has to guarantee safety.
1.2 Contributions
Our contributions are as follows:
2

---

Published in Transactions on Machine Learning Research (04/2025)
Uncertain node features C R
2
6
5
3
Presence of edge unknown
Figure 1: Graph with uncertain node features and uncertain graph structure.
We present the first approach to verify graph convolutional networks with uncertain node features and an uncertain graph structure input over multiple message- message-passing steps (Fig. I The con- sidered architecture of the graph convolutional network is generic and can have any element-wise activation function.
We explicitly preserve the non-convex dependencies of all involved variables through all layers of the graph neural network using (matrix) polynomial zonotopes.
The resulting verification algorithm has polynomial time complexity in the number of uncertain input features and in the number of uncertain edges.
We demonstrate our approach on three popular benchmark datasets with added perturbations on the node fcatures and the graph structure.
This work is structured follows: In Sec. statement, followed by defining the matrix variant of polynomial zonotopes in Sec. Our verification approach is described in Sec. We first show that graph-based layers in neural networks can be computed exactly using matrix polynomial zonotopes with only uncertain input features. The required adaptations when also the graph structure uncertain are described subsequently. Finally, we show experimental results in Sec. d and draw conclusions in Soc.
introduce all required preliminaries and the problem
2 Background
2.1
Notation
We denote scalars and vectors by lowercase letters, matrices by uppercase letters, and by calligraphic letters. The i-th element of vector R is written (())- The clement in the i-th row and j-th column of matrix A E Baxm is writlen A(,)), the entire i-th row and j-th column are written A(..)) and Aca)) respectively. The concatenation of A with a matrix B E Raxo is denoted by [A B] Rax(m++)) The emply matrix written as []. We denote with In the identity matrix of dimension 0 and 1 refer to matrices with all zeros and ones of proper dimensions, respectively. Given E N, use the shorthand notation [n] = (1....,n) The cardinality of a discrete set D is denoted by [D). Let D C [n]. then A(D,,) denotes all rows E D in lexicographic order; this is used analogously for columns. Let C R" be a set and f: R2 + R be a function, then S(S) = (f(x) x E S). An interval with bounds a, b E R" is denoted by [a, 6], where a < holds semenntwwiee.
N. The symbols
2.2 Neural Networks
Let us introduce the neural network architectures we consider in this work. We start by stating a general formalization of neural network and, afterward, several types of layers.
3

---

Published in Transactions on Machine Learning Research (04/2025)
k Message Passing Steps
Non-Gree Senn-Grahh-aaas Layers
Global Pooling
Input X, g
Output y
LGc
LACT LE
1 +1
LIIN
LACT
Figure 2: Example architecture of graph neural network.
Definition 1 (Neural Networks Bishop & Nasrabadi 2006 Sec. 5.1)). Let x E R be the inpul of a newral network & with K. layers, its output y = ((x)= E R" is obtained as follows:
ho = x, hg T ())- & [M],
y hx-
where Tx: 1R - Th represents the operation of layer k.
Standard, non-graph-based neural networks are usually composed of alternating linear layers and nonlinear activation layers:
Definition 2 (Linear Layer). A linear layer is defined by the operation
he = LIN (hs-1) Wwhu-- + bb.
with weight matris We E R and bias veclor by TR.. Definition 3 (Activation Layer). An activation layer is defined by the operation
hg = T.ACT T.ACT (hu-1)
hh (hx-)))
where (+) is the respective element- wise nonlinear activation function, e.g., sigmoid or ReLU.
Graph neural networks generalize standard neural networks and additionally take graph = (N, E) as an input, where N C N denotes the set of nodes and & S / x x the set of edges of G. For each node E N, associate feature vector X(.) E RIx with Co input features,
illustrated in Fig, 1 These feature
vectors of all I.] nodes are stacked vertically to obtain the input feature matrix X E R| Graph neural networks contain message-passing layers in which neighboring nodes exchange information (Fig. (2). In this work, consider the well-established graph convolutional layer (Kipf & Welling 2017), which combines node-level lincar layer and mossage-passing layer:
Definition 4 (Graph Convolutional Layer Kipp & Welling 2017 Eq. 2)). Given
weight matrix
W E R Kic,, an adjacency matria A E P of graph g. and an input Ha-1 E R 1. Let Ā A+ |N be the adjacency matrir with added self-loops and π = diag(1A) E RMVX be the diagonal degree matria. The computation for a graph convolutional layer k computed as
H = LGC (F) AD A H
The term P- P- computes the message passing between nodes. The adjacency matrix can also be weighted adjacency matrix for graphs with scalar edge weights (Kipf & Welling 2017 Sec. 7.2). Please note that activation layers (Def. 3 work identical for matrix inputs H₃ instead of vectors hg-
Please note that related verification approaches considering uncertainty in the graph structure (Bojchevski & Günnemann, 2019 Jin et al. 2020a) consider Á instead of D in their message passing step. This justified by the argument that corresponds to the personalized page rank matrix, which has a similar spectrum. However, without appropriate approximation errors, the verification of the original graph neural network remains unknown using this modification.
4

---

Published in Transactions on Machine Learning Research (04/2025)
Depending the use case, we let graph neural network & return node-level graph-level output. For node-level output, the output is simply the feature matrix of the last. layer: Y = (x TR| For a graph-level output, we aggregate all node feature vectors into single graph feature vector. Thus, = ( g E R This realized using a pooling layer, which is computed as follows:
Definition (Global Pooling Layer). A global pooling layer aggregates all node feature vectors HK-1 E R X within graph 9 into single graph feature vector h& RR as follows:
hg = GP
where vo(-)) denotes permutation invariant aggregation function across all nodes, e.g., sum, mean, mazimum.
For example,
the (b)))=1)) = (1Hxx1))
(1)
computes summation across all nodes in a global pooling layer k. For graph neural networks with graph-level output, there can be regular linear and activation layers after the pooling layer (Fig. 2
2.3 Set-Based Computing
We verify neural networks using continuous sets. For input set X Ro of neural network 4, the exact output set )" (xY) is computed by
H X, H I (H k e
(2)
y" H.
Polynomial zonotopes are well-suited set representation to verify graph neural networks due their polynomial computational complexity of the required operations. We briefly introduce polynomial zonotopes and all required operations here and give details and an example this set representation in Appendix A
Definition 6 (Polynomial Zonotope (Kochdumper Althoif 2020 Given an offset e R", a generator matrix of dependent generators G E Ra*h a generator matria of independent generators G E Raxq and exponent malrir E. E Npxh with identifier id E No, polynomial zomolope PZ (c, G, Gr, F) F) is defined as
P
9
PZ
c+
II
E(ca) a
G( + Σ 3,G1(.0) ax Me.Bee--1.1)
The identifier id is used to keep track of the dependencies of the factors o& between different polynomial zonotopes. Given two polynomial zonotopes PZ₁ (cr, (e, GI.,, E1) E.).E1))22 PZ2 (c2, G2 Gr,2, E2) R" the Minkowski sum is computed by (Kochdumper & Althoff 2020
Prop. 8)
p2, ( P2, = (0) + +32 æn E P2,, 32 E PZ2)
= =(c1 ci + c2, [G1 G2), [Gr, Græ)].
Ei
(3)
Eg PZ
and given E pm e Rm, the affine map is computed by (Kochdumper & Althoff 2020
Prop. 9)
APZ, + b= {Ar b x P21] (Acı b, AG1, AG11, E1)
(4)
As in Kochdumper 2022 adapt the definition from Kochdumper Althoff (2000 and not integrate the offset into the generator matrix and omit the identifier almost always simplicity.

---

Published in Transactions on Machine Learning Research (04/2025)
(a) Steps & 2
(b) Steps 3 & 4
(c) Steps 5 & 6
Output
Oulput
Output
Input
Input
Input
Set
Bounds
Polynomial
Approximation
Figure 3: Main steps of enclosing a nonlincar 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 Evaluate polynomial over the input set. Step 6: Add the approximation error.
2.4 Verification of Feedforward Neural Networks
Finally, we briefly introduce the main steps to propagate a polynomial zonotope through a standard, non- graph-based neural network (Def. D Since the set propagation through neural network (2) cannot be computed exactly in general, have to enclose the oulput of each layer:
Proposition 1 (Image Enclosure (Kochdumper et al. 2023 Sec. 3)). Let Ha-1 2 Hz-1 C R be
impul set to layer k, then
H4 = enclose(Ls, Ha-1) 2 Hi C R"
computes anter-approcimatioe output set. If the layer k is nonlinear (Def. 3, the output Hy has at most more generators than H4-1-
Using polynomial zonotopes, the output of a linear layer can be computed exactly
44 however, the output
of activation layers needs to be enclosed to obtain a sound outer approximation. We summarize the six main steps enclose nonlinear layer next and visualize them in Fig. 3 As we only consider element-wise activation functions,
enclose each neuron individually (step 1). In step we find bounds for input set. Next, we approximate the activation function using a polynomial (step and find an appropriate approximation error (step 4). Finally, the chosen polynomial is evaluated over the input set (step 5), and the output is enclosed using the approximation error (step 6), where one generator for each neuron of the current layer is added using (3). While we have depicted the steps in Fig. 3 using a polynomial of order one, higher-order polynomials can be used to obtain tighter enclosure (Ladner & Althoff 2023) using multiple applications of Prop. 6
2.5 Problem Statement
Given an uncertain graph 9 (N, E) with nodes N N and edges E' N consisting of fixed edges Ex and uncertain edges E, an uncertain input feature matrix X' C IR Nix,, a graph neural network 4 and an unsafe set C Rn where n. denotes the dimension of the output of Φ we want to compute an outer-approximative output set y such that encloses the output for all possible graph inputs:
Aε EE (x (N, 8 (E)) cV.
We can then verify the given specification by showing that: yns
Please note that the threat model considers the case where an attacker only has access to limited number of edges E. For example, an altacker partially controls the infrastructure of a power grid and can thus destroy certain connections. Therefore, we cannot be sure if the edges ? are present, leading to 2 gl possible graph inputs with uncertain node features.

---

Published in Transactions on Machine Learning Research (04/2025)
3 Matrix Polynomial Zonotopes
Before we present our approach, we introduce an extension to polynomial zonotopes to address a key challenge in the set-based evaluation of graph neural nelworks: Graph convolutional layers require a matrix Hk-1 E R as input (Def. 4 which means that uncertainty must be represented as set matrices. particular, set-based evaluation requires propagating uncertain matrices H4-1 C RIM through all layens, which we want to represent as polynomial zonotopes; however, a (standard) polynomial zonotope cannot represent set of matrices (Def. B To overcome this limitation, we define its matrix variant and few required operations on them in this section. While our focus is on verifying graph neural networks, matrix polynomial zonotopes are generic and have applications beyond this domain.
Definition 7 (Matrix Polynomial Zonotope). Given an offset C E IRxx", dependent generators G E R independent generators G₁ __xxxx, and exponent motriz E E Npxh with an identifier id E No, matriz polynomial zonotope PZ GI, P) C CRax
is defined as
h
P
PZ
C+
Σ
II
Og
G( + Σ 3,G1(05) 3x, E11,111-1,11
Please note that the sum in Def. 7 adds matrices instead of vectors (Def. 6), and each element of the set PZ C R2xm is a matrix: VX E Pz: E Raxm Thus, matrix polynomial zonotopes are a gen- cralization of standard polynomial zonotopes. The Minkowski sum of two matrix polynomial zonotopes P2, (C1, Gr,1, Pz) P22 = (C2, G2, Gr,,, F2) C Raam is computed analogously to (3:
p2 @ P22 (X1 X2 Xi P21, X2 E22)
E
(5)
C1 + C2 [G G2), [rr,1 Gr
[o
E2
P2
where the concatenation of the generators is along the last dimension. Given the matrices A₁ E Rkxn, Ag E Bmxk and the vectors dy RR ba Baxk, affine map is computed analogously to
A,P2, b = {A,X +h Р2 + b2 (xA2+M) b2 X E = (C2 A2 + b2, G1 G2, E1)
X X = (A, + bh, A,G,, A,Gr, E1)
(6a)
(6b)
where the matrix multiplications are broadcast across all generators. Reshaping and transposing matrix polynomial zonotope are computed by applying the respective operation on the center and each generator, respectively. In particular, reshaping a matrix polynomial zonotope into vector by stacking it column- results a standard polynomial zonotope, which we indicate by a vector decoration (δ). This allows us, for example, to seamlessly use a matrix polynomial zonotope H4-1 C ggMxxe during the enclosure of an
activation layer & by first reshaping it: Ha-1 C R M--1, then obtain Hd C R| using Prop. 1 and finally reshape it back to its original shape: H4 C RlAxx.
During the verification of graph neural networks, we also require the multiplication of two matrix polynomial zonotopes, which can be computed without inducing additional outer approximations.
Lemma 1 (Multiplication of Matrix Polynomial Zonotopes). Given two matriz polynomial zonotopes M1 (Ca, G1, E1) C Rnnk M2 (C2, G2. [ E2) C B with h1, h2 generators, respectively, and common identifier, then their multipliention is obtained by
M3 = Mi MM = M2) | Mi E M1, M2 E M2)
= (cc, C2 G2 T
Gm [n,
Eg E, EAd)) PZ
C maxm
where
C-C,C, GzC, G2ZG a GI
F F1 1 1 Fez
Vi [h]]
The matria muulliplications are broadeast across all generators. The oulput Ma has (1h)2) generators.

---

Published in Transactions on Machine Learning Research (04/2025)
Proof. See Appendix B
This operation is generalization of the multiplication of zonotopes (Althoff al, 2011 Eq. (10))
and also has connection to the quadratic map operation of polynomial zonotopes (Prop. 6/. Please visit
Appendix A and the proof in Appendix B for details. Additionally, we discuss the efficient implementation of this operation on GPU in Appendix
4 Formal Verification of Graph Convolutional Networks
In this section, we demonstrate how to generalize the verification of standard neural networks (Kochdumper et al. 2023 Ladner Althoff 2023) to graph convolutional networks. We start by (i) explaining how to verily graph neural networks that have only uncertain node features, and then (ii) describe the adaptations where, additionally, the graph structure is unknown. Moreover, extracted in cases where not the entire graph is relevant to verify the specification. Please follow Sec. 2.2 along with this section for the exact equations and the required adaptations made here if the inputs are scts.
show (iii) how subgraph can be efficiently
4.1 Verification with Uncertain Node Features
Uncertainty in the node features requires us to define how the graph-specific layers can be enclosed for an uncertain input. Using matrix polynomial zonotopes, the enclosure of a graph convolutional layer (Def. does not induce any additional outer approximation.
Proposition 2 (Enclosure of Graph Convolutional Layer). Given are weight matrix We E RC-- a graph G (N, E), and an input Hk-1 C R| represented as a matrix polymomial zonotope. Let A E [M be the adjacency matrix of 9, A A 4NT,, and let D = diag(1A) E R| be the diagonal degree matriz. The ezact output of a graph convolutional layer k Def. is computed by
GC (H+-1) = D AAD W H4 = Lk
Proof. See Appendix
The enclosure of pooling layer (Def. 5) with a summation as aggregation function as in 1 obtained analogously.
Proposition (Enclosure of Summation Pooling Layer). Given graph 9 and an imput Ha- 1 C RlA represented as a matriz polynomial zonolope, the exact oulput of a pooling across all nodes sunsmation is computed by
Hss = LE (HH-H119 =(1Hs-1)
Proof. See Appendix B
Thus, the graph-based layers can be computed without inducing additional outer approximations using matrix polynomial zonotopes when we only have uncertain node features.
4.2 Verification with Uncertain Graph Structure
Verifying graph neural networks bocomes more difficult if the presence of some edges is unknown in an uncertain graph g. This case requires us to enclose the outputs of all possible graph inputs (Sec. 2.5). We enclose these outputs by computing an aprroxiapooi output set of an equivalent graph with uncertain edge weights: Let have fixed edges Ex and uncertain odges E. Then, we set the edge weight for odges in Ex and the interval [0, 1] for edges in E. This uncertainty requires a set- bet-based evaluation of the message passing P - i AD- in graph convolutional layers (Def. 4). In particular, now have uncertain

---

Published in Transactions on Machine Learning Research (04/2025)
0.8
Inverse square root at -//
Approx. polynomial p(x)
Output
0.6
Approx. error
0.4
1
1.5
2
2.5
3.5
4
4.5
5
5.5
6
6.5
7
7.5
Inpuu x
Figure 4: Enclosure of the inverse square root function.
The x-axis corresponds to the degree of node in 91. and the y-axis to the respective entry in Daing
D
Dding
10
(weighted) adjacency matrix A C WM containing the respective edge weights, which in turn leads to an uncertain degrec matrix C RIMX| and eventually, an uncertain message passing
D D'=
(7)
Please note that the same applies the graph has uncertain scalar edge weights. Subsequently, we detail the required steps to compute an enclosure of the message passing P 2 p using matrix polynomial zonotopes (Def. 7 Please compare these steps with the definition of a graph convolutional layer (Def. 4 We construct the uncertain adjacency matrix matrix polynomial zonotope A C RW]xXW] where each generator of A corresponds to one uncertain edge. Then,
Ā= A+ [
(8)
adds self-loops to the adjacency matrix. Analogously to Prop. we compute the diagonal entries of the degree matrix D by summing across all rows of using 0
Daing = (1A)T.
(9)
To obtain D-1, we note that the inverse of diagonal matrix is given by the inverse of each entry on the main diagonal. Additionally, we are required to compute the square root of each entry individually. However, polynomial zonotopes are not closed under these operations. Thus, we enclose the output of the inverse square root function using Prop. [ The function is already applied element-wise, hence, it suffices to provide appropriate approximation error:
Lemma 2 (Approximation Error of Inverse Square Root). Given polynomial p(æ) = ax + approzimaling the inverse square root f(x) & on the domain [1, u] C E,, then the mazimum approzimation error is
d = max [f(x) ((t)) = 1f(x*) =E
p(x))l.
where
x" E {1,, 1./12/1/2))))) 2 011,
Proof. See Appendix
An example the enclosure of the inverse square root function for a polynomial found via regression is shown in Fig. 4 A tighter enclosure can be obtained using higher-order polynomials (Ladner & Althoff 2023) (scc
also Appendix D.2.1 Thus, we can enclose the diagonal entries of the degree matrix using Prop. |
D ding = enclose xt + x Dainn)) 2 D
(10)
ding!
9

---

Published in Transactions on Machine Learning Research (04/2025)
and place the entries D dlag on the main diagonal of
D diag D
2 D- dlagg
(11)
This computed by first projecting dimensions:
D dlag
C
IR M into a higher-diimensional space with zeros in the new
D 1S
Dani CRMI diag
(12)
where K. [M " contains the indices of the diagonal entries of diagonal matrix, and then
reshaping the polynomial zonotope to obtain D-1 1 c R| To obtain the entire uncertain message
passing P, we compute the matrix multiplication on the involved matrix polynomial zonotopes D- and A using Lemma
Proposition (Enclosure of Uncertain Message Passing). Given an uncerlain adjacency malrix A with h generators, then
= D BAAD Pt,
encloses the message passing with O(h)) generators.
Proof. See Appendix B
After obtaining the uncertain message passing P, we can enclose the output set of graph convolutional layer as follows:
Proposition 5 (Enclosure of Graph Convolutional Layer). Given are weight matria Wa R an uncertain graph G, and uncertain input HA-1 E IR M with hn generators. Let P C RIMIXIMI be the uncerlain message passing according to Prop. 4 with O(1)) generalors. The oulput for graph convolutional layer & (Def. is enclosed by
H4- enclose GC Ha-1, P) -PP DP HR-1)W& S LE (Ha-1,9),
with O(rrh)) h3) generators.
Proof. See Appendix
Our approach defines the enclosure layer-wise and thus realizes an arbitrary concatenation of the considered layers. To demonstrate the polynomial time complexity in the number of uncertain edges and input features for entire graph neural network with multiple message- pessage-passing steps, let consider the architecture visualized in Fig. 2 Alg. | computes the enclosure of the output set follows: The graph neural network has Ke' message-passeeee passing steps, cach consisting of one graph convolutional layer and one activation layer (lines 3 to (). For nelworks with a node-level output, the output of the last mnessage-passing step is directly the output of the network. For networks with a graph-leve output, the output is passed to a global pooling layer and optionally followed by standard, non-graph-bar layers (lines I1 to 14 With this algorithm, we can state the main theorem of this work:
Given a neural network & with i. layers and k' message passing sleps, an uncertain graph G (N, E) with W nodes and he uncertain edges, and an uncertain input X C. |ixi with he generators, then Alg. [ satisfies the problem statement in Sec. 2.5 The number of generators of the computed output enclosure y is given by:
Theorem
hy E -0( (hx [WCmmx) + (K 22." Mmmax) 2xxx'mmmxx)
where Cmax == max Czke denotes the marimum number of features within the graph layers and Rmax = maxpe(2n'+2.... mh denole the mazimean reumber of oulput neurons of the non-graph-bused layers after the global pooling layer.
Proof- See Appendix
10

---

Published in Transactions on Machine Learning Research (04/2025)
Algorithm Enclosing the Output of Graph Neural Network
Require: Neural network @, number of layers K, number of message passing steps k', imput set X, graph g.
1: Ho <- X'
2: p + Compute message passing based on g
>> Prop. 4
do 4: -x + enclose LGC 2x'2, P)
3: for k' = ,, 2k'
D Graph-based layers
> Prop.
5: H f enclose L ACT -1)
>> Prop.
6: end for
7: k = 2x' then
>> Graph-level output
V Hx.
else
Node-level output
10:
Ha 2'2x'1 (H2x's 9)
Global pooling layer, Prop. 3
11:
for k = 2n' + 2, 21' + .,...... do
b Standard, non-graph-based layers
12:
H4 t Lk
LIN (H+-1)
> Def. 2
13:
H4+1 < enclose
[ACC H.))
b Prop
14:
end for
15:
V Hr
16:
end if
17: return Enclosure of output set y 2 y"
Please note that all involved operations on polynomial zonotopes compute the output set 3 (affine map 6 Minkowski sum (5) and multiplication of (matrix) polynomial zonotopes (Lemma D have polynomial time complexity [Kochdumper] 2022] Tab. 3.2), and that the time complexity is dominated by the number of generators resulting from the applied multiplication of matrix polynomial zonotopes (Lemma D Thus, it follows directly from Thm. [ that Alg.
[ has polynomial time complexity in the number of uncertain input features h2 and uncertain edges hg compared to am exponential complexity when all 2d possible graphs need be verified individually. While our approach exponential in the number of message-passing steps n', we want to stress that x' usually small avoid ever-smoothing (Chen al.) 2020). To further improve the scalability of our approach, the number of generators
be limited using order reduction methods (Ladner] & Althoff 2024 Kochdumper 20022] Prop. 3.1.39) at the cost of additional outer approxinations (see also Appendix D.2.2 Additionally, we want to stress that many involved operations can be parallelized and efficiently be computed on a GPU (Appendix C
Let us demonstrate our approach for verifying graph neural networks by a small example:
Example 1. Let & be neural network with input x, graph 9, and output Y computed by two layers:
H1 g (X,9),
with W W2 12.
Y L GC 9H,
The input graph (N, E) is chosen
N -=
8=
2 1 2
and the input features for each node are
((,,) X(2.)
0.9. 1.1 [0.9. 1.1
H Thus, X=
Xa.)
X(2.) X(3.))
X
Let us now consider the presence of the edge Thus, the uncertainty of the features of node 1 is passed to node 3 after one message passing step if the edge 1-3 is present (in Hi I, (X,)),, and after two steps otherwise (in y T. via 2
as unknown during the evaluation of y ( g).
3
11

---

Published in Transactions on Machine Learning Research (04/2025)
(a) Craph g
(b) Message passing P
(c)
Hidden H1 of
(d) Output of
0.6
1.05
1.05
0.4
P(.3))
H (1,22)
Y13.2)
0.2
0.95
0.95
2
0.9
0.9
0.35
0.4
0.9
0.95
1.05
0.9
0.95
1.05
((.
(1(3.1)
Y(3,1)
Exact with
Exact without
1
3
Enclosure uncertain 1
3
Subset with
Subset without
Enclosure interval arithmetic
Figure 5: Visualization of Example input graph g.
Our approach allows a tight enclosure of the output with uncertain
Example is visualized in Fig. The input set X' given as an interval is converted to (matrix) polyno- mial zonotope (Kochdumper 2022, Prop. 3.1.10). We can obtain the exact output set for either case by propagating the respective graph through the network (purple and green) as well as their enclosure using our approach (Thm. I blue). Please note that we explicitly preserve the dependencies between the consid- ered sets via the identifier vector of matrix polynomial zonotope (Def. 7 We visualize the preserved dependencies in the enclosure of the uncertain edge: By plugging -1 and into the dependent factor ar corresponding to the uncertain edge, obtain the subset (Kochdumper) 2022 Prop. 3.1.43) corresponding to the respective case (orange and yellow). This demonstrates the tightness of our approach.
Additionally, we show the respective message passing P from node 1 to the nodes 2 and 3 for each case (purple and green) as well as their enclosure (blue), where we use a polynomial of order 2 to enclose D.-
ding in 11). While the message passing from node 1 to 3 trivially becomes 0 if we remove that edge, the message passing from node ! to also changes due to the normalization during the computation of P through the degree matrix. Moreover, we want to point out that the enclosure P is a non-convex, slightly bent stripe. Please note that the enclosure of the output y can also be non-convex in general. For include enclosure of the uncertain message passing P using interval arithmetic (Jaulin et al. 2001) in Fig. 5 We omit the enclosure of Hi and y" using interval arithmetic the obtained intervals are so large that the results using our approach described above would be barely visible, even for this small example. This large outer approximation comes from the lost dependencies between all involved variables.
comparison,
4.3 Subgraph Verification
For a graph neural network with node-level output, we are not always required to propagate the entire graph through all layers of the network. Given node of interest and a network with x' message passing steps, we are only required to verify the subgraph within the (x' + 1)-hop neighborhood
all other nodes do not influence the considered node (Zügner & Günnemann 2019 We require (w' + 1) hops due to the normalization through the degree matrix in the message passing (Def. 4.. The (w' 1)-hop neighborhood can easily be found using a breadth-first search on the given graph with the considered node as the root node. The graph and the respective feature matrix can be reduced as follows:
Corollary 1 (Subgraph Selection). Given an input Ha-1 RWixxe-1 to layer k, the message passing P D AD E RMxx of graph G, and the node indices K. of a subgraph g', we can construct projection matris M = [[NTUC)) such that
Ha-1= -HH-11 P'= TPM
contain the imput and the message passing corresponding to the subgraph.
12

---

Published in Transactions on Machine Learning Research (04/2025)
Table Properties of the benchmark datasets.
Name
Classification
# Graphs
#Nodes min/max
#Edges min/max
# Node features
# Classes
Perturbation
Co
R2
e
Enzymes
graph-level
600
11/66
34/186
21
0.001
Proteins
graph-level
1,113
4/238
10/869
4
2
0.001
Cora
node-level
1
2,708
10,556
1,433
7
0
Proof. See Appendix
After each graph convolutional layer (Def. []. we can further reduce the graph the number of remaining message-passinn passing steps decreases. This can be achieved by implicitly adding projection layers computing Cor. D after each graph convolutional layer. After the last graph convolutional layer, except for the considered node, as no information is exchanged between nodes from that point onward. This approach can also be naturally extended to multiple nodes of interest by considering all of them during the breadth-first search. As the selection of the subgraph only requires left and right matrix multiplications,
remove all nodes
Cor. 1 can also be computed the input H4-1 C R [Vxx or the message passing P C R (g X are uncertain and represented by matrix polynomial zonotope using (6)
5 Experimental Results
We use the MATLAB toolbox CORA (Althoff 2015) to verify graph neural networks, where we generalizo the existing approach of verifying neural networks using polynomial zonotopes (Kochdumper et al. 2023
Ladner Althoff 2023) to the graph domain. All computations were performed on an Intel Core Gen. 11 17-11800H CPU @2.30GHz with 64GB memory. Further evaluation details can be found in Tab. and Appendix D along with ablation study of cach component of our approach.
Subsequently, we (i) demonstrate that verification of graph neural networks on two benchmark datasets (Enzymes (Schomburg et al. 2004) and Proteins (Borgwardt et al.) (005)), (ii) compare our approach to a naive approach enumcrating all possible graph imputs, and (iii) test the scalability of our approach to large graph inputs taken from a third dataset (Cora") (Yang el al.j 2016 McCallum al. 2000b). We repeat each experiment 50 times with different graphs sampled from the respective dataset.
5.1 Verfiying Graph Neural Networks
In our first experiment, we examine the number of verified graphs with uncertain node features and uncertain graph structure by our approach (Fig, 6 The graphs are sorted by their size in ascending order, and we state the number of uncertain edges E relative to the total number of edges of a graph for better comparability across differently sized graphs. Surprisingly, we are able to verify more instances in the Proteins dataset than in the Enzymes dataset although the former contains larger graphs (Tab. [ This indicates that the networks trained on larger graphs are more formally robust against graph structure perturbations despite the normalization of the perturbation to the graph size. We omit a comparison due to
interval bound propagation (Jaulin et. al.) 2001) here as such results in large outer-approximationn the lost dependencies also shown in Example 1 To verify the specifications, excessive branch-and-bomm computations would have to be performed, which quickly exceeds reasonable timeouts. This highlights the necessity to maintain the dependencies during the set propagation.
5.2 Comparison to Graph Enumeration
In our second experiment, we evaluate the time complexity on graphs with uncertain node features and uncertain graph structure. For this experiment, we iteratively increase the number of uncertain edges E.
2The idinticall names of the toolbox CORA and the dataset Cora are coincidental, with no relation het ween the two.
13

---

Published in Transactions on Machine Learning Research (04/2025)
(a) Enzymes
(b) Proteins
Verified instances [%)
0.8
0.8
0.6
0.6
0.4
0.4
0.2
0.2
200
400
600
800
1,000
1,200
500
1,000
1,500
2,000
2,500
Cumulative verification time [s]
Cumulative verification time [s]
El 0.0%
[
0.1%
= 0.5%
|
1.0% [ 5.0%
Figure 6: Verified instances of the Enzymes dataset and the Proteins dataset, where the number of uncertain edges |8| is relative to the total number of edges |8| in the graph. The dotted lines marked with indicate upper bound of verifiable instances found via adversarial attacks (Appendix D.1
(a) Enzymes
(b) Proteins
Verificatiom time [s] [
60
60
40
40
20
20
Number of uncertain edges
Number of uncertain edges
Graph enumeration
Our approach
Figure 7: Time comparison of our approach with computing all possible graphs individually, where we normalized the verification time by the number of nodes [V] of the verified graphs.
and compare to enumerating all zi possible graphs based on the uncertain edges and verifying them individually. As illustrated in Fig. 7 the verification time using enumeration quickly explodes due to its exponential time complexity, whereas the verification time of our approach remains low due to its polynomial time complexity (Thm. D. Specifically, for E = 9, the verification time is reduced by 96%.
5.3 Scalability Through Subgraph Verification
In our third experiment, we demonstrate the scalability of our approach by applying it on the Cora dataset. For this dataset, we do not use a perturbation radius (c = 0) as the input data is binary and thus pertur- bations do not have an intuitive justification. As this dataset has node-level output, we can dynamically remove nodes that do not influence considered node throughout the verification process (Sec. 1.3). How- ever, want to stress that, average, about half of the nodes have to be considered initially, the graph is highly connected. The verification results for two graph neural networks with different numbers of peessgg-ppssingg steps (w' = 2 and k' = 3) are shown in Fig. g We obtain high verification rates despite the large size of the graph of the Cora dataset (Tab. D. Please note that for a fixed number of perturbed odges, the verification time varies significantly despite always verifying a node on the same graph. This is primarily due the dynamic subgraph extraction being able remove many nodes and, thus, obtaining a 7 speed up in computation time. Additionally, dynamically reducing the size after each message passing
14

---

Published in Transactions on Machine Learning Research (04/2025)
(a) Cora (w' 2)
(b) Cora (x' 3)
Verified instances [%)
0.8
0.8
0.6
0.6
0.4
0.4
0.2
0.2
0
100
200
300
400
500
600
200
400
600
800
1,000
1,200 1,400 1,600
Cumulative verification time
Cumulative verification time [s)
0.0%
0.1%
0.5%
1.0%
- E 5.0%
Figure 8: Verified instances of the Cora dataset with different numbers of message-passing steps, where the number of uncertain edges [8]] is relative to the total number of edges [8] in the graph.
step allows us to verify 2-3 times larger graphs measured in the number of nodes that need to be considered at the input of the network.
6 Conclusion
We present the first formal verification approach for graph convolutional networks, where both the node features and the graph structure can be uncertain. The considered network architecture is generic, may have arbitrary elerent-wise activation functions, and, for the first time, can be verified over multiple message- passing steps. This realized by generalizing existing verification approaches using polynomial zonotopes to graph neural networks. The use of (matrix) polynomial zonotopes allows dependencies of the involved variables and efficiently compute all underlying operations, resulting in an overall polynomial time complexity in the number of uncertain edges and uncertain input features. We demonstrate our approach using illustrative examples and an experimental evaluation on three benchmark datasets obtaining three key observations: Firstly, important to maintain the dependencies throughout the set propagation for tight enclosures during the verification of graph neural networks. Secondly, the polynomial time complexity our approach enables the verification of graphs with uncertain node features and uncertain graph structure in reasonable computational times. Lastly, the computation time can be further accelerated graph neural networks with node-level outputs by dynamically extracting the relevant subgraphs after cach message passing step. We hope that our work will inspire future rescarch on more complex network architectures.
preserve the non-convex
Acknowledgments
This work was partially supported by the project FAI (No. 286525601), the project SFB 1608 (No. 501798263), and the project SAFART (No. 458030766), all funded by the German Research Foundation (Deutsche Vorschungsgunninschaff, DFG). We also want to thank our colleagues Florian Finkeldei, Lukas Koller, and Mark Wetzlinger for their revisions of the manuscript.
References
Matthias Althoff. An introduction to CORA 2015. In Proceedings of the Workshop Applied Verification for Continuous and Hybrid Systems, pp. 120 151, 2015.
Matthias Althoff, Bruce Krogh, and Olaf Stursberg. Analyzing reachability of linear dynamic systems with parametric uncertainties. Modeling, Design, and Simulation of Systems with Uncertainties, pp. 69-94, 2011.
15

---

Published in Transactions on Machine Learning Research (04/2025)
Stanley Bak. nnenum: Verification of relu neural networks with optimized abstraction refinement. In NASA Formal Melhods Symposium, pp. 19 36-36, 2021.
Bishmu P. Bhattarai, Jake P. Gentle, Porter Hill, Tim McJunkin, Kurt S. Myers, Alex Abbound, Rodger Renwick, and David Hengst. Transmission line ampacity improvements of AltaLink wind plant overhead tie-lines using weather-based dynamic line rating. In IEEE Power & Energy Society General Meeting, 2017.
Christopher M. Bishop and Nasser M. Nasrabadi. Pattern recognition and machine learning, volume 4. 2006.
Sorgiy Bogomolov, Marcolo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. JuliaReach: A loolbox for set-based reachability. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 39 44, 2019.
Aleksandar Bojchevski and Stephan Günnemann. Certifiable robustness to graph perturbations. In Advances in Neural Information Processing Systems, volume 32, 2019.
Aleksandar Bojchevski, Johannes Gasteiger, and Stephan Günnemann. Efficient robust certificates for discrete data: Sparsity- aware randomized smoothing for graphs, images and more. In International Con- ference on Machine Learning, volume 119, pp. 1003-1013, 2020.
Karsten M. Borgwardt, Cheng S. Ong, Stefan Schönauer, S. V. N. Vishwanathan, Alex J. Smola, and Hans- Peter Kriegel. Protein function prediction via graph kernels. In Bioinformatics, volume 21, pp. i47-156, 2005.
Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio, and Ruth Misener. Efficient verifi- cation of relu-based neural networks via dependency analysis. In Proceedings of the AAAT Conference Artificial Intelligence, volume 34, pp. 3291 3299, 2020.
Christopher Brix and Thomas Noll. Debona: Decoupled boundary network analysis for tighter bounds and faster adversarial robustness proofs. In arXiv preprint ar Xiv: 09040, 2020.
Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. The fourth international verifi- cation of neural networks competition (VNN-COMP 2023): Summary and results. In arXie preprint arXiv:2812 16760 2023.
Michael M. Bronstein, Joan Bruna, Yann LeCun, Arthur Szlam, and Pierre Vandergheynst. Geometric deep learning: Going beyond Euclidean data. In IEEE Signal Processing Magazine, volume 34, pp. 18 88-42, 2017.
Rudy Bunel, lkker Turkaslan, Philip Torr, Mudigonda. P. Kumar, Jingyue Lu, and Pushmeet Kohli. Branch and bound for piecewise linear neural network verification. In Journal of Machine Learning Research, volume 21, pp. 39, 2020.
Deli Chen, Yankai Lin, Wei Li, Peng Li, Jie Zhou, and Xu Sun. Measuring and relieving the over-smoothing problem for graph neural networks from the topological view. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pp. 3438-34 3445,4455554 2020.
Sikai Chen, Jiqian Dong, Paul Ha, Yujie Li, and Samuel Labi. Graph neural network and reinforcement learning for multi-agent cooperative control of connected autonomous vehicles. volume 36, pp. 838-857. 2021.
Hanjun Dai, Hui Li, Tian Tian, Xin Huang, Lin Wang, Jun Zhu, and Le Song. Adversarial attack on graph structured data. In International Conference on Machine Learning, volume 80, pp. 1115-1124, 2018.
Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. Output range analysis for deep feedforward neural networks. In NASA Formal Methods Symposium, pp. 121-138, 2018.
Claudio Ferrari, Mark N. Mueller, Nikola Jovanović, and Martin Vechev. Complete verification via multi- neuron relaxation guided branch-and-bounde In International Conference on Learning Representations, 2022.
16

---

Published in Transactions on Machine Learning Research (04/2025)
Timon Gehr, Matthew Mirman, Dana Trachsler-Cohen, Petar Tsankov, Swarat Chaudhuuri and Martin Vechev. AT2: Safety and robustness certification of neural networks with abstract interpretation. In IEEE Symposium on Security and Privacy, pp. 3 18, 2018.
Ian Goodfellow, Jonathon Shlens, and Christian Szegody. Explaining and harnessing adversarial examples. International Conference on Learning Represenlations, 2015.
Stephan Günnemann. Graph neural networks: Adversarial robustness. In Graph Neural Networks: Founda- tions, Frontiers, and Applications, pp- 149-176, 2022.
Patrick Henriksen and Alessio Lomuscio. Efficient neural network verification via adaptive refinement and adversarial scarch. In European Conference on Artificial Intelligence, volume 325, pp. 2513-2520. 2020.
Chao Huang, Jiameng Fan, Xin Chen, Wenchao Li, and Qi Zhu. POLAR: A polynomial arithmetic framework for verifying neural-betwork controlled systems. In Automated Technology for Verification and Analysis, pp. 414 430, 2022.
Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In International Conference on Compuler Aided Verification, pp. 29, 2017.
Radoslav Ivanov, Taylor Carpenter, James Weimer, Rajeev Alur, George Pappas, and Insup Lee. Verisig 2.0: Verification of neural network controllers using Taylor model preconditioning. In International Conference on Computer Aided Verification, pp. 249 262, 2021.
Luc Jaulin, Michel Kieffer, Olivier Didrit, and Éric Walter. Interval analysis. 2001.
Jinyuan Jia, Binghui Wang, Xiaoyu Cao, and Neil Z. Gong. Certified robustness of community detection against adversarial structural perturbation via randomized smoothing. In Proceedings of The Web Con- ference, pp. 2718 1111822224422 2020.
Hongwei Jin, Zhan Shi, Venkata J. S. A. Peruri, and Xinhua Zhang. Certified robustness of graph convolution networks for graph classification under topological attacks. In Advances in Neural Information Processing Systems, volume 33, pp. 8463 8474, 2020a.
Wei Jin, Yao Ma, Xiaorui Liu, Xianfeng Tang, Suhang Wang, and Jiliang Tang. Graph structure learning for robust graph neural networks. In Proceedings of the 26th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining, pp. 66-74, 2020b.
Guy Katz, Clark Barrelt, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference Computer Aided Verification, pp. 97-117, 2017.
Guy Katz, Derek A. Huang, Duligur lbeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, David L. Dill, Mykel J. Kochenderfer, and Clark Barret. The Marabou framework for verification and analysis of deep neural networks. In International Conference on Computer Aided Verification, pp. 443-452, 2019.
Thomas N. Kipf and Max Welling. Semi-supervised classification with graph convolutional networks. In International Conference on Learning Representations, 2017.
Niklas Kochdumper. Falensions of polynomial zonolopes and their application to verification of cyber-phuysical systems. Phl) thesis, Technische Universität München, 2022.
Niklas Kochdumper and Matthias Althoff. Sparse polynomial zonotopes: A novel set representation for reachability analysis. In IEEE Transactions on Automatic Control, volume 66, pp. 4043 4058, 2020.
Niklas Kochdumper, Christian Schilling, Matthias Althoff, and Stanley Bak. Open- and closod-loop neural network verification using polynomial zonotopes. Tn NASA Formal Methods Symposium, pp. 16 16-36, 2023.
17

---

Published in Transactions on Machine Learning Research (04/2025)
Matthias König, Annelot W. Bosman, Holger H. Hoos, and Jan N. van Rijn. Critically assessing the state of the art in neural network verification. In Journal of Machine Learning Research, volume 25, pp. 1-53, 2024.
Anna-Kathrin Kopetzki, Bastian Schürmann, and Matthias Althoff. Methods for order reduction of sono- topes. In IEEE Conference on Decision and Comtrol, pp. 5626-5633, 2017.
Oliver Kosut, Liyan Jia, Robert J. Thomas, and Lang Tong. Malicious data attacks the smart grid. IEEE Transactions on Smart Grid, 2(4):645-658, 2011.
Tobias Ladner and Matthias Althoff. Automatic abstraction refinement in neural network verification us- ing sensitivity analysis. In Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1-13, 2023.
Tobias Ladner and Matthias Althoff. Exponent relaxation of polynomial zonotopes and its applications in formal neural work verification. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 38, pp.
2024.
Gaoqi Liang, Junhua Zhao, Fengji Luo, Steven R. Weller, and Zhao Yang Dong. A review of false data injection attacks against modern power systems. IEFE Transactions on Smart Grid, 8(4):1630-1635 2017.
Diego Manzanas Lopez, Sung Woo Choi, Hoang-Dung Tran, and Taylor T. Johnson. NNV 2.0: The neural network verification tool. In International Conference on Computer Aided Verification, pp. 397-412, 2023.
Andrew K. McCallum, Kamal Nigam, Jason Rennie, and Kristie Seymore. Automating the construction of internet portals with machine lcarning. In Information Retrieval, volume 3, pp. 127-163, 2000.
Mark N. Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. PRIMA: General and precise neural network certification via scalable convex hull approximations. In Proceedings of the ACM on Programming Languages, volume 6, pp. 1-33, 2022.
Anggoro Primadianto and Chan-Nan Lu. A review on distribution system state estimation. IEEE Transac- lions on Power Systems, 32(5))3875 3883, 2017.
Luca Pulina and Armando Tacchella. An abstraction--efinemnn approach to verification of artificial neural networks. In International Conference on Computer Aided Verification, pp. 243-257, 237, 2010.
Marco Sälzer and Martin Lange. Fundamental limits in formal verification of message-passing neural net- works. In International Conference Learning Representations, 2023.
Ida Schomburg, Antje Chang, Christian Ebcling, Marion Gremse, Christian Heldt, Gregor Huhn, and Di- elmar Schomburg. BRENDA, the enzyme database: Updates and major new developments. In Nucleic Acids Research, volume 32D, pp. 431 433, 2004.
Zhouxing Shi, Qirui Jin, Jeremy Z. Kolter, Suman Jana, Cho-Jui Hsieh, and Huan Zhang. Formal verifica- tion for neural networks with general nonlinearities via branch-and-bound. In 2nd Workshop on Formal Verification of Machine Learning, 2023.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. In Advances in Newral Information Processing Systems, volume 31, 2018a.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Boosting robustness certification of neural networks. In International Conference on Learning Representations, 2018b.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. In Proceedings of the ACM on Programmingg Languages, volume 3, pp. 30, 2019.
Simon Stock, Markus Dressel, Davood Babazadch, and Christian Bocker. Application of physics- graph convolutional network in real-time state estimation of anderdeeermmnned distribution grids. In IEEE PES Innovative Smart Grid Technologies Conference Furope, 2022.
18

---

Published in Transactions on Machine Learning Research (04/2025)
Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In International Conference on Learning Represenlations, 2019.
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsich, and Jeremy Z. Kolter. Beta- CROWN: Efficcintt bound propagation with per-neuron split constraints for complete and incomplete neural network verification. In Advances in Neural Information Processing Systems, volume 34, 2021.
Zhiwei Wang, Min Xia, Min Lu, Lingling Pan, and Jun Liu. Parameter identification in power transmission systems basod on graph convolution network. IEEE Tronsactions on Power Delivery, 37(4):3155-316; 2022.
Haoze Wu, Clark Barrett, Mahmood Sharif, Nina Narodylska, and Gagandeep Singh. Scalable verification GNN-based job schedulers. In Proceedings of the ACM on Programming Languages, volume 6, pp. 1036-1065, 2022a.
Zhaoyu Wu, Qi Wang, and Xuefei Liu. state estimation for power system based on graph neural network. In IEEE 5th International Electrical and Energy Conference, 2022b.
Zonghan Wu, Shirui Pan, Fengwen Chen, Guodong Long, Chengqi Zhang, and Philip S. Yu. A comprchensive survey graph neural networks. In IEEE Transactions on Newral Networks and Learning Systems, volume 32, pp. 2424, 2020.
Weiming Xiang, Doang-Dung Tran, and Taylor T. Johnson. Output reachable estimation and verifica- tion for multilayer neural networks. In IEEE Transactions on Neural Networks and Learning Systems, volume 29, pp. 5777 5783, 2018.
Zhilin Yang, William Cohen, and Ruslan Salakhudinov. Revisiting semi-supervised learning with graph embeddings. In International Conference on Machine Learning, volume 48, pp. 40-48, 2016.
Rex Ying, Ruining He, Kaifeng Chen, Pong Eksombatchai, William L. Hamilton, and Jure Leskovec. Graph convolutional neural networks for web-scale recommender systems. In Proceedings of the 24th ACM SIGKDD International Conference on Knowledge Discovery 8 Data Mining, pp. 974-983, 2018.
Huan Zhang, Tsui- Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Advances in Neural Information Processing Systems, volume 31, 2018.
Xiao-Meng Zhang, Li Liang, and Lin Liu. Graph neural networks and their current applications in bioinfor- matics. In Fronliers in Genelics, volune 12, 2021.
Daniel Zügner and Stephan Günnemann. Cortifiable robustness and robust training for graph convolutional networks. In Proceedings of the 25th ACM SIGKDD International Conference Knowledge Discovery 8 Data Mining, pp. 246-256, 2019.
19

---

Published in Transactions on Machine Learning Research (04/2025)
Appendix
A On Polynomial Zonotopes
(a)
(b)
0.5
0
2(1)
((1)
P2 PZ quadMap(P2, P2, Q)
Samples
Figure 9: Visualization of the quadratic map using the polynomial zonolope PZ from Appendix
In this section, provide further details on polynomial zonotopes (Def. 6
Uncertain inputs often
constructed by some -bal with radius around a vector x E I Brix et al. 2023 polynomial zonolope representing this ball is given by
For 3,
0
0
1
0
0
0
0
X'
T
1
0
1
0
=
x +
ai
02
+
0
on E
[-11,1]
(13)
1
0
0
PZ
Please note that each generator defines a line segment and the entire set is given by the Minkowski sum of each line segment. From this also follows the computation of the Minkowski sum ( as this operation simply adds more of these line segments to the set.
However, such set can also be represented using many other representations. The benefit of polynomial zonotopes over other set represent when nonlinear functions as in neural networks evaluated over the input set. Conceptually, applying nonlinear function bends the line segments by adding dependencies between generators:
becomes apparent if the represented set non-convex, which occurs
Let us consider the set {{a af+0.1a2 af] a1. [-1, 1}} C I visualized in Fig. 9a. This can be represented polynomial zonotope follows:
0
07
1 3 0 2 0
PZ
0
0.1
0
(14)
0 1 0
0
0
0
As we cannot evaluate general nonlinear function over the input set, the nonlinear function is often approximated using polynomials and the approximation error is bounded. The polynomial evaluation is computed using repeated executions of the quadratic map, which can be evaluated exactly for polynomial zonotopes and introduces dependencies between generators.
Proposition (Quadratic Map (Kochdumper 2022 Prop. 3.1.30)). Given two polymomial zonotopes PZ, (c1, (r. [, E,) C R" PZ, (02, G2, Ea) Ez)pz C _² with h and h generators, respec- tively, common identifier vector, and Q (Q), Qa). Qi Ruxxn, then the quadratic map is computed
20

---

Published in Transactions on Machine Learning Research (04/2025)
follows:
x 01
PZ = gua,
E P21, D2 E P22
= ( G1 G2 T. ... Gn [1, [i Bg Ei
Enl)
CR",
Pz
where
a Q102]
c
c GiG1
G R1G2
==
G =
G2
G =
Gle On
and E, = E2 + Ei(-,) 1, j [bi]. The outpul PZ has (b11h2) generalors.
Please note that the quadratic map operation defined for polynomial zonotopes with a common identifier vector. We can adjust two polynomial zonotopes with different identifiers by extending the exponent matrix accordingly [Kochdumper] 2022. Prop. 3.1.5). In this work, we only use matrices in Q with entries consisting of zeros and ones, which effectively selects which dimensions of the polynomial zonotopes multiplied part of quadratic map.
For example, the set {[o (. | from PZ using the quadratic map with Q (Q1, Q2), where
a1 02 E [-1,1]}
R2 visualized in Fig. 9p can be computed
0
0 1
0
0
0
Q1
0
0
0
Q2
0
(15)
0
0
0
0
0
0
Thus,
x: Qıæ Q2x
PZ = quadMap quadMap(PP2.10 P2,, PZ, Q)
x E PZ
(16)
(1)
1
3
6
=
0 0.2
0.01
0
Pz
where we compacted PZ by removing zero-length generators and adding generators whose dependent factors have equal exponents.
B Proofs
We include all proofs from the main body in this section in the order of appearance.
Lemma (Multiplication of Matrix Polynomial Zonotopes). Given two matriz polynomial zonotopes Mi (Cr, G1, 1,) C. Rank, M2 (C2, G2, E2) C kxxm with h1, h2 generators, respectively, and common identifier, then their multiplicntion is oblained by
M3 Mi E MM M2) M1 E M1, M2 E _2
(c, G G2 T
Gm,]
Es Ei
Emi)) pz
C paxm
where
E, = 1 Ez, vi [hi]. The matria maulliplieations broadeast across all generators. The oulput Ma has (1h)2) generators.
C=C,C2. G G
= G2
21

---

Published in Transactions on Machine Learning Research (04/2025)
Proof. The result My is obtained as follows:
M3 M1 +J M2 = ((M)M)) M1 E M1, M2 E M23
P
h2
p
+
O
C2
+
a
Catina)) an E e1-1,1]
A1
P II
Ag
CiO2
+
a
Bioka
C2
Okk
Ezck.))
C2
k=
G1
G2
11g
Okk
On 1111.11
A=
=G., E,
The number of generators follows directly from the size of G1, G2 and G,
An efficient implementation of Lemma is given in Appendix C Please note that Lemma is a special case of the quadratic map (Prop. 6 where we first vectorize the given matrix polynomial zonotopes to
Mi C R and M2 C I& (Sec. 3 and then compute
M3- quadMap (M, 2) Rmm
with Q = (Q1,1, Q2,1, ..., Qn.1. Q1
[ i n(k 1)] and wy = [kj 1) +1 k(j - 1) + k] be the respective indices involved to compute the (i.j)-th entry, then
2n.m). Let Us
Qi = aparse(t;, Wy, nk, km) E (nk))x(km)
with ones in positions (va()) wyw)), E [k], and zeros otherwise. Finally, the result M3 is re-written as a matrix polynomial zonotope M3 C Raxm
Proposition 2 (Enclosure of Graph Convolutional Layer). Given are weight matrix We E RC--1 graph g = (N, E), and an input Ha-1 C RW represented A E RI be the adjacency matriz of 9 -= A INN,, and let D = diag(1A) E RWWXxW be the dingonal degree matriz. The exact output of a graph convolutional layer k. in Def. 4 is computed by
matriz polynomial zonotope. Let
H4 - He-
Proof. As the graph convolutional layer is composed of a left and right matrix multiplication, the compu- tation is exact using G
Proposition 3 (Enclosure of Summation Pooling Layer). Given graph G and on inpul H4-1 C BiMixe--1 represented as a matrix polynomial zonotope, the enact output of pooling across all nodes via summation is computed by
Hys L (H+-1, (1Ha-1)
Proof. As the pooling layer is computed by left matrix multiplication, the computation is exact using 6
Lemma 2 (Approximation Error of Inverse Square Root). Given polynomial p(æ) az approzimating the inverse square root f(x) = xー on the domain [1 u] C R4, then the mazimum approrimation error is
d max [f(x) p(x)) 1f(x*) p(x")),
2 2E|1.a
22

---

Published in Transactions on Machine Learning Research (04/2025)
where
x" E (. (1/o)) ; u n [1, u).
{i,
Proof. The maximum approximation error it at the extreme point:
(f(x) - p(z))
dx
x 1 22
= V (1/2a)²
or on a boundary point 1, u if the extreme point lies outside [1, u/ due to monotonicity.
Proposition 4 (Enclosure of Uncertain Message Passing). Given on uncerlain adjacency matrix A with h generators, then
p D -AAD-- P",
encloses the message passing with O(h²) generators.
Proof. The enclosure is computed using set-based evaluation of the message passing in Def. usiin and Lemma 1 These steps are computed using affine maps (6) and matrix multiplications of polynomial zonolopes (Lemma 1, which are exact, and the enclosure Dring using Prop. [ with the approximation error in Lemma which is auter-approximative Thus, the enclosure of the message passing is sound.
12
Number of gencrators: Affine maps do not increase the number of generators 6 The enclosure of Daiay in (0) adds one generalor for each node with uncertain degree (Prop. D. which are at most 2h as each uncertain edge in A has two adjacent nodes. Finally, two applications of the matrix multiplication on matrix polynomial zonotopes (Lemma 1 obtains the O(h3) generators of P.
Proposition 5 (Enclosure of Graph Convolutional Layer). Given are weight matric Wa. E R uncertain graph 9, and an uncertain input H4 E [R with hı generators. Let P C. RWWXXN be the uncertain message passing according to Prop. 4 with Ohh)) generators. The output for a graph convolutional layer le (Def. 4 enclosed by
H4 = enclose ( LC H)-1,, = - H s GG (CC(Hx-1.9)
with O(h, h2) generators.
Proof. The enclosure follows directly from the enclosure of the message passing (Prop. 4 the matrix mul- tiplication on polynomial zonotopes (Lemmn D and the affine map (6) Given the number of generators of H4-1 and P, the number of generators of Hy follows from Lemma
Theorem 1. Given a neural network & with k layers and message passing steps, an uncertoin graph 9 = (N, E) with [ nodes and he uncertain edges, and an uncertain input X C W with h2 generators, then Alg. [ satisfies the problem statement in Sec. 2.5 The number of generators of the computed output enclosure. ) is given by:
hy 00(11 (h (cmma) (K (K- 2nx 22x'))maxx)
where Cmax = max C2k' denotes the marimum number of features within the graph layers and nmax = max max 22...)...)) ni denote the mazimum number of output neurons of the non-graph-bon based layers after the global pooling layer.
23

---

Published in Transactions on Machine Learning Research (04/2025)
outer- approximative (Prop. 4 Prop. 5 and Prop. 1 and the specification can be checked as in previous approaches using polynomial zonotopes Kochdumper et al. 2023: Ladner & Althofi, 2023]. The message passing P has ((h)) generators (Prop. neuron (Prop. D. The global pooling layer (Prop. 3 and linear layers (4) do not change the number of gencrators. Thus, the number of generators of y Alg. is:
Proof. The problem statement is satisfied as each step to compute Y is cither exact (Prop.
The enclosure a nonlinear layer adds at most one generator for each output
message passing stops (lines
6
(lines
14
h 0 h22 (.2.(-
(
he h
...) + (Vxc2222 + WMec
11
k=2k (Prop-
(Prop
(Prop.
=0 (h2)) (22)hhe he (ha) We
+ ( MMe22
1
nkk
2
Polynomial order x² w--1
0o
(hi))' he + (h2)a'-1
max kE(2k
Wick +
2
k=2n'+2 42
co haw he max kE[2x']
W Mo2w
Hy.
k=
Next, we simplify the term by bounding the number of output neurons with their maximum:
Hy 2 co
haah hhr [WCcmux +
Omax
k= +2
c 0
(he (hx + [[cmax) + (x 2x' )D haa
which shows that by H, C O0 h1 (hz + (Wcmmx) + (xc - 22'2 (k'))max))
Corollary 1 (Subgraph Selection). Given an input Ha-1 E RlWixe--1 to a layer k, the message passing D 1 E RM of a graph 9, and the node indices K. of a subgraph g', we can construct a projection matrir M [NI(K)) such that
Hk-1 MH
P'=MPM'
contain the input and the message passing corresponding to the subgraph.
Proof. The statement follows directly from the construction of the projection matrix M, where nodes that are not in g' are removed.
C Efficient Matrix Multiplication Implementation of Matrix Polynomial Zonotopes
We want to stress that Lemma ! can be efficiently computed using matrix broadcasting, as effectively the center matrix and cach generator matrix from one set is multiplied with the center matrix and cach generator matrix of the other set. Let us restate Lemma D here for convenience:
Lemma 1 (Multiplication of Matrix Polynomial Zonotopes). Given two matria polynomial zonotopes M1 = (C1, G1, F1 C Ronk M2 = (C2, G2, F22 pz C TR with h1, hy generators, respectively, and common identifier, then their multiplicatiion is oblained by
M3 = Mi E M2 = (2M M1 E M1, M2 E M2]
(c, G G2 T ... Gm.) [],
Ez E
Eml)
C cu
24

---

Published in Transactions on Machine Learning Research (04/2025)
where
C1C1C2 G C12,
G = Gi
E, E 1 E2, Vi [h1].
The matriz multiplications are broadcast across all generators. The output M3 has O(hrh2) generators.
The following code shows the efficient implementation of this multiplication using broadcasting in MATLAB syntax.
& Variable names as in Lemma 1:
2 & MI: C1 kn, G1 h,,k, E1 (p,
3 & M2: C2 (k G2 h2), E2 h2,
prepare for quadratic map computation such that
$ all matrices have the form m,,k, h2, and (p, h1, h2), respectively.
C1 reshape (C1, n, k,
Gl reshape (G1, n, k, 1, 1);
9 E1 reshape [E1, P, h1, 1);
10
C2 reshape (C2, 1, k, m)
12 G2 reshape (G2, 1, k, m, 1, h2);
E2 reshape (E2, P, 1,,, h2);
15
& compute matrix multiplicationn through broadcasting
16
C_bar = sum (C1 ** 22
8 (n,1,m)
17
hat sum (G1 . 22,2);
$ (n,1,m,hl)
18
G2 hat sum (C1 * 22,
8 (n,1,m, 1,h2)
19
G bar sum (G1 22,
$ (n,1,m,hl,no h2)
E. bar E1 + E2;
8 (p,h1,h2)
$ reshape back to correct dimensions C_bar reshape (C_bar, n,
23
24 G1 cha = reshape (G1_hat,, m, h1);
25
G2_ hat reshape (G2_hat, n, m, h2);
bar reshape (G bar, n, m, hl+h2);
E bar reshape bar_barraa p, h1 h1*h2)
The broadeasting in lines 16-20 is also parallelizable and can be efficiently computed on a GPU, which further enhances the computation of the multiplication of matrix polynomial zonotopes.
D Evaluation Details and Further Experiments
D.1 Evaluation Setup
Please recall the problem statement (Soc. 2.5 Given a graph ncural network 4 an uncertain graph G (W, E) with nodes N C N and edges E = UE c N x N consisting of fixed edges Ex and uncertain edges E, and uncertain node features X' C R Mixs, we compute an enclosure of the output y using Alg. The specification S is then verified as in previous works (Kochdumper et al. 2023 Ladner & Althoff 2023
We demonstrate our approach on three benchmark graph datascts: The first two, Enaymes and Proteins, represent protein structures lailored for the task of protein function classification (Schomburg et al. 2004 Borgwardt et al. 2005). The third dataset, Cora, represents a citation network with several classes of publications (Yang et al. 2016 McCallum
(2000). The main propertics of each datasct are summarized in Tab. D All graph neural networks considered here are as described in Alg, [ where we have three message- passing steps (H' 3) and tanh activation unless stated otherwise. The number of input and output neurons
25

---

Published in Transactions on Machine Learning Research (04/2025)
depends on the number of node features and classes of the dataset (Tab. 1 respectively, and the networks have 64 neurons per node in hidden layers.
To evaluate our approach on the datasets, we perturb the node features and graph structure as follows: We normalize all node features and perturb them using the same perturbation radius c E R,, on all features. Given a flattened input X E RR-Wee,,, our input set then becomes
X = x=xXx, (I, [I PZ
CRIMO
(17)
which we can reshape to a matrix polynomial zonotope X' R The partitioning of the edges into fixed odges Ex and uncertain edges E is as follows: To preserve the structure of the input graphs, the set of fixed edges Ex always contains a spanning tree of the graph, and we make the presence of some remaining edges unknown and, thus, part of the uncertain edges & depending on the respective experiment. The spanning tree is constructed using breadth-first scarch, with the root node being the one with the highest degree (e.g., node 1 in Fig. 1
In our experiments, we perturb the edges independently of each other. Thus, the resulting uncertain adja- cency matrix A is constructed analogous to (17). However, one can also construct an uncertain adjacency matrix with dependencies. For example, consider an undirected graph with three nodes. We can model that node ① has be connected with either or 3 (xor-relation) and a fixed edge 2 with the following matrix polynomial zonotope:
0
0.5
0.5
0.5
0.5
0.5
0.5
0
[1]
(18)
0.5
1
0.5
0
PZ
Due to the different signs within the generator, either the edge ① 2 or the edge I Similarly, other constraints can be modeled in the set representation itself as well. This can used to model budget constraints as was done in related work (Bojchevski & Günnemann, 2019 Sec. 4.1). Please note that Alg. 1 remains unchanged only the uncertain adjacency matrix A (and thus the uncertain message passing P via Prop. 4 is updated.
3 present.
We evaluate all experiments over 50 runs with graphs sampled from the respective dataset. Due to the exponential time complexity of the enumeration method, we repeated these runs only 20 times. We use a rather small perturbation radius e = 0.001 on the Enzymes and Proteins dataset as we have found that the graph neural networks are not robust for larger radii, and counterexamples can easily be found.
While our approach is able verify many instances, not all instances are verified. However, not all instances are indeed verifiable. Thus, provide upper bound of verifiable instances by extracting counterex- amples of given instance. This is achieved by enumerating all possible graphs and applying gradient- based adversarial attack (fast gradient sign method (Goodfellow et al.) 2015 ) on the node features for each graph Ginnneaann (2022). For large graphs with many uncertain edges, it is not feasible to enumerate all possible graphs. Thus, we only check at most 10, 000 graphs for each instance, and select those which differ the most from the original graph.
D.2 Ablation Study
We analyze the approximation errors induced by each component of our approach in more detail. In partic- ular, we investigate (i) the size of the approximation crror during the enclosure of the inverse square root function while computing the uncertain message passing (Prop. 4 and (ii) the outer approximation induced by different order reduction techniques to limit the number of generators.
D.2.1 Approximation Error of Inverse Square Root Function
Let us first analyze the outer approximation induced by the enclosure of the inverse square root function. Please recall that the input corresponds to the degree of a node in Daing ( and the output the respective
entry in Dー 10p. Enclosures be obtained by approximating the function using polynomial and diag
26

---

Published in Transactions on Machine Learning Research (04/2025)
0.5
Inverse square root -//² 1/2
Approx. error = 0.0092
0.4
Approx. 0.0016
Output
Approx. error = 0.0007
0.3
0.2
0.1
10
20
30
40
50
60
70
80
Input x
Figure 10: Approximation errors of inverse square root enclosure at different input domains. The x-axis
corresponds to the degree of a node in Daiag 9 and the y-axis to the respective entry in D (10 Please note that for nodes with larger degrees, linear approximations are usually sufficient obtain tight enclosures.
diag
(a) Linear polynomial
(b) Quadratic polynomial
(c) Cubic polynomial
0.8
0.8
Output
0.6
0.6
0.6
0.4
0.4
0.4
0.2
0.2
0.2
2
4
2
6
4
Input æ
Input æ
Input
Inverse square
1/2
Approx. error d 0.024
Approx. error d 0.006 Approx. error d = 0.001
Figure 11: Approximation errors of inverse square root enclosure for different orders of the approximation polynomial. Higher-order polynomials enable tight enclosures at the cost of additional generators.
computing the corresponding approximation error (Prop. Tighter enclosures can be obtained using higher-order polynomials at the cost of additional generators [adner & Althoff 2023). Fortunately, higher- order polynomials are usually not required for larger graphs as the degrees of the nodes become much larger and a linear polynomial can approximate the function quite well. We illustrate this in Fig. [0 where the approximation error becomes smaller with increasing node degree despite larger uncertainty. For smaller inputs, we illustrate in Fig. II how higher-order polynomials return tighter enclosures.
Finally, let evaluate the influence of the enclosure of the inverse square root function during the uncertain presage-passiing compulation (Prop. 4 on the output set. V Ideally, we would like to measure the relative volume of the obtained output set y with respect to the volume of the exact output set y*. However, computing ) is computationally infeasible (Katz et al.) 2017]. We approximate the volume of y" by ignoring the approximation errors to obtain an approximative output set Vapprox: ie., do not perform step in Fig. 3 As the volume of a polynomial zonotope also hard to compute, we use the volume of the enclosing zonotope (Kochdumperr 2022 Prop. 3.1.14) instead. Then, the relative volume Vit of y with respect to Vapprox is computed follows (Kopetzki et al.) 2017 Sec. IV-A):
vol(O)) (=vo(())
1/n-
Vral Vapproxx)
(19)
(vol()
27

---

Published in Transactions on Machine Learning Research (04/2025)
Table 2: Influence of approximation errors in uncertain gesssag-ppassing computations depending on the number of steps k', swith Ve indicating the relative volume of the output
19
Datasct
Veel
Verified instances [%]]
Verification time [s]
1
1.0336=0.0169
92.00
3.36=1.559
2
1.05733+0.041
94.00
16.20=13.90
3
1.1310=#0.154
90.00
53.06:+42.58
1.1417+0..440
90.00
115.63:1:2.96
1.2191=0.1444
74.00
184.58:110.29
Enzymes
1.2756=0.
82.00
179.92:+66.00
7
1.5455=0.7611
64.00
276.42+124.37
8
1.8605+1.3858
72.00
258.53+102.455
9
2.1041#1.2579
58.00
349.20-1132.9
10
2.0582+1.7807
54.00
398.55++148.96
where Viel normalized by the number of output dimensions nu. for better comparability between all datasets. The closer Viel is 1, the less contribute the approximation errors of the inverse square root enclosure the final output set. We present Viel averaged over 50 graph inputs for ten models trained on the Enzymes dataset with up 10 message passing steps x in Tab. 2 While the approximation errors accumulate over the layers of a graph neural network, the overall contribution to the output set is modest and other factors such as the uncertainty in the node features are more dominant. Thus, most uncertain input graphs remain verifiable even for many message passing stops x with reasonable verification times.
D.2.2 Approximation Error of Order Reduction Techniques
Let us also take closer look at different order reduction techniques. Order reduction is applied to remain computationally feasible for large sets with many generators at the cost of additional outer approximation, where the order of a polynomial zonotope PZ C R" with h generalors is defined as 1/4. Please note that barely any order reduction techniques exist for polynomial zonotopes (Ladner & Althoff 2024). and order reduction is achieved by applying them on the zonotope enclosure of the smallest generators instead [Kochdumper] 2022, Prop. 3.1.39). We evaluate two techniques here: box enclosure (Box) (Kopetzki et al., 2017| Sec. IT-A) and one based on principal component analysis (PCA) (Kopetzki al. 2017 Sec. III- A), which are visualized in Fig. 12 Additionally,
combine them with preprocessing step (ExpRelax) for polynomial zonotopes to reduce the outer approximation induced by the zonotope enclosure (Ladner & Althoff 2024), which is based on relaxing the exponents of the dependent factors ag of a polynomial zonotope (Def. G).
We apply each order reduction technique to 50 output sets y obtained on all datasets and networks.
Tab. 3 we show the relative volume Viei( of each reduced set Vred with respect to y for different orders P. The box enclosure obtains tighter results the Enzymes and Proteins dataset, wheras the PCA enclosure is tighter on the Cora dataset. For all datasets and order reduction techniques, the ExpRelax preprocessing slightly improves the result at the cost of additional computation time. However, want to stress that the chosen orders are very small and one usually uses higher values for during the verification of neural networks, for which the differonce between the individual techniques bocomes less noticeable. Wo also notice that for some values Tab. 3 Vra smaller than 1, which might indicate that the respective order reduction is anter-approximativv. However, as mentioned above, we cannot compute the volume of polynomial zonotope directly and rather compute the volume of the enclosing zonotope instead. Applying the respective order reduction seems to improve this zonotope enclosure, resulting in smaller volume for Dre than y.
28

---

Published in Transactions on Machine Learning Research (04/2025)
(a)
(b)
26
((1)
Box enclosure
PCA enclosure
Figure 12: Visualization of different order reduction techniques applied 7-dimensional output set y obtained on the Cora dataset. The relative volume with respect to y is Viel = 3.4505 for the box enclosure and Viel = 1.0638 for the PCA enclosure.
Table 3: Relative volume Vral for different order reduction techniques, where the respective output set y is reduced to order p.
p 2
P 1.5
Dataset
Order Reduction
Viol
Time [s]
Via
Time
Box
1.0010+0.0011
0.039++0.034
1.0015+000019
0.032++0.019
ExpRexxx
0.9997+000001
1.456+0.444
1.0003+1.0009
1.401
Enzymes
PCA
1.1465++0.0865
0.036+L0.015
1.1450++.0044
0.031++0.013
ExpRexx
1.146110.0871
1.534
1.142110.0091
1.453+003348
Box
1.0045110.0084
0.007100008
1.00681100008
0.007+00.005
ExpRexx
0.995440.0156
0.075::0.025
0.997710.0163
0.074#0.031
Proteins
PCA
1.028710.1073
0.0071000006
1.0410=0.10113
0.007
PCA ExpRelax
1.0276=0010033
0.0904:.001
1.0295++0.0900
0.082+00.038
Box
1.1295+0.1732
0.020+0.007
1.7904+11.0787
0.007+00.003
Box+ ExpReexx
1.1260+001141
0.100+-0.170
1.7815+1.0886
0.071+00099
Cora
PCA
L.0398+0.0633
0.023::0.018
L.0826+0.1193
0.008
PCA ExpRelax
1.0366+0.0580
0.122::0.900
1.0796+00.118
0.086+0.111
Box
1.1594++0.155 0.150
0.030+0.002
2.0779+1.0363
0.015+-0.012
Exx
1.1497+0.1599
0.59140.813
0.516+ 2.0661+1.0447
Cora
PCA
0.952140.0955
0.035++0.02
0.9590+0.1208
0.018+0.014
ExpRexx
0.9457-10.0933
0.597-10.857
0.9541+0.1113
0.504
29


Reviews:
[{"review_id": "FJ5DFG8LWd", "reviewer": "Reviewer_yJej", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n\n1. The method looks novel me and offers a new perspective on GNNs.\n\n2. The paper is well detailed and mathematically rigor.\n\n3. The method is scalable, compared with simple baseline.\n\nWeaknesses:\n\n1. The empirical evidence, while is nice, could be extended. For example, the authors can add more benchmarks and heterophilic graphs, as well as larger graphs.\n\n2. Since the authors discuss adversarial robustness, I would have expected to see some example of the proposed method vs. an adversarial attack on the graph.\n\n3. The paper is mathematically dense, making it challenging to follow for readers who are not deeply familiar with polynomial zonotopes. Some sections could benefit from additional intuitive explanations or visual illustrations. \n\n\nQuestions:\n\n1. With respect to the polynomials that approximate the activations, is there a preferred basis? It is not clear to me what was chosen in the paper. Also, are polynomials a preferred way to doing so? For example, in the recent [1] it was shown that many activation functions can be approximated and generalized with diffeomorphisms, so it would be interesting to read a comparison.\n\n2. Can the method be applied to GNNs where the underlying graph may change between layers, such as GAT [3] or GraphGPS [3] ?\n\n\nReferences:\n\n[1] DiGRAF: Diffeomorphic Graph-Adaptive Activation Function\n\n[2] Graph Attention Networks\n\n[3] Recipe for a General, Powerful, Scalable Graph Transformer", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The paper presents a novel approach to formally verifying Graph Convolutional Networks (GCNs) in the presence of uncertainty in both node features and graph structure. It offers an extension of methods that use analysis based on matrix polynomial zonotopes to preserve non-convex dependencies, ensuring robustness verification over multiple message-passing steps.\n\n The authors demonstrate the approach on three benchmark datasets, highlighting its polynomial time complexity concerning uncertain input features and edges.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "Please respond to my questions and address the weaknesses.", "broader_impact_concerns": "None.", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "2IZgEdpKUX", "reviewer": "Reviewer_4FWB", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "On the positive side, the authors indeed seem to be the first to introduce the concept of polynomial zonotope-based verification to graph neural networks (and matrices more generally). Although the high-level concept may be similar to previous verification work on other forms of neural network, the application to graph neural networks with uncertain node features and structure is certainly nontrivial.\n\nMoreover, the paper is overall well-written and presented, and the experimental and theoretical results are solid.\n\nThere are a few non-critical concerns:\n\n- First, the definition of a matrix polynomial zonotope is not sufficiently motivated, and may not be an obvious extension of the normal polynomial zonotope in definition 6. I would recommend adding more explanation as to why the generators have additional dimensions in definition 7, as well as clarifying whether/how a matrix polynomial zonotope can be seen as a generalization of a standard polynomial zonotope.\n\n- Experiments only compare with naive enumeration. While this is understandable given the lack of graph verification methods, I would recommend comparing with an GCN attack method as well. This would provide an upper bound on the maximum number of verifiable instances, and should likely be fast to run. Comparing a verifier with an attack method is also found in the standard verification literature, and provides an estimate of the gap between attacks and defenses.\n\n- Instead of using blue text for emphasis, I would recommend italics or bolding.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The paper proposes a method to formally verify graph convolutional networks  (GCN) based on polynomial zonotopes. In essence, polynomial zonotopes provide bounds on the possible values that the nodes and messages in a GCN can take. The authors first introduce the concept of a matrix polynomial zonotope and demonstrate key compositional properties. The authors then use this to provide verification operations on several different operations found in GCNs. Finally, the authors experimentally demonstrate the effectiveness of their approach at verifying real graph networks under reasonable time constraints.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "See weaknesses above; none of the suggestions are critical, but would strengthen the work in my view.", "broader_impact_concerns": "No broader impact concerns.", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "f2swMG4qtG", "reviewer": "Reviewer_fxjs", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "# Strengths\n\nThe paper is very well-written and easy to follow. The flow of the writing is very good. In addition, the followings are the main strengths of the paper:\n\n1. The methodology systematically addresses uncertainty in both node features and graph structure, covering essential aspects of GNN robustness verification. The use of matrix polynomial zonotopes is a novel and powerful tool to preserve non-convex dependencies.\n\n2. The algorithm is modular, defining enclosure at each layer, making it scalable to arbitrary GNN architectures.\n\n3. Polynomial Complexity: The claim of polynomial complexity (in hxh_x and heh_e) compared to exponential verification of all possible graphs is a major practical advantage.\n\n4. Subgraph Optimization: The reduction to the (number of message-passing steps+1)(\\text{number of message-passing steps} + 1)-hop neighborhood is efficient and reduces unnecessary computations.\n\n# Weaknesses\n1. The approach assumes a clear separation between fixed and uncertain edges. This assumption might not always be practical for real-world graphs, where edge uncertainty could follow complex probabilistic distributions or dynamic changes.\n\n2. The lemma for approximating the inverse square root relies on polynomial regression and introduces additional approximation error. While this is bounded in the methodology, the resulting error propagation through multiple message-passing steps is not explicitly analyzed.\n\n3. Non-convex enclosures, while tighter than convex ones, might be computationally expensive to handle for large-scale graphs due to the increased number of generators in matrix polynomial zonotopes.\n\n4. The number of generators grows as O(h_e^3) per message-passing step. For large graphs with high edge uncertainty, this could result in prohibitive computational costs, even with GPU parallelization\n\n5. While the methodology is well-defined, its practical applicability is not demonstrated in the methodology section. There is no clear discussion on how it handles diverse graph properties such as sparsity, size, or feature heterogeneity.\n\n6. The extension of polynomial zonotope to matrix polynomial zonotopes is not that surprising. To me, its mathematics are straightforward, although since the method is built upon that it should be discussed in the paper. Therefore, I would not consider this section as a contribution of the paper. Please also see [1].\n\n-----\nReferences\n\n[1] Michaux, J., Li, A., Chen, Q., Chen, C., Zhang, B., & Vasudevan, R. (2024). Safe Planning for Articulated Robots Using Reachability-based Obstacle Avoidance With Spheres. arXiv preprint arXiv:2402.08857.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This paper presents a novel framework for the formal verification of graph convolutional networks (GCNs) under uncertainty in both node features and graph structure. \n\nThe key contributions include: \n\n(1) the development of a reachability analysis methodology using matrix polynomial zonotopes to accurately capture and propagate uncertainties through GCN layers without introducing additional outer approximations; (2) the formalization of robust enclosures for graph convolutional and pooling layers, preserving non-convex dependencies across multiple message-passing steps; (3) a scalable solution for handling uncertain graph structures by modeling uncertain edges and their impact on the adjacency and degree matrices, ensuring computational efficiency with polynomial complexity in the number of uncertain features and edges; (4) a practical algorithm that leverages subgraph verification to significantly reduce computational overhead by focusing only on the relevant portions of the graph; and (5) a theoretical guarantee of soundness and tightness of enclosures, validated through illustrative examples. This framework addresses a critical gap in GNN verification, laying the foundation for robust deployment of GNNs in safety-critical applications.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "For each of the weaknesses I mentioned above, I suggest the following changes respectively:\n\n1. Provide justification for the practicality of this assumption or discuss how the methodology could extend to probabilistic or dynamic edge uncertainty.\n\n2. Include an analysis or empirical demonstration of how these approximation errors affect the overall tightness of the enclosures, especially for deep GNNs with many layers.\n\n3. Discuss the trade-offs between the tightness of the enclosures and computational efficiency, especially when scaling to larger graphs or deeper GNNs.\n\n4. Propose or evaluate specific generator reduction techniques (e.g., dimensionality reduction or pruning methods) to limit this growth while retaining accuracy.\n\n5. Propose or evaluate specific generator reduction techniques (e.g., dimensionality reduction or pruning methods) to limit this growth while retaining accuracy.", "broader_impact_concerns": "N/A", "additional_comments": "", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper presents a novel and rigorous framework for the formal verification of graph convolutional networks under uncertainty in both node features and graph structure. The authors have provided thorough and well-structured responses to the reviewers’ concerns. These revisions address key weaknesses and improve the paper's clarity and empirical support. I recommend acceptance with minor revisions, contingent on the authors finalizing these improvements as outlined in their rebuttal.
Decision: Accept (poster)