pith. sign in

arxiv: 2606.21282 · v1 · pith:VI2BU2O3new · submitted 2026-06-19 · 💻 cs.CR · cs.LO

Differential Zonotopes for Verifying Global Robustness of DNNs

Anagha Athavale , Samuel Teuber , Matteo Maffei , Ezio Bartocci , Dejan Nickovic , Georg Weissenbacher This is my paper

Pith reviewed 2026-06-26 14:11 UTC · model grok-4.3

classification 💻 cs.CR cs.LO
keywords global robustnessDNN verificationabstract interpretationzonotopesdifferential analysis2-safety propertiesneural network securitystatic analysis
0
0 comments X

The pith

Differential halo zonotopes verify global robustness of DNNs by jointly propagating input pairs and bounding their divergence.

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

The paper develops a static analysis method to check that a neural network produces the same prediction for any two inputs that differ by at most a given perturbation bound. Global robustness is a 2-safety property that quantifies over all such input pairs rather than around single points, which makes it harder to verify than local robustness. The core technique extends zonotopes into differential halo zonotopes that carry two inputs forward together while keeping a tight bound on how far apart their outputs can drift. A relaxed, symmetric version of confidence-based global robustness is also defined so the property remains useful for networks that produce low-confidence outputs on some pairs. If the method scales as claimed, it becomes possible to certify larger networks for security properties that previous tools could not reach.

Core claim

Differential halo zonotopes form an abstract domain that extends ordinary zonotopes to propagate pairs of perturbed inputs in lock-step while tightly bounding their divergence; combined with a symmetric variant of confidence-based global robustness that disregards low-confidence differing predictions, this domain supports a sound static analysis that verifies global robustness for networks an order of magnitude larger than those handled by prior techniques.

What carries the argument

differential halo zonotopes, which jointly track pairs of inputs and bound their output divergence

If this is right

  • Verification becomes feasible for networks an order of magnitude larger than those handled by earlier global-robustness tools.
  • The same abstract domain yields both higher precision and better scalability than prior techniques on standard benchmarks.
  • The symmetric confidence relaxation broadens the class of networks for which global robustness can be checked.
  • The approach is implemented in a tool that runs on widely deployed models and standard verification suites.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The pair-propagation idea could be lifted to other 2-safety properties beyond robustness, such as non-interference or fairness constraints.
  • If the divergence bound can be made even tighter, the method might support verification of networks with recurrent or transformer layers.
  • Combining the domain with existing local-robustness tools could produce a two-stage pipeline that first filters easy cases locally and then checks remaining pairs globally.

Load-bearing premise

The symmetric variant of confidence-based global robustness is a practically meaningful property that applies to more networks without changing the verification goal.

What would settle it

A concrete network and perturbation bound where two high-confidence inputs differ in label yet the analysis reports the network as robust.

Figures

Figures reproduced from arXiv: 2606.21282 by Anagha Athavale, Dejan Nickovic, Ezio Bartocci, Georg Weissenbacher, Matteo Maffei, Samuel Teuber.

Figure 1
Figure 1. Figure 1: Running example: a DNN with 2 inputs, 2 hidden [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: ReLU approximation To this end, the zono￾tope’s generator dimen￾sion 𝑛 is increased once per ReLU neuron and the additional generator 𝝐new is used to represent the approximation error incurred through repre￾senting ReLU via a linear approximation [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Zonotope propagation through the running example (Example 2.6): the input zonotope is transformed by the affine [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Symmetric vs asymmetric confidence-based global [PITH_FULL_IMAGE:figures/full_fig_p005_4.png] view at source ↗
Figure 1
Figure 1. Figure 1: 4.1 A Tale of Three Failed Encodings To provide a better intuition for our encoding, we first describe three encodings which are either semantically unsound or imprecise for zonotope propagation. Common Generators. One may be tempted to initialize 𝔷 ′ = 𝔷′′ = ( (𝑟, 0) , 𝑐) with 𝔷 Δ = ( (0, 𝜀) , 0). However, while h 𝔷 Δ ,𝔷 Δ i would in￾deed be [−𝜀, 𝜀], this is unsound, as shown by the following example: Exa… view at source ↗
Figure 5
Figure 5. Figure 5: Intuition for Differential Halo Zonotopes set 𝑐 = 𝑢+𝑙 2 and 𝑟 = 𝑢 − 𝑐. We then define a differential halo affine form as 𝔷 ′ ,𝔷 ′′ ,𝔷 Δ  : 𝔷 ′ =   𝑟 − 𝜀 2  , 𝜀 2 , 0  , 𝑐 𝔷 ′′ =   𝑟 − 𝜀 2  , 0, 𝜀 2  , 𝑐 𝔷 Δ =  0, 𝜀 2 , − 𝜀 2  , 0  We will call the first component of 𝔷 ′ ’s and 𝔷 ′′’s generator vector the primary generator while the latter two components are the secondary generators. Differ… view at source ↗
Figure 6
Figure 6. Figure 6: Visualization of robustness verification with differential halo zonotopes: Dotted border represents truly reachable [PITH_FULL_IMAGE:figures/full_fig_p009_6.png] view at source ↗
read the original abstract

The robustness of deep neural networks (DNNs) is critical in security-sensitive applications, where small input perturbations should not alter model predictions. This property is commonly formalized as local or global robustness: the former considers perturbations around a single input, while the latter -- strictly stronger -- quantifies over all input pairs. While local robustness can be expressed as a safety property, global robustness is a 2-safety property, making it substantially more challenging to verify. We present a novel static analysis technique for verifying the global robustness of DNNs. Our approach is based on differential halo zonotopes, a new abstract domain that extends zonotopes to jointly propagate pairs of perturbed inputs in lock-step while tightly bounding their divergence. In addition, we introduce a symmetric variant of confidence-based global robustness that disregards perturbations leading to differing but low-confidence predictions. This relaxation yields a practically meaningful notion of robustness that applies to a broader class of networks. We implement our approach in a new tool, called TwoSafe, and evaluate it on standard DNN verification benchmarks, including widely deployed models. Our results show that TwoSafe significantly outperforms the state of the art in both precision and scalability, enabling the verification of networks an order of magnitude larger than those handled by prior techniques.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The manuscript introduces differential halo zonotopes, a new abstract domain extending zonotopes to jointly propagate pairs of perturbed inputs in lock-step while bounding their divergence, for verifying global robustness of DNNs (a 2-safety property). It also defines a symmetric confidence-based relaxation of global robustness that ignores low-confidence differing predictions, implements the approach in the TwoSafe tool, and reports superior precision and scalability over prior techniques on standard benchmarks including deployed models.

Significance. If the central claims hold, the work would advance DNN verification by addressing the harder global robustness property with a specialized abstract domain that enables tighter joint analysis. The explicit framing of the confidence relaxation as a deliberate practical weakening, combined with empirical results on larger networks, strengthens applicability. Strengths include the new domain construction and the tool's reported outperformance.

major comments (1)
  1. [Abstract, §4] Abstract and §4 (definition of the symmetric variant): the claim that the relaxation 'yields a practically meaningful notion of robustness that applies to a broader class of networks' without invalidating the verification goal is load-bearing for the practical contribution; the manuscript should provide a formal statement of the relaxed property and a soundness argument showing when it preserves the intended 2-safety guarantee.
minor comments (2)
  1. [§5] §5 (experimental setup): clarify the exact definition of 'order of magnitude larger' networks (e.g., layer count or parameter count) and report raw numbers alongside the relative improvement to allow direct comparison with prior work.
  2. [§3] Notation in §3: ensure the halo component of the differential zonotope is defined with explicit generators and center before the propagation rules are stated, to avoid forward references.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive feedback and positive assessment of the work. We address the single major comment below.

read point-by-point responses

  1. Referee: [Abstract, §4] Abstract and §4 (definition of the symmetric variant): the claim that the relaxation 'yields a practically meaningful notion of robustness that applies to a broader class of networks' without invalidating the verification goal is load-bearing for the practical contribution; the manuscript should provide a formal statement of the relaxed property and a soundness argument showing when it preserves the intended 2-safety guarantee.

    Authors: We agree that an explicit formal statement and soundness argument would strengthen the presentation of the symmetric confidence-based relaxation. In the revised version we will augment §4 with (i) a precise mathematical definition of the relaxed 2-safety property (symmetric confidence-based global robustness) and (ii) a soundness theorem together with a proof sketch establishing the conditions under which the relaxation preserves the original 2-safety guarantee for high-confidence predictions while correctly identifying networks that satisfy the relaxed property. This addition will directly support the claim in the abstract without altering any technical results. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper introduces differential halo zonotopes as a novel abstract domain extending zonotopes for joint propagation of input pairs to verify global robustness as a 2-safety property, along with a symmetric confidence-based relaxation framed as a deliberate practical weakening. No equations, derivations, or load-bearing steps are present that reduce any claimed result to fitted parameters, self-definitions, or self-citation chains by construction. The central technique is presented as an independent extension with external evaluation on benchmarks, making the derivation self-contained against external verification goals.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Review performed on abstract only; no free parameters, axioms, or invented entities can be identified from the provided text.

pith-pipeline@v0.9.1-grok · 5768 in / 1008 out tokens · 23923 ms · 2026-06-26T14:11:14.260512+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

57 extracted references · 33 canonical work pages

  1. [1]

    Davide Anguita, Alessandro Ghio, Luca Oneto, Xavier Parra, and Jorge Luis Reyes-Ortiz. 2013. A Public Domain Dataset for Human Activity Recognition using Smartphones. In21st European Symposium on Artificial Neural Networks. https://www.esann.org/sites/default/files/proceedings/legacy/es2013-84.pdf

    2013

  2. [2]

    Shuang Ao, Stefan Rueger, and Advaith Siddharthan. 2023. Two Sides of Mis- calibration: Identifying Over and Under-Confidence Prediction for Network Calibration. InUncertainty in Artificial Intelligence (Proceedings of Machine Learn- ing Research, Vol. 216), Robin J. Evans and Ilya Shpitser (Eds.). PMLR, 77–87. https://proceedings.mlr.press/v216/ao23a.html

    2023

  3. [3]

    Anagha Athavale, Ezio Bartocci, Maria Christakis, Matteo Maffei, Dejan Nickovic, and Georg Weissenbacher. 2024. Verifying Global Two-Safety Properties in Neural Networks with Confidence. In36th International Conference on Computer Aided Verification (LNCS, Vol. 14682), Arie Gurfinkel and Vijay Ganesh (Eds.). Springer, 329–351. doi:10.1007/978-3-031-65630-9_17

    work page doi:10.1007/978-3-031-65630-9_17 2024

  4. [4]

    Stanley Bak. 2021. nnenum: Verification of ReLU Neural Networks with Opti- mized Abstraction Refinement. In13th NASA Formal Methods Symposium (LNCS, Vol. 12673), Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, and Ivan Perez (Eds.). Springer, 19–36. doi:10.1007/978-3-030-76384-8_2

    work page doi:10.1007/978-3-030-76384-8_2 2021

  5. [6]

    Debangshu Banerjee and Gagandeep Singh. 2024. Relational DNN Verifica- tion With Cross Executional Bound Refinement. In41st International Confer- ence on Machine Learning. OpenReview.net. https://openreview.net/forum?id= HOG80Yk4Gw

    2024

  6. [7]

    Debangshu Banerjee, Changming Xu, and Gagandeep Singh. 2024. Input- Relational Verification of Deep Neural Networks.Proc. ACM Program. Lang.8, PLDI (2024), 1–27. doi:10.1145/3656377

    work page doi:10.1145/3656377 2024

  7. [8]

    Anahita Baninajjar, Kamran Hosseini, Ahmed Rezine, and Amir Aminifar. 2023. SafeDeep: A Scalable Robustness Verification Framework for Deep Neural Net- works. InIEEE International Conference on Acoustics, Speech and Signal Processing. IEEE, 1–5. doi:10.1109/ICASSP49357.2023.10097028

    work page doi:10.1109/icassp49357.2023.10097028 2023

  8. [9]

    Jeff Bezanson, Alan Edelman, Stefan Karpinski, and Viral B. Shah. 2017. Julia: A Fresh Approach to Numerical Computing.SIAM Rev.59, 1 (2017), 65–98. doi:10.1137/141000671

    work page doi:10.1137/141000671 2017

  9. [10]

    Luigi Bibbo and Marley MBR Vellasco. 2023. Human activity recognition (HAR) in healthcare. 13009 pages

    2023

  10. [11]

    Sumon Biswas and Hridesh Rajan. 2023. Fairify: Fairness Verification of Neural Networks. In45th IEEE/ACM International Conference on Software Engineering, ICSE. IEEE, 1546–1558. doi:10.1109/ICSE48619.2023.00134

    work page doi:10.1109/icse48619.2023.00134 2023

  11. [12]

    Bosman, Aaron Berger, Holger H

    Annelot W. Bosman, Aaron Berger, Holger H. Hoos, and Jan N. van Rijn. 2025. Robustness Distributions in Neural Network Verification.J. Artif. Intell. Res.83 (2025). doi:10.1613/JAIR.1.18403

    work page doi:10.1613/jair.1.18403 2025

  12. [14]

    Michael R Clarkson and Fred B Schneider. 2010. Hyperproperties.Journal of Computer Security18, 6 (2010), 1157–1210

    2010

  13. [15]

    Miguel Angel Alvarez de la Concepcion, Luis Miguel Soria Morillo, Juan Anto- nio Álvarez García, and Luis Gonzalez-Abril. 2017. Mobile activity recognition and fall detection system for elderly people using Ameva algorithm.Pervasive and Mobile Computing34 (2017), 3–13

    2017

  14. [16]

    Javier Duarte, Song Han, Philip Harris, Sergo Jindariani, Edward Kreinar, Ben- jamin Kreis, Jennifer Ngadiuba, Maurizio Pierini, Ryan Rivera, Nhan Tran, et al . 2018. Fast inference of deep neural networks in FPGAs for particle physics.Journal of instrumentation13, 07 (2018), P07027. arXiv:1804.06913 doi:10.1088/1748-0221/13/07/P07027

    work page doi:10.1088/1748-0221/13/07/p07027 2018

  15. [17]

    Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. 2018. Output Range Analysis for Deep Feedforward Neural Networks. In10th NASA Formal Methods Symposium (LNCS, Vol. 10811), Aaron Dutle, César A. Muñoz, and Anthony Narkawicz (Eds.). Springer, 121–138. doi:10.1007/978-3-319-77935-5_9

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

  16. [18]

    Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin T. Vechev. 2018. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. InIEEE Symposium on Security and Privacy. IEEE Computer Society, 3–18. doi:10.1109/SP.2018.00058

    work page doi:10.1109/sp.2018.00058 2018

  17. [19]

    Yonatan Geifman and Ran El-Yaniv. 2017. Selective Classification for Deep Neural Networks. InAdvances in Neural Information Processing Systems, Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett (Eds.). 4878–4887

    2017

  18. [20]

    Chuqin Geng, Nham Le, Xiaojie Xu, Zhaoyue Wang, Arie Gurfinkel, and Xujie Si. 2023. Towards Reliable Neural Specifications. InInternational Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 202), Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelhardt, Sivan Sabato, and Jonathan Scarlett (Eds.). PMLR, 11196–11212. ht...

    2023

  19. [21]

    Khalil Ghorbal, Eric Goubault, and Sylvie Putot. 2009. The Zonotope Abstract Domain Taylor1+. In21st International Conference on Computer Aided Verification (LNCS, Vol. 5643), Ahmed Bouajjani and Oded Maler (Eds.). Springer, 627–633. doi:10.1007/978-3-642-02658-4_47

    work page doi:10.1007/978-3-642-02658-4_47 2009

  20. [22]

    Goodfellow, Yoshua Bengio, and Aaron C

    Ian J. Goodfellow, Yoshua Bengio, and Aaron C. Courville. 2016.Deep Learning. MIT Press. http://www.deeplearningbook.org/

    2016

  21. [23]

    Pasareanu, and Clark W

    Divya Gopinath, Guy Katz, Corina S. Pasareanu, and Clark W. Barrett. 2018. Deep- Safe: A Data-Driven Approach for Assessing Robustness of Neural Networks. In16th International Symposium on Automated Technology for Verification and Analysis (LNCS, Vol. 11138), Shuvendu K. Lahiri and Chao Wang (Eds.). Springer, 3–19. doi:10.1007/978-3-030-01090-4_1

    work page doi:10.1007/978-3-030-01090-4_1 2018

  22. [24]

    Weinberger

    Chuan Guo, Geoff Pleiss, Yu Sun, and Kilian Q. Weinberger. 2017. On Calibration of Modern Neural Networks. In34th International Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 70), Doina Precup and Yee Whye Teh (Eds.). PMLR, 1321–1330. http://proceedings.mlr.press/v70/guo17a.html

    2017

  23. [25]

    Gurobi Optimization, LLC. 2023. Gurobi Optimizer Reference Manual. https: //www.gurobi.com

    2023

  24. [26]

    Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. 2017. Safety Veri- fication of Deep Neural Networks. In29th International Conference on Computer Aided Verification (LNCS, Vol. 10426), Rupak Majumdar and Viktor Kuncak (Eds.). Springer, 3–29. doi:10.1007/978-3-319-63387-9_1

    work page doi:10.1007/978-3-319-63387-9_1 2017

  25. [27]

    Julian, Jessica Lopez, Jeffrey S

    Kyle D. Julian, Jessica Lopez, Jeffrey S. Brush, Michael P. Owen, and Mykel J. Kochenderfer. 2016. Policy compression for aircraft collision avoidance systems. In35th IEEE/AIAA Digital A vionics Systems Conference. 1–10. doi:10.1109/DASC. 2016.7778091

    work page doi:10.1109/dasc 2016

  26. [28]

    Barrett, David L

    Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer

  27. [29]

    Observational and Physical Classification of Supernovae

    Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In 29th International Conference on Computer Aided Verification (LNCS, Vol. 10426), Rupak Majumdar and Viktor Kuncak (Eds.). Springer, 97–117. doi:10.1007/978-3- 319-63387-9_5

    work page doi:10.1007/978-3-

  28. [30]

    Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L

    Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, and Clark W. Barrett. 2019. The Marabou Framework for Verification and Analysis of Deep Neural Networks. In31st Inter- national Conference on Computer Aided Verification (...

    work page doi:10.1007/978-3-030-25540-4_26 2019

  29. [31]

    Konstantin Kaulen, Tobias Ladner, Stanley Bak, Christopher Brix, Hai Duong, Thomas Flinkow, Taylor T Johnson, Lukas Koller, Edoardo Manino, ThanhVu H Nguyen, et al . 2025. The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results. arXiv:2512.19007 [cs.LG] https://arxiv.org/abs/2512.19007

    arXiv 2025

  30. [32]

    Philipp Kern, Edoardo Manino, and Carsten Sinz. 2025. Certified Error Analysis of Homomorphically Encrypted Neural Networks. In2nd International Symposium on AI Verification (LNCS, Vol. 15947), Mirco Giacobbe and Anna Lukina (Eds.). Springer, 156–179. doi:10.1007/978-3-031-99991-8_8

    work page doi:10.1007/978-3-031-99991-8_8 2025

  31. [33]

    Haitham Khedr and Yasser Shoukry. 2023. CertiFair: A Framework for Certified Global Fairness of Neural Networks. In37th AAAI Conference on Artificial In- telligence, Brian Williams, Yiling Chen, and Jennifer Neville (Eds.). AAAI Press, 8237–8245. doi:10.1609/AAAI.V37I7.25994

    work page doi:10.1609/aaai.v37i7.25994 2023

  32. [34]

    Brian Hyeongseok Kim, Jingbo Wang, and Chao Wang. 2025. FairQuant: Certi- fying and Quantifying Fairness of Deep Neural Networks. InProceedings of the IEEE/ACM 47th International Conference on Software Engineering(Ottawa, On- tario, Canada)(ICSE ’25). IEEE Press, 527–539. doi:10.1109/ICSE55347.2025.00016

    work page doi:10.1109/icse55347.2025.00016 2025

  33. [35]

    Niklas Kochdumper, Christian Schilling, Matthias Althoff, and Stanley Bak. 2023. Open- and Closed-Loop Neural Network Verification Using Polynomial Zono- topes. In15th NASA Formal Methods Symposium (Lecture Notes in Computer Science, Vol. 13903), Kristin Yvonne Rozier and Swarat Chaudhuri (Eds.). Springer, 16–36. doi:10.1007/978-3-031-33170-1_2

    work page doi:10.1007/978-3-031-33170-1_2 2023

  34. [36]

    Meelis Kull, Miquel Perelló-Nieto, Markus Kängsepp, Telmo de Menezes e Silva Filho, Hao Song, and Peter A. Flach. 2019. Beyond temperature scaling: Obtaining well-calibrated multi-class probabilities with Dirichlet calibration. In Annual Conference on Neural Information Processing Systems, Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’A...

    2019

  35. [37]

    Tobias Ladner and Matthias Althoff. 2024. Exponent Relaxation of Polynomial Zonotopes and Its Applications in Formal Neural Network Verification. In38th AAAI Conference on Artificial Intelligence, Michael J. Wooldridge, Jennifer G. Dy, and Sriraam Natarajan (Eds.). AAAI Press, 21304–21311. doi:10.1609/AAAI. V38I19.30125 13 Anagha Athavale, Samuel Teuber, ...

    work page doi:10.1609/aaai 2024

  36. [38]

    Jianlin Li, Jiangchao Liu, Pengfei Yang, Liqian Chen, Xiaowei Huang, and Lijun Zhang. 2019. Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification. In26th International Sympo- sium on Static Analysis (LNCS, Vol. 11822), Bor-Yuh Evan Chang (Ed.). Springer, 296–319. doi:10.1007/978-3-030-32304-2_15

    work page doi:10.1007/978-3-030-32304-2_15 2019

  37. [39]

    Rex Liu, Albara Ah Ramli, Huanle Zhang, Erik Henricson, and Xin Liu. 2021. An overview of human activity recognition using wearable sensors: Healthcare and artificial intelligence. InInternational Conference on Internet of Things. Springer, 1–14

    2021

  38. [40]

    John- son

    Diego Manzanas Lopez, Sung Woo Choi, Hoang-Dung Tran, and Taylor T. John- son. 2023. NNV 2.0: The Neural Network Verification Tool. In35th International Conference on Computer Aided Verification (LNCS, Vol. 13965), Constantin Enea and Akash Lal (Eds.). Springer, 397–412. doi:10.1007/978-3-031-37703-7_19

    work page doi:10.1007/978-3-031-37703-7_19 2023

  39. [41]

    Seyed-Mohsen Moosavi-Dezfooli, Alhussein Fawzi, Omar Fawzi, and Pascal Frossard. 2017. Universal Adversarial Perturbations. InIEEE Conference on Computer Vision and Pattern Recognition. IEEE Computer Society, 86–94. doi:10. 1109/CVPR.2017.17

    2017

  40. [42]

    Brandon Paulsen, Jingbo Wang, and Chao Wang. 2020. ReluDiff: differential verification of deep neural networks. In42nd International Conference on Software Engineering, Gregg Rothermel and Doo-Hwan Bae (Eds.). ACM, 714–726. doi:10. 1145/3377811.3380337

    arXiv 2020

  41. [43]

    Brandon Paulsen, Jingbo Wang, Jiawei Wang, and Chao Wang. 2020. NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Ap- proximation. In35th IEEE/ACM International Conference on Automated Software Engineering. IEEE, 784–796. doi:10.1145/3324884.3416560

    work page doi:10.1145/3324884.3416560 2020

  42. [44]

    Lawrence C. Paulson. 1994.Isabelle - A Generic Theorem Prover (with a contribu- tion by T. Nipkow). LNCS, Vol. 828. Springer. doi:10.1007/BFB0030541

    work page doi:10.1007/bfb0030541 1994

  43. [45]

    Luca Pulina and Armando Tacchella. 2010. An Abstraction-Refinement Approach to Verification of Artificial Neural Networks. In22nd International Conference on Computer Aided Verification (LNCS, Vol. 6174), Tayssir Touili, Byron Cook, and Paul B. Jackson (Eds.). Springer, 243–257. doi:10.1007/978-3-642-14295-6_24

    work page doi:10.1007/978-3-642-14295-6_24 2010

  44. [46]

    Luca Pulina and Armando Tacchella. 2012. Challenging SMT solvers to verify neural networks.AI Commun.25, 2 (2012), 117–135. doi:10.3233/AIC-2012-0525

    work page doi:10.3233/aic-2012-0525 2012

  45. [47]

    Ashwin Sankaran. 2025. The future of smart healthcare: how ai and har are reshaping hospital workflows.Well Testing J34, 1 (2025), 68–92

    2025

  46. [48]

    Fatemeh Serpush, Mohammad Bagher Menhaj, Behrooz Masoumi, and Babak Karasfi. 2022. Wearable sensor-based human activity recognition in the smart healthcare system.Computational intelligence and neuroscience2022, 1 (2022), 1391906

    2022

  47. [49]

    Seshia, Ankush Desai, Tommaso Dreossi, Daniel J

    Sanjit A. Seshia, Ankush Desai, Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, and Xi- angyu Yue. 2018. Formal Specification for Deep Neural Networks. In16th In- ternational Symposium on Automated Technology for Verification and Analysis (LNCS, Vol. 11138), Shuvendu K. Lahiri and Chao Wang (Ed...

    work page doi:10.1007/978-3-030-01090-4_2 2018

  48. [50]

    Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin T. Vechev. 2018. Fast and Effective Robustness Certification. InAnnual Conference on Neural Information Processing Systems, Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett (Eds.). 10825–10836

    2018

  49. [51]

    Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T. Vechev. 2019. An abstract domain for certifying neural networks.Proc. ACM Program. Lang.3, POPL (2019), 41:1–41:30. doi:10.1145/3290354

    work page doi:10.1145/3290354 2019

  50. [52]

    Tarun Suresh, Debangshu Banerjee, and Gagandeep Singh. 2024. Relational Veri- fication Leaps Forward with RABBit. InAnnual Conference on Neural Information Processing Systems, Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Paquet, Jakub M. Tomczak, and Cheng Zhang (Eds.)

    2024

  51. [53]

    Samuel Teuber, Marko Kleine Büning, Philipp Kern, and Carsten Sinz. 2021. Geometric Path Enumeration for Equivalence Verification of Neural Networks. In33rd IEEE International Conference on Tools with Artificial Intelligence. IEEE, 200–208. doi:10.1109/ICTAI52525.2021.00035

    work page doi:10.1109/ictai52525.2021.00035 2021

  52. [54]

    Samuel Teuber, Philipp Kern, Marvin Janzen, and Bernhard Beckert. 2025. Re- visiting Differential Verification: Equivalence Verification with Confidence. In 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (LNCS, Vol. 15697), Arie Gurfinkel and Marijn Heule (Eds.). Springer, 257–278. doi:10.1007/978-3-031-...

    work page doi:10.1007/978-3-031-90653-4_13 2025

  53. [55]

    Vincent Tjeng, Kai Yuanqing Xiao, and Russ Tedrake. 2019. Evaluating Ro- bustness of Neural Networks with Mixed Integer Programming. In7th In- ternational Conference on Learning Representations. OpenReview.net. https: //openreview.net/forum?id=HyGIdiRqtm

    2019

  54. [56]

    Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, and Taylor T. Johnson. 2020. NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems. In32nd International Conference on Computer Aided Verification (LNCS, Vol. 12224), Shuvendu K. Lahiri...

    work page doi:10.1007/978-3-030-53288-8_1 2020

  55. [57]

    Zico Kolter

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. 2021. Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification. InAnnual Con- ference on Neural Information Processing Systems, Marc’Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jenn...

    2021

  56. [58]

    Linda F Wightman. 1998. LSAC National Longitudinal Bar Passage Study. LSAC Research Report Series

    1998

  57. [59]

    Wang et al., ‘Optimal Dispatch and Routing of Electrified Heavy-Duty Truck Fleets: A Case Study with Fleet Data’, Proceedings of the American Control Conference, vol

    Yuhao Zhang and Xiangru Xu. 2023. Reachability Analysis and Safety Verifi- cation of Neural Feedback Systems via Hybrid Zonotopes. InAmerican Control Conference. IEEE, 1915–1921. doi:10.23919/ACC55779.2023.10156417 A Proofs Lemma 4.8(Soundness of Symmetric Confidence LP).Assume 𝜏1, 𝜏2 ∈ [0.5,1 ) and let 𝒵out be a differential zonotope returned for ReachΔ ...

    work page doi:10.23919/acc55779.2023.10156417 2023