Pith. sign in

REVIEW 3 major objections 5 minor 2 cited by

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

T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper proves that theoretically sound neural verifiers are not sound for deployed networks, and shows every tested verifier misses its backdoors.

desk verdict A clean, correct proof that interval-based verifiers are not practically sound for sum-like computations, but the paper's universal title claim outruns its formal results. read the letter →

arxiv 2506.01054 v1 pith:52MBQUTA submitted 2025-06-01 cs.LG

Attila Szász , Balázs Bánhelyi , Márk Jelasity This is my paper
classification cs.LG
keywords neuralnetworkverificationsoundnessfloatingpointarithmeticnon-associativitydeploymentenvironmentbackdoorattackintervalboundpropagationadversarialrobustness
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper argues that the formal verification of neural networks, as currently practiced, does not guarantee the safety of the networks once deployed. The authors distinguish theoretical soundness—bounding the full-precision mathematical model—from practical soundness—bounding the actual floating-point output in a deployment environment that may be stochastic. They prove that theoretical soundness does not imply practical soundness for interval analysis and for zonotope-based widening, and they construct adversarial networks with backdoors triggered by environment features such as floating-point precision and operation order. Empirically, every state-of-the-art verifier they tested missed the strongest backdoors. If the claim holds, any verification that ignores the deployment environment can certify networks that behave maliciously in the field.

What carries the argument

The load-bearing objects are the deployed network $r(x;\theta,E)$ and the special floating-point number $\omega$, defined as the smallest representable positive number whose successor is $\omega+2$ ($\omega=2^{24}$ in binary32, $2^{53}$ in binary64). The environment $E$ is modelled by the number representation, rounding mode, and the set of possible binary expression trees with non-zero probability; because floating-point addition is non-associative, different trees give different outputs. The proofs show that interval arithmetic on one tree can exclude the true extremal value $L_r$ or $U_r$, so the verifier's interval is not practically sound, and detector neurons built from sums like $\omega+1-\omega$ trigger adversarial behavior exactly when the deployment evaluation order differs from the verifier's assumption.

What would settle it

Run a verifier that explicitly models every expression tree in the deployment set, for example by exhaustive enumeration of tree shapes for the detector sum in Equation (5), and check whether it bounds all observed outputs across the eight environments of Table 2. If such a verifier certifies the Order3 backdoored network as robust while the network flips classes in one of those environments, the claim that environment-blind verifiers are unsound would be falsified; if it succeeds, the negative result is limited to methods that ignore the environment.

Watch

Extended reading notes

Core claim

The central discovery is that the deployed network is a different mathematical object from the full-precision model: floating-point arithmetic is non-associative, so the same network can produce different outputs depending on the expression tree, rounding mode, and precision chosen by hardware and software. The deployed function $r(x;\theta,E)$ is defined over a set of possible outputs, and a practically sound verifier must bound every possible output. The paper proves (Propositions 6.2 and 6.5) that interval bound propagation and zonotope widening, evaluated on a single expression tree, can miss the true minimum or maximum floating-point output even for a sum of constants. It then shows how detector neurons using the number $\omega$ can make a deployed network behave arbitrarily while the full-precision model looks safe, and demonstrates that the tested verifiers certify the backdoored networks as robust.

Load-bearing premise

The argument depends on modelling the deployment environment as a set of possible expression trees, rounding modes, and precisions with possibly random choice among them; if a particular deployment is deterministic with a single known evaluation order, the proof's negative conclusion does not apply.

Editorial extensions

If this is right

  • A verifier that is only theoretically sound can certify a network that is unsafe in a stochastic deployment, because the certification is about the wrong function.
  • Practical soundness requires knowing or bounding the set of possible expression trees in the deployment environment, which is generally harder than the theoretical verification problem.
  • Deterministic deployment with a known expression tree restores practical soundness, because interval propagation along the actual tree bounds the actual output.
  • Backdoor detectors can be embedded into any network using the paper's construction, so the attack does not require altering the input.
  • The same proof strategy extends to symbolic bound propagation methods, which reduce to interval analysis on the sum-of-constants case.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If accepted, this result shifts the verification target: certification should be issued for a specific deployment environment, not for a network in the abstract.
  • A natural extension is to test whether enumerating all expression trees for small sums, or using exact rational arithmetic, yields practically sound bounds; the paper does not implement such a verifier.
  • The same deployment-gap argument likely applies to other non-associative computations beyond sums, such as matrix multiplications in convolutions, though the paper proves the worst-case only for sums.
  • Standardized benchmark pairs of verifier and deployment environment would be a concrete next step for comparing practical soundness.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper argues that neural network verifiers which are sound with respect to a full-precision, theoretical model of a network are not necessarily sound with respect to the actually deployed, floating-point implementation in a given environment. It formalizes the deployed network r(.;θ,E) as a function whose output set is determined by the environment E (number representation, rounding mode, and a set of possible expression trees with nonzero probability). It proves that interval bound propagation (IBP) and zonotope-based widening can fail to cover the full deployed output range, even for the simple function f(x)=Σx_i with constant representable inputs (Propositions 6.2, 6.3, 6.5). It then constructs backdoored MNIST networks containing detector neurons that are triggered by precision or expression-tree order, and empirically shows that ten configurations of six state-of-the-art verifiers all fail to detect the precision backdoor and the hardest order backdoor (Table 3). The paper concludes that 'theoretical soundness does not imply practical soundness' and that the deployment environment should be part of the verification problem.

Significance. If the result is taken at face value, it is significant: it challenges the common practice of verifying a full-precision model while ignoring the nondeterminism of floating-point execution, and it provides a concrete attack that the tested verifiers provably miss. The formal counterexamples for interval and zonotope bound propagation are simple, explicit, and correctly proved; they are a genuine and useful addition to the literature. The paper also gives credit where due: it ships source code, specifies hardware/software environments, and includes the proofs in the appendix. The main weakness is that the formal results cover only the sum of constants, while the sweeping title and abstract claim a universal absence of practical soundness for all verifiers. The empirical evaluation is solid but limited to 100 MNIST inputs and ten configurations, so the universal conclusion rests on an unproven transfer from the sum-of-constants counterexample to arbitrary ReLU networks. With a rigorous transfer argument or appropriately scoped claims, this would be an accept-quality contribution.

major comments (3)
  1. [§6.1, §7, Appendix B] The formal results (Propositions 6.2, 6.3, 6.5) are proved only for the function f(x)=Σx_i with constant representable inputs. The paper asserts in §6.1 that generalizations to neural network architectures 'will inherit these problems', but no theorem in the paper proves that any theoretically sound verifier of a full ReLU network must miss the embedded detector. Appendix B describes a backdoor construction and Table 3 gives empirical evidence on ten verifier configurations, but that does not establish the universal claim 'no soundness in the real world'. Indeed, Table 3 shows that Order2 is detected by six of the ten configurations, demonstrating that ReLU propagation and verifier-specific widening can cover adversarial outputs even when IBP on a fixed default tree would not. The authors should either prove a transfer theorem (e.g., showing that for the embedded detector, the bounds computed by any interval or zonotope verifier on the full network are exactly the bounds on the corresponding sum, up to ReLU composition) or explicitly limit the scope of the theoretical claim to the sum function and treat the neural-network failure as an empirical observation on the tested verifiers.
  2. [§5.1, §6.1, §9] The negative results rely on a specific modeling choice: practical soundness is defined as bounding the output for every expression tree in the set E, and the counterexamples require an E that contains 'every correct expression tree'. The paper itself acknowledges in §9 that deterministic environments are an advantage and that IBP following the deterministic expression tree is practically sound (Proposition 6.1). Hence the abstract's claim that 'all the state-of-the-art verifiers we are aware of fail to reach this goal' is an overstatement: a verifier that is explicitly given the deterministic tree and the deployment precision would be practically sound by Proposition 6.1. The universal claim should be scoped to environments with multiple or stochastic expression trees, or the environment model should be defended as the only realistic threat model. As written, the paper risks conflating 'not practically sound for every possible E' with 'not practically sound for any interesting deployment'.
  3. [§8.2.2, Table 2, §8.4, Table 3] The Order3 column in Table 3 labels every verifier as unsound even though Table 2 shows that the Order3 adversarial behavior is not triggered in any of the eight deployment environments tested (accuracy is 98.11% in all environments). The justification in §8.4 is that it is hard to model the set of possible expression trees, so a practically sound verifier should be prepared for all of them. This is a normative threat-model decision, not a demonstrated empirical failure. Under the paper's own definition of E as the set of trees with nonzero probability in a given environment, if the triggering tree has zero probability in the tested environments, then missing the backdoor is not practical unsoundness for those environments. To support the Order3 unsound verdict, the authors should either exhibit a concrete environment where Order3's adversarial behavior occurs (or a reproducible stochastic model with nonzero triggering probability), or explicitly state that they are adopting a conservative universal-E threat model and separate that definitional claim from the empirical evaluation.
minor comments (5)
  1. [§6 and Table 3] The labels 'sound' and 'unsound' in Table 3 describe whether the verifier detected the backdoor, which is not the standard use of 'sound' in verification. The paper should define these labels operationally (e.g., 'detected' vs. 'missed') or explicitly state that 'sound' here means 'correctly reported 0% verified robust accuracy'.
  2. [Appendix A.2, proof of Proposition 6.5] The notation in the proof is sloppy: 'the multiset of nine 1s and ω {1,1,1,1,1,1,1,1,1,ω}' is missing a set brace and the count is ten numbers, not nine. Also, the variables δ_l and δ_u are said to satisfy '0<δ_l ≪1' without a precise bound, which makes the inequalities in Equations (9) and (10) slightly informal.
  3. [§4.4] The example '253 + 1 − 253 = 0 when computed in double-precision arithmetic and with rounding towards −∞' is correct for double precision, but the text uses '253' without a superscript; using 2^{53} and 2^{24} consistently would improve readability.
  4. [§6.3] The statement 'We hypothesize that finding the expression tree that maximizes or minimizes the output is an NP-hard problem in general' is accompanied by a citation to Kao & Wang for a 'very similar problem'. Since this is only a hypothesis and is not used later (the paper only claims that approximation is not enough), it could be moved to future work or made conditional.
  5. [Appendix C.2.1] In the MIPVerify description, the sentence 'MIPVerify was attacked using the 32-bit adversarial precision backdoor, leading to incorrect outputs of 97 safe answers' is unclear: it is the verifier's verification result that is incorrect, not the 'outputs of MIPVerify' in the sense of the network output. Please rephrase to avoid ambiguity.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the unsoundness theorems rest on explicit counterexamples, not on self-referential predictions.

full rationale

The paper's central formal claims are self-contained. Proposition 6.2 is proved by constructing explicit witness inputs and expression trees (e.g., (1+1)+omega with appropriate rounding modes) and showing that the interval evaluation misses L_r or U_r. Proposition 6.5 is likewise proved with explicit multisets and zonotope widening formulas from Miné (2004). No parameter is fitted to verifier outputs and no empirical result is renamed as a theoretical prediction: the attack networks in Section 7 are constructive witnesses to the claimed gap, and the empirical Table 3 tests whether those witnesses defeat existing verifiers. The only potentially definitional element is the model of the deployment environment E in Sections 5.1 and 6.1, where practical soundness is defined as bounding every output over all expression trees with nonzero probability; the negative theorems are then derived from that definition with explicit arithmetic examples rather than assumed. The generalization from constant-sum counterexamples to full ReLU networks is an extrapolation supported by construction, not a circular reduction. The paper does cite the authors' prior work (Zombori et al., 2021) for the backdoor insertion method, but that citation is methodological and not load-bearing for the formal theorems, and the construction is described in Section B with released code. This is at most a minor self-citation, well below the threshold for circularity.

Assumptions & free parameters 3 free parameters · 4 assumptions · 2 invented entities

The formal core is self-contained; the listed free parameters are only attack construction constants. The load-bearing assumptions are the representation of a deployment environment by a set of possible expression trees and the requirement that a practically sound verifier covers all of them, plus the demonstrated but not formally proven embedding of detectors into general networks. These are the assumptions a rebuttal would need to challenge.

free parameters (3)
  • h1, h2 = 4, 15
    Manual construction constants for the Order1 detector (Equation 3); they set the number of repeated summands but do not affect the central proof.
  • h = 512
    Manual construction constant for the Order2 and Order3 detectors (Equations 4 and 5); chosen to make the default tree output distinguishable from the triggered zero output.
  • alpha, beta backdoor shifts = alpha1=1, alpha2=-2, beta1=0, beta2=1 and swapped
    Manual parameters in Section B that decide whether detector output zero or non-zero shifts the logits; needed for the specific attack implementation.
assumptions (4)
  • domain assumption IEEE 754 floating point with a fixed rounding mode is a faithful model of the deployed computation.
    Used throughout Section 4.4 and the proofs; standard for numerical analysis but not the only possible deployment model.
  • ad hoc to paper A deployment environment E can be represented by the number representation, rounding mode, and the set of possible expression trees, and a practically sound verifier must cover all trees in that set.
    This definition in Sections 5.1 and 6.2 is what makes the negative result meaningful; if the environment is deterministic and known, Proposition 6.1 gives soundness.
  • domain assumption The detector neurons can be embedded into an arbitrary ReLU network using the method of Zombori et al. without changing the verifier's view of the theoretical model.
    This is the bridge in Sections 7 and B from the sum-of-constants counterexample to general neural networks; it is demonstrated by construction, not formally proven.
  • standard math Standard arithmetic background: interval arithmetic with outward rounding contains the full-precision value.
    Used in Proposition 6.1(1) and the appendix; textbook result.
invented entities (2)
  • Precision detector neuron (omega + 1 - omega) independent evidence
    purpose: Triggers on a mismatch between the verifier's assumed floating-point precision and the deployment precision, producing different outputs in 32-bit and 64-bit environments.
    The detector is a concrete construction whose behavior is verified empirically in Table 1 across 32-bit and 64-bit inference.
  • Expression-tree detector neurons (Order1, Order2, Order3) independent evidence
    purpose: Trigger on the order in which floating-point additions are performed, so the deployed output can differ from the full-precision output.
    These are explicit witnesses to the theoretical gap; Table 2 shows activation in different framework, hardware, and batch-size environments. Independent evidence is the observable accuracy difference, not a fitted claim.

how reviews work

0 comments
Cite this review

Pith. "Pith review of No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks." pith.science (2026). https://pith.science/paper/52MBQUTA

@misc{pith2026250601054,
  author       = {Pith},
  title        = {Pith review of: No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/52MBQUTA}},
  note         = {Machine review of arXiv:2506.01054}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2506.01054 by the authors.

Figure 1
Figure 1. A malicious binary classifier with a 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 (E3) where a malicious behavior (flipping classes) manifests itself. An input x and its sensitivity domain are also shown. The work of (Zombori et al., 2021) also addresses num… view at source ↗
Figure 2
Figure 2. Backdoor integration. Circles represent ReLU neurons with the parameter inside the circle being the bias term. Simple arrows represent connections with the weights indicated on them. the weight matrix (assuming a row input vector), with the last n elements configured according to the detectors and the remaining elements set to zero. The bias is also configured according to the detector patterns. The shifting mechani… view at source ↗

Discussion (0). Sign in to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Lipschitz-Based Robustness Certification Under Floating-Point Execution

    cs.LG 2026-03 conditional novelty 7.0 of 10 partial

    Lipschitz-based robustness certificates that assume real arithmetic can be unsound under floating-point execution; a formal FP-aware theory and certifier close that gap for dense ReLU networks.

  2. TAO: Tolerance-Aware Optimistic Verification for Floating-Point Neural Networks

    cs.CR 2025-10 conditional novelty 7.0 of 10

    A tolerance-aware optimistic verification protocol makes floating-point neural-network inference verifiable on heterogeneous GPUs by accepting outputs within per-operator error bounds and resolving disputes via a Merk...

Reference graph

Works this paper leans on

41 extracted references · 30 canonical work pages · cited by 2 Pith papers

  1. [1]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION format.date year duplicate empty "emp...

  2. [2]

    Introduction to neural network verification

    Albarghouthi, A. Introduction to neural network verification. Foundations and Trends in Programming Languages, 7 0 (1-2): 0 1--157, 2021. ISSN 2325-1107. doi:10.1561/2500000051. URL http://dx.doi.org/10.1561/2500000051

    doi:10.1561/2500000051 2021

  3. [3]

    and Herzberger, J

    Alefeld, G. and Herzberger, J. Introduction to Interval Computation. Academic Press, 1983. ISBN 9780120498208

    work page 1983

  4. [4]

    Bunel, R., Lu, J., Turkaslan, I., Torr, P. H. S., Kohli, P., and Kumar, M. P. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21 0 (42): 0 1--39, 2020. URL http://jmlr.org/papers/v21/19-468.html

    work page 2020

  5. [5]

    C., Daggitt, M

    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 challenge. In Vafeiadis, V. (ed.), Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the...

    work page 2025

  6. [6]

    de Figueiredo, L. H. and Stolfi, J. Affine arithmetic: Concepts and applications. Numer. Algorithms, 37 0 (1-4): 0 147--158, 2004. doi:10.1023/B:NUMA.0000049462.70970.B6. URL https://doi.org/10.1023/B:NUMA.0000049462.70970.b6

    arXiv 2004

  7. [7]

    Output range analysis for deep feedforward neural networks

    Dutta, S., Jha, S., Sankaranarayanan, S., and Tiwari, A. Output range analysis for deep feedforward neural networks. In Dutle, A., Mu \ n oz, C. A., and Narkawicz, A. (eds.), NASA Formal Methods - 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings , volume 10811 of Lecture Notes in Computer Science, pp.\ 121--138...

    work page doi:10.1007/978-3-319-77935-5 2018

  8. [8]

    Formal verification of piece-wise linear feed-forward neural networks

    Ehlers, R. Formal verification of piece-wise linear feed-forward neural networks. In D'Souza, 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 10482 of Lecture Notes in Computer Science, pp.\ 269--286. Springer, 2017. doi:10.1007/9...

    work page doi:10.1007/978-3-319-68167-2 2017

Show all 41 references
  1. [9]

    N., Jovanovic, N., and Vechev, M

    Ferrari, C., M \" u ller, M. N., Jovanovic, N., and Vechev, M. T. Complete verification via multi-neuron relaxation guided branch-and-bound. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022 . OpenReview.net, 2022. U...

    2022

  2. [10]

    The zonotope abstract domain taylor1+

    Ghorbal, K., Goubault, E., and Putot, S. The zonotope abstract domain taylor1+. In Bouajjani, A. and Maler, O. (eds.), Computer Aided Verification, pp.\ 627--633, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. ISBN 978-3-642-02658-4

    2009

  3. [11]

    A., and Kohli, P

    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.12715, 2018. URL http://arxiv.org/abs/1810.12715

    arXiv

  4. [12]

    A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability

    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: Verification, testing, adversarial attack and defence, and interpretability. Comput. Sci. Rev., 37: 0 100270, 2020. doi:10.1016/...

    2020

  5. [13]

    and Rinard, M

    Jia, K. and Rinard, M. Exploiting verified neural networks via floating point numerical error. In Dr a goi, C., Mukherjee, S., and Namjoshi, K. (eds.), Static Analysis, pp.\ 191--205, Cham, 2021. Springer International Publishing. ISBN 978-3-030-88806-0

    2021

  6. [14]

    and Wang, J

    Kao, M.-Y. and Wang, J. Linear-time approximation algorithms for computing numerical summation with provably small errors. SIAM J. Comput., 29 0 (5): 0 1568–1576, March 2000. ISSN 0097-5397

    2000

  7. [15]

    L., Julian, K., and Kochenderfer, M

    Katz, G., Barrett, C., Dill, D. L., Julian, K., and Kochenderfer, M. J. Reluplex: An efficient smt solver for verifying deep neural networks. In Majumdar, R. and Kun c ak, V. (eds.), Computer Aided Verification, pp.\ 97--117, Cham, 2017. Springer International Publishing. ISBN...

    2017

  8. [16]

    J., and Bengio, S

    Kurakin, A., Goodfellow, I. J., and Bengio, S. Adversarial machine learning at scale. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings , 2017. URL https://openreview.net/forum?id=BJm4T4Kgx

    2017

  9. [17]

    Sok: Certified robustness for deep neural networks

    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.\ 1289--1310. IEEE , 2023. doi:10.1109/SP46215.2023.10179303. URL https://doi.org/10.1109/SP462...

    2023

  10. [18]

    A., Barrett, C

    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., 4 0 (3-4): 0 244--404, 2021. doi:10.1561/2400000035. URL https://doi.org/10.1561/2400000035

    2021 doi

  11. [19]

    Sound mixed fixed-point quantization of neural networks

    Lohar, D., Jeangoudoux, C., Volkova, A., and Darulova, E. Sound mixed fixed-point quantization of neural networks. ACM Trans. Embed. Comput. Syst. , 22 0 (5s): 0 136:1--136:26, 2023. doi:10.1145/3609118. URL https://doi.org/10.1145/3609118

    2023 doi

  12. [20]

    Towards deep learning models resistant to adversarial attacks

    Madry, A., Makelov, A., Schmidt, L., Tsipras, D., and Vladu, A. Towards deep learning models resistant to adversarial attacks. In International Conference on Learning Representations, 2018. URL https://openreview.net/forum?id=rJzIBfZAb

    2018

  13. [21]

    Relational abstract domains for the detection of floating-point run-time errors

    Min \'e , 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

    2004

  14. [22]

    Differentiable abstract interpretation for provably robust neural networks

    Mirman, M., Gehr, T., and Vechev, M. Differentiable abstract interpretation for provably robust neural networks. In Dy, J. and Krause, A. (eds.), Proceedings of the 35th International Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Research, pp.\ 3...

    2018

  15. [23]

    D., Behl, H

    Palma, A. D., Behl, H. S., Bunel, R., Torr, P. H. S., and Kumar, M. P. Scaling the convex barrier with active sets. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021 . OpenReview.net, 2021. URL https://openreview.net/...

    2021

  16. [24]

    Sanders, D. P. and Benet, L. Intervalarithmetic.jl, 2014. URL https://github.com/JuliaIntervals/IntervalArithmetic.jl

    2014

  17. [25]

    o gl, A., Hofer, N., and B \

    Schl \" o gl, A., Hofer, N., and B \" o hme, R. Causes and effects 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 Syste...

    2023

  18. [26]

    R., Coletti, M., and Sedova, A

    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 Comput...

    2024

  19. [27]

    R., and Sedova, A

    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 vulnerability. CoRR, abs/2503.17173, 2025. doi:10.48550/ARXI...

    2025 doi arXiv

  20. [28]

    Singh, G., Gehr, T., Mirman, M., P \" u schel, M., and Vechev, M. T. Fast and effective robustness certification. In Bengio, S., Wallach, H. M., Larochelle, H., Grauman, K., Cesa - Bianchi, N., and Garnett, R. (eds.), Advances in Neural Information Processing Systems 31: Annua...

    2018

  21. [29]

    An abstract domain for certifying neural networks

    Singh, G., Gehr, T., P\" u schel, M., and Vechev, M. An abstract domain for certifying neural networks. Proc. ACM Program. Lang., 3 0 (POPL), January 2019 a . doi:10.1145/3290354. URL https://doi.org/10.1145/3290354

    2019 doi

  22. [30]

    Boosting robustness certification of neural networks

    Singh, G., Gehr, T., Püschel, M., and Vechev, M. Boosting robustness certification of neural networks. In International Conference on Learning Representations (ICLR). 2019 b

    2019

  23. [31]

    uller, C., Maurer, J., Hoffmann, A., Baader, M., Mirman, M., Gehr, T., Tsankov, P., Drachsler Cohen, D., P\

    Singh, G., Balunovic, M., Ruoss, A., M\"uller, C., Maurer, J., Hoffmann, A., Baader, M., Mirman, M., Gehr, T., Tsankov, P., Drachsler Cohen, D., P\"uschel, M., and Vechev, M. ERAN user manual, 2025. URL https://files.sri.inf.ethz.ch/eran/docs/eran_manual.pdf. accessed: 2025:01:13

    2025

  24. [32]

    J., and Fergus, R

    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/1312.6199

    2014 arXiv

  25. [33]

    Y., and Tedrake, R

    Tjeng, V., Xiao, K. Y., and Tedrake, R. Evaluating robustness of neural networks with mixed integer programming. In International Conference on Learning Representations, 2017. URL https://api.semanticscholar.org/CorpusID:47016770

    2017

  26. [34]

    Effects of floating-point non-associativity on numerical computations on massively multithreaded systems

    Villa, O., Chavarr \' i a-Miranda, D., Gurumoorthi, V., M \' a rquez, A., and Krishnamoorthy, S. Effects of floating-point non-associativity on numerical computations on massively multithreaded systems. In Proceedings of the Cray User Group Meeting (CUG), 2009. URL https://cug...

    2009

  27. [35]

    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 neural network robustness verification. In Ranzato, M., Beygelzimer, A., Dauphin, Y. N., Liang, P., and Vaughan, J. W. (ed...

    2021

  28. [36]

    and Kolter, Z

    Wong, E. and Kolter, Z. Provable defenses against adversarial examples via the convex outer adversarial polytope. In Dy, J. and Krause, A. (eds.), Proceedings of the 35th International Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Research, pp.\ ...

    2018

  29. [37]

    Automatic perturbation analysis for scalable certified robustness and beyond

    Xu, K., Shi, Z., Zhang, H., Wang, Y., Chang, K., Huang, M., Kailkhura, B., Lin, X., and Hsieh, 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 Neural Infor...

    2020

  30. [38]

    Fast and Complete : Enabling complete neural network verification with rapid and massively parallel incomplete verifiers

    Xu, K., Zhang, H., Wang, S., Wang, Y., Jana, S., Lin, X., and Hsieh, C.-J. Fast and Complete : Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference on Learning Representations, 2021. URL https://openr...

    2021

  31. [39]

    Efficient neural network robustness certification with general activation functions

    Zhang, H., Weng, T., Chen, P., Hsieh, C., and Daniel, L. Efficient neural network robustness certification with general activation functions. In Bengio, S., Wallach, H. M., Larochelle, H., Grauman, K., Cesa - Bianchi, N., and Garnett, R. (eds.), Advances in Neural Information ...

    2018

  32. [40]

    Zhang, H., Wang, S., Xu, K., Li, L., Li, B., Jana, S., Hsieh, C., and Kolter, J. 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. (eds.), Advances in Neural Information...

    2022

  33. [41]

    Fooling a complete neural network verifier

    Zombori, D., B \' a nhelyi, B., Csendes, T., Megyeri, I., and Jelasity, M. Fooling a complete neural network verifier. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021 . OpenReview.net, 2021. URL https://openreview.n...

    2021

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.