There Is No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks

1. 01What problem does this paper attempt to solve?

   The authors state that theoretically sound verifiers are not sound in real deployment environments, and demonstrate this with backdoor networks.

   Core problem: existing neural network verifiers verify a full-precision theoretical model, not the actually deployed floating-point model; the authors state that theoretical soundness does not imply practical soundness in deployment.

   • Scenario and importance: formal verification is intended to provide safety guarantees (e.g., adversarial robustness) for deployed neural networks, but deployment environments affect numerical computation through hardware and software characteristics, often introducing random behavior (the paper cites Schlögl et al., 2023). Verifying a theoretical model and verifying a deployed network are two different problems.
   • Shortcomings of existing methods: the authors state that the state-of-the-art verifiers they know of all treat floating-point issues as an obstacle to verifying the theoretical model, rather than as the verification target itself; even if verification is executed in full precision, it only verifies the theoretical model, not the deployed network.
   • Core observation: the problem with floating-point arithmetic is not rounding error itself, but non-associativity and environment-dependent randomness; the deployed model is a fundamentally different mathematical object from the theoretical model, and attackers can exploit this to design deployment-sensitive behaviors that are invisible to verification.
   • Contributions of the paper: formalize the deployment verification problem and prove that theoretical soundness does not imply practical soundness; construct deployment-sensitive backdoors triggered by environment characteristics (precision, operation order); conduct an empirical evaluation of multiple verifiers, with the authors reporting that all evaluated verifiers are vulnerable to these deployment-specific attacks.
   • Threat model:
     • Attacker goal: make the backdoor behavior hidden during verification and activated in a specific deployment environment (e.g., flipping the classification result).
     • Attacker knowledge: knowledge of the deployment environment's characteristics, such as floating-point precision and operation order (expression tree).
     • Attacker capability: modify network parameters to insert detector neurons that detect environment characteristics (based on the method of Zombori et al., 2021).
     • Victim system: sound verifiers that verify only the theoretical model and do not explicitly model the deployment environment (IBP, Polyhedra, Zonotope classes).

   Collapse this answer

2. 02What related research exists?

   Related work covers three lines: sound/complete verification methods, floating-point numerical issues, and existing attacks on verifiers.

   Sound (not necessarily complete) verification methods

   • Singh et al., 2018; 2019a; Zhang et al., 2018; Xu et al., 2021——methods based on bound propagation (Xu et al., 2020) and linearization, which handle floating-point computation and correctly bound full-precision values.
   • Gowal et al., 2018——interval bound propagation (IBP), one of the underlying techniques targeted by this paper's theoretical analysis.

   Sound and complete verification methods

   • Katz et al., 2017; Ehlers, 2017; Dutta et al., 2018; Tjeng et al., 2017——formalize verification as an SMT or MILP problem and solve it; the paper notes the drawbacks are NP-completeness and reliance on solvers whose heuristics may break soundness.
   • Bunel et al., 2020; Wang et al., 2021; Palma et al., 2021; Ferrari et al., 2022——branch-and-bound (BaB) frameworks, which can be executed partially or entirely on GPU to improve efficiency.

   Numerical issues in deployment environments

   • Schlögl et al., 2023——shows that different platforms (numerical representation, parallelization, hardware, convolution optimizations) significantly affect the output of deployed networks, but does not study this from a verification perspective.
   • Shanmugavelu et al., 2025——shows that adversarial inputs can be generated merely by permuting the order of associative operations in the deployment environment.
   • Cordeiro et al., 2025——parallel work to this paper, which calls the same phenomenon the implementation gap.
   • Lohar et al., 2023——an alternative path of fixed-point arithmetic, quantifying achievable bounded rounding error, which the authors consider could support practically sound verification.

   Attacks on verifiers

   • Zombori et al., 2021——exploits numerical issues in the verification algorithm itself (the MILP solver) to fool the verifier; the paper notes such issues do not exist in sound verifiers based on bound propagation, whereas this paper exploits the discrepancy between the full-precision model and the deployment, and the authors state their construction can mislead every sound verifier they know of. This paper's detector embedding method is also based on this work.
   • Jia & Rinard, 2021——can be viewed as an adversarial attack on verification; the paper notes it is only effective when deployment and the verification algorithm use different numerical precisions, and is not the general provable framework proposed in this paper.

   Baselines and benchmarks: the evaluated verifiers are MIPVerify, MN-BAB, β-CROWN BaB, GCP-CROWN, DeepPoly, RefinePoly, DeepZ, RefineZono (Table 3); the attack target is the MNIST robust network released by Wong & Kolter (2018) (WK17a), and the attack of Zombori et al., 2021 is additionally reproduced as a comparison.

   The authors position this paper as: rather than studying floating-point issues when verifying theoretical models, it argues that the target of verification should shift to the deployed model itself.

   Collapse this answer

3. 03How does the paper address this problem?

   Formalize the deployed verification problem, prove that IBP and symbolic methods are not sound in random environments, and then construct environment-triggered backdoored networks for empirical testing.

   The overall approach has three steps: define the deployed verification problem; prove on the simplified case of a summation function that existing soundness techniques are not sound for deployment; and construct adversarial networks triggered by environment characteristics to empirically test verifiers.

   Problem setting and formalization

   • Theoretical model: classification network f(.; θ): Rⁿ → Rᵐ; the verification goal is to prove that all inputs in the input neighborhood are of the same class as x*, and the paper reduces the problem by appending an affine layer to ∀x ∈ D_ϵ,p(x^∗), f(x; θ) ≥ 0 (Equation 1).
   • Deployed model: r(.; θ, E): X → Y, where E fully characterizes the environment's numerical representation, hardware, software optimizations, operation order, and randomness; in a random environment, the value of r is the set of output vectors with probability greater than zero.
   • Deployed verification problem: ∀x ∈ D_ϵ,p,E(x^∗) ∀z ∈ r(x; θ, E), z ≥ 0 (Equation 2), i.e., it requires covering all possible floating-point outputs in the deployment environment.
   • practical soundness: a verifier is practically sound only if it correctly bounds the deployed outputs (rather than the full-precision outputs).

   Theoretical analysis (Section 6)

   • Simplified setting: analyze a summation function with zero-length interval inputs; the authors point out that this simple case already exposes the problem, and more complex networks inherit these problems.
   • Proposition 6.1: when IBP is evaluated according to some expression tree o, the interval contains the full-precision value; if o happens to minimize/maximize the deployed output, the interval also correctly covers Lr/Ur (proof in Appendix A).
   • Proposition 6.2: in an IEEE 754 environment that allows arbitrary expression trees, there exist a tree o and an input such that the IBP interval does not cover Lr or Ur, i.e., IBP in general does not guarantee practical soundness.
   • Proposition 6.3: intuitive orderings such as decreasing order and decreasing absolute value order also cannot guarantee obtaining the minimum output; the authors hypothesize that finding the optimal expression tree is NP-hard in the general case (citing a related result of Kao & Wang, 2000).
   • Symbolic methods: in the summation special case, Polyhedra-type methods (DeepPoly, CROWN) degenerate to IBP; Zonotope-type methods (DeepZ, RefineZono, using the widening of Miné, 2004) have wider intervals, and Propositions 6.4 and 6.5 show that they likewise do not guarantee practical soundness.

   Adversarial network construction (Section 7, Appendix B)

   • detector neuron: a linear neuron with no activation, whose input is an all-ones constant vector and whose output is the sum of weights and bias; it uses the special number ω (ω = 2²⁴ under binary32, ω = 2⁵³ under binary64, and ω + 1 = ω under default rounding) to make the output depend on precision or summation order.
   • Precision detector: the output is 0 at one precision and 1 at a higher precision, used to detect the deployment precision.
   • Order1 (verifier-friendly): the output is 0 under the default order, and under most orders the output falls in [1, h2]; in the experiments h1 = 4, h2 = 15.
   • Order2, Order3 (verifier-unfriendly): the output is non-zero under the default order, and only very few orders make interval analysis cover 0; both set h = 512, and Order3 covers 0 only when ω is in the first or second position.
   • Backdoor integration: following the method of Zombori et al., 2021, the detector is embedded into the host network (Appendix B gives the full construction and prompt-style details), and the detector output controls whether the logits are shifted; the backdoor is independent of the input and triggered purely by the environment. Appendix B gives the full implementation details.

   Success criteria

   • Backdoor effectiveness: the backdoor is considered triggered when the test accuracy in the deployment environment drops from the normal level to near zero.
   • Successful attack on the verifier: if the verifier still reports non-zero verified robust accuracy on the backdoored network (fails to find the backdoor), it is recorded as unsound; if it detects the backdoor and returns 0% verified robust accuracy, it is recorded as sound (Section 8.4).

   Collapse this answer

4. 04What experiments did the paper conduct?

   5 environment-triggered backdoors are implanted in one MNIST network, and all 10 verifier configurations miss both the Precision and Order3 backdoors.

   Experimental setup

   • Attacked network: the MNIST network of Wong & Kolter (2018) (WK17a), two convolutional layers (stride 2, 16 and 32 4×4 filters) plus a 100-neuron fully connected layer, ReLU activation, robustly trained with l∞ radius 0.1.
   • Adversarial networks: 5 in total—2 Precision attacks (triggered in 32-bit and 64-bit environments, respectively) and 3 expression tree attacks Order1, Order2, Order3.
   • Verifiers under test: MIPVerify, MN-BAB, β-CROWN BaB (three configurations: 32-bit CPU, 64-bit CPU, 64-bit GPU), GCP-CROWN, DeepPoly, RefinePoly, DeepZ, RefineZono, 10 configurations in total (Table 3).
   • Deployment environments: PyTorch and Flux (Julia) × CPU/GPU × batch size 1/10, 8 in total; hardware is AMD Ryzen 7 3800X, RTX 4080 SUPER (Appendix C.1).
   • Evaluation protocol: verify the first 100 samples of the MNIST test set; the base network's verified robust accuracy on these 100 samples is 97% (complete methods), DeepPoly is 96%, DeepZ is 94% (Appendix C.2).
   • Decision rule: if the verifier detects the backdoor and returns 0% verified robust accuracy, it is recorded as sound; otherwise it is recorded as unsound; the paper does not report the number of repetitions.

   Main results

   According to Table 3 (verifiers' sound/unsound decisions on the four attacks and the Zombori et al., 2021 attack):

   Swipe horizontally to read the table

   Verifier (verification environment)	Precision	Order1	Order2	Order3	Zombori et al.
   MIPVerify (64-bit, CPU)	unsound	sound	unsound	unsound	unsound
   MN-BAB (64-bit, GPU)	unsound	sound	unsound	unsound	unsound
   β-CROWN BaB (32-bit, CPU)	unsound	sound	unsound	unsound	not reported (no 32-bit model)
   β-CROWN BaB (64-bit, CPU)	unsound	sound	unsound	unsound	sound
   β-CROWN BaB (64-bit, GPU)	unsound	sound	unsound	unsound	sound
   GCP-CROWN (64-bit, CPU)	unsound	sound	unsound	unsound	sound
   DeepPoly (64-bit, CPU)	unsound	sound	sound	unsound	sound
   RefinePoly (64-bit, CPU)	unsound	sound	sound	unsound	unsound
   DeepZ (64-bit, CPU)	unsound	sound	sound	unsound	sound
   RefineZono (64-bit, CPU)	unsound	sound	sound	unsound	not reported (Gurobi error)

   • The authors state that none of the tested methods is practically sound: all miss the Order3 and Precision networks.
   • The authors state that the harder the task, the more verifiers fail; the partial success on Order2 is attributed by the authors to wider intervals and accidental coverage by the operation order, and they state that there is no theoretical guarantee.
   • The authors state that all verifiers are vulnerable to the Precision attack, supporting that verifiers should be tailored to specific floating-point precisions.

   Backdoor effectiveness (Section 8.2)

   • Precision attack: the network triggered in 32-bit has test accuracy 0.11% in the 32-bit environment and 98.11% in 64-bit; the network triggered in 64-bit is the exact opposite (Table 1).
   • Order attacks: at batch size 1, Order1 is 0.11% on PyTorch CPU/GPU and Flux GPU, and 98.11% on Flux CPU; Order2 is 0.11% only on Flux GPU; Order3 is 98.11% in all 8 environments (Table 2).
   • Authors' interpretation: the three backdoors are activated in at least one environment, showing that these environments execute different expression trees; no trigger was observed for Order3, but the authors argue this does not mean the network is safe, and a sound verifier should still detect it.

   Comparison with Zombori et al., 2021 (Section 8.5)

   • What was tested: a reproduction of the network of Zombori et al., 2021 (similar to Order1), which triggers the verifier's own numerical error.
   • Results: MIPVerify, MN-BAB, and RefinePoly are unsound on this attack, while DeepPoly, DeepZ, β-CROWN (64-bit), and GCP-CROWN are sound (Table 3).
   • Authors' interpretation: this attack is effective only against verifiers that use a certain optimization; the attacks in this paper exploit the difference between the full-precision model and the deployment, among which the strongest, Precision and Order3, are effective against all verifiers that have only theoretical soundness.

   Other ablations and analyses

   • Effect of batch size: after changing batch size from 1 to 10, the triggering of Order1 on PyTorch GPU and Flux CPU flips (Table 2).
   • MIPVerify details: for the Precision attack it incorrectly outputs 97 safe answers; for Order2 and Order3 it incorrectly verifies 97% robust accuracy (Appendix C.2.1).
   • RefinePoly details: for Order3 it incorrectly reports 96% robust accuracy, and the MILP solver errors on the remaining 4 samples (Appendix C.2.2).
   • GCP-CROWN details: for the undetected backdoor it incorrectly reports 97 safe results, and errors on the remaining 3 samples (Appendix C.2.4).

   Collapse this answer

5. 05What are some points that can be further explored?

   The authors note that this paper does not provide an implementation plan for a practically sound verifier; the experiments cover only one MNIST network and 10 verifier configurations.

   Limitations and future directions noted by the authors

   • No solution proposed: the authors explicitly state that this paper contains no proposal for implementing a practically sound verifier, focuses only on exposing the problem, and considers solving the problem important (Section 9).
   • Strong assumptions about the environment required: the authors believe a practically sound verifier must make strong assumptions about the deployment environment, otherwise the problem becomes prohibitively costly; a deterministic environment is an advantage, but verification must know and exploit every detail of the environment (Section 9).
   • Applicability conditions for bound propagation: the authors believe bound propagation is practically sound only when it follows a deterministic expression tree and the propagation accounts for the environment's (deterministic) precision and rounding rules (Section 9).
   • Backdoors are easy to detect: the authors note that this paper's backdoor weights are large and input-independent, making them fairly easy to detect, because the motivation is theoretical, so aspects of actually implementing an attack were largely ignored (Appendix B).
   • Ideas for reducing detectability: the authors suggest spreading large weights across multiple layers, or making the backdoor effective only for specific input perturbations (e.g., requiring both that a certain pixel exceeds a threshold and that the precision is 32-bit), but this is not implemented in the paper (Appendix B).

   Scope of experiments

   • The attacked network is 1 MNIST convolutional network (WK17a, the checkpoint of Wong & Kolter, 2018); the paper does not report experiments on other datasets or architectures.
   • There are 8 verifiers in 10 configurations, all based on IBP, Polyhedra, or Zonotope bound propagation class methods (Table 3).
   • The verification evaluation uses the first 100 samples of the MNIST test set; the paper does not report the number of repetitions (Section 8.4, Appendix C.2).
   • Deployment environments cover 8 in total: PyTorch and Flux × CPU/GPU × batch size 1/10; hardware and software versions are given in Appendix C.1.
   • The theoretical analysis targets the summation function with zero-length interval inputs; the authors state that more complex function classes would inherit these problems, but no proof is given for other function classes.

   Collapse this answer

6. 06Summarize the main content of the paper

   The authors state that theoretically sound verifiers are not sound for deployment, provide a proof, and use environment-triggered backdoors to make all 10 verifier configurations miss detection.

   An attack and analysis paper on the reliability of neural network verification, arguing that the verification target should shift from the full-precision theoretical model to the actually deployed model.

   • Problem: deployment environments, through floating-point non-associativity and randomness, make the deployed network a different mathematical object from the theoretical model; the authors state that the state-of-the-art verifiers they know of verify only the theoretical model, and theoretical soundness does not imply practical soundness.
   • Method: formalize the deployment verification problem (Equation 2); prove on the summation function that IBP generally does not cover the extrema of the deployed output (Proposition 6.2), and that Polyhedra and Zonotope class symbolic methods degenerate to interval methods in this special case and are likewise unsound (Proposition 6.4, 6.5); construct input-independent detector backdoors triggered by precision or operation order and embed them in an MNIST network.
   • Backdoor effectiveness: when the Precision backdoor is triggered, test accuracy drops from 98.11% to 0.11% (Table 1); Order1 and Order2 are triggered in at least one of 8 deployment environments, while Order3 was not observed to trigger (Table 2).
   • Main results: 10 verifier configurations (MIPVerify, MN-BAB, β-CROWN BaB×3, GCP-CROWN, DeepPoly, RefinePoly, DeepZ, RefineZono) all judge the Precision and Order3 attacks as unsound, i.e., they miss the backdoor (Table 3, first 100 MNIST test samples).
   • Comparison: the attack of Zombori et al., 2021 is effective only against some verifiers that use optimization; the authors state that this paper's attack exploits the discrepancy between the model and the deployment and is generally effective against verifiers with only theoretical soundness.
   • Authors' conclusion: verification should focus on the behavior of the deployed network; a practically sound verifier may need strong assumptions about the deployment environment (e.g., a deterministic environment following its expression tree), and this paper does not provide an implementation plan.

   Collapse this answer

Related papers