The Complexity of Verifying Feedforward Neural Networks in Quantised Settings

1 Introduction

Feedforward Neural Networks (FNN) are ubiquitous in deep learning, not only as a stand-alone model for classifying inputs or transforming input values into outputs, but also as components in other machine learning models, for instance transformers, cf. [Vaswani et al., 2017]. The ever-growing quest for machine-learning methods to solve various computational tasks, in particular for safety-critical applications, comes with a need for methods that formally verify properties like safety or robustness of such models, including FNN.

In this paper, we are concerned with verification tasks of the following form: given an FNN N and a safety property ω, decide whether ω holds for N or not. To distinguish this from other forms of verification, such as testing N on a sample set of inputs or adjusting the training procedure to meet certain safety criteria, we refer to this as static (FNN) verification.

In its most rigorous form, static verification tasks are stated as formal decision problems. In one of the most prominent variants, addressed by a wide-range of practical solvers, cf.

[Brix et al., 2024; Brix et al., 2023], or analysed formally, cf. [Sälzer and Lange, 2022; Wurm, 2023; Henzinger et al., 2021], static verification is concerned with the question of whether the pairs of inputs and corresponding outputs of a given FNN satisfy certain linear constraints. Problems of this kind are often referred to as reachability problems, cf. [Huang et al., 2020], and other formal problems like robustness can usually be reduced to reachability.

The reachability problem for FNN was claimed (see [Katz et al., 2017; Katz et al., 2022; Ruan et al., 2018]) and shown (see [Sälzer and Lange, 2021; Sälzer and Lange, 2022]) to be NP-complete. In this setting, FNN are considered to be mappings on real-valued vector spaces. In practice, the arithmetic operations internal to the FNN are of course executed not in arithmetic over R which would be infeasible on any bounded-memory computer, but in some fixed-width arithmetic using 64bit floating-point or fixed-point numbers for instance. This shift from real-valued inputs and outputs to such discrete values is also known as quantisation, and it comes not only with a loss of precision but also with artefacts like rounding or over-/underflows. One may therefore argue that (I) NP-completeness of the reachability problem for FNN in arithmetic over R does not necessarily predict the computational complexity of formal verification for FNN over a quantised arithmetic, and (II) that the quantised setting is more interesting for practical purposes anyway.

We investigate the computational complexity of formal verification, i.e. reachability, for quantised FNN. Quantisation does not make formal verification easier, i.e. NPhardness remains a lower bound. This is not really surprising since computational hardness is often tightly linked to discretisation, see for instance the NP-completeness of Mixed-Integer Linear Programming versus the polynomialtime solvability of R-valued linear programs. [Henzinger et al., 2021] recently studied the verification problem for quantised FNN and provided a result that suggests higher complexity, namely PSPACE instead of NP. There seems to be some widespread misunderstanding about the actual results, perhaps fuelled by the fact that the paper is seen to be hard to read. First of all, [Henzinger et al., 2021] only provides a lower bound of PSPACE-hardness, not PSPACEcompleteness. Second, they consider a richer specification language for safety properties: while NP-completeness holds for safety properties that are convex sets of vectors, i.e. specifications in the form of linear programs, [Henzinger et al., 2021] uses bit-vector logics which allow non-convex sets to be specified. Thus, the increase in complexity from NP to PSPACE is not due to quantisation, as that paper may suggest, but due to the use of a richer specification language for safety properties.

In this paper, we aim to provide an overall picture of the computational complexity of formal verification for quantised FNN. We classify the complexities depending on (I) the involved specification formalisms for safety properties, as they are commonly used in the literature, (II) the exact nature of the fixed bit-width arithmetic that determines how the FNN's internal computations are performed on common hardware architectures and, finally, (III) the dependence on the parameter determining the bit-width of such numbers, in particular whether this is given in unary or in binary. The motivation for studying the effect that this parameter has, also comes from practice: suppose we import a trained FNN to run on our hardware. The FNN may come with advice saying that arithmetic operations should be carried out with a certain bitwidth. In this case, that width would normally be given as a decimal number, i.e. the actual width is exponential in the representation size of that parameter. On the other hand, when verifying a quantised FNN on the hardware where it already resides, the bit-width rather corresponds to the size of actual CPU registers, and therefore a unary encoding of this length may be a more realistic measure of the space needed to represent such quantised values.

The paper is organised as follows. In Section 2, we provide thorough definitions of all fundamentals necessary for the findings presented in this paper. In Section 3, we formally present reachability problems of FNN as decision problems. In Section 4, we examine the complexity of reachability in different quantisation settings where specifications are given by linear constraints. In Section 5, we study the complexity of verifying quantised FNN in the context of bit-vector logic, complementing the work of [Henzinger et al., 2021]. Finally, in Section 6, we briefly discuss our findings and outline prospective next steps.

2 Preliminaries

Numbers, vectors and matrices. We exclusively consider numbers from Q. Typically, we denote vectors using small, bold symbols like x, y or z and matrices using big, bold symbols like A, B or C. We denote by xi the i-th entry of vector x and by Ai↪j the entry in the i-th row and j-th column of matrix A. Let x → Q with p → Z and q → N>0 such that x = pq . If not stated otherwise, we define the size of x, denoted by ♣x♣, as ♣x♣ = ♣p♣+♣q♣ where ♣p♣ = (↑log2(p)+1↓)+1 and ♣q♣ = ↑log2(q) + 1↓. Analogously, we extend the definition of ♣ · ♣ to vectors x → Qm and matrices A → Qm→n by ♣x♣ = ∑mi=1 ♣xi♣ and ♣A♣ = ∑mi=1 ∑nj=1 ♣Ai↪j♣.

Finite-width arithmetics. We consider two kinds of finite arithmetics: fixed- and floating-point arithmetics. A fixedpoint arithmetic Fix b↪f is a tuple (Qfix b↪f ↪ o↪ r), where Qb↪f = ¶ n 2f ♣ ↔2b↑1 ↗ n < 2b↑1 ↪ n → Z♦ is the sets of rationals representable using b bits with f bits for representing the fractional parts, o: Q ↘ Qb↪f is a map called overflow mode and r : Q ↘ Qb↪f is a map called rounding mode. We associate with Fix b↪f the typical arithmetic operations, carried out as ≃Fix b↪f := o(r(x ≃ y)) for all ≃ → ¶+↪ ·↪÷♦↪ x↪ y → Q, and binary comparisons, carried out as ⇐Fix b↪f := o(x) ⇐ o(y) for all ⇐→ ¶<↪↗↪=♦↪ x↪ y → Q. Similarly, a floating-point arithmetic Float p↪e is a tuple (Qfloat p↪e ↪ r) where

is the set of rationals representable with p-bit significant and e-bit exponent width, and r : Q ↘ Qfloat p↪e is a rounding mode. We associate with Float p↪e the typical arithmetic operations, carried out as ≃Float p↪e := r(x ≃ y) for all ≃ → ¶+↪ ·↪÷♦↪ x↪ y → Q, and binary comparisons, carried out as ⇐Float p↪e := r(x) ⇐ r(y) for all ⇐ → ¶<↪ ↗↪ =♦ and x↪ y → Q. To keep things concise, we refer to both of these as finite-width arithmetics Fn1↪n2 and represent them as tuples F = (n1↪ n2↪ r↪ o), where n1↪ n2 are the total bit number and fractional width (fixed-point), or the significant and exponent width (floating-point); r is the rounding mode and o the overflow mode (in the case of floating-point, we simply assume o = r w.l.o.g.). We use Fn1↪n2 to refer to the full arithmetic as well as the set of numbers representable in Fn1↪n2 .

Feedforward neural networks. An FNNN, of some class of FNN N, is a tuple (A(i) ↪ b(i) )ki=1 of matrices A(i) → Qmi→ni and vectors b(i) → Qmi . We call k the number of layers (or depth) of N, n1 the input dimension of N, nk the output dimension of N, mi the size of layer i for all i ↗ k, and generally assume that mi = ni+1 for all i ↗ k ↔ 1. This concise representation of FNN from N assumes unambiguity in the definition of N regarding which and how activation functions are used by N → N. We generally assume that this is relu(x) = max(0↪ x), the prominent ReLU activation function, across all layers. 1

Regarding different assumptions about the underlying arithmetic, we consider two distinct types of FNN for verification:

Rational FNN: A rational FNN N = (A(i) ↪ b(i) )ki=1 has weights and biases from Q. It computes a function N : Qn1 ↘ Qnk by the standard forward propagation with N(x) =

For rational FNNs, we define ♣N♣ = ∑ki=1 ♣A(i) ♣ + ♣b(i) ♣. Quantised FNN: Given some finite-width arithmetic F = (n1↪ n2↪ r↪ o), a quantised FNN has weights and biases from Fn1↪n2 . Such an FNN N♣F computes a function N♣F : Fn1 ↘ Fnk by N♣F(x) =

1 As done in other works such as [Sälzer and Lange, 2022], our results can be extended to FNN using general piecewise linear activation functions.

where ε(i) (·) denotes the entrywise application of activation function ε(i) : Q ↘ Q. We assume that the definition of F determines how ε(i) is carried out in F. We associate with N♣F the tuple (A(i) F ↪ b(i) F )ki=1 where all weights and biases are represented in Fn1↪n2 . For quantised FNN, we define ♣N♣F♣ = ∑ki=1 ♣A(i) ♣F +♣b(i) ♣F, where ♣ · ♣F denotes the representation size as specified by F.

Linear Programs. A linear program (LP) is a system of linear constraints of the form L = ∧mi=1 (∑nj=1 ai↪j · xj ⇐i bi ) where ai↪j↪ bi → Q, xj are variables, and ⇐i → ¶<↪↗↪= ↪ ⇒↪ >♦ for each i. The feasibility problem for such linear programs is: given an LP, does there exist an assignment of values to the variables x1↪ ▷ ▷ ▷ ↪ xn, that satisfies all constraints? We can encode neural network verification problems as feasibility problems over linear constraints, where the constraints capture both the network's behaviour and the property specification. We define ♣L♣ = ∑mi=1 ♣bi♣ + ∑nj=1 ♣ai↪j♣.

A fundamental result in linear programming theory establishes a polynomial bound on the size of solutions:

Theorem 1 ([Korte and Vygen, 2018]). Let L be a linear program with input size ♣L♣.If L has a solution, then there exists a solution (x1↪ ▷ ▷ ▷ ↪ xn) such that ∑nj=1 ♣xj ♣ ↗ poly(♣L♣).

This polynomial bound is crucial for our analysis as it ensures that solutions to linear programs used in neural network verification have representations whose size is polynomially bounded by the input representation size.

Bit-Vector Logics (BV). We consider fixed-size bit vector logics as introduced in [Kovásznai et al., 2016]. Let ϑ → N+ be a fixed bit-width and V be a finite set of variables. A BV formula ω is inductively defined as

A BV formula ω is evaluated over bit-vectors of fixed size ϑ. An assignment is a function ϖ : V ↘ ¶0↪ 1♦ω that maps each variable to a bit-vector of length ϑ. The semantics of formulas is defined inductively as

The interpretation of terms under an assignment ϖ is defined as

llbracket⇐trrbracketε = ⇐llbrackettrrbracketε llbrackett1 ↖ t2rrbracketε = llbrackett1rrbracketε ↖ llbrackett2rrbracketε for ↖ → ¶&↪ ♣♦, where '&', '♣' and '⇐' denote the standard bitwise AND, OR, and NOT operations and encω(c) is the ϑbit binary representation of c.

A BV formula ω is satisfiable over bit-vectors of length ϑ if there exists an assignment ϖ such that ϖ ♣= ω.

Proposition 2 ([Kovásznai et al., 2016]). The satisfiability problem for BV formulas with bit length and constants given in binary is NP-complete.

The model checking problem for BV is: given a BV formula ω with bit-width b and an assignment ϖ, determine whether ϖ ♣= ω.

Proposition 3. The model-checking problem for BV formulas can be decided in polynomial time.

Proof. This is trivial, as given an assignment ϖ, one can evaluate ω bottom-up by traversing the syntax tree. Each term can be evaluated in time O(b), thus the whole procedure can be done in time O(b · ♣ω♣).

3 Verifying Quantised FNN: Overview

We consider five distinct reachability problems in this paper, differentiated by the type of arithmetic presumed for numerical operations and two separate formalisms utilised to specify valid inputs and outputs in the literature. We start with the most standard, yet somewhat idealised setting.

REACHQ(LP): given rational FNNN, and two rational linear programs L1↪ L2, decide whether there is input x of N that satisfies L1 such that the output N(x) satisfies L2.

REACHQ(LP) assumes the computations of N, including the representation of its numerical parameters, to be performed in full-precision, rational arithmetic. However, this assumption is unrealistic for concrete computer architectures, which are limited to specific finite-width arithmetics, such as IEEE 754 floating-point arithmetic using 32 bits to represent numbers in binary. Neglecting these real-world restrictions, as done by various solvers addressing REACHQ(LP) or similar problems relying on idealised assumptions, has severe consequences as shown in [Jia and Rinard, 2021]. Thus, it is crucial to account for the quantisation of FNN due to some finite-width arithmetic during verification. Let F = ¶Fn1↪n2 ♣ n1↪ n2 → N♦ denote the set of all finite-width arithmetics as defined in Section 2. We assume w.l.o.g. that F only contains well-defined arithmetics, excluding, for instance, fixed-point arithmetics Fix b↪f with f > b.

REACHF(LP): given a quantised FNN N♣F with input dimensionality d, and two quantised linear programs L1♣F↪ L2♣F for some F → F, decide whether there is x → Fd that satisfies L1♣F such that N♣F(x) satisfies L2♣F.

In the context of quantised FNN, [Henzinger et al., 2021] considered specifications other than plain linear constraints, namely those expressed by bit-vector logic (BV); see Section 2 for details.

REACHF(BV): given a quantised FNN N♣F with input dimensionality d for some F = Fn1↪n2 → F, and two BV formulas ω1↪ ω2 both with bit-length ϑ = n1 + n2, decide whether there is x → Fd that satisfies ω1 such that N♣F(¯x) satisfies ω2.

While REACHF(LP) and REACHF(BV) realistically assume restrictions imposed by finite-width arithmetic, they permit further generalisation: quantisation often occurs posttraining, cf. [Gholami et al., 2021], implying that the FNN is initially trained and delivered using more exacting representations. In actual implementations, it is quantised to different small-width arithmetics, meaning that the size of the FNN and the size of the finite-width arithmetic are independent.

REACH(F↪ LP): given a finite-width arithmetic F → F, a rational FNN N with input dimensionality d, and two rational linear programs L1↪ L2, decide whether there exists x → Fd that satisfies L1♣F such that N♣F(x) satisfies L2♣F.

REACH(F↪ BV): given a finite-width arithmetic F → F, a rational FNN N with input dimensionality d, and two BV formulas ω1↪ ω2 with bit-length ϑ = n1 + n2, decide whether there exists x → Fd that satisfies ω1 such that N♣F(x) satisfies ω2.

We remark that post-training quantisation techniques, as assumed in REACH(F↪ LP) and REACH(F↪ BV), typically involve more than merely rounding numerical parameters using standard rounding methods specified by some finite-width arithmetic F, like rescaling weights prior to quantisation. Nonetheless, we note that such variations do not affect the aforementioned problems because they examine the safety of the resulting quantised FNN, independent of its relation to the unquantised version.

4 Verifying Quantised FNN in Relation to Linear Constraints

REACHQ(LP) is the problem considered most often in the context of reachability w.r.t. linear constraints. It assumes FNN to work over full-precision, rational arithmetic and input- and output-specifications given by sets of linear constraints, i.e. linear programs.

Theorem 4 ([Sälzer and Lange, 2021]). REACHQ(LP) is NPcomplete.

We briefly recapitulate the proof of Theorem 4 to reuse certain arguments for subsequent results. NP-membership is shown using the certificate-based understanding of NP: guess a witness w of polynomial size in ♣N♣ + ♣L1♣ + ♣L2♣ which is the size of an instance (N↪ L1↪ L2) of REACHQ(LP), and then verify in polynomial time relative to ♣w♣ + ♣N♣ + ♣L1♣ + ♣L2♣ whether (N↪ L1↪ L2) is a valid instance. Here, the key insight is that for each input x of N, there is a fixed activation pattern of N, meaning a tuple w → ¶0↪ 1♦n , where n is the number of nodes in N, such that w[i] = 1 if and only if the input of the ith node in N is greater than or equal to 0. Clearly, such an activation pattern w is of size polynomial in the size of N. Having this, the argument for NP-membership is as follows: given FNN N, LP L1 and L2, (I) guess an activation pattern w of N. (II) Fix all ReLU nodes of N by replacing the activation of the ith node by the identity if w[i] = 1, and by the constant 0-function if w[i] = 0. (III) Construct a single LP L by combining L1, L2, and N, which is possible since N computes a linear function now, and add constraints ensuring that any solution respects w, and (IV) solve L. Since L is essentially just the combination of N, L1, and L2, and LPs can be solved in polynomial time, the procedure above runs in nondeterministic polynomial time.

NP-hardness of REACHQ(LP) is shown via a reduction from 3SAT, the satisfiability problem of propositional Boolean formulae in three-conjunctive normal form (3CNF). Given a 3CNF formula ω = ∧ni=1 Ci with n → N where each Ci = (ϑi↪1 ↙ ϑi↪2 ↙ ϑi↪3) is a clause with literals ϑi↪j of the

Figure 1: FNN gadgets, one for each component of a propositional 3CNF formula ω, that output 1 if the corresponding subformula is satisfied and 0 otherwise. Additionally, it shows a gadget that for x → [0; 1] outputs 0 if x = 0 or x = 1, and some value greater than 0 otherwise.

form X or ≻X for propositional variables X → X, we construct an FNN Nϑ that accepts precisely those inputs x that encode a satisfying assignment I : X ↘ ¶0↪ 1♦ for the propositional variables used in ω. The construction of Nϑ involves combining specific gadgets as presented in Fig. 1. We have one gadget for each kind of subformula in ω, mimicking their semantics in a straightforward manner, and combine them as determined by the structure of ω. To ensure that Nϑ only accepts inputs corresponding to an encoded variable assignment, which is essential for a correct reduction from 3SAT, the FNN Nϑ also includes an "x → ¶0↪ 1♦" gadget (see Fig. 1) for each input dimension. Additionally, we use L1 to ensure that each input is within [0↪ 1], which is necessary for the idea underlying the "x → ¶0↪ 1♦"-gadgets, as well as L2 to ensure that the output of the final "∧ni=1 Ci" gadget in Nϑ is exactly 1 and the output of all "x → ¶0↪ 1♦" gadgets is exactly 0. For details, we refer to [Sälzer and Lange, 2021].

Turning to quantised settings, we find that while specific arguments for Theorem 4 require additional support, the overall complexity of verifying reachability in the context of linear constraints remains unchanged. Remember that REACHF(LP) takes as input FNN and LP that are already quantised.

Theorem 5. REACHF(LP) is NP-complete.

Proof. Membership in NP relies on the certifier-based understanding of NP and is straightforward. Let (N♣F↪ L1♣F↪ L2♣F) with F = Fn1↪n2 . (I) Guess an input x → F, (II) check whether L1♣F is satisfied, (III) compute N♣F(x), and (IV) check whether N♣F(x) satisfies L2♣F. Clearly, ♣x♣ is linear in n1 + n2, which is polynomial in ♣N♣ since N contains numerical parameters represented in F. Furthermore, steps (II) to (IV) can be done in polynomial time with respect to ♣L1♣ + ♣N♣ + ♣L2♣ since all numerical parameters are represented in F. Note that we assume constant time for basic arithmetic operations. The correctness is implied by Theorem 1, which states that feasible LP have solutions of polynomial size. The reasoning used for Theorem 4, as sketched above, carries over to parts (I)-(IV).

Regarding NP-hardness, we refer to the same argument used in Theorem 4, namely, the reduction from 3SAT translating a 3CNF formula ω into an FNN Nϑ. The key insight is that the same reduction described above works here because the gadgets shown in Figure 1 use only low-precision parameters, specifically 1, 0, and 12 , which are exactly representable in all non-trivial finite-width arithmetics F. Moreover, the sums in the "∧ni=1 Ci" and "∨3j=1 ϑi↪j" gadgets are at most n. Thus, it is sufficient to assume that Nϑ♣F to be quantised by any F with at least ∝log n′ bits to represent integer parts.

The other quantised problem we consider in this section is REACH(F↪ LP). In contrast to REACHF(LP), the given FNN contains full-precision rational parameters, and the quantisation to some finite-width arithmetic Fn1↪n2 is not assumed a priori, making Fn1↪n2 part of the input. At first glance, this may lead one to thinking that this problem must be more difficult, since we have to deal with numbers of bit size n1 +n2, and the parameters n1↪ n2 are given as binary numbers. However, it is easily argued that this is not the case.

Theorem 6. REACH(F↪ LP) is NP-complete.

Proof. NP-membership is shown as in Theorem 5: given (Fn1↪n2 ↪N↪ L1↪ L2), we quantise N, L1, and L2 using Fn1↪n2 , guess an input x → Fn1↪n2 and check whether it is a witness for the validity of (N↪ L1↪ L2). Note that this assumes that the quantisation method used for N, L1 and L2 works in polynomial time. Given that, we need to argue why the size of x is polynomial in the size of (Fn1↪n2 ↪ N↪ L1↪ L2). We make a case distinction. First, assume that ♣n1♣ +♣n2♣ is larger than the maximum size of any rational parameter of N, L1 or L2. Then, guessing x, which is polynomial in ♣n1♣ + ♣n2♣, is sufficient since this also subsumes solutions for the LP resulting from combining (N↪ L1↪ L2), utilising the activation pattern of N for x, according to Theorem 1. Second, assume that ♣n1♣ + ♣n2♣ is smaller than the maximum size of any rational parameter of N, L1 or L2. Then, guessing x, which is polynomial in ♣N♣ + ♣L1♣ + ♣L2♣ is also sufficient, again using Theorem 1. In combination, it is sufficient to take x which is polynomial in the size of (Fn1↪n2 ↪N↪ L1↪ L2).

NP-hardness is shown similarly to Theorems 4 and 5 by establishing a reduction from 3SAT. In this case, we introduce a finite-width arithmetic Fn1↪n2 with a sufficient number of bits. We observe that n1 +n2 is polynomial in the size of the 3CNF formula ω.

5 Verifying Quantised FNN in Relation to BV Constraints

As seen in Section 4, using linear constraints always guarantees solutions of polynomial size with respect to the size of the FNN and specification LP. [Henzinger et al., 2021] investigated the verification of quantised FNNs with respect to bit-vector logics, cf. [Kovásznai et al., 2016], instead. This is motivated by the fact that BV allow non-linear constraints to be specified and single bits of the FNN's in- and output to be addressed. This can avoid rounding and overflow problems in contrast to the standard specifications via linear constraints, which crucially depend on the type of arithmetic and bit-width used when evaluating an FNN.

First, for already quantised FNN, these non-linear constraints do not change anything complexity-wise.

Theorem 7. REACHF(BV) is NP-complete.

Proof. Membership in NP is shown as in Theorem 5. Let (N♣F↪ ω1↪ ω2) with F = Fn1↪n2 . (I) Guess an input x → F, (II) check whether x ♣= ω1, (III) compute N♣F(x), and (IV) check whether N♣F(x) ♣= ω2. First, ♣x♣ is linear in n1 + n2 which is polynomial in ♣N♣ since N contains numerical parameters represented in F. By Prop. 3, model checking for BV formulas can be done in polynomial time.

Regarding NP-hardness,we use the same argument as in Theorem 5. As the lower bound construction does not need any input or output specification, NP-hardness already holds for BV specifications as well.

Analogously to Section 4, problem REACH(F↪ BV) assumes the FNN given with full-precision parameters together with some finite-width arithmetic as part of the input. This problem was already considered in [Henzinger et al., 2021], where only a lower bound was shown.

Theorem 8 ([Henzinger et al., 2021]). REACH(F↪ BV) is PSPACE-hard.

The remainder of this section is dedicated to establishing upper bounds. While the lower bound in [Henzinger et al., 2021] is independent of the arithmetic, the upper bounds depend on them. We therefore distinguish two cases and establish the following.

Theorem 9. REACH(F↪ BV) is PSPACE-complete for fixedpoint and floating-point arithmetic with constant exponent width.

We show this by reducing REACH(F↪ BV) to the problem of checking non-emptiness for non-deterministic finite automata (NFA), represented in a succinct way. Using automata to recognise relations induced by linear arithmetics (cf. [Wolper and Boigelot, 2000] and [Esparza and Blondin, 2023, Chp. 14]) or for recognising the input-output behaviour of rational FNN in particular [Sälzer et al., 2024] was already explored in previous work. We show that these results can be extended to quantised FNNs as well and use it for a complexity analysis.

Unlike explicit automata defined by state transition tables, a succinct NFA describes a machine with an exponentially large state space via a compact, implicit representation. Formally, an NFA with state space of size 2n is succinctly represented if each state has a polynomial description size in n and there are two polynomial-time algorithms: (1) TRANS takes two state descriptions q↪ q↓ and a symbol ε and decides whether there is a transition from q to q↓ with symbol ε. FINAL takes a state description q and decides whether q is a final state. The problem of deciding non-emptiness for such NFAs is equivalent to the reachability problem in succinctly represented graphs, which was explored in previous work.

Proposition 10 ([Galperin and Wigderson, 1983]). The nonemptiness problem for succinctly represented NFA is in PSPACE.

Succinctly represented NFAs are closed under intersection and union. The state of the product/union automaton is the tuple of the states of the component automata. The size of the combined state description is the sum of the individual sizes, which remains polynomial. Functions TRANS checks for all components to be true. Function FINAL checks that both states are final (for intersection) or at least one is (for union).

The input-output behaviour of rational FNNs evaluated over a given fixed-width arithmetic can be captured by succinct NFA. We start with the case of fixed-point arithmetic, encoding fixed-point numbers over the alphabet ! = ¶0↪ 1♦ with least-significant bit first and in two-complement representation. I.e. the word bfbf↑1 · · · b1a0a1 · · · ab↑1 → ¶0↪ 1♦b+f is the encoding of the number x with

Now fix an FNN N with parameters ϱ, input and output dimensions m and n, and a fixed-point arithmetic Fix b↪f with bit-width k = b + f. Its input-output relation is RN↪Fix b↪f =

Lemma 11. There exists a succinct NFA MN↪Fix b↪f with description size in poly(♣N♣ + log(b + f )) accepting RN↪Fix b↪f .

Proof. We construct MN↪Fix b↪f to process the input-output relation bitwise. A state qt = (t↪ c↪ r↪ cinit↪ w) is a tuple, where t → ¶0↪ · · · ↪ k♦ is a bit counter, c → Z♣ϖ♣ represents a vector of carry values for all linear operations, r → Q♣ϖ♣ is a fractional accumulator for rounding and w = ¶0↪ 1♦♣ϖ♣ is the activation pattern. At t = 0, the automaton non-deterministically guesses the activation pattern w and the vector cinit, which represents the carry bit that would be generated by rounding the fractional result of the scalar products. The accumulator r is initialised to 0. The accumulator aggregates computations shifted below the LSB, in order to verify the rounding decisions.

Note that for a single neuron with i inputs and maximum weight ς, the carry is bounded by O(i·ς) and especially independent of the bit-width k. Additionally, the fractional accumulator is always bounded by the size of the weights, which are multiplied. Thus, each state needs space O(log k + ♣N♣) which is polynomial in the input size. Note that weights are not stored in the state. Instead, we use a function GetBit(w↪ j) that computes the j-th bit of a rational weight w = p◁q in polynomial time (see Lemma 15 in Appendix).

At step t, MN↪Fix b↪f reads the t-th bits of input x and output y. It updates the carry state from c to c↓ by using the t-th bit of each weight, which can be computed in polynomial time (for detailed information on the calculation of carry values consider [Wolper and Boigelot, 2000]). Regarding the activation pattern, if wi = 1 then it checks whether yi is the correct sum bit or yi = 0, when wi = 0, meaning that the corresponding ReLU is inactive.

For t = k, a state is accepting when the corresponding sign bit of every neuron's internal sum is consistent with the activation pattern. Additionally, the automaton verifies consistency. For ReLU, if the accumulated carry indicates that the result should have been negative, but wj = 1, or positive but wj = 0, this may imply overflow or incorrect guessing. Specifically, if the carry into the sign bit differs from the carry out, an overflow occurred. The NFA checks that, if overflow to a positive value occurred, the output y represents the maximum representable value, and similarly for a negative overflow. Moreover, it is verified that the accumulated tail r justifies the initial guess cinit. For the rounding mode round-tonearest, it checks whether r ⇒ 0▷5 ∈∋ cinit = 1.

Next, we will consider the case of floating-point arithmetic. The crucial difference here is that while addition and multiplication in fixed-point arithmetic are local operations, meaning that the computation of the i-th bit depends only on the i-th bit of the operands and a carry from position i ↔ 1, in floating-point arithmetic addition and multiplication involve an alignment step. When two numbers x1 = m1 · 2e1 and x2 = m2 · 2e2 have different exponents, the mantissa of the smaller number must be right-shifted by φ = ♣e1↔e2♣. Therefore, a finite automaton reading the numbers bitwise would need to buffer O(φ) bits to align the operands. As k is given in binary, this would lead to a description of the resulting NFA of exponential size. It remains open whether there is another way to obtain a PSPACE upper bound for the general floatingpoint arithmetic or whether the lower bound of [Henzinger et al., 2021] can be lifted. However, to obtain a PSPACE upper bound when using floating-point arithmetic, we can restrict to formats where the exponent width e is fixed, while the precision of the mantissa is variable. This is reasonable for hardware designs where dynamic range is static but precision varies (for example bf16 vs. fp32).

We encode floating-point numbers with bounded exponent width E and mantissa width k as a word se0 · · · eE↑1m1 · · ·mk → ¶0↪ 1♦E+k+1 encoding the number

Lemma 12. There exists a succinct NFA MN↪Float k↪E with description size in poly(♣N♣ + log(k)) accepting RN↪Float k↪E.

Proof. A state qt in MN↪Float k↪E is a tuple (t↪E↪S↪ c↪ r↪ cinit↪w), where (t↪ c↪ r↪ cinit↪w) is as in the fixed-point case. Additionally, E → ¶0↪ · · · ↪ 2E ↔1♦♣ϖ♣ stores the exponent values for every neuron and S → (¶0↪ 1♦E )♣ϖ♣ stores the last E mantissa bits of every neuron's activation value. Since E is fixed, E and S only take polynomial space, and each state needs space O(log k + ♣N♣), which is polynomial in the input size.

The construction relies on E being constant in three ways. Alignment: since all exponents lie in ¶0↪ ▷ ▷ ▷ ↪ 2E ↔ 1♦, the maximum alignment shift is 2E ↔ 1, a constant; the mantissa bits that fall into this window are exactly those stored in Sj, so aligned operands can be recovered from the state alone. Normalisation: after addition or multiplication of normalised values the leading bit shifts by a constant amount bounded by E, so normalisation is a constant-size state update. Rounding: the sub-LSB contributions are tracked by r as in the fixedpoint case; the rounding decision depends only on r and the LSB, so the fixed-point rounding argument carries over directly. The t-th bit of every rational weight can be extracted in polynomial time (see Lemma 16 in Appendix), so TRANS and FINAL both run in polynomial time.

Lemma 13. Let ω a BV formula over variables x1↪ ▷ ▷ ▷ ↪ xk and bit-width b (given in binary). There exists a succinct NFA Mϑ with description size in poly(♣ω♣ + log(b)), such that Mϑ accepts the set of models of ω.

Proof. Assume ω to be in negation normal form, i.e. it consists of disjunction and conjunctions of atomic formulas of the form (t1 = t2) or ≻(t1 = t2). As succinct NFA are closed under union and intersection, it is sufficient to construct succinct NFA for each atomic subformula.

Let ↼ be such a term. A state is a tuple q = (j↪ feq), where j → ¶0↪ ▷ ▷ ▷ ↪ b♦ is a bit-counter and feq → ¶0↪ 1♦ is a flag tracking whether the evaluated terms equal up to position j. The description size is in O(b), which is polynomial. The start state is (0↪ 1). Let ε → ¶0↪ 1♦♣V ♣ be the input symbol representing the j-th bit-slice of the variables. We define a recursive evaluation function Eval(t↪ j↪ ε) for a term t: If t = x → V then Eval(x↪ j↪ ε) = ε(x), if t = c then Eval(c↪ j↪ ε) = cj (the j-th bit of c), if t = (ta ↖ tb) for ↖ → ¶&↪ ♣↪△♦ then Eval(t↪ j↪ ε) = Eval(ta↪ j↪ ε) ↖ Eval(tb↪ j↪ ε) and if t = ⇐ta then Eval(t↪ j↪ ε) = 1 ↔ Eval(ta↪ j↪ ε).

Since the depth of the term tree is bounded by ♣↼♣, Eval runs in polynomial time.

Algorithm TRANS((j↪ feq)↪ ε↪ (j ↓ ↪ f ↓eq )) returns true iff j ↓ = j + 1 and f ↓eq = 1 if feq = 1 and Eval(t1↪ j↪ ε) = Eval(t2↪ j↪ ε) or f ↓eq = 0 otherwise. This transition logic ensures that feq starts at 1 and acts as a "sink": once a mismatch is detected at position j, feq becomes and remains 0 for all subsequent steps.

Algorithm FINAL((j↪ feq)) returns true iff j = b and the flag matches the formula type: if ↼ is (t1 = t2) then accept iff feq = 1 (all bits matched). If ↼ is ≻(t1 = t2) then accept iff feq = 0 (at least one bit mismatch occurred).

We are now ready to prove Theorem 9.

Proof (of Thm. 9). We aim to check whether there is an x such that (x↪N♣F) ♣= ω1 ⇑ ω2. This corresponds to the non-emptiness of the intersection of the FNN automaton and the specification automaton for L(M) = L(MN↪F) ▽ L(Mϑ1↔ϑ2 ). Succinct NFA are closed under intersection.

We can therefore construct the succinct product NFA and check for emptiness using the PSPACE algorithm from Proposition 10. PSPACE-hardness follows from Theorem 8.

For general floating-point arithmetic, we can derive an upper bound from Theorem 7.

Proposition 14. REACH(F↪ BV) is in NEXPTIME for general floating-point arithmetic.

Proof. This is a direct consequence of Theorem 7. Due to the binary encoding of the bit-width b we can guess a witness of exponential length. Analogously to Theorem 7, we can check the witness in polynomial time.

These results complement the recently established results from [Henzinger et al., 2021] with upper bounds.

6 Outlook

We established the complexity landscape of verifying quantised FNN (see Table 1 for an overview), showing that the complexity in most cases matches the complexity of verification in full rational arithmetic. Current NN verification tools operate under idealised real-valued assumptions, while actual implementations use finite-width arithmetic. As shown in [Jia and Rinard, 2021], this mismatch can invalidate formal guarantees. Our results show that, for the standard case of linear specifications, verification of quantised networks remains NP. Hence, developing sound verification tools for quantised FNNs is not only necessary for correctness, but feasible without any asymptotic overhead compared to existing real-valued solvers. Moreover, we complemented the previous PSPACE lower bound for verifying dynamically quantised FNN with bit-vector specifications by giving matching upper bounds in the cases of fixed-point and floating-point arithmetic with bounded exponent width. We identified that in case of general floating-point arithmetic it seems like the problem could be even harder than PSPACE, due to the fact that the buffer size needed for alignment prevents the PSPACE upper bound. It remains open whether this need for alignment can be exploited to show a matching NEXPTIME lower bound for this case. Additionally, investigating the practical implementation of our succinct automata approach could offer a promising direction for creating solvers that accurately verify networks in quantised settings.