Verifying Quantized Graph Neural Networks is PSPACE-complete

1 Introduction

Graph Neural Networks (GNNs) are neural network models computing functions over graphs or graph-node pairs. Their ability to extract feature and structural information from graphs has made GNNs a promising candidate for tackling tasks in fields such as social network analysis, chemistry applications, and knowledge graphs. For a comprehensive survey of GNN applications, see Zhou et al. [2020], and for a survey of GNNs for knowledge graphs, see Ye et al. [2022].

The increasing use of GNNs (or neural network-based models in general) leads to a heightened necessity for reliable safety guarantees or explanations of their behavior, in order to meet legal requirements or client desiderata. Let us illustrate some guarantees we may expect.

Example 1. Consider a GNN N used to identify bots in a fictitious social network NEWSNET (see Figure 1). The network forms a graph where any registered account is a node and the edges represent relationships between accounts. In such a setting, the GNN decides, based on account-specific features, such as the frequency of posts or time of activity, whether an account is a regular human user or a (malicious) bot.

For the trustworthiness of NEWSNET, it is essential that the GNN N comes with guarantees such as:

• A "Every account that spams 100 messages or more per minute is identified as a bot by N."
• A' "If there is a significant, humanly impossible activity of a user within a short amount of time, then N will identify it as a bot."
• B "Every account whose friends sendmore than 1000messages per minute in total is flagged as part of a bots' network by N."
• B' "If an account is a friend with active bots, then N will flag it as a bot by association."

The properties A and B can be seen as safety properties, indicating that N is somewhat robust in its decision making. The properties A′ and B′ provide reasonable explanations for the decision-making process of N.

Unfortunately, like most neural network-based models, GNNs exhibit a black-box nature, making them particularly challenging to analyze. The ultimate goal in this context is formal reasoning, which involves using sound and complete procedures to interpret the behavior of GNNs, and to certify or falsify specific safety properties of GNNs. Unfortunately, recent works such as [S¨alzer and Lange, 2023; Benedikt et al., 2024] suggest that formal reasoning is practically intractable for highly expressive models like GNNs. Consequently, most of the research so far has focused on less rigorous types of reasoning, such as sound but incomplete or probabilistic procedures. For a comprehensive overview of non-formal verification procedures, see G¨unnemann [2022].

Several works have explored the expressivity and the verification of GNNs through logical frameworks ([Barcel´o et al., 2020; Benedikt et al., 2024; Nunn et al., 2024; Ahvonen et al., 2024; Cucala and Grau, 2024]). However, much of this work focuses on idealized GNNs with real-valued or unbounded integer parameters, whereas practical GNNs are typically quantized-their numerical parameters and internal computations are constrained by fixed-size representations. For example, the PyG library ([Fey and Lenssen, 2019]) uses 32- or 64-bit floating-point arithmetic, and recent research increasingly targets quantized models with reduced precision ([Gholami et al., 2021; Zhu et al., 2023]). In addition, most existing results focus on eventually constant activation functions such as truncated ReLU ([Barcel´o et al., 2020; Nunn et al., 2024]), or provide only partial results for standard ReLU ([Benedikt et al., 2024]). Orthogonally, [Ahvonen et al., 2024] investigates the expressivity of recurrent GNNs over floats, while [Cucala and Grau, 2024] addresses a weaker class of GNNs but considers a broader range of activation functions.

The contributions of the paper are as follows.

• We introduce a logic LquantGNN capturing a meaningful class of quantized (aggregate-combine) GNNs as well as linear input and output constraints on these GNNs (Section 3).
• We introduce the linear-constrained validity problem (LVP) that enables to model properties like the ones in Example 1. We show how to solve LVP by reducing it to the satisfiability problem of LquantGNN (Section 4).
• We provide a proof system that enables to create graph counterexamples. A prototype of the proof system is implemented in Python. Noticeably, the proof system gives a PSPACE upper bound for a large class of GNNs, with any reasonable activation function (Section 5).
• We also study the PSPACE lower bound and establish that LVP as well as satisfiability of LquantGNN are indeed PSPACE-complete (Section 6).

2 Fundamentals

Fixed-width Arithmetic We consider different sets of numbers, denoted by K, represented in binary using a fixed number of bits. Depending on the underlying (fixed-width) arithmetic, like fixed- or floating-point arithmetic, we denote the respective variants of operations like +, ·,÷ or relations like ≤,≥,= by +K,≤K, . . . and so on. For mathematically rigorous definitions of such arithmetics, see, for example, Ercegovac and Lang; Goldberg [2004; 1991]. To keep the notation uncluttered, we use K to refer to the set of values as well as the underlying fixed-width arithmetic. In general, we assume K contains 0, 1 and -1.

Example 2. 16-bit fixed-point arithmetic may be used in micro-controllers. For instance, K may be the set of numbers, of the form (-1)s k 104 with four decimal places precision, where s ∈ {0, 1} is the sign, k ∈ {0, . . . , 215 - 1}.

Example 3. In IEEE754 32-bit floating-point arithmetic, K exactly contains 0, -∞, +∞ and numbers that are of the form (-1)s 2e (1 + k 223 ) where s ∈ {0, 1} is the sign, e ∈ {-128, -125, . . . , 127}, k ∈ {0, . . . , 223 - 1}.

Graphs We consider directed, vector-labelled graphs G = (V,E, ℓ) where V is a finite set of nodes, or vertices, E is a set of directed edges and ℓ : V → Rm. We denote the class of all such graphs by G. We call a pair (G, v) where v is a node of G a pointed graph. We denote the class of all pointed graphs by G·. If we restrict the classes G and G· to vector labels with values from some fixed-width arithmetic K, we denote this by G[K] and G·[K].

Example 4. Figure 2 shows a vector-labelled graph with three nodes. Here ℓ : V → R2 and ℓ(v) = (11) for instance.

GraphNeural Networks AGraph Neural Network (GNN) N is a tuple (L1, . . . , Lm,Lout). Each layer Li computes Li(x,M) = combi(x, aggi(M)) where x is a real-valued vector, M is a multiset of vectors, agg is called an aggregation function, mapping a multiset of vectors onto a single vector, and comb is called a combination function. Unless explicitly stated otherwise, agg denotes the sum. Layer Lout computes a function from vectors to vectors. The GNN N computes a function G· → Rn , where n is the output dimension of N, in the following way. Let (G, v) where G = (V,E, ℓ) be a pointed graph. First, N computes a state xmu for all u ∈ V in a layer-wise fashion by xiu = combi(xi-1 u , aggi({{xi-1 u′ | (u, u′ ) ∈ E}})) and x0u = ℓ(u). The overall output N(G, v) is given by Lout(xmv ). If we restrict the computation of N to some fixed-width arithmetic, it computes a function G·[K] → Kn and we assume that all numerical parameters of N as well as internal computations are carried out in K. We call N quantized (to K) in this case.

Example 5. Consider a GNN N = (L1,L2,Lout) with Li(x,M) = comb(x, agg(M)) where agg is the sum and with the same combination function comb : R2·2 → R2 in both layers where comb((x, x′ ), (a, a′ )) is given by

for some activation function α, such as ReLU. The output layer Lout computes R2 → R and is given by α(x1 +x2 -2).

3 Boolean Combinations Over Modal Expressions

To reason about broad classes of GNNs and overcome the limitations of existing logical characterizations, we propose the logic LquantGNN, which enables reasoning about general but quantized GNNs with arbitrary fixed-width arithmetic and activation functions. Existing characterizations, such as graded modal logic ([Barcel´o et al., 2020]), modal logic on linear inequalities over counting ([Nunn et al., 2024]), or fragments of Presburger logic ([Benedikt et al., 2024]), typically relate to GNNs with eventually constant activation functions, like truncated ReLU x ↦→ max(0,min(1, x)). In contrast, LquantGNN extends beyond these constraints using the sole assumption of a quantized setting.

3.1 Syntax

Let F be a finite set of features and K be some finite-width arithmetic. We consider a set of expressions defined by the following grammar:

·

where c ∈ K, xi ∈ F. A formula of the logic LquantGNN is then a Boolean formula where the atomic formulas are of the form ξ ≥ k for some k ∈ K. When there is no ambiguity and to lighten the notation, we sometimes use more standard expressions, like -x instead of -1×x, or cξ instead of c×ξ, etc. We use ξ = k as an abbreviation for (ξ ≥ k)∧(-1×ξ + k ≥ 0). Formulas are represented as DAGs. For example, in (ξ ≥ k) ∧ (-1 × ξ + k ≥ 0) the expressions ξ and k are not duplicated as shown in Figure 3. The symbol ⊤ denotes the tautology (any universally true formula, e.g. x1 - x1 ≥ 0).

3.2 Semantics

Recall that K is a finite set of numbers, equipped with an addition +K, multiplication ×K operation, and comparison operations ≤K, <K. We fix [[α]] to be an activation function. For instance, [[α]] = ReLU, with ReLU(x) = x if x ≥K 0 and 0 otherwise. Formulas are evaluated over the class of pointed, labelled graphs G = (V,E, ℓ) where ℓ : V → KI , defined as follows. The semantics [[ξ]]u of an expression ξ with respect to a vertex u ∈ V is inductively defined on ξ:

The semantics [[xi]]u is the value of i-th feature in vertex u. Note that agg(ξ) is motivated by the message-aggregation process in a GNN and is the 'modal' part of LquantGNN. Its semantics [[agg(ξ)]]u consists in summing up the values/semantics of ξ in the successors v of u. We write G, u |= φ to say that the formula φ is true in the pointed graph (G, u), and we say that (G, u) is a model of φ. Given δ ∈ N∪{+∞}, a formula φ is δ-satisfiable (simply satisfiable if δ = +∞) if it has a model in which each vertex is of out-degree (number of successors) at most δ.

Example 6. The formula x1 + α(x2) ≥ 0 is true in the pointed graphs (G, u) where the sum of the first feature at u plus the result of the application of the activation function on the second feature at u is positive (i.e., (ℓ(u))1 + [[α]](ℓ(u))2 ≥K 0). The formula agg(1) = 4 is true in the pointed graphs (G, u) with u having exactly 4 successors. The formula agg(3) = 10 is unsatisfiable.

4 Enabling Formal Reasoning About GNNs Using LquantGNN

Let us now formally define linear-constrained validity problem (LVP) for GNNs.

Definition 7. The linear-constrained validity problem (LVP) is defined as follows:

• given a quantized GNN N with input dimensionality m and output dimensionality n, two systems of linear inequalities Lin over variables x1, . . . , xm and Lout over variables y1, . . . , yn, and a bound δ ∈ N ∪ {+∞},
• decide whether (N,Lin,Lout, δ) is valid, that is all pointed graphs (G, v) where the out-degree of each vertex is less or equal than δ, v has m features, and v satisfies system Lin imply that N(G, v) satisfies system Lout.

We write (N, Lin, Lout) instead of (N, Lin, Lout, +∞).

Example 1 (Continued). Recall the setting of Example 1 where we considered the safety property, "Every account that spams 100 messages or more per minute is identified as a bot by N ."

This property is expressed by the LVP instance (N,Lin,Lout) with Lin := x1 ≥ 100 and Lout := y1 ≥ 0.6 where x1 is the feature corresponding to the number of messages sent by a user, and y1 is the output of N corresponding to its classification as a bot (y1 ≥ 0.6) or a regular user (y1 < 0.6). Note that in this simple example Lin and Lout are systems consisting of a single inequality.

We show that LVP over quantized GNNs, where aggregation is given by summation, and combination functions and output functions are realized by classical feedforward neural networks (FNNs) using some kind of activation α, is reducible to the satisfiability problem of LquantGNN.

We denote the size of the GNN N by |N|, with |N| ∈ O(|Ncomb1 |+· · ·+|Ncombm |+|Nout |) where m is the depth of N and |Ncombi | and |Nout | are the sizes of the FNN used in N. The size of an FNN is simply the sum of the sizes of all its numerical parameters, namely weights and biases.

Theorem 8. Let I = (N,Lin,Lout, δ) be an LVP instance. There is a LquantGNN formula φI such that I is valid if and only if φI is not δ-satisfiable. Furthermore, φI can be computed from N,Lin,Lout in polynomial time with respect to |N| + |Lin| + |Lout |.

Proof. Let I = (N,Lin,Lout) be an LVP instance where the GNN N has l layers Li, each having a combination function combi represented by an FNN Ncombi as well as aggregation function aggi represented by the sum ∑ and output function represented by FNN Nout , Lin consists of linear inequalities φ1, . . . , φk1 working over variables x1, . . . , xn1 and Lout consists of linear inequalities ψ1, . . . , ψk2 working over variables y1, . . . , yn2 . Formula φI is the conjunction φ1 ∧ · · · ∧ φk1 ∧ φN ∧ (¬ψ1 ∨ · · · ∨ ¬ψk2 ) where φN is constructed as follows. Formula φN is a conjunction ξN,y1 - y1 = 0 ∧ · · · ∧ ξN,yn - yn2 = 0 where ξN,yi captures the computation of N corresponding to its i-th output as follows.

Consider layer L1 and assume that Ncomb1 has input dimension 2i1 and output dimension o1. We define the sub-expression ξL1,j = ξNcomb1 ,j(z1, . . . , zi1 , agg(z1), . . . , agg(zi1 )) for j ≤ o1 where ξNcomb1 ,j is the straightforward unfolding of the function of Ncomb1 corresponding to its j-th output using c, cξ,+ and α(ξ) operators on the inputs z1, . . . , agg(zi1 ). Next, consider the layers Lh for 2 ≤ h ≤ l. We assume that Ncombh has input dimension 2oh-1 and output dimension oh. We define the sub-expression ξLh,j equal to ξNcombh ,j(ξLh-i,1, . . . , ξLh-1,oh-1 , agg(ξLh-1,1), . . . , agg(ξLh-1,oh-1 )) for each j ≤ oh. Finally, we define ξN,xj = ξNout,j (ξLm,1, . . . , ξLm,om ) where ξNout,j is again the unfolding of the function of Nout corresponding to its j-th output.

The correctness follows from the construction above, as we simply unfold the computation of the GNN N using operators available in LquantGNN. The polynomial bound is due to the fact that we represent formulas as DAGs and, thus, avoiding any duplication of subformulas.

Example 9. Consider the simple GNN N of Example 5. The formula equivalent to N in the sense of Theorem 8 is φN := α(ξ2 + ξ ′2 ) - y = 0 with

ξ0 = x and ξ ′0 = x′ . Assuming that Lin := x + x′ ≥ 0 and Lout := y ≥ 0.6, the overall LquantGNN formula would be φI := x+x′ ≥ 0 ∧φN ∧¬(y ≥ 0.6).

Remark 10. The translation in Theorem 8 can be straightforwardly extended beyond the capabilities of LVP. For instance, we can generalize to instances of the form (N, φ, ψ), where N is a GNN and φ, ψ are LquantGNN formulas.

Note that if an LVP instance I is not valid, then φI is satisfiable. A model of φI offers a counterexample for I.

5 Satisfiability of LquantGNN Formulas

In this section, we tackle the following satisfiability problem, in which δ is a bound on the out-degrees of the pointed graph and n is the number of bits to represent an element of K. For instance, for n = 32, K could be Example 3. We write Kn to emphasize that the numbers are encoded on n bits. In the sequel, we fix a sequence K0,K1,K2 . . . with the following reasonable poly-space assumption for each Kn:

1. there is a uniform algorithm, taking n, k1, k2 and k in Kn as an input and checking whether k1+k2=k in polyspace in n (same for whether k1=k2, k×k1=k2).
2. given n written in unary, k, k′ ∈ Kn written in binary, deciding whether [[α]](k′ ) = k can be performed in polynomial space in n. This assumption is weak and is true for a large class of activation functions [[α]] (for instance ReLU, truncatedReLU for fixed-point or floating-point arithmetics on n bits).

Definition 11 (satisfiability problem). The satisfiability problem of LquantGNN is:

• input: an integer nwritten in unary, an integer δ (or δ = +∞) in unary or in binary, a formula Φ in LquantGNN
• question: does there exist a pointed graph with outdegree at most δ with features in a set Kn that satisfies φ?

Note that n is written unary is reasonable since n is precisely of the same order of magnitude as the size of the representation of an element in Kn, and we have to store the bits of numbers in Kn fully in memory anyway.

Bounding the out-degree δ is justified in applications such as chemistry. Generally, it is sufficient to represent δ in unary since the bound is often small. For instance, a carbon atom has 4 neighbors. Having δ in unary means also that we can keep all the successors/neighbors of a given vertex in memory at once. A graph can be exponential in δ; a tree may contain δdepth nodes, making the search space exponential in the input size when the depth is unbounded. Using a binary representation for δ is also interesting since the search space is already exponential with a fixed depth. For instance, we could search for a pointed graph which is a tree of depth 1 where the root has an exponential number of children.

5.1 TableauMethod

We propose a tableau method ([H¨ahnle, 2001; Gasquet et al., 2014]) to reason in our logic, i.e. to check whether a formula Φ is δ-satisfiable. For presentation purposes, we focus on the case where the degree bound δ is finite and given in unary. The cases where δ is written in binary or δ = +∞ are more involved, and are discussed in [S¨alzer et al., 2025].

The idea of tableau methods is to construct a model satisfying an initial formula by propagating constraints and creating new vertices when needed. We consider terms of the form (w φ) where w is a word (that intuitively denotes a vertex in the graph in construction) and φ is a formula. The intuitive meaning of (w φ) is that φ should be true in the vertex w.

We start the tableau method with the following term (ϵ Φ), saying that Φ should be true in the initial vertex, denoted by the empty word ϵ. Figure 4 shows our tableau rules.

The rules for (¬ ≥), (≥), (+), (α), (×) exploit the fact that the set Kn is finite. For instance, rule (≥) nondeterministically chooses a value for ξ that is greater than k in Kn. The rule (+) on the term (w ξ1 + ξ2 = k) (whose meaning is that the value of ξ1 + ξ2 should be equal to k) non-deterministically chooses values k1 and k2 for ξ1 and ξ2 respectively so that k1 + k2 = k. The rule (clashc) stops the current execution when the constant c is different from the value k to which it is constrained to be equal. Similarly, the rule (clash=) clashes when the feature xi at the vertex denoted by w is supposed to be equal to k and k′ with k ̸= k′ . The rules (α) and (×) work similarly to the rule (+) but for the activation function and for multiplication by a scalar. The rule (degree) non-deterministically guesses the out-degree of the vertex specified by w.

The rule (agg) is 'modal' and creates new successors w1, . . . , wδ′ where w1 is the word w on which we concatenated the letter 1, and so on. When the aggregation for the expression ξ is supposed to be equal to k and the out-degree is supposed to be δ′ , we create δ′ successors and impose that the sum of the values of ξ taken in these successors is equal to k (to this aim, we non-deterministically choose values k1, . . . , kδ′ for ξ in these successors).

The proposed tableau method is a non-deterministic procedure that applies as long as possible the rules given in Figure 4 from the initial set {(ϵ Φ)}.The method either fails or

Figure 4: Tableau rules for the satisfiability problem in LquantGNN when δ is written in unary.

stops successfully if no more rules are applicable.

A prototype implementation 1 of the proof system is presented in [S¨alzer et al., 2025].

5.2 Upper Bound

Theorem 12. The satisfiability problem of LquantGNN is in PSPACE, whether δ is given in unary, binary or is infinite.

Proof. The proof is given for δ in unary. For the proof when δ in binary or infinite, we can adapt the proof system, see [S¨alzer et al., 2025]. We have to prove that Φ is satisfiable iff there is an accepting execution of the tableau method.

The ⇒ direction is proven by taking a pointed graph G, v satisfying Φ and making the non-deterministic choices by letting oneself be guided by the evaluation of formulas in G. To do that, we start the execution of the tableau method with (ϵ φ) and we set f(ϵ) = v. We then show that we can always continue the execution maintaining the invariant: the partial mapping f from the labels in the tableau to V is such that if (w φ) appears in the tableau then G, f(w) |= φ; and if (w degree = δ′ ) appears then f(w) is of out-degree δ′ .

More precisely, we make the non-deterministic choices so that we can build a partial mapping f from the labels in the tableau to V , starting from f(ϵ) = v so that if (w φ) appears in the tableau then G, f(w) |= φ; and if (w degree = δ′ ) appears then f(w) is of out-degree δ′ .

Let us explain the principle with the (agg) rule. Suppose (w agg(ξ) = k) and (w degree = δ′ ) appears in the tableau. By the invariant, it means that G, f(w) |= agg(ξ) = k and that f(w) is of out-degree δ′ . But then f(w) has δ′ successors: u1, . . . , uδ′ . As G, f(w) |= agg(ξ) = k, there exists k1, . . . , kδ′ with k1+Kn · · ·+Kn kδ′ = k with G, ui |= ξ = ki for all i = 1..δ′ . We then set f(w1) := u1, . . . , f(wδ′ ) = uδ′ . We also apply the rule (agg) by choosing (w1 ξ = k1), . . . , (wδ′ ξ = kδ′). The invariant remains true.

1 https://github.com/francoisschwarzentruber/ ijcai2025-verifquantgnn

By the invariant, the premises of rules (clashc) or (clash=) are never in the tableau. For instance, if some (w c = k) with c ̸= k appears, we would G,w |= c = k which is a contradiction.

The ⇐ direction is proven by constructing a pointed graph G, v from the choices made in the accepting execution. The graph G = (V,E) is defined with V the set of labels w and E is the set of edges of the form (w, wu) with w a label and u ∈ {1, . . . , δ′ } with (w degree = δ′ ) appearing in the tableau. The label is ℓ(w) = (v1, . . . , vm) with vi such that (w xi = vi) appears in the tableau, or vi can be any number in Kn if no term (w xi = ...) appears.

We then prove that G, ϵ |= φ. To do that, we prove that if (w ψ) appears in the final tableau, then G,w |= ψ by induction on ψ. We show it for ψ =: agg(ξ) = k. Suppose that (w agg(ξ) = k) appears in the final tableau. Then it means that the rule (agg) has been applied on it. So (w1 ξ = k1), . . . , (wδ′ ξ = kδ′) for some (ku)u=1..δ′ , with k1 +Kn · · · +Kn kδ′ = k appear in the final tableau. By induction, it means that G,wi |= ξ = ki. So G,w |= agg(ξ) = k. Finally, as (ϵ φ) is in the tableau, the induction hypothesis gives G, ϵ |= φ.

It can be implemented in poly-space, in the same spirit as the tableau method for modal logic K ([Halpern and Moses, 1992]). The idea is to backtrack on rules (agg): first we try to add all the (w1 ξ = k1) for all applications of (agg), then try to add the (w2 ξ = k2) and so on. The algorithm is then a depth-first-search on the tree relying on the labels w (see Figure 5). We conclude by Savitch's theorem ([Savitch, 1970]) to obtain a deterministic algorithm.

Now, Theorem 8 and 12 imply an upper bound for LVP. Actually, we consider a quantized variant of LVP. Extending Definition 7, that problem also takes n in unary and δ in unary or in binary (as in Definition 11).

Corollary 13. LVP is in PSPACE.

Note that when δ is in unary, the satisfiability problem is in NP when the number of nested agg operators in the input formula is bounded by a fixed integer i. Indeed, the certificate is a pointed labelled tree of depth i of out-degree at most δ (it contains O(δi ) vertices). In consequence, LVP when we bound the number of layers by i is in coNP.

5.3 Usage Example

We assume that K is signed 32-bit fixed-point numbers, with four decimal places precision, similar to Example 2. The number 1 125 is stored as (the binary encoding of the decimal number) 80, 1 1000 is stored as 10, 0.9 is stored as 9000, 1000 is stored as 10000000, 250 is stored as 2500000, etc.

N has only one layer, with input dimension 1 (the value of x1 that labels a node indicates the number of messages per minute sent by the individual), and output dimension 2. The output layer is the identity. Consider again the LVP I = (N, Lin, Lout) where Lin = x1 ≥ 100 and Lout = y1 ≥ 0.6.

LquantGNN formula. As per Theorem 8 and its proof, the LVP I = (N, Lin, Lout) is valid iff φI = φin ∧ φN ∧ ¬ψout is not satisfiable, where:

• φin := x1 ≥ 100
• φN := ReLU( 1 125 x1)-y1 = 0∧ 1 1000 agg(x1)-y2 = 0
• ψout := y1 ≥ 0.6

Automated reasoning. We could show that (agg(x1) ≥ 1000)∧φN ∧¬(y2 ≥ 1.0) is not satisfiable, establishing that N comes with the guarantee of property B. Here we focus on property A. If the pointed graph (G, v) satisfies Lin, then N(G, v) will satisfy Lout. We could use the tableau method to automatically show that φI is not satisfiable and therefore that I is valid. Unfortunately, a complete formal proof cannot be reasonably presented here or even done by hand. Hence, to illustrate how the reasoning method can be used for the verification of quantized GNNs, we slightly modify the LVP I with a different output constraint.

Let I ′ be the LVP (N, Lin, L′out , δ), where N and Lin are as before, L′out := y1 ≥ 0.9, and δ = 5. We are going to show that the new output constraint is not always satisfied. I ′ is valid iff φI ′ := φin ∧φN ∧¬ψ′out is not satisfiable, where:

We employ our tableau method to prove that φI ′ is satisfiable and therefore that I ′ is not valid. We use ✓ to indicate that we have reached a term for which there are no rules to apply, except possibly (clash=). If in the end (clash=) does not apply, then we can read a model of φI ′ where the ✓s appear. We start the tableau method by applying the rule (∧)

and resolve inequalities with rules (≥) and (¬ ≥) (we write (∆) when we just use the definition of a formula):

(∧) (ϵ φin), (ϵ φN), (ϵ ¬ψ′out) (ϵ φin) (∆) (ϵ x1≥100) (≥) (ϵ x1=100) ✓ (ϵ φN ) (∆) (ϵ C1∧C2) (∧) (ϵ C1), (ϵ C2) (ϵ ¬ψ′out ) (∆) (ϵ ¬y1≥0.9) (¬≥) (ϵ y1=0.8) ✓ where we write C1 for the conjunct ReLU( 1 125 x1) - y1 = 0 and C2 for the conjunct 1 1000 agg(x1) - y2 = 0. We handle the conjunct C1 in φN. (ϵ ReLU( 1 125 x1) + (-1)y1 = 0) (+) (ϵ ReLU( 1 125 x1) = 0.8), (ϵ (-1)y1 = -0.8) (ϵ ReLU( 1 125 x1) = 0.8) (α) (ϵ 1 125 x1 = 0.8) (×) (ϵ x1 = 100) ✓ (ϵ (-1)y1 = -0.8) (×) (ϵ y1 = 0.8) ✓ Finally, we handle the conjunct C2 in φN. (ϵ 1

Obtaining amodel. We obtain a counterexample (G, v) for the formula φI ′ , with the node v labelled (x1) = (100), which has 4 successors, all labelled (x1) = (250). So, by Theorem 8, I ′ is not valid. Indeed, G, v satisfies Lin. But N(G, v) is (y1, y2) = (0.8, 1) which does not satisfy L′out .

This illustrates how the proof system serves to verify the properties of quantized GNN, but also to exhibit counterexamples when they exist.

6 Lower Bounds

If not said otherwise, we suppose now the activation function is truncated ReLU; it corresponds to the settings in many works ([Barcel´o et al., 2020; Nunn et al., 2024; Benedikt et al., 2024]). Furthermore, to obtain stronger PSPACE lower bound results, we will consider two restrictions:

• Case{0,1,2},δ=2: K contains 0, 1, 2 and the out-degree is bounded by δ=2;
• Case{-2..3},satu: K includes {-2,-1, 0, 1, 2, 3} and moreover, K saturates in the following sense: for all integers x, x ≥ 3 implies xK ≥K 3K. In particular, it means that we have no modulo behavior in K (e.g., K = Z10 would not saturate since despite 10 ≥ 9 as integers, we would not have 0 = 10 ≥K 9 modulo 10).

In both cases, n = 3 bits are enough to represent the numbers. Our lower bound results rely on graded modal logic which extends modal logic with constructions ∃≥k φ whose truth conditions is: G, v |= ∃≥k φ iff there are at least k successors u of v such that G, u |= φ. We call GMLK the syntactic fragment where occurrences of ∃≥k are such that k ≤ K.

Lemma 14. The satisfiability of GML1 on graphs wit outdegree at most 2, and the satisfiability of GML3 is PSPACEhard.

Theorem 15. LVP is PSPACE-complete. PSPACE-hardness holds already for Case{0,1,2},δ=2 or Case{-2..3},satu.

Proof. PSPACE-membership is stated in Corollary 13. The lower bound relies on the poly-time transformation τ of a GML-formula φ into an equivalent GNN N = τ(φ) in the sense that N(G, v) satisfies x1 ≥ 1, given in Barcel´o et al. [2020, proof of Proposition 4.1]. More specifically, we carefully analyze the GNN N when the formula φ is in GMLK .

In N, the activation function is truncated ReLU. The layers in τ(φ) are all the same. The matrices C contain coefficients

-1, 0, 1 and all coefficients on a column are 0 except two at most. The matrices A only contain 0 and 1. On each column of A, all coefficients are 0 except one which may be 1. Coefficients in the biases b are in {-K+1, -K+2, . . . , 1}.

Propositional variables in φ are among p1, . . . , pJ, N(G, v) starts with the state (x0u )j = 1, if j ∈ {1, . . . , J} and pj holds in u, and (x0u )j = 0 otherwise. As the activation function is truncated ReLU, all vectors xiu are 0-1-vectors.

Given the coefficients in the matrices, intermediate values are all integers.We end the proof of our Theorem 15 by stating the reductions and arguing that the computation is safe when done in K, meaning that there is no overflow and that the computation in K and in Z yields the same result.

Proof for Case{0,1,2},δ=2 We reduce the satisfiability of GML1 on graphs of out-degree at most 2 which is PSPACEhard (Lemma 14) into the dual problem LVP of LVP with δ=2: from φ a GML1-formula, we compute the LVP-instance (τ (φ), ⊤, y1 ≤ 0, δ=2), and φ is satisfiable on graphs of outdegree 2 iff (τ(φ),⊤, y1 ≤ 0, δ=2) is a negative instance of LVP. LVP is PSPACE-hard, so is LVP. The computation is safe because there are at most two successors, so we never exceed 2 in a computation in K.

Proof for Case{-2..3},satu We reduce the satisfiability of GML3 which is PSPACE-hard (Lemma 14) into LVP: given φ a GML3-formula, we compute the LVPinstance (τ(φ),⊤, y1 ≤ 0, δ=+∞). We have that φ is GML3-satisfiable iff there exists G, v s.t. G, v |= φ iff (τ(φ),⊤, y1 ≤ 0, δ=+∞) is a negative instance of LVP. The computation is safe because, even if there are an arbitrary large number x of successors, if x ≥ 3, we also have xK ≥K 3K because K saturates.

Corollary 16. The satisfiability problem of LquantGNN is PSPACE-complete, and already PSPACE-hard for Case{0,1,2},δ=2 or Case{-2..3},satu, and also when the activation function is ReLU.

7 RelatedWork

Starting with Graded Modal Logic ([Fine, 1972]), there are numerous logics that capture modal aspects of graphs and express arithmetic constraints, ([Demri and Lugiez, 2010; Baader, 2017; Bednarczyk et al., 2021; Galliani et al., 2023; van Benthem and Icard, 2023]).

Previous research has already established several correspondences between logic and GNNs. For instance, Barcel´o et al. [2020] explore the relationship between graded modal logic and GNNs, while Nunn et al. [2024] examine a modal logic over linear inequalities with counting and its connection to GNNs. Additionally, Benedikt et al. [2024] investigates fragments of Presburger logic in the context of GNNs. However, these existing works focus on GNNs with specific activation functions and do not consider the broader class of quantized GNNs. In particular, decidability in PSPACE has been established only for cases where the activation function is either a truncated ReLU ([Nunn et al., 2024]) or eventually constant functions ([Benedikt et al., 2024]). Ahvonen et al. [2024] offer several logical characterizations of recurrent GNNs over floats and real numbers. Also related, is the work of Grohe [2023], which establishes that the graph queries computable by a polynomial-size, bounded-depth family of GNNs are precisely those definable in the guarded fragment of first-order logic with counting and built-in relations.

Henzinger et al. [2021] also address the verification of quantized neural networks, but in contrast to this paper they focus on FNN. The authors establish a PSPACE-hardness result, relying on a binary representation of the number of bits. In contrast, if the number of bits were unary, their problem is presumably in NP (using a guess and check argument, relying on similar arguments as used by [S¨alzer and Lange, 2021]).

There are other aggregation functions, like weighted sums in graph attention networks [Velickovic et al., 2018], maximum in Max-GNNs [Cucala and Grau, 2024], or average. LquantGNN and the tableau method can be adapted to capture these aggregation functions, too (see [S¨alzer et al., 2025]).

On the practical side, Huang et al. [2024] presents a solution to the verification of quantized FNNs using heuristic search, and outperforming the approach of Zhang et al. [2023] based purely on integer linear programming.

8 Conclusion and Perspectives

We introduced a method for explicitly verifying and reasoning about properties of a practical class of quantized Graph Neural Networks. It allows us to establish new foundational results about the computational complexity of GNNs' tasks.

We proposed a tableau method for reasoning about quantized GNNs using the new logic LquantGNN. As the domain for numbers is finite, we are able to work out our details using a parameterized class of quantized GNNs, allowing us to consider various activation functions. We showed that for such classes of GNNs using FNNs in their internal parts, we can answer basic formal reasoning questions using a reduction to the satisfiability problem of LquantGNN. We showed that satisfiability of LquantGNN is solvable in PSPACE.

This work is a first step to further develop concrete methods for reasoning about quantized GNNs and other neural network models. Now, it will be interesting to implement our approach on a broader scale in order to tackle tasks such as certifying (adversarial) robustness properties ([G¨unnemann, 2022]) or giving formal explanations ([Marques-Silva and Ignatiev, 2022]) for certain GNN behaviours.

Ethical Statement

There are no ethical issues.

Acknowledgments

This work was supported by the ANR EpiRL project ANR22CE23-0029, and by the MUR (Italy) Department of Excellence 2023-2027.