Lipschitz-Based Robustness Certification Under Floating-Point Execution

• URL: http://arxiv.org/abs/2603.13334v2
• Date: Tue, 17 Mar 2026 04:15:22 GMT
• Title: Lipschitz-Based Robustness Certification Under Floating-Point Execution
• Abstract summary: We develop a theory relating real arithmetic sensitivity bounds to the sensitivity of floating-point execution.<n>We derive sound conditions for robustness under floating-point execution, including bounds on certificate degradation and sufficient conditions for the absence of overflow.
• Score: 4.441866681085517
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Sensitivity-based robustness certification has emerged as a practical approach for certifying neural network robustness, including in settings that require verifiable guarantees. A key advantage of these methods is that certification is performed by concrete numerical computation (rather than symbolic reasoning) and scales efficiently with network size. However, as with the vast majority of prior work on robustness certification and verification, the soundness of these methods is typically proved with respect to a semantic model that assumes exact real arithmetic. In reality deployed neural network implementations execute using floating-point arithmetic. This mismatch creates a semantic gap between certified robustness properties and the behaviour of the executed system. As motivating evidence, we exhibit concrete counterexamples showing that real arithmetic robustness guarantees can fail under floating-point execution, even for previously verified certifiers, with discrepancies becoming pronounced at lower-precision formats such as float16. We then develop a formal, compositional theory relating real arithmetic Lipschitz-based sensitivity bounds to the sensitivity of floating-point execution under standard rounding-error models, specialised to feed-forward neural networks with ReLU activations. We derive sound conditions for robustness under floating-point execution, including bounds on certificate degradation and sufficient conditions for the absence of overflow. We formalize the theory and its main soundness results, and implement an executable certifier based on these principles, which we empirically evaluate to demonstrate its practicality.

Related papers

• Conformal Reliability: A New Evaluation Metric for Conditional Generation [62.761166941396844]
  Conditional generative models have recently remarkable success in various applications.<n>We propose a novel evaluation metric called reliability based on prediction set at a pre-specified confidence level.<n>We introduce Conformal ReLiability (CReL), a framework that can (i) construct a prediction set and (ii) accurately optimize the reliability score within the constructed prediction set.
  arXiv  Detail & Related papers  (2026-05-29T03:52:44Z)
• Certified Robustness from Approximate Gaussian Mixture Structures in Pretrained Latent Spaces [42.97530488302465]
  Deep learning models are vulnerable to adversarial perturbations.<n> Empirical defenses can achieve strong robustness in practice, but lack formal guarantees.<n>We propose a framework for designing certifiably robust classifiers that leverage latent structure in data representations.
  arXiv  Detail & Related papers  (2026-05-25T02:12:58Z)
• TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
  We introduce TorchLean, a framework that treats learned models as first-class mathematical objects with a single, precise semantics shared by execution and verification.<n>We validate TorchLean end-to-end on certified robustness, physics-informed residual bounds for PINNs, and Lyapunov-style neural controller verification.
  arXiv  Detail & Related papers  (2026-02-26T05:11:44Z)
• MathLedger: A Verifiable Learning Substrate with Ledger-Attested Feedback [0.0]
  Contemporary AI systems achieve extraordinary performance yet remain opaque and non-verifiable.<n>We introduce MathLedger, a substrate for verifiable machine cognition that integrates formal verification, cryptographic attestation, and learning dynamics.<n>The contribution is infrastructural: a working prototype of ledger-attested learning that enables auditability at scale.
  arXiv  Detail & Related papers  (2025-12-22T19:27:55Z)
• Fast and Flexible Robustness Certificates for Semantic Segmentation [6.1903263165298945]
  We introduce a new class of certifiably robust semantic networks with built-in Lipschitz constraints.<n>Our approach unlocks real-time compatible certifiably robust semantic segmentation for the first time.<n>We find our approach to be around 600 times faster than randomized smoothing methods at inference with comparable certificates on an NVIDIA A100 GPU.
  arXiv  Detail & Related papers  (2025-12-03T10:10:16Z)
• No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks [1.3108652488669736]
  We argue that theoretical soundness does not imply practical soundness.<n>We create adversarial networks that detect and exploit features of the deployment environment.<n>We demonstrate that all the tested verifiers are vulnerable to our new deployment attacks.
  arXiv  Detail & Related papers  (2025-06-01T15:47:37Z)
• A Formally Verified Robustness Certifier for Neural Networks (Extended Version) [0.0]
  Neural networks are susceptible to minor perturbations in input that cause them to misclassify.<n>Globally-robust neural networks employ a function to certify that the classification of an input cannot be altered by such a perturbation.<n>We describe the program, its specifications, and the important design decisions taken for its implementation and verification.
  arXiv  Detail & Related papers  (2025-05-11T12:05:14Z)
• Adaptive Hierarchical Certification for Segmentation using Randomized Smoothing [87.48628403354351]
  certification for machine learning is proving that no adversarial sample can evade a model within a range under certain conditions. Common certification methods for segmentation use a flat set of fine-grained classes, leading to high abstain rates due to model uncertainty. We propose a novel, more practical setting, which certifies pixels within a multi-level hierarchy, and adaptively relaxes the certification to a coarser level for unstable components.
  arXiv  Detail & Related papers  (2024-02-13T11:59:43Z)
• Mixing Classifiers to Alleviate the Accuracy-Robustness Trade-Off [8.169499497403102]
  We propose a theoretically motivated formulation that mixes the output probabilities of a standard neural network and a robust neural network. Our numerical experiments verify that the mixed classifier noticeably improves the accuracy-robustness trade-off.
  arXiv  Detail & Related papers  (2023-11-26T02:25:30Z)
• The Lipschitz-Variance-Margin Tradeoff for Enhanced Randomized Smoothing [85.85160896547698]
  Real-life applications of deep neural networks are hindered by their unsteady predictions when faced with noisy inputs and adversarial attacks. We show how to design an efficient classifier with a certified radius by relying on noise injection into the inputs. Our novel certification procedure allows us to use pre-trained models with randomized smoothing, effectively improving the current certification radius in a zero-shot manner.
  arXiv  Detail & Related papers  (2023-09-28T22:41:47Z)
• Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks [58.195261590442406]
  We study the problem of training and certifying adversarially robust quantized neural networks (QNNs) Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization. We present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs.
  arXiv  Detail & Related papers  (2022-11-29T13:32:38Z)
• Robust Implicit Networks via Non-Euclidean Contractions [63.91638306025768]
  Implicit neural networks show improved accuracy and significant reduction in memory consumption. They can suffer from ill-posedness and convergence instability. This paper provides a new framework to design well-posed and robust implicit neural networks.
  arXiv  Detail & Related papers  (2021-06-06T18:05:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.