Pith. sign in

REVIEW 3 major objections 5 minor 55 references

Lipschitz-Based Robustness Certification Under Floating-Point Execution

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

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

Pith's one-line read Classical Lipschitz-based robustness certificates assume real arithmetic and can be false under floating-point execution; this paper derives sound floating-point-aware certification conditions for dense ReLU networks.

desk verdict The FP deviation theory is a real step forward, but the main theorem has an unaccounted input-rounding gap and the paper ships neither code nor proofs. read the letter →

arxiv 2603.13334 v6 pith:QWIPP43B submitted 2026-03-06 cs.LG cs.CVcs.PL

Toby Murray This is my paper · ORCID
classification cs.LGcs.CVcs.PL
keywords robustnesscertificationfloating-pointerrorLipschitzboundsReLUnetworksroundinganalysisneuralnetworkverificationcertifiedoverflow
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

The paper establishes that Lipschitz-based robustness certificates, which are computed by numerical sensitivity bounds under an assumed real-arithmetic model, can certify inputs as robust when the actually deployed floating-point network would misclassify a nearby input. It then builds a compositional theory, specialised to feed-forward ReLU networks, that relates real-arithmetic sensitivity bounds to floating-point execution under the standard round-to-nearest error model. The main result, Theorem 6.2, gives a checkable condition: if the observed floating-point margin at the centre point, minus the Lipschitz-radius term and minus two provable error bounds (one for the centre execution, one for any point in the ball), is positive, then floating-point classification is preserved throughout the ball. The paper also provides layerwise overflow-freedom conditions, a cumulative deviation bound via a two-coefficient linear recursion, and a hybrid pre-deployment method that uses high-precision measurements to reduce certificate degradation. If correct, it is the first sound and practical Lipschitz-based certifier that accounts for floating-point execution.

What carries the argument

The central object is the floating-point deviation vector between the floating-point-executed and real-arithmetic activations at each layer. The paper bounds its norm uniformly over the perturbation ball by a scalar satisfying a two-coefficient linear recursion, where one coefficient is an amplification factor (essentially the layer's spectral norm plus a floating-point correction) and the other captures fresh rounding error in terms of a deterministic activation-radius bound. Overflow-freedom is certified layerwise by two scalar inequalities, and the final-layer analysis specialises the deviation to each output margin to produce the two error bounds used in the main certification theorem. T

What would settle it

Find a dense ReLU network and a point satisfying all conditions of Theorem 6.2, then execute it in IEEE float32 on a standards-conforming platform and locate any nearby point whose argmax differs; because the theorem is machine-checked, such a case would point to a gap in the error model rather than the proof. Alternatively, a single input where the measured deviation between floating-point and real-arithmetic activations exceeds the certified bound would directly falsify the deviation recursion.

Watch

Extended reading notes

Core claim

The central claim is that a real-arithmetic Lipschitz certificate can be made sound for floating-point execution by adding a worst-case margin degradation term. For each competitor class, the paper defines two error bounds, one for the centre point and one for any point in the perturbation ball, built from layerwise deviation bounds and a final-layer pairwise analysis. Theorem 6.2 states that if overflow-freedom holds over the ball, each margin is Lipschitz in the real-arithmetic sense, and the actual floating-point margin at the centre minus the Lipschitz-radius term minus the two error bounds is positive, then every point in the ball has positive floating-point margin and the floating-poin

Load-bearing premise

The certificates rely on the deployed runtime conforming to the standard rounding model: round-to-nearest ties-to-even, gradual underflow, no fused or re-associated operations, and no flush-to-zero.

Editorial extensions

If this is right

  • Real-arithmetic Lipschitz certificates are not automatically sound for deployed networks: the paper exhibits counterexamples, including at float32 with adversarially modified weights, where a verified certifier claims robustness yet a nearby input is misclassified.
  • The certification condition of Theorem 6.2 quantifies the price of floating-point soundness; for MNIST and Fashion MNIST at float32 the price is small (0.24 and 1.49 percentage points of certified coverage), while CIFAR-10 loses 27.22 points.
  • The method rejects every counterexample instance that fools the real-arithmetic certifier, across all tested floating-point formats and models, including the adversarially biased model.
  • At float16, and for models with injected large biases even at float32, certification becomes vacuous (0% of test points) while remaining sound, showing the limits of worst-case deviation bounds at low precision.
  • The pre-deployment hybrid method, which measures actual deviation against a high-precision execution, substantially reduces margin degradation and scales to full 10,000-point test sets.

Reading between the lines

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

  • The deviation recursion supplies a per-layer rounding-amplification profile of a network; this could be used as a diagnostic to identify which layers most amplify floating-point error and to target mixed-precision training there.
  • The margin-degradation formula suggests a testable prediction: models with larger spectral norms relative to their floating-point format should show systematically larger certificate loss, so retraining with smaller Lipschitz constants should recover much of the lost certified coverage.
  • Since the theory only assumes floating-point-exact activations, extending it to smooth activations like tanh would require adding activation-rounding terms to the fresh-error coefficient; the recursion structure suggests a natural place to insert them.
  • The vacuousness at float16 hints that worst-case bounds are intrinsically too loose for low-precision deployment; probabilistic or input-specific deviation bounds, or per-instance hybrid measurements, may be the only route to non-vacuous low-precision certification.
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 investigates the gap between real-arithmetic Lipschitz-based robustness certification and actual floating-point execution of dense ReLU networks. It first demonstrates the gap with counterexamples, then develops a compositional theory: layer-wise overflow-freedom conditions (Section 4), a linear recursion bounding the deviation between floating-point and real activations (Section 5), and a floating-point robustness certificate condition (Theorem 6.2, Section 6). It also proposes a hybrid pre-deployment method that tightens the center-point error bound using high-precision execution (Section 7), reports an implementation and evaluation on MNIST, Fashion MNIST, and CIFAR-10 (Section 8), and claims a Rocq/LAProof formalization of the main results. The central claim is that Theorem 6.2 is the first sound Lipschitz-based robustness certificate under standard floating-point semantics for dense ReLU networks at practical scale.

Significance. If the proof of Theorem 6.2 is correct in its stated form, the paper would be a substantial step forward: it would give the first sound method for accounting for floating-point execution in Lipschitz-based certification, and the first floating-point-sound checkers to certify full test sets at the reported scale. The counterexample study in Section 2.3 is a useful and concrete motivation, and the compositionality of the deviation recursion and the explicit treatment of overflow are valuable. The claimed formalization in Rocq/LAProof is a notable strength, as is the hybrid method for reducing certificate degradation. However, as detailed below, the central theorem currently has a correctness gap for non-representable inputs in the perturbation ball, and some claimed artifacts and contributions (the Gram iteration algorithm, the formalization, and the implementation) are not actually available, so the contribution as presented cannot yet be fully assessed.

major comments (3)
  1. [Section 3.2, Section 4, Theorem 6.2] The proof of Theorem 6.2 does not account for the initial rounding of a non-representable input x'. Sections 3.2 and 4 set ẑ0 = x and D0 = 0, so the entire deviation recursion bounds only errors introduced after the input is already represented. But the theorem quantifies over all x' in B(x, ε) ⊂ R^n. For an x' that is not exactly representable in the target floating-point format, a deployed network computes on fl(x'), not x', producing an initial deviation δ0 = fl(x') - x' with ||δ0|| up to roughly 0.5 ulp · √n. This term propagates through αℓ and is not reflected in E_ctr, E_ball, or condition (iii). Thus the theorem as stated over the real ball does not follow from the proof. This is an internal gap, independent of the acknowledged FTZ/fused-operator limitation. The fix is to either (a) state the theorem only for floating-point-representable points and adjust the definition of robust
  2. [Abstract vs. full text] The abstract announces an 'efficient floating-point Gram iteration algorithm for Lipschitz bounds' with a proof that it 'never under-estimates the true norm,' but no such algorithm, theorem, or proof appears anywhere in the body (Sections 1–10). The only mention is a passing reference in Section 2.1 to Gram iteration as an existing method. This is a claimed contribution that the paper does not deliver. The authors should either add the corresponding section with the algorithm and its correctness proof, or remove this claim from the abstract.
  3. [Sections 1, 2, 8, 10] The paper states that the theory is formalized in Rocq/LAProof and that a Python implementation was written, but neither artifact is provided or linked. Given that machine-checked soundness is one of the paper's advertised strengths, and the evaluation relies on the Python implementation, the absence of these artifacts prevents independent verification. Please provide the Rocq theories and the Python code (or a clear public repository) as supplementary material.
minor comments (5)
  1. [Section 5, paragraph after Corollary 5.2] The sentence 'A straightforward induction using Theorem 5.2' should cite Corollary 5.2, not Theorem 5.2 (there is no Theorem 5.2).
  2. [Section 8.1 / RQ1] For float16, the paper notes that robustness certification is vacuous. It should be clarified in RQ1 whether the rejection of adversarial counterexamples at float16 is due to the new accounting or simply because certification is vacuous for all points in that format.
  3. [Abstract] The phrase 'entire test set -- seven those with 500,000 examples' appears garbled; presumably 'even those with 500,000 examples' is meant. Also, the evaluation uses 10,000-point test sets, so the 500,000-example claim is unsupported and should be removed or replaced.
  4. [Sections 6 and 7] The certification condition of Theorem 6.2 uses the actual floating-point margin m̂_j,i*(x) at the center point. The paper should specify how this value is obtained in the implementation (e.g., by an FP forward pass or an FP emulator), and state the representation of x itself. This connects to the input-rounding issue raised above.
  5. [Section 7] In the definition of D_hybrid, the quantity D^hi_{L-1}(x,0) is itself a worst-case bound. It would help to explicitly write how this bound is instantiated for the high-precision model (i.e., with which r and overflow checks), to avoid any appearance of circularity.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: FP-soundness certificate follows from the standard floating-point error model, with self-citations only as benchmarks.

full rationale

The central derivation is not circular. Section 3.2 imports the standard round-to-nearest/gradual-underflow floating-point error model from Higham [17] via LAProof [24], an external machine-checked formalization. Lemma 4.1 and Theorem 4.2 derive overflow-freedom from this model plus layer radii r_{ℓ-1}, which are computed from network weights and ε, not from the target robustness conclusion. The deviation bounds D_ℓ in Corollary 5.2 are linear recurrences obtained from the same error model; they contain no fitted parameter and are not calibrated to make Theorem 6.2 pass. Theorem 6.2's condition (iii) uses the actual FP margin \hat m_{j,i*}(x), which is a measured execution value, not a fitted parameter, and the ball-side error E_ball is a uniform worst-case bound; the conclusion for all x'∈B(x,ε) is therefore not equivalent to the input. The hybrid method in Section 7 uses a measured high-precision deviation at x, but Lemma 7.1 proves ||\hat z_{L-1}-z_{L-1}|| ≤ ||\hat z_{L-1}-\hat z^hi_{L-1}|| + D^hi_{L-1}(x,0) by the triangle inequality, so it is an empirical tightening of a sound bound, not a circular definition. The only self-citations are to [43]/[44] as benchmark models, baseline certificate rates, and validation outputs; [43] is machine-checked, and no theorem needed for the FP-soundness claim is imported from it. Section 10's caveat about FTZ, fused operators, and non-conforming runtimes is a scoping limitation, not circularity. A possible independent soundness gap is the assumption \hat z_0 = x and D_0 = 0 for all x'∈R^n, since non-representable inputs would introduce an initial conversion deviation; but that is a correctness concern, not circularity. Overall, the derivation is self-contained apart from benchmark usage and receives score 0 for circularity.

Assumptions & free parameters 1 free parameters · 5 assumptions · 0 invented entities

The theory itself introduces no fitted constants; all numerical constants (u, a_mul, Fmax, gamma_n) come from the IEEE/standard FP model. The ledger records the semantic assumptions the soundness result rests on: the FP model itself, FP-exact activations, trusted norm-computation bounds, and the trusted LAProof/Rocq basis.

free parameters (1)
  • Gram iteration count per dataset = MNIST 20 / Fashion-MNIST 13 / CIFAR-10 12 for RQ1; 11/12/12 for RQ2/3
    Chosen by hand; affects tightness of spectral-norm bounds and hence reported certification coverage. Not fitted to test-set outcomes, but it does influence the headline coverage numbers.
assumptions (5)
  • domain assumption Standard floating-point error model: fl(x∘y) = (x∘y)(1+δ)+η with |δ|≤u, |η|≤a_mul, valid absent overflow (Section 3.2, Eq. 1)
    The deviation and overflow analyses assume deployed arithmetic follows round-to-nearest with gradual underflow; Section 10 acknowledges real deployments may use FTZ, fused ops, or reduced-precision kernels, which would void certificates.
  • domain assumption Activation functions (ReLU, identity) are FP-exact for all finite inputs (Section 3.1 assumption iv)
    Excludes sigmoid/tanh and other rounded activations; stated by the author as a limitation, not proved for all floating-point implementations.
  • standard math Matrix spectral norm properties are axiomatised in the Rocq formalisation (Section 1, AI-use disclosure paragraph)
    Author states these are the only axioms in the Rocq proofs; they are standard properties but not machine-derived in a provided artifact.
  • domain assumption Gram iteration returns valid upper bounds on spectral norms, so margin Lipschitz constants are sound (Sections 2.1, 8.1, ref [8])
    Approximate norm bounds are external to this paper; no verified zero-underestimation theorem is presented in the body.
  • standard math LAProof library correctly formalises the standard FP error models used here (Sections 1, 3.2)
    Foundation for the Rocq proofs; trusted as a prior artifact without shipped certificates in this paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Lipschitz-Based Robustness Certification Under Floating-Point Execution." pith.science (2026). https://pith.science/paper/QWIPP43B

@misc{pith2026260313334,
  author       = {Pith},
  title        = {Pith review of: Lipschitz-Based Robustness Certification Under Floating-Point Execution},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QWIPP43B}},
  note         = {Machine review of arXiv:2603.13334}
}
read the original abstract

Lipschitz-based robustness certification bounds a network's sensitivity through concrete numerical computation rather than symbolic reasoning, and so scales efficiently. It is increasingly used even where verifiable guarantees matter. Yet, as with most prior work on robustness certification and verification, soundness is typically proved against a semantic model assuming exact real arithmetic. Deployed networks instead execute in floating-point, creating a gap between certified properties and executed behaviour. As motivating evidence, we give counterexamples showing that real arithmetic robustness guarantees can fail under floating-point execution, even for previously verified certifiers. We then develop a formal, compositional theory relating real arithmetic Lipschitz-based sensitivity bounds to floating-point execution under standard rounding-error models for feed-forward ReLU networks. We derive sound conditions for floating-point robustness, including bounds on certificate degradation and sufficient conditions for the absence of overflow. We also give an efficient floating-point Gram iteration algorithm for Lipschitz bounds and prove that it never under-estimates the true norm. Separately, when a model is certified pre-deployment, we show how measuring its actual deviation against a high-precision execution can substantially reduce certificate degradation. We formalise the theory and its soundness, and implement an executable certifier, evaluated across dense networks spanning image, tabular, and many-class classification. To our knowledge, ours is the first method for soundly accounting for floating-point effects in Lipschitz-based robustness certification, and, done efficiently, the first floating-point-sound robustness checking procedure of any kind to certify models' entire test set -- seven those with 500,000 examples -- while retaining enough precision to be practical.

Figures

Figures reproduced from arXiv: 2603.13334 by the authors.

Figure 1
Figure 1. Instances for which Tobler et al.’s verified certifier produces misleading robustness certifications. [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. MNIST instances for which Tobler et al.’s verified certifier produces misleading robustness certifications [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. MNIST instances for which Tobler et al.’s verified certifier produces misleading robustness certifications, [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

55 extracted references · 8 linked inside Pith

  1. [1]

    In: Proc

    Althoff, M.: An introduction to CORA 2015. In: Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH). pp. 120–151 (2015)

    2015

  2. [2]

    IMA Journal of Numerical Analysis1, 21 (2025)

    Arar, E.M.E., Filip, S.I., Mary, T., Riccietti, E.: Mixed precision accumulation for neural network inference guided by componentwise forward error analysis. IMA Journal of Numerical Analysis1, 21 (2025)

    2025

  3. [3]

    In: NASA Formal Methods Symposium

    Bak, S.: nnenum: Verification of ReLU neural networks with optimized abstraction refinement. In: NASA Formal Methods Symposium. pp. 19–36. Springer (2021)

    2021

  4. [4]

    In: 32nd International Conference on Computer-Aided Verification (CAV) (July 2020)

    Bak, S., Tran, H.D., Hobbs, K., Johnson, T.T.: Improved geometric path enumeration for verifying ReLU neural networks. In: 32nd International Conference on Computer-Aided Verification (CAV) (July 2020)

    2020

  5. [5]

    Springer Science & Business Media (2013)

    Bertot, Y., Castéran, P.: Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer Science & Business Media (2013)

    2013

  6. [6]

    IMA Journal of Numerical Analysis p

    Beuzeville, T., Buttari, A., Gratton, S., Mary, T.: Deterministic and probabilistic rounding error analysis of neural networks in floating-point arithmetic. IMA Journal of Numerical Analysis p. draf130 (2026)

    2026

  7. [7]

    In: European Symposium on Programming

    Cordeiro, L.C., Daggitt, M.L., Girard-Satabin, J., Isac, O., Johnson, T.T., Katz, G., Komendantskaya, E., Lemesle, A., Manino, E., Šinkarovs, A., et al.: Neural network verification is a programming language challenge. In: European Symposium on Programming. pp. 206–235. Springer (2025)

    2025

  8. [8]

    In: International Conference on Machine Learning (ICML)

    Delattre, B., Barthélemy, Q., Araujo, A., Allauzen, A.: Efficient bound of Lipschitz constant for convolutional layers by Gram iteration. In: International Conference on Machine Learning (ICML). pp. 7513–7532. PMLR (2023)

    2023

Show all 55 references
  1. [9]

    Soft Computing (2024)

    Demarchi, S., Guidotti, D., Pulina, L., Tacchella, A.: NeVer2: Learning and verification of neural networks. Soft Computing (2024)

    2024

  2. [10]

    In: FoMLAS

    Demarchi, S., Guidotti, D., Pulina, L., Tacchella, A., Narodytska, N., Amir, G., Katz, G., Isac, O.: Supporting standardiza- tion of neural networks verification with VNN-LIB and CoCoNet. In: FoMLAS. pp. 47–58 (2023)

    2023

  3. [11]

    SIAM (1997)

    Demmel, J.W.: Applied numerical linear algebra. SIAM (1997)

    1997

  4. [12]

    Duong, H., Li, L., Nguyen, T., Dwyer, M.: A DPLL(T) framework for verifying deep neural networks (2023), arXiv, 25 pages

    2023

  5. [13]

    In: International Conference on Computer Aided Verification

    Duong, H., Nguyen, T., Dwyer, M.B.: NeuralSAT: A high-performance verification tool for deep neural networks. In: International Conference on Computer Aided Verification. pp. 409–423. Springer (2025)

    2025

  6. [14]

    Proceedings of the ACM on Software Engineering1(FSE), 859–881 (2024)

    Duong, H., Xu, D., Nguyen, T., Dwyer, M.B.: Harnessing neuron stability to improve DNN verification. Proceedings of the ACM on Software Engineering1(FSE), 859–881 (2024)

    2024

  7. [15]

    Gouk, H., Frank, E., Pfahringer, B., Cree, M.J.: Regularisation of neural networks by enforcing Lipschitz continuity. Mach. Learn.110(2), 393–416 (2021). https://doi.org/10.1007/S10994-020-05929-W, https://doi.org/10.1007/s10994-020- 05929-w

    2021 doi

  8. [16]

    In: Automated Technology for Verification and Analysis: 19th International Symposium, ATVA 2021, Gold Coast, QL D, Australia, October 18–22, 2021, Proceedings 19

    Guidotti, D., Pulina, L., Tacchella, A.: pyNeVer: A framework for learning and verification of neural networks. In: Automated Technology for Verification and Analysis: 19th International Symposium, ATVA 2021, Gold Coast, QL D, Australia, October 18–22, 2021, Proceedings 19. pp...

    2021

  9. [17]

    SIAM (2002)

    Higham, N.J.: Accuracy and stability of numerical algorithms. SIAM (2002)

    2002

  10. [18]

    arXiv preprint arXiv:2601.18513 (2026)

    Hu, K., Hu, H., Fredrikson, M.: Lipnext: Scaling up lipschitz-based certified robustness to billion-parameter models. arXiv preprint arXiv:2601.18513 (2026)

    2026

  11. [19]

    In: International Static Analysis Symposium

    Jia, K., Rinard, M.: Exploiting verified neural networks via floating point numerical error. In: International Static Analysis Symposium. pp. 191–205. Springer (2021) Lipschitz-Based Robustness Certification Under Floating-Point Execution 23

    2021

  12. [20]

    In: Proceedings of the 2024 Workshop on Artificial Intelligence and Security (AISec) (2024)

    Jin, J., Ohrimenko, O., Rubinstein, B.I.P.: Getting a-round guarantees: Floating-point attacks on certified robustness. In: Proceedings of the 2024 Workshop on Artificial Intelligence and Security (AISec) (2024). https://doi.org/10.1145/3689932.3694761

    2024

  13. [21]

    In: International Conference on Computer Aided Verification (CAV)

    Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: International Conference on Computer Aided Verification (CAV). pp. 97–117. Springer (2017)

    2017

  14. [22]

    In: International Conference on Computer Aided Verification

    Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljić, A., et al.: The Marabou> framework for verification and analysis of deep neural networks. In: International Conference on Computer Aided Verification. pp. 443–452. Spri...

    2019

  15. [23]

    arXiv preprint arXiv:2512.19007 (2025)

    Kaulen, K., Ladner, T., Bak, S., Brix, C., Duong, H., Flinkow, T., Johnson, T.T., Koller, L., Manino, E., Nguyen, T.H., et al.: The 6th international verification of neural networks competition (VNN-COMP 2025): Summary and results. arXiv preprint arXiv:2512.19007 (2025)

    2025

  16. [24]

    In: 2023 IEEE 30th Symposium on Computer Arithmetic (ARITH)

    Kellison, A.E., Appel, A.W., Tekriwal, M., Bindel, D.: LAProof: A library of formal proofs of accuracy and correctness for linear algebra programs. In: 2023 IEEE 30th Symposium on Computer Arithmetic (ARITH). pp. 36–43. IEEE (2023)

    2023

  17. [25]

    In: NASA Formal Methods

    Kochdumper, N., Schilling, C., Althoff, M., Bak, S.: Open- and closed-loop neural network verification using polynomial zonotopes. In: NASA Formal Methods. pp. 16–36 (2023)

    2023

  18. [26]

    arXiv (2025)

    Koller, L., Ladner, T., Althoff, M.: Out of the shadows: Exploring a latent space for neural network verification. arXiv (2025)

    2025

  19. [27]

    TMLR (2025)

    Koller, L., Ladner, T., Althoff, M.: Set-based training for neural network verification. TMLR (2025)

    2025

  20. [28]

    Krizhevsky, A.: Learning multiple layers of features from tiny images. Tech. rep., University of Toronto (2009)

    2009

  21. [29]

    In: Proc

    Ladner, T., Althoff, M.: Automatic abstraction refinement in neural network verification using sensitivity analysis. In: Proc. of the Int. Conf. on Hybrid Systems: Computation and Control (HSCC). pp. 1–13 (2023)

    2023

  22. [30]

    Proceedings of the IEEE86(11), 2278–2324 (1998)

    LeCun, Y., Bottou, L., Bengio, Y., Haffner, P.: Gradient-based learning applied to document recognition. Proceedings of the IEEE86(11), 2278–2324 (1998)

    1998

  23. [31]

    In: International Conference on Machine Learning (ICML)

    Leino, K., Wang, Z., Fredrikson, M.: Globally-robust neural networks. In: International Conference on Machine Learning (ICML). Proceedings of Machine Learning Research, vol. 139, pp. 6212–6222. PMLR (2021), http://proceedings.mlr. press/v139/leino21a.html

    2021

  24. [32]

    arXiv preprint arXiv:2410.23903 (2024)

    Lemesle, A., Lehmann, J., Tristan, L.G.: Neural network verification with PyRAT. arXiv preprint arXiv:2410.23903 (2024)

    2024 arXiv

  25. [33]

    In: 35th International Conference on Computer-Aided Verification (CAV) (July 2023)

    Lopez, D.M., Choi, S.W., Tran, H.D., Johnson, T.T.: NNV 2.0: The neural network verification tool. In: 35th International Conference on Computer-Aided Verification (CAV) (July 2023)

    2023

  26. [34]

    arXiv preprint arXiv:2510.23389 (2025)

    Manino, E., Farias, B., Menezes, R.S., Shmarov, F., Cordeiro, L.C.: Floating-point neural network verification at the software level. arXiv preprint arXiv:2510.23389 (2025)

    2025

  27. [35]

    Moosavi-Dezfooli, S.M., Fawzi, A., Frossard, P.: Deepfool: a simple and accurate method to fool deep neural networks (2015)

    2015

  28. [36]

    https://github.com/eth-sri/eran (2018), secure, Reliable, and Intelligent Systems Lab, ETH Zürich

    Müller, M.N., Singh, G., Balunovic, M., Makarchuk, G., Ruoss, A., Serre, F., Baader, M., Drachsler-Cohen, D., Gehr, T., Hoffmann, A., Maurer, J., Müller, C., Püschel, M., Tsankov, P., Vechev, M.: ERAN: ETH robustness analyzer for neural networks. https://github.com/eth-sri/era...

    2018

  29. [37]

    arXiv preprint arXiv:1807.01069 (2018)

    Nicolae, M.I., Sinn, M., Tran, M.N., Buesser, B., Rawat, A., Wistuba, M., Zantedeschi, V., Baracaldo, N., Chen, B., Ludwig, H., et al.: Adversarial Robustness Toolbox v1.0.0. arXiv preprint arXiv:1807.01069 (2018)

    2018 arXiv

  30. [38]

    arXiv preprint arXiv:2405.21063 (2024)

    Shi, Z., Jin, Q., Kolter, Z., Jana, S., Hsieh, C.J., Zhang, H.: Neural network verification with branch-and-bound for general nonlinearities. arXiv preprint arXiv:2405.21063 (2024)

    2024 arXiv

  31. [39]

    Advances in neural information processing systems31(2018)

    Singh, G., Gehr, T., Mirman, M., Püschel, M., Vechev, M.: Fast and effective robustness certification. Advances in neural information processing systems31(2018)

    2018

  32. [40]

    Proceedings of the ACM on Programming Languages3(POPL), 1–30 (2019)

    Singh, G., Gehr, T., Püschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages3(POPL), 1–30 (2019)

    2019

  33. [41]

    arXiv preprint arXiv:2111.13110 (2021)

    Song, X., Manino, E., Sena, L., Alves, E., Bessa, I., Lujan, M., Cordeiro, L., et al.: QNNVerifier: A tool for verifying neural networks using SMT-based model checking. arXiv preprint arXiv:2111.13110 (2021)

    2021 arXiv

  34. [42]

    arXiv preprint arXiv:2506.01054 (2025)

    Szász, A., Bánhelyi, B., Jelasity, M.: No soundness in the real world: On the challenges of the verification of deployed neural networks. arXiv preprint arXiv:2506.01054 (2025)

    2025 arXiv

  35. [43]

    In: International Conference on Computer Aided Verification (CAV)

    Tobler, J., Syeda, H.T., Murray, T.: A formally verified robustness certifier for neural networks. In: International Conference on Computer Aided Verification (CAV). pp. 327–348. Springer (2025)

    2025

  36. [44]

    Tobler, J., Syeda, H.T., Murray, T.: A formally verified robustness certifier for neural networks (extended version) (2025), https://arxiv.org/abs/2505.06958

    2025 arXiv

  37. [45]

    In: 32nd International Conference on Computer-Aided Verification (CAV) (July 2020) 24 Toby Murray

    Tran, H.D., Yang, X., Lopez, D.M., Musau, P., Nguyen, L.V., Xiang, W.., Bak, S., Johnson, T.T.: NNV: The neural network verification tool for deep neural networks and learning-enabled cyber-physical system s. In: 32nd International Conference on Computer-Aided Verification (CA...

    2020

  38. [46]

    arXiv preprint arXiv:2103.06624 (2021)

    Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J., Kolter, Z.: Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. arXiv preprint arXiv:2103.06624 (2021)

    2021 arXiv

  39. [47]

    In: International Conference on Machine Learning (ICML)

    Weng, L., Zhang, H., Chen, H., Song, Z., Hsieh, C.J., Daniel, L., Boning, D., Dhillon, I.: Towards fast computation of certified robustness for relu networks. In: International Conference on Machine Learning (ICML). pp. 5276–5285. PMLR (2018)

    2018

  40. [48]

    Numerische Mathematik2(1), 319–340 (1960)

    Wilkinson, J.H.: Error analysis of floating-point computation. Numerische Mathematik2(1), 319–340 (1960)

    1960

  41. [49]

    In: International Conference on Computer Aided Verification

    Wu, H., Isac, O., Zeljić, A., Tagomori, T., Daggitt, M., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., et al.: Marabou 2.0: a versatile formal analyzer of neural networks. In: International Conference on Computer Aided Verification. pp. 249–264. Springer (2024)

    2024

  42. [50]

    arXiv preprint arXiv:1708.07747 (2017)

    Xiao, H., Rasul, K., Vollgraf, R.: Fashion-MNIST: a novel image dataset for benchmarking machine learning algorithms. arXiv preprint arXiv:1708.07747 (2017)

    2017 arXiv

  43. [51]

    Advances in Neural Information Processing Systems33(2020)

    Xu, K., Shi, Z., Zhang, H., Wang, Y., Chang, K.W., Huang, M., Kailkhura, B., Lin, X., Hsieh, C.J.: Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems33(2020)

    2020

  44. [52]

    In: International Conference on Learning Representations (2021), https://openreview.net/forum?id=nVZtXBI6LNn

    Xu, K., Zhang, H., Wang, S., Wang, Y., Jana, S., Lin, X., 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), https://openreview.n...

    2021

  45. [53]

    In: Asia-Pacific Software Engineering Conference (APSEC)

    Yang, S., Chen, L., Yin, B., Li, M., Zhou, Y., Wang, J.: Sound floating-point neural network verification with MILP. In: Asia-Pacific Software Engineering Conference (APSEC). pp. 01–10. IEEE (2024)

    2024

  46. [54]

    Advances in Neural Information Processing Systems (NeurIPS) (2022)

    Zhang, H., Wang, S., Xu, K., Li, L., Li, B., Jana, S., Hsieh, C.J., Kolter, J.Z.: General cutting planes for bound-propagation- based neural network verification. Advances in Neural Information Processing Systems (NeurIPS) (2022)

    2022

  47. [55]

    In: International Conference on Learning Representations (2021)

    Zombori, D., Bánhelyi, B., Csendes, T., Megyeri, I., Jelasity, M.: Fooling a complete neural network verifier. In: International Conference on Learning Representations (2021)

    2021

Pith tools

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