No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks
Authors: Attila Szász
Balázs Bánhelyi
Márk Jelasity
Venue: ICML 2025 spotlightposter (2025)
Keywords: sound verification
floating point computation
interval analysis
Primary area: deep_learning->robustness
TL;DR: Sound verifiers that correctly bound the full-precision model while computing in floating point fail to bound deployed neural networks, that is, they are not practically sound, and this vulnerability can be exploited in practice.

Abstract: The ultimate goal of verification is to guarantee the safety of deployed neural networks. Here, we claim that all the state-of-the-art verifiers we are aware of fail to reach this goal. Our key insight is that theoretical soundness (bounding the full-precision output while computing with floating point) does not imply practical soundness (bounding the floating point output in a potentially stochastic environment). We prove this observation for the approaches that are currently used to achieve provable theoretical soundness, such as interval analysis and its variants. We also argue that achieving practical soundness is significantly harder computationally. We support our claims empirically as well by evaluating several well-known verification methods. To mislead the verifiers, we create adversarial networks that detect and exploit features of the deployment environment, such as the order and precision of floating point operations. We demonstrate that all the tested verifiers are vulnerable to our new deployment-specific attacks, which proves that they are not practically sound.

No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks
Attila Szász'
Balázs Bánhelyi Márk Jelasity 12
Abstract
network, that is, they seek to characterize the behavior of the full- full-precision computation. Most solutions carefully address floating point issues as well, but only as an obstacle in the way of verifying the theoretical model, c.g. (Singh et al., 2019a; 2018).
The ultimate goal of verification is to guarantee the safety of deployed neural networks. Here, we claim that all the state-of-the-art verifiers we are aware of fail to reach this goal. Our key in- sight is that theoretical soundness (bounding the full-precision output while computing with float- ing point) does not imply practical soundness (bounding the floating point output in a poten- tially stochastic environment). We prove this ob- servation for the approaches that are currently used to achieve provable theoretical soundness, such as interval analysis and its variants. We also argue that achieving practical soundness is sig- nificantly harder computationally. We support our claims empirically as well by evaluating sev- eral well-known verification methods. To mis- lead the verifiers, we create adversarial networks that detect and exploit features of the deployment environment, such as the order and precision of floating point operations. We demonstrate that all the tested verifiers are vulnerable to our new deployment-speciffe attacks, which proves that they are not practically sound.
At the same time, deployment environments affect numeric computation through hardware and software features, of- ten resulting in stochastic behavior (Schlög) et al., 2023; Villa et al., 2009; Shanmugavelu et al., 2024), This means that the verification of the theoretical model and the ver- ification of the deployed network are different problems. Parallel to our work, similar observation was also made by (Cordeiro et al., 2025), where this problem is referred to as the implementation gap.
We formally prove that a verifier that is theoretically sound (i.c., bounds the full-precision output correctly) is not nec- essarily practically sound, that is, might not bound the actual output correctly in a given deployment environment.
The problem has practical implications. Recently, (Shanmu- gavelu et al., 2025) demonstrated that adversarial inputs can be generated simply by permuting the order of associative operations in the deployment environment.
We demonstrate a more severe, practically exploitable vul- nerability as well: the deployed network is shown to be fundamentally different from the theoretical network be- cause the behavior of the network can be changed arbitrarily with deployment-senen sensiiiieee backdoors.
1. Introduction
The formal verification of an artificial neural network pro- duces a mathematical proof that the network has (or does not have) a certain important property. One important prop- erty to verify the adversarial robustness (Szegedy al., 2014) of classifier networks, where wish to prove that subset of inputs are all assigned the same class label.
Thus, the deployment environment should be a fundamental part of any verification effort because otherwise an attacker can hide potentially harmful behaviors from the verifier enough information about the deployment environment is available.
There is a wide variety of approaches that address this prob- lem (see Section 2). However, these methods invariably focus on the verification of the theoretical model of the
We summarize our contributions below:
'University of Szeged, Szeged, Hungary "HUN--EN-SS Research Group on Artificial Intelligence, Szeged, Hungary. Cor- respondence to: Attila Szász <szasz@ wnw..u-zng..eeeee... szt.us-zzgd.......
We prove that verifiers that theoretically sound not necessarily sound for deployed networks
We demonstrate that deployed networks may differ arbitrarily from the full-precision model, with the help of backdoors triggered by features of the environment
Proceedings of the ndnd International Conference Machine Learning, Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).

---

No Soundness in the Real World
We complement our theoretical analysis by empir- ical evaluation, showing that the state-of-the-ar veri- fiers that are theoretically sound indeed fail to correctly bound the deployments of our backdoored networks'
Theoretical Model
2. Related work
E,
Verification methods can be classified in various ways (Li et al., 2023; Albarghouthi, 2021; Huang et al., 2020; Liu et al., 2021), but from a safety perspective, the most im- portant classification categorizes algorithms based on their completeness and soundness. A verification algorithm is sound if every property it predicts to be true is true, and complete if it predicts every true property to be true. (Differ- ent terminology has also been used in the literature (Bunel et al., 2020)).
Figure I. A malicious binary classificr with decision boundary and two classes in two colors (conceptual illustration). The theo- retical network and its three different deployments are illustrated, including a deployment in an adversarial environment (Ex) where malicious behavior (flipping classes) manifests itself. An input x and its sensitivity domain are also shown.
Most proposed methods assume a special class of neural networks, typically ReLU networks. Sound (but not nec- essarily complete) methods, such as (Singh et al., 2018; 2019a; Zhang et al., 2018; Xu et al., 2021), are often based on bound propagation (Xu et al., 2020) and linearization. These methods deal with floating point computations as well and bound the full-precision value correctly.
The work of (Zombori et al., 2021) also addresses numeric vulnerabilities in verification, but they exploit the numerical issues of the verification algorithm itself (specifically, the MILP solver). These kinds of exploitable issues are not present in sound verifiers based on bound propagation. In- stead, here, we focus on exploiting the discrepancy between full-precision models and their deployment that provably mislead every sound verifier we are aware of.
Methods claimed to be both sound and complete often for- malize the verification problem satisfiability modulo theories (SMT) problem (Katz et al., 2017; Ehlers, 2017) or a mixed-integer integer linear programming (MILP) model (Dutta et al., 2018; Tjeng et al., 2017) and use SMT or MILP solvers to solve them.
The main disadvantages of these methods include being NP- complete (Katz et al., 2017), and relying on sophisticated solvers that might include heuristics that break soundness (Zombori et al., 2021). To mitigate the scaling issue, some methods (Tjeng et al.. 2017; Singh et al., 2019b) incorporate sound (but not complete) approaches in a preprocessing phase to make the SMT or MILP models more manageable by reducing the number of integer variables.
(Jia Rinard, 2021) also address related issues. Their work can be considered an adversarial attack on verification and not generic and provable framework propose. It works only if the deployment and the verification algorithms use a different numerical precision, unlike our constructions.
While we focus on the problems stemming from floating point arithmetic, fixed-point arithmetic should be mentioned as an interesting alternative path where quantization can be implemented with bounded rounding error (Lohar et al., 2023), allowing for practically sound verification.
In addition, a branch-and-bound (BaB) verification frame- work was also proposed for sound and complete verification (Bunel et al., 2020). The basic idea is to recursively divide the verification problem into simpler subproblems, where inexpensive sound methods can prove robustness. Verifiers based on this framework mainly differ in how they solve the subproblems and how they perform the branching process. The main advantage of the BaB framework is that the verifi- cation process can be performed partially (Xu et al., 2021) or fully (Wang et al., 2021; Palma et al., 2021; Ferrari et al., 2022) on a GPU, significantly increasing the efficiency of the verification.
3. An Intuitive Overview
Here, we discuss the main intuition behind our work in an informal manner, as well as some of the misunderstandings we often encounter.
Main idea. Neural networks are functions that have real valued parameters. This real valued version is the theoret- ical model. A deployed neural network model, however, is almost always computed using floating point arithmetic, furthermore, deployments are inherently stochastic due to the non-associa nature of floating point arithmetic and
Source code: wttpt::p///ti... https://githhp cww/szassa 1/no_ soundness
2

---

No Soundness in the Real World
parallelization. Our main message is while current verification efforts always target the theoretical model-we we should target the deployed model. The main reason is that a deployed model is fundamentally different mathemati- cal object and this difference allows an attacker to design deployment-senae senniissniiivee behaviors that remain hidden when verifying the theoretical model of the same network without taking the deployment environment into account.
without loss of generality.
4.2. Verification Problem
The robustmess verification problem seeks to decide whether every input in some small neighborhood of a fixed input x* has the same class label as x². More formally, we are given input domain D S I=" that defines the small environ- ment. D is usually defined by norm and parameter e: Dr (x=) ) = {x || x 1| S e).
What this work is not. Our work is not about the float- ing point issues related to the verification of the theoretical model of the neural network. For example, doing the verifi- cation in full precision arithmetic does not solve the problem we raise here because that way, one verifies the theoretical model and not the deployed network, except if full precision used in deployment as well. Also, floating point arith- metic is a problem here not because of rounding errors, but because of its non-associativity and the stochastic nature of the computation depending on the deployment environment.
We wish to prove that over this domain, every input satis- fies a safety property P. In our case, P S R captures the fact that the input has the same label x². Let us as- sume the class label of x is y(x"). Then, P(x*) = {x (z; y) max; (x; 0):}. The goal of verification is to prove that the property P holds over the input domain, that is, (=p( C P(x*).
To make our equations simpler, but without loss of general- ity, we extend the neural network with an additional affine layer that computes output vector of dimension m by computing fa; 0) y)(()) fx;; for every index i. This assumption simplifies the formulation of the verification problem, which now amounts to proving
An illustration. Figure is a conceptual illustration of a binary classifier that was manipulated by an attacker in order to produce malicious behavior in a specific deployment environment that we call adversarial environment, In this illustration, the theoretical model of the network does not show malicious behavior and it is safe for input x: as well, that is. the sensitivity domain of x is inside the class of x. In non-adversarial deployments (environments & and E2) the deployed model shows variations relative to the theoretical model and it might or might not be safe for r. However, in the adversarial deployment environment Ea, the model is unsafe for most inputs by design, as the class predictions are flipped. Note that this behavior is not triggered by specific inputs, instead, it is triggered by the deployment environment. We discuss such malicious networks in Section 7.
Vo (x",)) f(x; 20
(1)
where, with a slight abuse of notation, we used the same f to denote the modified network. From now on, f will denote this modified function.
4.3. Classification of Verifiers
A verifier is an algorithm to prove the property in Equa- tion (1) for a given x². The potential outputs a verifier include true, false and unknown. The verifier is called com- plete if for every x², for which Equation (1) is true, it returns true. The verifier is called sound if for every x", for which it returns true, Equation (1) is true.
4. Background and Notations
Here, we introduce the basic notations our study focuses on: the neural network and the verification problem. We also discuss some basic properties of floating point computation briefly.
Sound verifiers have been proposed for special classes of neural networks (see Section 2). However, they are sound only in the sense of bounding [(: ()) (the full-precision
model) from below, which-as as we argue in this paper-is not the right target for verification.
4.1. Theoretical Model of Neural Networks
Our formulation is inspired by (Ferrari et al., 2022). Let the theoretical neural network be the function f-: : R + RTM where R is a vector of constant real parameters. Throughout the paper, we work with classifier networks, that is, the network ((; classifies each input x R to one of m classes. The class label of is given by y(x)= = arg max; J (x;; 0);, that is, the index of the maximal output value. Note that in many applications the input is often restricted to a subset of IR.. Here, we allow every input,
4.4. Floating-Point Issues
A doating-point number is represented as s -b. where s the signed significand, b is the base (usually, 6 = 2), and e is the exponent. Available floating -pont implementations mainly differ in the number of bits used to represent the significand and the exponent. The IEEE 754-1985 stan- dard introduced the well-known double and single precision formats. In double- prrbccspreeiiion (or binary64) representation, the exponent and the significand are represented by 11 and
3

---

No Soundness in the Real World
52 bits, respectively. In single-precision (or binary32), the exponent is represented by 8 bits, and the significand by 23 bits. In both cases, 1 bit is used to store the sign.
vations about the relationship of f(;;0) and (1;0,))
Domain and range. The domain X is restricted, more precisely, X C IR, where X is defined by the representable numbers in I" within E. The range Y behaves similarly (assuming & is deterministic), that is, Y C TR"" where Y is defined by the representable numbers in R" within E.
Since floating-poin arithmetic has finite precision, rounding is applied to determine the floating-poit result of mathe- matical expressions, making the arithmetic order-dependent (or nonsassociative) For the same expression, different rounding modes and operation orders can introduce numer- ical errors of varying magnitudes. Next, we demonstrate the two most significant issues that arise with floating-point arithmetic through examples.
Range in stochastic environments. The environment can be stochastic, depending on a number of factors such as randomly changing operation order, or even unpredictable rounding due to using several different platforms in parallel. In this case, we do not model the distribution of the output. Instead, we define the range to be the representable subsets of Rm and the value of r(a; 0, is the subset containing the vectors with probability larger than zero. In other words, Y C 2 ddefined by the representable numbers in 2 within E.
Non-associative operations. Different orders of operations in a summation can lead to different results. For example 253 + 1 253 0 when computed in double-precision arithmetic and with rounding towards -0 (in this fixed order). However, if we change the order to 253 - -253 + 1, the result will be in the same environment.
Even for representable input z E X, and a deterministic E, we have r(x; 0) + f(x; 0) in gen- cral. First of all, I might not be representable exactly. Even if is representable, due to floating point issues, the output of the deployed network will typically be different, except in rare cases when all the sub-computations are exactly rep- resentable. In Section 7 we argue that these differences can be arbitrary.
Different Output.
Precision. Different floating-point representations (such as double and single precision) have a different number of bits to represent the significand. Thus, for example, the result of 224 +1 1-2 is 0 under single precision, but I under double precision.
5. Deployed Verification
The effect of different deployment environments have al- ready been investigated in (Schlögl et al., 2023), although not from the point of view of verification. was shown that different platforms-thal differ in number representa- tion, parallelization, hardware, and optimizations during convolution-signiicanl impact the output of deployed neural networks.
5.2. Verification of Deployed Networks
Given an input x²' E X, the verification problem is now to prove that
Vx E D Dep.e(x") E (r(:0,0)) = 0,
(2)
Here, we define the deployed verification problem and show that it differs significantly from the theoretical problem in Equation (I).
where Dp.c.c is defined below. The problem is formulated assuming a stochastic environment, but note that the de- terministic environment is a special case of the stochastic one. Apart from this, and the differences between f and r discussed above, there are other significant differences from Equation (1) regarding De.p,(('') and the underlying property Pa P=(x").
5.1. Deployed Neural Networks
For a theoretical model f(; and a deployment environ- ment E, let r(.:0,)) 8) X Y be the deployed network. The notation & fully captures every property of the envi- ronment, including every detail of number representation, hardware, software optimizations, operation order, and po- tentially the stochasticity of the environment.
Verified domain. For an x² E X, the verification problem will have domain Dp...E = fx E X || x² < cJ. Now, it is unclear whether Dp.c,E = Dp.c n X because the rounding issues affecting Dp...E might depend on the verification algorithm as well, but for simplicity we will use Dp... Dp, N. as a definition of Dp....
The idea is that r(=;6,)) E) implements fl:(0) in E. This means that r(:00,) E) computes the same function as [(: 0), and the (thcoretically) associative operations are executed in some (potentially random) order defined by ε, and the number representation and rounding details are also defined by& E
Verified property. The properties P and Pe signifi- cantly differ because we have Pe(x*) = {ar E X r(2;0, E) = max; r(x; 0, 8))).. Thus, in general, Pe Ø P because some negative outputs of f might be- come zero for r due to rounding. So, here, we do not have Pg = Pn X. (Also, obviously, P c Pc.)
Let us now elaborate on r(.; (,)) and discuss a few obser-
4

---

No Soundness in the Real World
6. No Soundness in Deployment
minimum and maximum elements of r(;; E), respectively.
Clearly, practically complete (but not sound) solutions are known: every solution based on a heuristic search for adver- sarial examples in the given domain is a complete method for the deployed problem, e.g., (Kurakin et al., 2017; Madry et al., 2018), although only if the search uses the deployed implementation of the network. We only need the method to return true if no adversarial input is found: if there are no adversarial inputs, none will be found, making the method complete.
The proofs of the propositions are given in Appendix A.
6.2. Interval Bound Propagation
When using interval arithmetic on a given expression tree, each binary addition will have two intervals as inputs and will output an interval that also considers the numerical error due to rounding: if the lower or upper bound is not representable, it is rounded towards co or no, respectively.
Our first proposition will state a nice soundness property of IBP in two particular cases: (1) when we wish to bound the full-precision value, and (2) when we wish to bound the floating point value and we also know a specific expression tree that minimizes or maximizes this value.
Thus, we focus on soundness. Here, we examine theoreti- cally sound methods from the literature (see Table 3 for list) and investigate whether they are practically sound, that is, whether they are sound regarding the deployed verifica- tion problem in Equation (2). We will show that in general the answer is no. In particular, we are not aware of any method that sound in stochastic environments, despite explicit claims (Singh al., 2025).
Proposition 6.1. Let |a, b].- [(x, xI) (x E X) be the interval evaluation of f using expression tree o and the floating point representation defined by E. Then, (1) f(x) e [a, bl (2) if r(x; E, minimizes or maximizes r(x; E) then S L,p or U, S b, respectively.
In the following, we first discuss preliminary assumptions and then we address techniques applied in the literature to achieve soundness, indicated in Table 3: interval bound propagation (IBP) (Gowal et al., 2018) that is based on inter- val arithmetic (Alefeld & Herzberger, 1983), and more ad- vanced propagation methods based on symbolic approaches such affine arithmetic (de Figueiredo & Stolfi, 2004).
In the special case of deterministic environment, this means that if we know the deterministic expression tree and compute IBP accordingly, then IBP will be sound, since this expression tree will both minimize and maximize the floating point output. Unfortunately, we do not know the deterministic order, or if the environment is stochastic, then there is no guarantee that IBP will be practically sound, as formulated by the next proposition.
6.1. Preliminaries
In our theoretical discussion, we shall focus on a very simple class of functions: the sum of the input variables. The input variables will be zero-length intervals, that is, constants that are representable in the deployment environment. Since the problems we identify can be demonstrated already in this simple function class with constant inputs, generalizations of this class, such as neural network architectures, will inherit these problems.
Proposition 6.2. For any environment & that allows for every correct expression tree and uses IEEE 754 floating point representation with any fixed rounding mode, there is an expression tree o, and input x E X, such that for the interval evaluation [a, bl. = [[2, æ)) in environment & we have L, a or U,.
Recall, that in practice, deployment environments are often inherently stochastic (Schlögl et al., 2023). Proposition 6.2 means that in stochastic environments we must find an ex- pression tree that guarantees practical soundness, because not all of them do in general. This task depends on the environment but, for example, the expression tree that mini- mizes the output of r(:: E) is a suitable choice for bounding the output from below in any environment according to Proposition 6.1.
The sum computation is associative, furthermore, it can be parenthesized arbitrarily, leading to a large variety of possible binary expression trees. Here, we will assume that the environment& & defines two aspects: the floating point representation (along with the rounding mode) and the set of expression trees with non-zero probability. Thus, here, an expression tree defines a deterministic hierarchy of binary sum operations, all of which are computed using the same precision and rounding mode, leading to a deterministic output for any input given in the leaves.
6.3. Notes Computational Complexity
Since the sum function does not use any parameters, we will omit f from our notation. Thus, here, f(x) = Σ, x4 and r(x; E) is the deployed version of the sum using the number representation and expression tree set defined by E.
Practically sound verification with IBP, thus, requires find- ing special expression trees. One might think that some orderings-such such as adding numbers in a decreasing order, or maybe in a decreasing order according to absolute value- might minimize r(.; E)) and thus might be suitable to make IBP sound. This is not the case.
Let us introduce the notation r(æ; E) {r(x; o,).): : or is possible expression tree in ) and let L, and U, be the
5

---

No Soundness in the Real World
Proposition 6.3. For any environment & that allows for every correct expression tree and uses IEEE 754 floating point representation with any fixed rounding mode, there is an input z E X. such that we have Lr < rr E, o) for o E (decreasing-ordle decreasing- absooout----aall-orderr
Proposition 6.4. Proposition 6.1 holds also when com- puting the interval using the widening technique in (Miné, 2004) used by (Singh et al., 2019b).
Proposition 6.5. Proposition 6.2 holds also when com- puting the interval using the widening technique in (Miné, 2004) used by (Singh et al., 2019b).
Note that good approximation algorithms might exist for the minimum and maximum output, but in verification mindset, we wish to eliminate any mistakes completely, otherwise the system remains vulnerable to attacks.
7. Practical Attacks on Verifiers
Here, based on our the theoretical results, we design neural networks with the purpose of fooling state-of-the-ar sound verifiers practical deployment. The basic idea is that we design small detector neurons that are triggered by certain properties of an environment-such as precision the order of computation in order to activate arbitrary adversarial behavior.
We hypothesize that finding the expression tree that max- imizes or minimizes the output an NP-hard problem in general. It was shown in (Kao & Wang, 2000) that a very similar problem, namely finding the order that minimizes the worst-case error is NP-hard in the general case when both positive and negative numbers are added.
Adversarial networks. These detector neurons can be in- serted into any neural network using the method proposed in (Zombori et al., 2021). This way, they can enable back- doors that can alter the behavior of the network arbitrarily, triggered by a specific property of the environment. In Ap- pendix B we discuss the technical details of creating the complete backdoored networks. Here, we detail our detector neurons.
6.4. Symbolic Bound Propagation
Due to the so called dependency problem, naive interval arithmetic might greatly overestimate the output interval of multivariate functions of a large complexity. Symbolic approaches mitigate this problem via propagating symbolic representations instead of values. We briefly summarize two important approaches here, for more details and proofs please refer Appendix A.I.
The detector neuron. The generic scheme of a detector neuron is the following. We use a linear neuron with n inputs without an activation function. We assume that the neuron gets the constant input vector of all ones (1,---? 1). This way, the output of the neuron is W1 + wn + 6. that is, we sum the edge weights and the bias. We will call this order of summands without parenthesis the default expression tree, often implemented in environments using a single-threaded CPU.
Our main observation is that, in our special case of comput- ing the sum of zero-length intervals, these symbolic methods simplify to non-symbolic interval methods.
Poly Polyhedra-based approaches. In this special case, polyhedra- based approaches like DeepPoly (Singh et al., 2019a) and CROWN (Zhang al., 2018; Xu et al., 2021; Wang et al., 2021) first find the symbolic expression for the sum of the input variables. During sound verification, however, the implementations evaluate this formula using interval arithmetic, based on some binary expression tree defined by the verifier. Thus, the method is equivalent to IBP discussed in Section 6.2. In other words, this method is not practically sound either in the general case.
Note that assuming a constant input for the detector neurons is not essential because, on the one hand, our constructions can easily be generalized to random input point from a bounded interval, and on the other hand, even a constant input can be fabricated when embedding the neuron into the host network (see Appendix B).
Zonotope-based approaches. DeepZ. (Singh et al., 2018) and RefineZono (Singh et al., 2019b) are based on the zono- tope abstraction, using affine arithmetics (de Figuciredo & Stolfi, 2004) to propagate bounds throughout the network, computing the so-called zonotope domain (Ghorbal et al., 2009). This case, too, simplifies to interval analysis in our special case, only the intervals will be strictly wider than those computed by IBP due to the application of technique proposed in (Miné, 2004).
Preliminaries. We assume that the deployment environ- ment uses IEEE 754 floating point representation with the default round-to-nearee to-nearest rounding. We will use special number w, which is defined as the smallest representable positive number such that the next representable number after w is w + 2. For example, for the binary32 format w = 224 and for the binary64 format w = 253 Using the default rounding mode, w + w.
Since this latter case is not equivalent to IBP, we explicitly state propositions describing the zonotope domain, indicat- ing that the verification is not practically sound in general, very similarly to IBP.
7.1. Detecting Precision
We define the detector neuron as W + w. Assuming the default expression tree (summing left to right) this detector
6

---

No Soundness in the Real World
neuron will output O if the precision of the deployment is the same the precision represented by w, and it will return I in higher precision deployments.
Assuming the default expression tree the value of this sum is 2 in deployment, thus, any non-zero value will trigger the normal behavior, and the value of zero triggers adversarial behavior.
For a verifier that uses given precision during verification, we will integrate this detector neuron into the adversarial network in such way that the adversarial behavior will be triggered by a precision different from the one used by the verifier. This way, we can test whether the verifier is able to cover every precision that is possible in deployment.
It is a harder expression for verifiers, because now, a veri- fication using interval arithmetic on the default expression tree will no longer be sound: it will not contain the output O, which is a possible output. Indeed, if we sum the edge weights in an order where w is in a position earlier than position h/2 and we add the bias -w in the end, the result is O. But, in this case, there is a large number of orders that do result in covering 0 (and thus a practically sound behavior). In fact, the only order of the edge weights that does not result in covering is the default order.
7.2. Detecting Expression Trees
For detecting expression trees, we define three different detector neurons. The idea behind these definitions is that the three detectors represent an increasingly challenging problem for verifiers.
For verification, the hardest problem we will test is the sum
In each case, these detectors will be integrated into adver- sarial networks so that using the default expression tree activates the normal behavior of the network. To be more precise, if evaluating the detector in the default order re- sults in zero then the adversarial behavior is triggered by any non-zero output of the detector, and if the default order results in non-zero output then the output of zero triggers the adversarial behavior.
1 tw w.
hx
which has much fewer possible orderings of the edge weights that result in covering the output 0 using interval arithmetic. In fact, we cover zero only if w is first second in the order of summation (assuming the bias is added last). This means that verifiers that are not guaranteed to cover all possible orders will almost certainly fail to detect the adversarial behavior.
7.2.1. A VERIFIER-FRIENDE DETECTOR
The detector neuron returns the following sum of (2h1 + 1 h2/2 summands:
As for the parameter h, we set 512 for both unfriendly detectors.
w
w
h1
8. Empirical Evaluation
bix
To demonstrate the practical relevance of our observations, we evaluated state-of-the-ar verifiers using our adversarial networks test whether they indeed cover all possible exe- cutions in a number of different deployment environments. As predicted, the answer we found is no.
hgg x
where the bias weight is zero and thus omitted.
Assuming the default expression tree the value of this sum is 0 in deployment, thus, the value 0 will trigger normal behavior.
8.1. Adversarial Networks
For verifiers, dealing with this sum is relatively easy, be- cause even simple interval arithmetic will be sound, cov- cring every possible order, if the analysis is executed ac- cording to the default expression tree. At the same time, this trigger will be activated often, because there a large number of possible orderings that return a value from h2)- Note that the full-precision value is hg. In our experiments we will use h = 4 and h2 = 15.
In our evaluation, we used MNIST network checkpoint made available by (Wong & Kolter, 2018). This checkpoint was used to evaluate MIPVerify (Tjeng et al., 2017) as well as the attacks proposed by (Zombori et al., 2021). This network has two convolutional layers with stride 2: one with 16 and one with 32 filters of size 4x4, followed by a 100 neuron fully connected layer. ReLU activations are used by all the neurons. The network was trained to be robust against attacks within radius of 0.1 in the -orm (Wong & Kolter, 2018).
7.2.2. VERIFIER UNFRIENDLY DETECTORS
Our first unfriendly detector returns the sum of h + sum- mands
We augmented this network with our detectors presented in Section using the methodology proposed in (Zombori et al., 2021), as detailed in Appendix B. We created five adversarial networks: two precision-bant based attacks (one with
2
2 h
+
tw
(4)
hx
7

---

No Soundness in the Real World
Appendix C.I.
Table 1. Test accuracy of backdoored networks.
Results. Table 2 contains the accuracy results over different environments. Three of our backdoors are activated in at least one environment, which gives further support that these environments execute different expression trees, including those that we used as backdoors. The Order3 adversarial network is an exception because as we explained before- it has very few expression trees that trigger its adversarial behavior. Nevertheless, this does not make the Order3 net- work safe, and this fact should still be detected by sound verifiers.
Attack
Precision of the environment
bit
64-bit
Precision, 32-bit adversarial
0.11%
98.11%
Precision, 64-bil adversarial
98.11%
0.11%
Table 2. Test accuracy of backdoored networks, evaluated with different batch size and environment settings.
Attack
Batch
PyTorch
Flux
Size
CPU
GPU
CPU
GPU
Orderl
0.11% %
0.11%
98.11%
0.11 %
Order2
1
18%
98.11%
98.11%
0.11%
8.3. Pool of Verifiers
Order3
1
98.11%
98.11%
98.11%
98.11%
Orderl
10
0.11 %
98.11%
0.11 %
98.11% %
Table 3 lists the verifiers that we tested. Here, we briefly describe them, for more detail, please refer to Appendix C.2.
Order2
10
98.11 11%
98.11%
98.11%
98.11%
Order3
10
98.11%
98.11%
98.11%
98.11%
MIPVerify, RefineZono, and RefinePoly are claimed to be sound and complete verifiers. They rely on a cheap sound bounding method that is then refined using -inteer linear programming (MILP) to achieve completeness.
adversarial behavior in 32-bit environments, and one in 64- bit environments) based on the detector in Section 7.1, and three expression tree based attacks described in Section 7.2 based on the detectors in Equations (3) to (5). We will refer to these three attacks as Order1, Order2, and Order3, respectively.
RefineZono and RefinePoly rely on DeepZ and DeepPoly as their sound bounding method, respectively. DeepZ and DeepPoly are both claimed to be sound under floating-point arithmetic.
8.2. Effectiveness of our Adversarial Networks
3-CROWN BaB built on the fast and sound (but incom- plete) bound propagation algorithm 3-CROWN and inte- grates it with branch-and-bount framework to ensure com- pleteness. The verification process can be configured to run on either CPU or GPU and supports numerical representa- tions in both 32-bit and 64-bit precision. GCP-Crown is also a BaB method similar to 3-CROWN, but it is capable of managing general cutting- plane constraints.
Here, we wish to demonstrate that the adversarial behavior of our networks is indeed activated in certain environments.
8.2. 1. PRECISION ATTACKS
In Table 1, the accuracy of the adversarial networks with precision attacks is presented. The first row corresponds to the configuration where the backdoor changes the prediction under bit precision, while the second row corresponds the 64-bit precision trigger. The columns correspond to 32-bit and 64-bit inference. It is clearly visible that our backdoors indeed trigger adversarial behavior as designed. Note that the adversarial behavior has larger than zero accuracy due to some of the test examples that are misclassified by the host model.
8.4. Attacking Verifiers
Here, we verify our adversarial networks with our pool of verifiers. Note that here, the verifiers do not consider the deployment environments explicitly, instead, the verifiers themselves have their own deployment environments, in which they executed indicated in Table 3 (see Ap- pendix C.2 for a detailed discussion).
8.2.2. EXPRESSION TREE ATTACKS
As for the deployment environments of our networks, we know from Section 8.2.2 that for all the adversarial networks there is least one environment where the adversarial be- havior is observed, except for Order3. Thus, it a rightfil expectation that the verifiers find the planted backdoor.
The environments. The effective expression tree in de- ployment depends on numerous factors, such as hardware specificationss memory size, underlying linear algebra li- braries, machine learning frameworks, optimizations, batch size during inference, and on (Schlögl et al., 2023). We defined 8 different environments that provide sufficient diversity to support our claims. The libraries we tested were Py PyTorch and Flux on Julia. As for hardware, we tested CPU and GPU, and we also tested different batch sizes during inference. For a more detailed description please refer to
In the case of Order3, we argue that we should also require the verifiers to find the backdoor, because in general it is very hard to explicitly model the set of possible expression trees in a given complex environment, so practically sound verifiers should be prepared for all of them.
8

---

No Soundness in the Real World
Table The vulnerability of the verifiers to our four attacks and to the attack of (Zombori al., 2021). The Precision attack is adversarial to the 32-bit environment, except for 32-bit B-CROWN, where it is adversarial to 64-bit.
Verifier
Ver. Env.
Bounding
Precision
Orderl
Order2
Order3
(Zombori et al., 2021)
MIPVerify (Tjeng et al., 2017)
64-bit, CPU
IBP
unsound
sound unsound
unsound
unsound
MN-BAB (Ferrari et al., 2022)
64-bit, GPU
Polyhedra
unsound
sound
unsound
unsound
unsound
B-CROWN BaB (Wang al., 2021)
32-bit, CPU
Polyhedra
unsound
sound
unsound
unsound
[no 32-bit model] sound
3-CROWN BaB (Wang et al., 2021)
64-bit, CPU
Polyhedra
unsound
sound
unsound
unsound
3-CROWN BaB (Wang et al., 2021)
64-bit, GPU
Polyhedra
unsound
sound
unsound
unsound
sound
OCP-CROWN (Zhang et al.. 2022)
64-bit, CPU
Polyhedra
unsound
sound
unsound
unsound
sound
DeepPoly (Singh et al., 2019a)
64-bit, CPU
Polyhedra
unsound
sound
sound
unsound
sound
RefinePoly (Singh et al., 2019a)
64-bit, CPU
Polyhedra
unsound
sound
sound
unsound
unsound sound
DeepZ (Singh et al., 2018)
64-bit, CPU
Zonotope
unsound
sound
sound
unsound
RefineZono (Singh et al., 2019b)
64-bit, CPU
Zonotope
unsound sound
sound
unsound
[Gurobi error]
Table 3 contains the results of the verification of the first 100 examples from the MNIST test set. The label sound in- dicates that the verifier was able to detect the backdoor each time, returning a 0% verified robust accuracy. Otherwise the result is labeled unsound.
9. Conclusions and Limitations
Our main conclusion that verifiers that are theoretically sound (cover the full-precision output despite floating point computations) are not necessarily practically sound, in that they might not cover every possible output when the net- work is used in a deployment environment. We are therefore proposing to focus on the behavior of deployed neural net- works as opposed to the full-precision behavior.
8.5. Discussion
No practically sound verifiers. The results in Table 3 reveal that none of the listed approaches are practically sound, given that they missed the backdoor in the most difficult Order3 network as well as in the Precision network.
As for limitations, our present work does not include any pro- posals for implementing practically sound verifiers. Here, we focused on exposing the problem, which in itself is of value, given that every verifier we aware of suffers from this. Nevertheless, solving the problem would be important.
Difficulty matters. It is also clear that as the task becomes more difficult, more and more verifiers fail. The Orderl net- work is solved by all the verifiers since bound propagation in the default operation order covers the adversarial output as well. The relatively easy Order2 network solved by some of the verifiers, which could be due to the wider intervals used during propagation, and potentially the operation order used by the verifier could deviate from the default, thereby accidentally covering the adversarial output. However, we know that these successful cases are due to lucky accidents, as we have proven theoretically that there is no guarantee for practical soundness for these methods.
We believe that practically sound verifiers will have to make strong assumptions about the deployment environment, oth- erwise the problem becomes prohibitively expensive. For example, deterministic environments are great advantage, but then verification must be aware of and exploit every detail. Bound propagation will be practically sound if it follows the deterministic expression tree, provided the prop- agation takes into account the (deterministic) precision and rounding rules of the environment.
Precision matters. All the verifiers are vulnerable to the precision attack, which provides further empirical support for our observation that verifiers should explicitly be tailored to specific floating point precision.
Acknowledgements
This work was supported by the European Union project RRF-2.3.1-21-2222--0 within the framework of the Artificial Intelligence National Laboratory and project TKP2021-NVA-09, implemented with the support provided by the Ministry of Culture and Innovation of Hungary from the National Research, Development and Innovation Fund, financed under the HMP2001-NVA funding scheme. We thank the support by the PIA Project, collaboration between the University of Szeged and Continental Au- tonomous Mobility Hungary Ltd. with the goal of sup- porting students' research in the field of deep learning and autonomous driving. We thank Andras Balogh for his ini- tial feedback and our anonymous reviewers for the relevant
(Zombori et al., 2021) propose a network similar to Order1 in that in the default order bound propagation covers the adversarial output. This network was designed to trigger numerical errors in the verifier, so only those ones are vul- nerable that use optimization in some form. Our attacks, on the other hand, exploit the difference between the behav- ior of the full-precision model and the deployed network, and the strongest ones (Precision and Order3) are effective against all the verifiers that are only theoretically (but not practically) sound.
9

---

No Soundness in the Real World
pointers and suggestions.
Ehlers, R. Formal verification of piece-wise linear feed- forward neural networks. In D' Douzz, D. and Kumar, K. N. (eds.), Automated Technology for Verification and Analysis 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings, volume
Impact Statement
This paper presents work with the goal of advancing the field of Machine Learning. There are many potential societal consequences of our work, none of which we feel must specifically highlighted here.
10482 of Lecture Notes in Computer Science, pp. 269-
286. Springer, 2017. doi: 10. 10.1007/978--3331-6611600
1-19. URL https: /tt///o.i..///// 1ttp:///...110/7789
319-68167-2
References
Ferrari, C., Müller, M. N., Jovanovic, N., and Vechev, M. T. Complete verification via multi-neuron relaxation guided branch-and-bound. In The Tenth International Confer- ence on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. URL https: ht////ppeeeiiiee http::ee////ruuree iididdi am Hfloak.
Albarghouthi, A. Introduction to neural network verification.
Foundations and Trends in Programming Languages.
(1-2):1-157, 2021. ISSN 2325- 1107. doi: 10.1561/2500
000051. URL http: / doi http:///.d..o..r1111.....1.. 500000051.
Alefeld, G. and Herzberger, J. Introduction to Interval Com- putation. Academic Press, 1983. ISBN 97801 20498208.
Ghorbal, K., Goubault, E., and Putot, S. The zonotope abstract domain taylorl+. In Bouajjani, A. and Maler, O. (eds.), Computer Aided Verification, pp. 627-633, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. ISBN 778-3-642-02658-4
Bunel, R., Lu, J., Turkaslan, I., Torr, H. S., Kohli, P., and Kumar, M. P. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21(42):1-39 2020. URL http::/ /ttp: //mt:://////.o rg/papers/ /veer///v211 111/19911-1 1...994468..... html.
Gowal, S., Dvijotham, K., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arandjelovic, R., Mann. T. A., and Kohli, P. On the effectiveness of interval bound propagation for training verifiably robust models. CoRR, abs/1810. 2018. URL http: www.xii...o./aa..eee aabs 1810. 127 15.
Cordeiro, L. C., Daggitt, M. L., Girard- Satabin, J., Isac, O., Johnson, T. T., Katz, G., Komendantskaya, E., Lemesle, A., Manino, E., Sinkarovs, A., and Wu, H. Neural network verification is a programming language chal- lenge. In Vafciadis, V. (ed.), Programming Languages and Systems 34th European Symposium on Program- ming, ESOP 2025, Held as Part of the International Joint Conferences Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part I, volume 15694 of Lecture Notes in Computer Science, pp. 206-235. Springer, 2025. doi: 10. 10.1007/978-33-31--11118--- URL //do:: 105//00.107/978--1
Huang, X., Kroening, D., Ruan, W., Sharp, J., Sun, Y., Thamo, E., Wu, M., and Yi, X. A survey of safety and trustworthiness of deep neural networks: Verifica- tion, testing, adversarial attack and defence, and inter- pretability. Comput. Sci. Rev. 37:100270 2020. doi: 10. 00.006J..OOSREV.200.... 100270. URL httph::t///// //do i i. wlorr/11.111000 cosrev. 2020 100270.
Jaa, and Rinard, M. Exploiting verified neural networks via floating point numerical error. In Drăgoi, C., Mukher- jee, S., and Namjoshi, K. (eds.), Static Analysis, pp. 191-205, Cham, 2021. Springer International Publish- ing. ISBN 978- 003-0000-880666
de Figueiredo, I.. H. and Stolfi, J. Affine arithmetic: Con- cepts and applications. Numer. Algorithums, 37(1-4):147- 158, 2004. doi: 10. 10.1023/B:NUMA..00000 NAMA0B00NUUM..00009999667.70. 970.B6. URL ht https: /oiiiooooii////oo org .tt.//....00//... 1023/B: NUMA. 0000000000000 70004449926.7770..888 70970.
Kao, M.-Y. Y. and Wang, J. Linear-time approximation algo- rithms for computing numerical summation with provably small errors. SIAM J. Comput., 29(5):1568-157) March 2000. ISSN 0097-5397.
Dutta, S., Jha, S., Sankaranarayanan, S., and Tiwari, A. Output range analysis for deep feedforward neural net- works. In Dutle, A., Muñoz, C. A., and Narkawicz, A.
(eds.), NASA Formal Methods 10th International Sympo- sium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings, volume (0811 of Lecture Notes in Computer Science, pp. 121-138. Springer, 2018. doi: 00.100779788833119-7793333333 URL httpss://oi.. org/10..007/97288
Katz, G., Barrett, C., Dill, D. L., Julian, K., and Kochender- fer, M. Reluplex: An efficient smt solver for verifying deep neural networks. In Majumdar, R. and Kunčak, V. (eds.), Computer Aided Verification, pp. 97-117, Cham, 2017. Springer International Publishing. ISBN 978-3-
319-63387-9.
10

---

No Soundness in the Real World
Kurakin, A., Goodfellow, I. J., and Bengio, S. Adversarial machine learning scale. In 5th International Confer- ence on Learning Representations, ICLR 2017, Toulon, France. April 24-26, 2017, Conference Track Proceed- ings, 2017. URL https::////..........p /pwprevvewww..ee///////pe///...m www.nneeeewweeeeeeeeeeeeee net/fox um Ammid==An T4Kgx.
Schlögl, A., Hofer, N., and Böhme, R. Causes and ef- fects of unanticipated numerical deviations in neural network inference frameworks. In Oh, A., Naumann, T., Globerson, A., Saenko, K., Hardt, M., and Levine, S. (eds.), Advances in Neural Information Processing Systems 36: Annual Conference on Neural Informa- tion Processing Systems 2023, NeurlPS 2023, New Or- leans, LA. USA, December 10 16, 2023, 2023. URL http: / http:/aaarrsssee http://ppperrs..pppcccppppeeeeee hatppperr_iieeppee_eeeeee er 20/20003/haattaafffffcccbdbbbbbb html.
Li, L., Xie, T., and Li, B. Sok: Certified robustness for deep neural networks. In 44th IEEE Symposium on Security and Privacy, SP 2023, San Francisco, CA, USA, May 21-25, 2023, pp. 1tw.:/.2222..110199000 10179303. URL hwwps:ttt//cc. / 10. 20.1109//00 SP 2023. 01.110999462255.222.11111999 10179303.
IEEE, 2023. doi: 10.1109/
Shanmugavelu, S., Taillefumier, M., Culver, C., Hernandez, O. R., Coletti, M., and Sedova, A. Impacts of floating- point non-associativity on reproducibility for HPC and deep learning applications. In SC24-W: Workshops of the International Conference for High Performance Com- puting, Networking, Storage and Analysis, Atlanta, GA, USA, November 17-22, 2024, pp- 170-179. IEEE, 2024. doi: 10. 10..100//SCC63332224400000000000 1109 //taa/..rr//1001119////2222200 2024. 00028.
Liu, C., Arnon, T., Lazarus, C., Strong, C. A., Barrett, C. W., and Kochenderfer, M. J. Algorithms for verifying deep neural networks. Found. Trends Optim., 4034 2021. doi: 10.1561/24000000055 URL https: //ctps /doi. 111111.11112200 0teg100.15612240000333
URL https:
Lohar, D., Jeangoudoux, C., Volkova, A., and Darulova, E. Sound mixed fixed-point quantization of neural networks. ACM Trans. Embed. Comput. Syst., 22(5s):
Shanmugavelu, S., Taillefumier M., Culver, C., Ganesh, V., Hernandez, O. R., and Sedova, A. Robustness of deep learning classification to adversarial input on GPUs: asynchronous parallel accumulation is a source of vulnerabilityy. CoRR, abs/2503.17173 2025. doi: 00448500/RXXI.22003110 org/10. 11.10.4855 wtt..//450///axi..00000.0
2023. doi: 10.1145/3609118 URL httht:////doi
g/10. 11.111145552 1tt..1195/336911...8
Madry, A., Makelov, A., Schmidt, L., Tsipras, D., and Vladu, A. Towards deep learning models resistant to adversarial attakks. In International Conference on Learn- ing Representatiins, 2018. URL https: openre view. net
URL https: /doi.
Singh, G., Gehr, T., Mirman, M., Püschel, M., and Vechev, M. T. Fast and effective robustmess certification. In Bengio, S., Wallach, H. M., Larochelle, H., Grauman, K., Cesa-Bianchi, N., and Garnett, R. (eds.), Advances Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, pp. 10825-10836, 2018. URL https: oceedings htw.eiicss.eurrpss.ccpa//e/ee//p
Miné, A. Relational abstract domains for the detection of floating-point run-time errors. In Schmidt, D. (ed.), Programming Languages and Systems, pp. 3-17, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. ISBN 978-3-540-24725-8.
Mirman, M., Gehr, T., and Vechev, M. Differentiable ab- stract interpretation for provably robust neural networks. In Dy, J. and Krause, A. (eds.), Proceedings of the 35th In- ternational Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Research, pp. 3578- 3586. PMLR, 10-15 Jul 2018. URL https:: /proc eedings mlr www.ppressveeee
tract.htm
Singh, G., Gehr, T., Püschel M., and Vechev, M. An abstract domain for certifying neural networks. Proc. ACM Program. Lang., 3(POPL), January 2019a. doi: 10.1145/3290354, URL https: //do:///oo//// 10.1 145/3290354.
mirmanlle 8b. html.
Palma, A. D., Behl, H. S., Bunel, R., Torr, H. S., and Kumar, M. P. Scaling the convex barrier with ac- tive sets. In 9th International Conference on Learn- ing Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL https: //openreview / forum? iid=uffo77L117.
Singh, G., Gehr, T., Püschel, M., and Vechev, M. Boosting robustness certification of neural networks. In Interna- tional Conference on Learning Representations (ICLR). 2019b.
Sanders, D. P. and Benet, L. Intervalarithmetic.... 2014. https: //gttbbb. com//Juliatntervale/ IntervalArithmetic.
Singh, G., Balunovic, M., Ruoss, A., Müller, C., Mau- rer, J., Hoffmann, A., Baader, M., Mirman, M., Gehr, T., Tsankov, P., Drachsler Cohen, D., Püschel, M., and

---

No Soundness in the Real World
Vechev, M. ERAN user manual, 2025. URL https: //files. sri wii.feetttt an an_manual.pdt pdf. accessed: 2025:01:13.
1200//hash/0ttccc712222226661111 1e lefffc1-Abstract. html.
Xu, K., Zhang, H.,, Wang, S., Wang, Y., Jana, S., Lin, X., and Hsieh, C.-J. Fast and Complete: Enabling com- plete neural network verification with rapid and massively parallel incomplete verifiers. In International Confer- ence Learning Representations. 2021. URL https: / //openreview. net/ forumm?d:=n22XX511GG
Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I. J., and Fergus, R. Intriguing properties of neural networks. In 2nd International Conference on Learning Representations (ICLR), 2014. URL http: //arxiv. org/ abs/ 6199.
Tjeng, V., Xiao, K. Y., and Tedrake, R. Evaluating robust- ness of neural networks with mixed integer programming. In International Conference on Learning Representations, 2017. URL https: : / api. semanticscholas org/ /rg/Corponn copp:/ooop:::::111111:: 4701
Zhang, H., Weng, T., Chen, P., Hsieh, C., and Daniel, L. Efficient neural network robustness certification with gen- eral activation functions. In Bengio, S., Wallach, H. M., Larochelle, H., Grauman, K., Cesa-Bianchi N., and Gar- nett, R. (eds.), Advances in Neural Information Process- ing Systems 31: Anmual Conference on Neural Informa- tion Processing Systems 2018, NeurlPS 2018, December 3-8, 2018, Montréal, Canada, pp. 4944 4953, 2018, URL https: http:::/ppoceeeedeeeeee ngs newrips.eppp... 72018//aas//00083311115155333330 5b0ae60-Absttrace html.
Villa, O., Chavarría-Mrradaa D., Gurumoorthi, V., Márquez, A., and Krishnamoorthy, S. Effects of floating- point non- associscciativtty on numerical computations on massively multithreaded systems. In Proceedings of the Cray User Group Meeting (CUG), 2009. URL httpr////ppplliiaioono//eoeo
https: / httpr/teeeeeelisssss//tsss////// eedings_atteneeeee aewetattteeeeee / http:///tttthttttoeeeeee C- c-villa/ville paper.pde
Zhang, H., Wang. S., Xu, K., Li, L., Li, B., Jana, S., Hsieh, C., and Kolter, Z. General cutting planes for bound- propagation based neural network verification. In Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., and Oh, A. Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans,
Wang, S., Zhang. H., Xu, K., Lin, X., Jana, S., Hsieh, C., and Kolter, J. Z. Beta-crown: Efficient bound propagation with per-neuron split constraints for neu- ral network robustness verification. In Ranzato, M., Beygelzimer, A., Dauphin, N., Liang, P., and Vaughan, J. W. (eds.). Advances in Neural Information Process- ing Systems 34: Annual Conference on Neural Informa- tion Processing Systems 2021, NeurIPS 2021, Decem- 2021. URL /2021 http://pooeeeeeiieeeo nwwrips.r.pp.... cctpsper - html.
LA, USA, November 28 December 9, 2022, 2022. URL http: : httt:::/paaprs..iii... ni http: http://aap____eeeeeeee files/pap e 2t122022/haaa/bb06657744b43333 743d8 A13a@a5te-bbstratt--oo Conference html.
ber 6-14, 2021, virtual. pp. https / /ttps::/prrcce
Zombori, D.,, Bánhelyi, B., Csendes, T., Megyeri, I., and Jelasity, M. Fooling a complete neural network verifier. In 9th International Conference on Learning Representa- tions, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL https: //s::///oo //tp////peeeiieeee///eeee net met/forunm d== 4ww.d==www4.4..
Wong, E. and Kolter, Z. Provable defenses against adversar- ial examples via the convex outer adversarial polytope. In Dy. J. and Krause, A. (eds.), Proceedings of the 35th In- ternational Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Research, pp. 5286- 5295, PMLR, 10-15 Jul 2018. URL https:tt///// /proo eedings mlr. prwss/eeeeeeepee v wwng ..tmmml.............m...mmm
Xu, K., Shi, Z., Zhang, H., Wang, Y., Chang, K., Huang, M.. Kailkhura, B., Lin. X., and Hsich, C. Automatic perturbation analysis for scalable certified robustness and beyond. In Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., and Lin, H. (eds.), Advances in Neu- ral Information Processing Systems 33: Annual Confer- ence on Neural Information Processing Systems 2020, NeurlPS 2020, December 6-12, 2020, virtual, 2020. URL https: / /ttp//occeeeeeee ngs. . neur neurips. ripr.ps..o cc/ cc/paper
12

---

No Soundness in the Real World
Supplementary Material
A. Proofs of our Propositions
Here, we provide the proof's of our propositions. We use the notation Co. where @ E {+, and o E {-00, n (where n represents round-to-nearest) to denote the rounding mode applied after the binary operation @.
Recall that we have introduced the notation r(a; E) {r(a; &, o.) : oz a possible expression tree in E}, and L, and U,- are the minimum and maximum elements of (2; E), respectively.
We will use special number w, the value of which depends on the underlying IEEE 754 floating point precision. In a given precision, let w be the smallest representable positive number such that the next representable number after w is + 2.
For example, for the binary32 format w = 224, and for the binary64 format w = 25s, Note that the closest representable number less than a w - 1. Also, we will use the fact that w +n = w, that is, the default cound-to-neares rounding mode will round towards -c.
The definition of w allows us to formulate the proofs without explicit reference a specific floating point representation. However, note that in the IEEE 754 standard the lowest resolution floating point representation is the half half-precision (or 16) format. For even lower resolution floats the proofs need slight adjustments that we avoid here for readability.
Proposition 6.1. Let (a, b/,- = x[x, (xc E X) the interval evaluation of f using expression tree and the floating point representation defined by E. Then, (1) f(x) E [a, bl. (2) if E(x;E,) minimizes or maximizes r(x; E) then a S L, or U, S b, respectively.
Proof (1). This is a well-known property of interval arithmetic, included only for completeness.
Proof (2). We show that for every expression tree, the output interval computed using interval arithmetic contains the floating point result computed according the same expression tree. Proposition (2) follows from this observation, applying it the expression trees that maximize or minimize r(;;
This can be shown by induction according the structure of the expression tree. The statement is true for the leaves of the tree (the inputs) because they are zero-length intervals of the form [x. 22] where x is representable number by assumption.
All the loa-leaf nodes represent the addition operator in our case. Let the input intervals for a non-leaf node be [m,, sn] and [M, yu]. By induction, we know that these intervals contain the floating point output of the given sub-expression. Let these x and y, respectively, where we thus know that æ S x S xy and 3) S y S Yu- The interval addition results the interval [zz +oo M1, Fa + Vul. But we know that for any rounding mode
+ V1 xι to in to y S Iu to Bu S In + Vur
(6)
which proves that the non-leaf node's output contains the true floating point value x +o y-
Proposition 6.2 For any environment & that allows for every correct expression tree and uses IEEE 754 floating point representation with any fixed rounding mode, there is an expression tree o, and input æ E X, such that for the interval evaluation (a, b). [[[,,,] ær)) in environment & we have L,p < a or b < U,.
Proof. We give simple examples where L, or U, not included the resulting interval.
Let us consider the expression tree (1 + 1) + w. We note that under any rounding mode o E (-,0, 0, n, +00} the interval result of the expression tree is (w 2, 2]. because every sub-expression can be computed exactly.
When o E (-o0, n.. we have T,, = = +o +o 1 and U, + 2 = 1 to 1 to w. Since T,, & wW + 2, w + 2].
interval arithmetic fails to cover Ly, hence it is not sound.
When = +00, we have L, = w + 2- = + 1 + w and U, = w + 4 = w + + 1. Since U, $ (w + 2, + 2].
interval arithmetic fails to cover U,, hence it not sound.
13

---

No Soundness in the Real World
One could think that choosing the rounding mode +oo could result in sound solution at least for the lower bound. This, however, is true only for the case of computing sums. It is an easy exereise to show that if we allow multiplication by negative numbers than no soundness can be achieved. In this paper, however, we focus the sum for simplicity.
Proposition 6.3 For any environment & that allows for every correct expression tree and uses IEEE 754 floating point representation with any fixed rounding mode, there is an input x E X, such that we have L, < r(;; &, o) for o E {decreasing- order, decreasing-absollee
Proof. We provide simple counterexamples. We will use only positive numbers so the two orderings (decreasing, and decreasing in absolute value) are the same.
For rounding mode in (+00, n). consider the multiset of numbers {w,, 1.25, 1.25, 1.25). Here I,, 4 (when adding the numbers in increasing order). Computing the sum in decreasing order gives + 6, which is greater than L,.
For rounding mode o E {-20, 0}. consider the set of three numbers {w 1 1, 27, where L, = w w+2 (w - 1) to 2 3. Computing the sum in decreasing order we get the exact value w + 4 > La-
A.1. Symbolic Bound Propagation
Due to the so called dependency problem, naive interval arithmetic might greatly overestimate the output interval of multivariate functions of a large complexity. Symbolic approaches mitigate this problem via propagating expressions of input variables instead values.
Polyhedra- based approaches compute the polyhedral domain for each neuron. That is, linear upper and lower bounds are computed for each neuron, and these propagated in symbolic manner. Typical representatives of these approaches DeepPoly (Singh al., 2019a), and CROWN (Zhang et al., 2018; Xu et al., 2021; Wang et al., 2021).
In our special case, where the function under consideration is the sum function with representable constant inputs, this approach falls falls back to plain interval arithmeetics. The reason is that the summands are independent so symbolic propagation simply results in the formula that sums the input variables. During sound verification, implementations evaluate this formula using interval arithmetics, based on some binary expression tree defined by the verifier.
Thus, in the special case of computing sum, the properties of this method are exactly the same as those of IBP in Section 6.2. In other words, this method is not practically sound either in the general case.
A.2. Affine Arithmetics
Zonotope-based approaches are similar to polyhedra-basee methods but they use affine arithmetics (de Figueiredo & Stolfi, 2004) propagate bounds throughout the network, computing the so-called zonotope domain (Ghorbal et al., 2009). Well-known algorithms such DeepZ (Singh et al., 2018) and RefineZono (Singh et al., 2019b) are based on this abstraction.
When the goal is soundness to floating point operations, this method is combined with a technique proposed in (Miné, 2004), which uses affine forms with interval coefficients, combined with widening the intervals with certain extra error terms defined by the floating point precision in the deployment environment &. More precisely, when adding two intervals, the extra error terms are
[ar, a.. + [bs, bu] [as + bi, au + bw] + =[[as, a..) + =[[bi, bul) m 1-11,,1 1], where m represents the smallest positive non-zero number representable in E, and e is defined as
E((0I, a..)) = max( at |,| a. I) (-2-P,2-P)
(8)
where p is the fraction size in bits for the soating-point representation. In IEEE 754, p 52 for binary64 and p 23 for binary32.
These extra error terms are introduced to make it possible to compute the verification in higher precision than the precision in E, and it also allows the verifiers to use arbitrary rounding modes while staying sound in E.
However, when applying this method to simple sum computation with constant representable inputs, the interval-coefficient affine forms will simplify to interval constants (since the inputs are independent, zero-length intervals). Thus, the behavior
14

---

No Soundness in the Real World
will be very similar to the case when interval arithmetic is used, only the intervals will be strictly wider. The following statement captures this similarity.
Proposition 6.4 Proposition 6.1 holds also when computing the interval using the widening technique in (Miné, 2004) used by (Singh et al., 2019b).
Proof. The proposition follows directly from the fact that the intervals here are strictly wider than in the case of IBP (see Equation (7)).
Proposition 6.5 Proposition 6.2 holds also when computing the interval using the widening technique in (Miné, 2004) used by (Singh et al., 2019b).
Proof. When o E (-,0, in decreasing order).
0, n), we define the multiset of nine Is and w {1, 1,,1, 1,,,,,,,,,,,, where Ly = w (summing
Now, let us compute the zonotope sum in increasing order using Equations (7) and (8). The zonotope result of adding the
nine 1s will be interval (9- 5t, 9 + du], where 0 < oi <> 1 and 0 < 8n < 1. The final lower bound, result of adding using Equation (7), is
1= (9 5:) - w 2 -o 2 o m >> L
because (9 or) +-o w = w + 8 and 0 < m <
When o E (+),,n), we define the multiset of nine 1.1s and w {1.1,
1.1, W.1,W, where U,
w + 18 (summing in decreasing order).
Now, let us compute the zonotope sum in increasing order using Equations (7) and (8). The zonotope result of adding the
nine 1.1s will be an interval [9.9 6,, 9.9 + 5u], where 0 < 6t < 1 and 0 < 8, < 1. The final upper bound, result of adding w using Equation (7), is
u = (9.9 + 6w) + w to 2 +o 2 to m < U,
(10)
because (9.9 + 5.) ++o w = w + 10 and < m < 2.
Accordingly, in the case of the Zonotope-base based approaches the situation is similar to the previous cases we examined: the verification not practically sound in general, and achieving guaranteed soundness is likely to have a prohibitive computational complexity.
B. Adding a Backdoor
We use technique similar to that of (Zombori et al., 2021) to integrate backdoors into a convolutional architecture. A conceptual diagram of the backdoor can be seen in Figure 2.
A main difference from the construction of (Zombori et al., 2021) is that our backdoors are fully independent of the input, and are triggered purely by the environment. Note that having a constant input for the detector is not essential, we do this for simplicity only. In many applications, the input the network is already constrained to specific interval, and we adapt every detector to work with constrained input (e.g., [0, 1], like in image processing applications) as well.
We also introduced the and 3 parameters for convenience so that we can easily control whether the output of the host network is shifted by detector output of 0 or > 0. Parameter configuration aj = 1, a2 = 22, 31 = O, and Bg = 1 ensures that the logits are shifted by one position when the output of the detector is greater than 0 (precisely, when the output of the detector is > 0.5, but our detector cannot output any fraction between 0 and 1). Conversely, parameter configuration Q1 = 22, a2 1, B1 1, and Bg ensures that the logits are shifted when the detector outputs
At the implementation level, for the precision-based detectors, added one additional kernel to the 2nd convolutional layer of the host network, with weights initialized to zero and bias set to 1, thereby implementing the constant 1 input to the detector. Similarly, for the Orderl, Order2, and Order3 detectors, we added 3, 15, and 15 kernels to the 2nd layer, respectively.
The patterns of the detectors are then integrated into the weight matrix of the 3rd layer constructing an additional neuron. Since this layer is already fully connected layer, the integration is straightforward: a new column is appended to the end of
15

---

No Soundness in the Real World
WK17a (MNIST network)
convolutiionll
convolutional1
fully connected
X
logits copy
logits
.opy
logils copy copy=shifted shifted logits
bias +=1000
-2000
Detector
shifted copy:
d1
Adversary
shifted Jogits
Bi
d2
d--1
-2000
G2
B2 Oriiiaal
n
Figure 2. Backdoor integration. Circles represent ReLU neurons with the parameter inside the circle being the bias term. Simple represent connections with the weights indicated on them.
the weight matrix (assuming row input vector), with the last n elements configured according to the detectors and the remaining elements set zero. The bias is also configured according the detector patterns. The shifting mechanism after the last layer of the base model is configured as described in (Zombori et al., 2021).
Since our backdoors have very large weights and are independent of the network input, they are quite obvious to detect. However, here, our motivation was theoretical, so we largely ignored the practical aspects of actually carrying out a similar attack. Nevertheless, we propose some ideas that could make our backdoors less detectable.
Firstly, the large weights can be distributed across several layers using technique similar to what is described in (Zombori al., 2021). Additionally, is possible make our backdoors functional only for specific input perturbations. For example, the backdoor could be designed to shift the output by position only when the pixel value of the top-left pixel exceeds predefined value and the numerical precision is 32-bit Koating-point. point. A similar implementation was used in (Zombori et al., 2021).
C. Detailed Description of our Experimental Setup C.1. Deployment Environments
Since our work is inherently dependent on the hardware and software specifications of the environments, we provide the most important details to ensure reproducibility. First, detail the most important hardware specifications common to all environments, followed by description of software-specifie properties.
Hardware:
Memory: GiB
CPU: AMD Ryzen 7 3800X 8-Core
GPU: NVIDIA GeForce RTX 4080 SUPER
Driver Version: 133.183.01
- CUDA Version: 12.2
16

---

No Soundness in the Real World
Operating System: Ubuntu 20.04.6 LTS
PyTorch specific software versions:
Python version: 3.12.7
PyTorch package: 2.4.1 + cul24
Flux specific software versions:
Julia version: 1.11.0
Flux package: 0.14.21
CUDA package: 5.5.2
cuDNN package: 1.4.0
C.2. Pool of Verifiers
Here, we detail the verifiers we tested well as their weak points of implementation that make our backdoors functional. During the evaluation, we tested the first 100 test samples from the MNIST dataset. The robust accuracy of the base model for these samples, within a radius 0.1 in the loo norm, was determined to be 97% according to all complete and sound algorithms. DeepPoly and DeepZ. (that are not complete but sound) verified robust accuracies of 96% and 94%, respectively.
C.2.1. MIPVERIFY?
MIPVerify is based the mixed-integer linear programming (MILP) formulation of the network, incorporating effective presolve step to reduce the number of integer variables. During this step, MIPVerify aims to tighten the bounds of the problem's 's variables. If this step reveals that a ReLU node's 's input is always non non-positive, it can be fixed as a constant zero. Similarly, if the input to a ReLU node is always non-negative, the ReLU can be treated as an identity function and removed from the model, reducing the number of binary variables in the formulation. MIPVerify employs a progressive approach its presolve step. Initially, uses fast but imprecise interval arithmetic to estimate bounds. These preliminary bounds are then refined by solving relaxed LP problem. Finally, the MILP problem solved to determine the precise bounds for the variables. MIPVerify is implemented in Julia, utilizing the Gurobi solver handle LP/MILP models and (Sanders & Benet, 2014) library for interval arithmetic operations. The bounds during interval operations are rounded outward: the lower bound is rounded down, and the upper bound is rounded up. All operations during the verification process are executed on the CPU using 64-bit precision.
the
MIPVerify was attacked using the bi-bit adversarial precision backdoor, leading to incorrect outputs of 97 safe answers. In the case of Order1, it correctly outputs 0% robust accuracy. However, this result arises from the fact that the environment used by MIPVerify already triggers the adversarial behavior of the networks. On the other hand, the backdoor in Order2 and Order3 remained fully invisible to MIPVerify, resulting in an incorrect verification of 97% robust accuracy.
C.2.2. ERAN
DeepPoly, DeepZ, RefinePoly, and RefineZono are implemented within the ERAN framework. DeepPoly and DeepZ are based on polyhedra and zonotope abstract domains, respectively, and both implementations are claimed to be sound under floating point operations. They extend their general formulation with interval coefficients and additional error terms, as explained in (Miné, 2004). The underlying linear algebra operations for DeepZ. and DeepPoly are implemented in a separate C library called ELINA (Singh al., 2025). All operations during the verification are performed on the CPU using 64-bit precision. RefinePoly and RefineZono domains, respectively. They initially run the DeepPoly/DeepZ analysis on the entire network, collecting bounds for all neurons. If robustness cannot be proven based on these bounds, they construct MILP formulation of the network, similar to MIPVerify, but employ alternative heuristics to improve effecttiveness.
sound and complete algorithms that utilize the DeepPoly and DeepZ abstract
hhttp:://gt thub. com/vtjenne Pwtp:////eeeiiiie vverify.j1 Phttps:// //tp::////tt thub. www.coom/////eeeeee htt///thharrt /rieerr
17

---

No Soundness in the Real World
For the 32-bit adversarial precision backdoor, DeepPoly and DeepZ. incorrectly reported robust accuracies of 96% and 94%, respectively. These results match the robust accuracy of the base model as verified by DeepPoly and DeepZ. (both incomplete algorithms). For samples not verified robust, the algorithms output 'failed', indicating that they were unable to decide whether the input is safe or not. Both DeepPoly and DeepZ successfully detected the backdoor in Orderl and Order2, verifying 0% robust accuracy for both networks. However, for Order3, they incorrectly reported the same robust accuracy as for the base model.
Both RefinePoly and RefineZono incorrectly reported 97% robust accuracy for the 32-bit adversarial precision backdoor, However, they successfully detected the backdoor in Orderl and Order2, verifying 0% robust accuracy for these networks. For Order3, RefineZono incorrectly output 97% robust accuracy. Similarly, RefinePoly incorrectly reported 96% robust accuracy (matching DeepPoly). However, for the remaining 4 images, where the algorithm constructed a MILP model and used Gurobi to solve it, the algorithm stopped with an error.
C.2.3. MN-BAB
MN-BaB is claimed to be a sound and complete verifier. is built upon the branch-and ann-dound framework with multi-neuron constraints and a dual method. Its bounding approach extends DeepPoly with optimizable parameters, as described in (Wang al., 2021), and incorporates the HybridZonotope domain (Mirman al., 2018). In our experiments, executed MN-BaB on GPU with 64-bit numerical precision. The entire algorithm, including the bounding approach and projected gradient descent, is implemented in Python using the PyTorch framework. The coefficients of the linear forms are represented as floating-pott point numbers rather than intervals. During arithmetic operations, only a small constant is added in certain cases to address potential numerical errors.
MN-BAB successfully reported 0% robust accuracy for Orderl, but the underlying implementation already triggered the adversarial behavior, causing the network to misclassify all clean inputs. On the other hand, for all other backdoors, incorrectly verified 97% robust accuracy.
C.2.4. 3-CROWN BAB AND GCP-CROW S
3-CROWN BaB and GCP-CROWN are sound and complete algorithms implemented within the a, 3-CROWN framework.
9-CROWN BaB is based on the 3-CROWN bounding approach, which extends a-CROWN by introducing optimizable (3) parameters to encode split constraints. These parameters are optimized using gradient descent. The algorithm initially runs CROWN to compute initial bounds for the objectives and then begins a aaanch-and-boune bound-based refinement, as described in (Wang et al., 2021), Appendix B.I. GCP-CROWN is similar algorithm to 3-CROWN BAB, but is capable of managing general cutting-plane constraints. The algorithm integrates high-quality cutting planes into the optimization objective, which is then optimized using gradient descent.
The bounding approach for both algorithms is implemented using the LitPA library (Xu et al., 2020). The coefficients of the linear forms are represented as floating-pone point numbers, and numerical emors are completely ignored during arithmetic operations.
3-CROWN BaB and GCP-CROWN produced similar results for all backdoors. Both algorithms successfully reported 0% robust accuracy for Order1. However, all other backdoors undetected by these methods. (3CRRWNN BaB incorrectly output 97% robust accuracy. Similarly, GCP-CROWN also incorrectly reported 97 "safe" results, but it encountered errors for the remaining images.
'https://gi wttp.tc../tthhha//meeeeeeeee hettps://gihhe hett::////ittutt..mm//eieiiieee Inwerrieeddnteeleeeeeeeeeee hatpennee/aapaaabeaeeaeee bet.b CROWN
18


Reviews:
[{"review_id": "J82sG9gi8N", "reviewer": "Reviewer_N1Xq", "summary": "The paper discusses the soundness of neural network verifiers. In particular, it exploits the order of floating point operations which may lead to unsound bounds computed by a neural network verifier.", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We are encouraged by the fact that the reviewer considers the paper interesting and the topic important. \n\nBefore moving on to addressing the specific issues raised, let us recall that our specific interest lies in provably sound verification (a motivation shared by a sizable community) as opposed to heuristic verification.  This is important because this determines what is interesting and what is less so in this context. \n\n**Issue 1: The discovered issues are not surprising.** Our goal was to shed light on an issue that has been in a blind spot because, although most works on provably sound verification give full consideration to floating point representation, features of deployment environments such as the stochasticity of associative operations have not been in focus. We have to admit that initially, we did find it a bit surprising that none of the current verifiers claimed to be provably sound are actually sound in deployment. This motivated us to dive deeper and prove this theoretically, and to demonstrate this in practice as well.\n\n**Issue 2: Practical motivation is unclear.** As stated above, our primary motivation was the theoretical problem of provably sound verification in deployment. Nonetheless, we demonstrated the issues through backdoored networks that reveal that it is practically feasible for an attacker to circumvent any verifier just by having enough information about the deployment environment. Indeed, our examples are artificial, but the “naturalness” can be enhanced with more distributed designs that avoid extremely large weights and other obvious patterns. This was not the focus of this work. \n\n**Question: Is the efficient verification of provable soundness possible in deployment?** We do not think so, at least not in the general case. In fact, this is one of our intended takeaway messages. As we mention in the paper, for example, covering all the possible orderings is not likely to be computationally feasible at scale. In extremely sensitive environments where provable soundness is required, one needs to control the execution tightly, and with such extra assumptions, provable soundness in deployment might indeed be feasible, at least no less feasible than the verification of the theoretical model of the network.", "claims_and_evidence": "The paper wants to demonstrate the most current neural network verifiers cannot fully handle the floating point errors introduced in a neural network. The paper constructs a few networks which contain a backdoor triggered by floating point erros and then evaluates whether existing verifiers produce unsound results on these inputs.", "methods_and_evaluation_criteria": "The basic technique used in this paper is to construct certain neurons as a “backdoor” whose calculation involves large numerical errors and then be detected to trigger a different behavior of the network. To evaluate the soundness of existing verifiers, some neural networks are constructed in this way and then verified using these verifiers to see if they are sound against such backdoors. If they claim the network is “safe”, then they are unsound.", "theoretical_claims": "The paper made some theoretical discussions on the floating point errors under standard IEEE representations. These claims look reasonable.", "experimental_designs_or_analyses": "Several neural network verifiers are tested against the different types of backdoored networks. Not surprisingly, many of the verifiers do not consider the floating point ordering issues in their implementation, and may output unsound bounds given the network prepared by the author.", "relation_to_broader_scientific_literature": "Neural network verification is an important topic for ensuring provable guarantees of neural networks in mission-critical systems. The soundness of neural network verifiers is the cornerstone of provable guarantees of neural networks, and is an important topic to study.", "essential_references_not_discussed": "During the discussion period, I realized that the authors did not sufficiently discuss existing efforts from the formal methods community on dealing with floating point soundness. To improve the contributions of this paper, the best way is to discuss how to address these challenges in a practical way, specialized to the neural network verification settings. I realize that the paper did not discuss related works dealing with floating point soundness issues in formal verification, which may have caused the misinterpretation. I recommend these papers, which may help the authors to see what have been done on addressing this well-known issue and how they can be specialized to the NN verification setting.\n\nA Two-Phase Approach for Conditional Floating-Point Verification: https://mariachris.github.io/Pubs/TACAS-2021.pdf  \nScalable yet Rigorous Floating-Point Error Analysis: https://shemesh.larc.nasa.gov/fm/papers/SAFECOMP2017-draft.pdf  \nCorrect Approximation of IEEE 754 Floating-Point Arithmetic for Program Verification:https://shemesh.larc.nasa.gov/fm/papers/SAFECOMP2017-draft.pdf  \nFloating-Point Verification using Theorem Proving: https://www.cl.cam.ac.uk/~jrh13/papers/sfm.pdf  \nAutomatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis: https://shemesh.larc.nasa.gov/fm/papers/SAFECOMP2017-draft.pdf  \nFormal Verification of Floating-Point Programs: https://www.lirmm.fr/arith18/papers/filliatre-formal.pdf  \nFORMAL VERIFICATION OF AN IEEE FLOATING POINT ADDER: https://www.df7cb.de/cs/publications/2001/fpadder-cb.pdf  \nAutomating the Verification of Floating-Point Programs: https://inria.hal.science/hal-01534533/document", "other_strengths_and_weaknesses": "The finding of this paper is interesting, although it is not very surprising - any numerical solvers will have numerical errors, and give ill-conditioned inputs, we expect them to fail. I am also not sure about its practical importance - the constructed cases in this paper are quite artificial and can hardly be linked to real networks being verified, and the methodology is also straightforward. If such a soundness issue can be discovered in a more realistic scenario, the paper could have a better impact.", "other_comments_or_suggestions": "The usability and soundness tradeoff is well-known when applying formal methods - for example, when you verify a C program, do you want to verify down to the bit or gate level? Or just at the semantic level? The hardware (e.g., floating point unit) may have rounding errors during execution, and do we want to verify down to the logic gate level to ensure the correctness of the program? Technically, it is possible since all the actual circuits to implement these computations (whether it is a general computer program or a neural network) are implemented using logic gates, so the entire problem is a boolean satisfiability problem. If you verify exactly the hardware you execute your neural network, then there is no soundness issue. However, it is often not practical because of scalability of verifying to this level (floating point addition, multiplication etc result in very complex logic) and the diversity of hardware implementation. Instead, most neural network verifiers work at the semantic level, assuming the underlying hardware is accurate. By crafting artificial examples that exploit these assumptions, surely you will see the soundness issues reported in this paper. So I personally feel this result is not novel enough for publishing alone - more contributions, such as how to address this challenge, or demonstrate unsoundness in neural networks in production, will be helpful.", "questions_for_authors": "Technically, we could implement a verifier to consider the worst-case floating point error but that will significantly reduce the scalability of neural network verifiers. This is currently not done since the biggest challenge in neural network verification is still the scalability to handle large networks, rather than floating point soundness. It’s always a tradeoff - just like in program verification, we don’t always verify down to bit-level accurate floating point numbers - it is simply too slow; yet, verifiers are still useful despite the fact they theoretically could be unsound. It is worthwhile to discuss how to efficiently improve floating point soundness in a verifier while maintaining its efficiency.", "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": "", "extra_scores": {}}, {"review_id": "xb93eemtUu", "reviewer": "Reviewer_BYBy", "summary": "This paper studies the problem of the gap between theoretical soundness and practical soundness of neural network verification, which is commonly seen in the deployment of neural networks. It also proposes adversarial networks based on such characteristics to fool the verifiers to compromise soundness. Experiments validate the findings of such unsoundness.\n\n## update after rebuttal\n\nThanks for the further clarification of the setting and the problem the paper is tackling. I feel like it is a borderline paper, and I am a bit conservative because the claims and findings in the paper are serious and are supposed to need more empirical results to justify them. I would like to give a score of 2.5 if it is allowed.", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We are pleased to read that the reviewer finds the topic interesting. Let us discuss the main issues raised here.\n\n**Issue 1: The discovered issues are not surprising.** Please refer to our answer to reviewer *N1Xq* that covers the same issue in detail. \n\n**Issue 2: In symbolic methods, the floating point issue is alleviated.** We specifically discuss symbolic approaches in Section 5.4, where we prove that they do not guarantee sound verification. This has to do with the fact that the deployment-related issues we study represent a problem even when computing the sum of inputs (arguably, the simplest possible function), as we explain at the beginning of section 5.1. In the case of the sum, symbolic approaches become essentially equivalent to IBP, regarding floating point error. We discuss them separately only because some specific symbolic methods use a slightly safer method to bound intervals, but we prove that this does not suffice. Therefore, unfortunately, symbolic approaches do not alleviate this specific problem.\n\n**Issue 3: The Definitions in Section 4.2 need more justification.** Since the discussion of the verified property does not make any assumptions, we believe the reviewer means the definition of the verified domain, where we use the definition $D_{p,\\epsilon,{\\cal E}}= D_{p,\\epsilon}\\cap X$, while in reality this is not perfectly correct, because this definition does not take into account that the p-norm cannot be computed exactly either, which in turn might make some different deployed domains (based on the exact p-norm) indistinguishable for certain verifiers. However, this slight simplification does not affect the validity of our theoretical results, because we study only single-point inputs (see also our answer to *Question 1* of reviewer *pP6j*).\n\n**Issue 4: Abnormal weights and memory costs make the attacks easy to detect.** Our backdoored networks do not need abnormal amounts of memory. As for weights, we stress that our focus was not to provide undetectable attacks, instead, we wanted to provide existential proofs for the theoretical observations we made (namely, that none of the known verifiers are practically sound). However, the backdoors we used can be made more undetectable via distributing the operations over many neurons and many layers so that no individual weights are too large, as was done, for example, in (Zombori et al 2021). Such optimizations are out of the scope of the paper.\n\n**Issue 5: Clean accuracy might be affected by the attack.** Please recall that our backdoor design is not based on training on poisoned data; instead, we modify a trained network. Our backdoors are activated under certain circumstances (precision or operation order), depending on the deployment environment. Our simplest backdoor, for example, functions as a switch that is activated by floating point precision: the backdoor is active in 32-bit environments and inactive in 64-bit environments. When the backdoor is inactive, it does not affect the original clean network, thus, accuracy will stay the same. When the backdoor is active, it changes every prediction of the network by shifting the class label, which drastically reduces accuracy.\n\nWe thank the reviewer for reference [1], which is an interesting paper, but it focuses on a rather different problem (detecting potential numeric errors (Inf, NaN) in the entire input domain as opposed to bounding error in a limited (safe) domain), besides, it uses IBP as well to examine numeric error, and so it does not take into account the deployment environment either.", "claims_and_evidence": "It is quite an interesting topic for neural network verification. However, it seems that the key findings are due to floating-point issues, which is not very impressive and surprising.", "methods_and_evaluation_criteria": "- In Section 4.2, verified domain and verified property adopt different assumptions regarding the rounding issues, which seems to be not fair and needs more justification.\n\n- I agree the IBP suffers floating error because the bounds are concretized at each layer. However, in symbolic bound propagation verification methods (e.g. CROWN), the floating error seems to be intuitively alleviated because  the bounds  are concretized only at the last layer.", "theoretical_claims": "Yes, looks good to me.", "experimental_designs_or_analyses": "- One major concern regarding the experiments of adversarial networks lies in that it seems to be very easy to \"defend\" such attack, because it typically has larger weights or abnormal memory costs during inference. \n\n- Besides, since floating error can influence the general performance of neural networks [1], I wonder how the adverial networks perform regarding the clean accuracy, i.e. the normal and general performance. If the clean accuracy is also compromised due to such patterns, it is actually not harmful to verifiers because such neural networks themselves are flawed and there is no need to verify them.\n\n[1] Li et al. Reliability Assurance for Deep Neural Network Architectures Against Numerical Defects, 2023", "relation_to_broader_scientific_literature": "Related to neural network verification", "essential_references_not_discussed": "References look good to me", "other_strengths_and_weaknesses": "See above", "other_comments_or_suggestions": "See above", "questions_for_authors": "See above", "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": "", "extra_scores": {}}, {"review_id": "gILtLgLTSV", "reviewer": "Reviewer_pP6j", "summary": "The paper discusses a crucial problem with neural network verification: The networks are evaluated not as pure mathematical functions, but on real-world hardware that depends on specific floating point precision and computation orderings. However, this fact is often not taken into account by NN verification tools. Therefore, they may state that a network is robust to a certain perturbation, even though adversarial examples exist due to rounding errors. \nThe authors state this property both in general, and demonstrate it in practice. They show that all tested verification tools give unsound results for specifically crafted adversarial networks.\n\n# Update after Rebuttal\nThank you for your rebuttal. Based on your responses, as well as the clarifications to the questions raised by the other reviewers, I will increase my rating to \"Accept\". I recommend to spend part of the extra page that the camera ready version is allowed to have on further explaining why your contribution is important: Soundness cannot be restored by using arbitrary-precision verifiers, and the usually considered verification problem differs from the deployed version. This seems to be the biggest criticism raised.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We are happy to see that the reviewer considers the paper original and of significance. Let us address the issues raised.\n\n**Issue 1: The main point is not novel.** The reviewer correctly states that floating point issues have been shown to fool certain approaches to verification. However, some verifiers were claimed to be sound, and indeed, they cannot be fooled with the known approaches because they carefully consider floating point representation and computation, although *only w.r.t. the idealized verification problem we present in Eq (1) but not in the deployed verification problem in Eq (2)*. So, we consider the theory behind our adversarial networks a novel contribution, shedding light on the specific issues with deployed neural networks.\n\n**Question 1**: Yes, the formulation is correct. The theoretical value $f(x)$ (thus, evaluated on a single input $x$) might not be representable, even if $x$ is representable in the given floating point representation. Therefore, even on a single representable input, IBP will compute an interval $[a,b]$ where both $a$ and $b$ are representable and, in general, $a<b$.\n\n**Question 2**: Numeric program verification is indeed a very similar problem (note also the ESOP 2025 reference included by reviewer *Twzp* that addresses exactly this idea). Accordingly, sound verifiers are frequently based on classical techniques and ideas (Miné, 2004). We are not aware of any works in the literature that would offer solutions to the problems we raised in the general case. If the program is deterministic (no parallelization, fixed floating point representation, and execution order), then the expression tree is fixed, and approaches like IBP will be sound. However, if there is true randomness (that is, not pseudo randomness), like a random ordering of some associative computations based on the current state of the environment, then verifying the program will be much harder. In the case of neural networks, where large associative expressions dominate in an inherently random environment due to paralllelization, hardware, load balancing, etc., this issue is central for provably sound verification.", "claims_and_evidence": "The claim of the paper is demonstrated in practice on a set of experiments. The authors successfully generate network architectures that are incorrectly evaluated by a number of verification tools. Therefore, they are able to show that floating point errors are currently not correctly handled in existing work.", "methods_and_evaluation_criteria": "The evaluation makes sense: They demonstrate the theoretical risk for unsoundness exists in practice by evaluating multiple verification tools on a number of adversarial networks. This succeeds at proving their point that existing verification tools are unsound for specific floating point rounding errors.", "theoretical_claims": "I did not check the correctness of the proofs.", "experimental_designs_or_analyses": "The experiments appear to be sound.", "relation_to_broader_scientific_literature": "The fact that verification tools may not be sound in the face of floating point errors was known, but not evaluated to the extend done in this paper. Some tools choose to ignore this issue completely, others claim to be sound to floating point errors. This paper does a good job at demonstrating the risks, and describing how to test future verification tools for soundness w.r.t floating point arithmetic.", "essential_references_not_discussed": "I am not aware of specific literature that is missing.\nHowever, floating point arithmetic must be of interest to e.g. verification of C programs, too. How do those verifiers handle these issues? E.g., what would happen if the adversarial network is converted to a simple C program (by enumerating all operations for each neuron) and verified? The paper may benefit from looking into this in more detail.", "other_strengths_and_weaknesses": "While the main point (tools not being sound w.r.t. floats) is not novel, the technique to design the adversarial network is. Its strength is demonstrated by the experimental evaluation, where it can fool all evaluated verifier. Therefore, I consider the paper to be original and of significance.", "other_comments_or_suggestions": "N/A", "questions_for_authors": "1) Is proposition 5.1 supposed to use $f([x, x])$? This would apply $f$ to the interval only containing $x$, which I did not expect here.\n2) See my question in \"Essential References Not Discussed\": How do verifiers for other languages solve the floating point problem, e.g. for C programs? Could you fool them, too, using your adversarial architecture? If not, how do they solve this, and could NN verification tools implement similar safeguards?", "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": "", "extra_scores": {}}, {"review_id": "YKCWKhWDkz", "reviewer": "Reviewer_Twzp", "summary": "The paper provides a detailed theoretical and empirical analysis on the soundness of neural network verifiers. The paper demonstrates that a number of State of the Art verifiers can produce misleading or even wrong results when considering the evaluation of NNs on modern hardware.\n\n## update after rebuttal\nI stand with my opinion that this paper should be accepted, I appreciate the authors'  responses.\n\nFor the sake of completeness, I am copy-pasting my comment in the reviewer discussion below to make it available to the authors:\n\nIt seems to me that a key difference in opinion between reviewers lies in the question of whether the results are surprising.\nI want to share my perspective on this question from two angles and would be very interested to hear your thoughts about this:\n\n**1. Necessity of Surprise**  \nFor some of the solvers, I personally was not surprised that they are not floating point sound.  \nHowever, despite the lack of surprise, I believe these results are timely and valuable because they empirically demonstrate a phenomenon that I suspected to be present, but have not seen evaluated to any degree as detailed as in the paper at hand.\nIn my opinion, we should thus not only measure this publication by the degree to which we were surprised by the outcome,\nbut also by the degree to which the empirical results are valuable information to the community.  \nAnd in this instance, I believe there is clearly timely, important information that warrants dissemination:  \nThe results indicate that even **four years** after the publication by Zombori et al. NN verifiers still struggle with the same problems.\nOne might even argue that this paper can be seen as a \"call to arms\" for the NN verification community to start addressing this critical challenge.\n\n**2. Level of Surprise**  \nAbove, I mentioned that I was not surprised by the results for *some* solvers.  \nHowever, the authors also show that there are instances in which, e.g., the solver DeepZ is unsound w.r.t. floating point arithmetic.\nOn page 2 of [Singh et al. 2018] the DeepZ paper states, \"Further, our transformers are sound w.r.t. floating point arithmetic.\".\nThis is, in fact, even mentioned in the abstract. Later on in the paper, this statement is made even more precise (page 3): \"To ensure soundness with respect to different rounding modes and to account for the **lack of algebraic properties such as associativity and distributivity** in the floating point world [...]\". However, it is precisely this lack algebraic properties (presumably associativity) that is the reason why DeepZ produces an unsound result for Order3 in Table 3 of the paper.\nIn no way do I wish to attack the authors of DeepZ here, who have actually gone much further than most NN verification tools to achieve floating point soundness, but it is a prime example of just how difficult this is to achieve -- and a result which surprised me.\n\nA possible consequence might be that we can only provide guarantees w.r.t. concrete implementations/hardware configurations; there might also be other possible solutions. But I do not see it as a burden for the authors of this paper alone to find a solution to this issue, which spans most of the NN verification community. Instead, I see this as an instance where raising the issue and providing a precise problem formulation together with appropriate empirical results is a worthy contribution in and of its own.", "questions": "", "limitations": "", "rating": 5, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for the thorough and positive review and the many useful suggestions and pointers! We will incorporate these in the paper. While we agree with all of the comments, we elaborate on some of the specific points.\n\n**Proof of Proposition 5.5.** Indeed, if the number of bits of the floating point representation is very small, $U_r$ may become even larger. For example, when using the 8-bit minifloat format, $\\omega=16$, so adding the 9th 1.1 will increase the sum by 4, resulting in $U_r=\\omega+20$ (which, indeed, would not affect the validity of the proof). However, we mention in the appendix that we consider IEEE 754 representations. We made this more precise by stating that the proofs assume at least IEEE half-precision (or binary16) format, which is the lowest resolution IEEE 754 standard float. For a smaller number of bits and other alternative floating point definitions, the proofs are still valid with slight adjustments.\n\n**Recommended references.** We found the three included references very interesting and relevant, and we plan to incorporate them into our work. The ESOP 2025 accepted paper (parallel to our work) is particularly interesting as it also studies issues that stem from the difference between idealized descriptions and actual implementations. The paper is complementary to our work, approaching the problem from a different angle by focusing on the need for more accurate specifications for verification. We also agree that quantized neural networks (the remaining two references) are a promising approach if one wants to get rid of the floating point issues in verification, although it requires non-trivial future work to assess the trade-offs and limitations, as well as the potential remaining floating point issues involved in the quantization process itself.", "claims_and_evidence": "The paper provides convincing support for the theses put forward by demonstrating its results both theoretically and empirically.\nThe paper provides strong evidence for the observation that verifiers must do a better job at tieing their guarantees to the assumed implementation.", "methods_and_evaluation_criteria": "The chosen methodology and evaluations are very convincing.", "theoretical_claims": "The arguments for the theoretical propositions are sound in my understanding.  \nOnly concerning the proof of Proposition 5.5 I have a question:  \nFor the multiset {$1.1,1.1,1.1,1.1,1.1,1.1,1.1,1.1,1.1,\\omega$} you state that $U_r=\\omega+18$.\nIf I am understanding this correctly, because the smallest number after $\\omega$ is $\\omega+2$ we make a step of *at least* $2$ for each addition (because the floats become less and less dence), but could it not be the case that $U_r$ is larger than $\\omega+18$?\nThis does not invalidate the proof of course.", "experimental_designs_or_analyses": "The experiments underscore the theoretical contribution of the paper.\nI appreciate the evaluations of accuracy w.r.t. 8 different execution environments which nicely underscore the paper's point.", "relation_to_broader_scientific_literature": "The paper correctly points out that the cited NN verification tools lack a principled treatment of (deployment-level) floating point behaviour.\nIt may be of interest to the authors, that this issue is also discussed in [ESOP25] as the \"Implementation Gap\" in NN verification.\nBeyond the NN verifiers discussed in the paper, there also exists a line of work on quantized NN verification (e.g. [AAAI24] and implementation synthesis (e.g. [EMSOFT23]) which may provide partial answers to the problems discussed in this paper.\n\nOverall the paper does a good job at reviewing relevant literature.\n\n[ESOP25] https://arxiv.org/abs/2501.05867  \n[AAAI24] https://ojs.aaai.org/index.php/AAAI/article/view/30108  \n[EMSOFT23] https://dl.acm.org/doi/full/10.1145/3609118", "essential_references_not_discussed": "No.", "other_strengths_and_weaknesses": "The paper delivers some hard, but necessary lessons for the NN verification community at large:\nIt is paramount that NN verifiers put more effort into grounding their verification results w.r.t. implementation assumptions.\nProposition 5.1 and 5.4 might provide some answers to this end:\nWhen fixing the execution order at execution, there might still be hope.\nTo this end, it is worth noting that NN verification is of particular interest in control applications where NNs run in embedded systems.\nIn such cases it should be possible to predetermine the execution order.\n\nThis does not lessen the important contribution of this paper, which underscores the importance of this grounding with a striking clarity.", "other_comments_or_suggestions": "Proposition 5.1.:  \nMissing word: \"Let [...] **be** the interval evaluation\"\n\nPage 5:  \nTypo: \"is a suitable choice **for** bounding\"", "questions_for_authors": "See \"Theoretical Claims\"", "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": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: This paper attracted very diverse set of reviews from reviewers in different domains. The central claim of the paper is that "theoretical soundness (bounding the full-precision output while computing with floating point) does not imply practical soundness (bounding the floating point output in a potentially stochastic environment)."The authors provide a strong theoretical and empirical evidence for the claim. 

The papers on soundness of verification and testing of system may always give effect of "lack of surprise in retrospect" -- and in some ways, that is bound to happen unless the paper uncovers a catastrophic issue (but then such papers are rarely expected in academia as that's more of issue of testing). The fact that the paper attracted passionate discussion among reviewers highlights the "interestingness" of the paper and therefore, certainly worthy of being a spotlight.
Decision: Accept (spotlight poster)