Hierarchical End-to-End Taylor Bounds for Complete Neural Network Verification

• URL: http://arxiv.org/abs/2605.10621v1
• Date: Mon, 11 May 2026 14:16:13 GMT
• Title: Hierarchical End-to-End Taylor Bounds for Complete Neural Network Verification
• Abstract summary: Reachability analysis of neural networks seeks to compute or bound the set of outputs attainable over a given input domain.<n>Existing approaches exploit at most second-order information and do not systematically leverage higher-order information.<n>We introduce textscHiTaB, a novel verification framework that exploits second-order smoothness through both the Hessian, $nabla2 f$, and its Lipschitz constant, $L_nabla2 f$.
• Score: 10.685380941330687
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Reachability analysis of neural networks, which seeks to compute or bound the set of outputs attainable over a given input domain, is central to certifying safety and robustness in learning-enabled physical systems. Since exact reachable set computation is generally intractable, existing methods typically rely on tractable overapproximations. Examining the state of the art for smooth, twice-differentiable networks, we observe that existing approaches exploit at most second-order information and do not systematically leverage higher-order information. In this work, we introduce \textsc{HiTaB}, a novel verification framework that exploits second-order smoothness through both the Hessian, $\nabla^2 f$, and its Lipschitz constant, $L_{\nabla^2 f}$. We further develop a unified hierarchy of zeroth-, first-, and second-order bounds, together with precise conditions under which higher-order approximations yield provable improvements. Our main technical contribution is a compositional procedure for efficiently bounding $L_{\nabla^2 f}$ in deep neural networks via layerwise propagation of curvature bounds. We extend the framework to both $\ell_2$- and $\ell_\infty$-constrained input sets and show how it can be integrated into branch-and-bound verification pipelines. To our knowledge, this is the first practical reachability analysis framework for smooth neural networks that systematically exploits Lipschitz continuity of curvature, leading to tighter and more informative safety certificates.

Related papers

• Mildly Overparameterized ReLU Networks on Orthogonal Data: Incremental Learning and Implicit Bias [11.187895893664484]
  We study the gradient flow dynamics of two-layer ReLU networks with training data.<n>We prove the limiting flow converges to a saddle-to-saddle jump process.<n>More broadly, our work provides the first rigorous proof of an incremental learning process for ReLU networks.
  arXiv  Detail & Related papers  (2026-05-26T14:39:20Z)
• Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial [23.69448525306035]
  $,!$-CROWN is a general-purpose bounding engine for nonlinear functions represented as graphs.<n>In this tutorial, we discuss the basics of $,!$-CROWN and introduce its application to various control-related computation tasks.
  arXiv  Detail & Related papers  (2026-05-26T05:49:19Z)
• 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)
• Probabilistically Tightened Linear Relaxation-based Perturbation Analysis for Neural Network Verification [83.25968588249776]
  We present a novel framework that combines over-approximation techniques from LiRPA-based approaches with a sampling-based method to compute tight intermediate reachable sets.<n>With negligible computational overhead, $textttPT-LiRPA$ exploiting the estimated reachable sets, significantly tightens the lower and upper linear bounds of a neural network's output.
  arXiv  Detail & Related papers  (2025-07-07T18:45:53Z)
• Computable Lipschitz Bounds for Deep Neural Networks [0.0]
  We analyse three existing upper bounds written for the $l2$ norm. We propose two novel bounds for both feed-forward fully-connected neural networks and convolutional neural networks.
  arXiv  Detail & Related papers  (2024-10-28T14:09:46Z)
• Compositional Curvature Bounds for Deep Neural Networks [7.373617024876726]
  A key challenge that threatens the widespread use of neural networks in safety-critical applications is their vulnerability to adversarial attacks. We study the second-order behavior of continuously differentiable deep neural networks, focusing on robustness against adversarial perturbations. We introduce a novel algorithm to analytically compute provable upper bounds on the second derivative of neural networks.
  arXiv  Detail & Related papers  (2024-06-07T17:50:15Z)
• DualApp: Tight Over-Approximation for Neural Network Robustness Verification via Under-Approximation [17.924507519230424]
  We propose a novel under-approximation-guided approach to define tight over-approximations and two complementary under-approximation algorithms. The overestimated domain guarantees the soundness while the underestimated one guides the tightness. We implement our approach into a tool called DualApp and extensively evaluate it on a benchmark of 84 collected and trained neural networks.
  arXiv  Detail & Related papers  (2022-11-21T05:09:34Z)
• Robust Training and Verification of Implicit Neural Networks: A Non-Euclidean Contractive Approach [64.23331120621118]
  This paper proposes a theoretical and computational framework for training and robustness verification of implicit neural networks. We introduce a related embedded network and show that the embedded network can be used to provide an $ell_infty$-norm box over-approximation of the reachable sets of the original network. We apply our algorithms to train implicit neural networks on the MNIST dataset and compare the robustness of our models with the models trained via existing approaches in the literature.
  arXiv  Detail & Related papers  (2022-08-08T03:13:24Z)
• Scalable Lipschitz Residual Networks with Convex Potential Flows [120.27516256281359]
  We show that using convex potentials in a residual network gradient flow provides a built-in $1$-Lipschitz transformation. A comprehensive set of experiments on CIFAR-10 demonstrates the scalability of our architecture and the benefit of our approach for $ell$ provable defenses.
  arXiv  Detail & Related papers  (2021-10-25T07:12:53Z)
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition [161.09660864941603]
  We improve the scalability of Branch and Bound (BaB) algorithms for formally proving input-output properties of neural networks. We present a novel activation-based branching strategy and a BaB framework, named Branch and Dual Network Bound (BaDNB) BaDNB outperforms previous complete verification systems by a large margin, cutting average verification times by factors up to 50 on adversarial properties.
  arXiv  Detail & Related papers  (2021-04-14T09:22:42Z)
• Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
  A fundamental component of neural network verification is the computation of bounds on the values their outputs can take. We propose a novel approach based on Lagrangian Decomposition. We show that we obtain bounds comparable with off-the-shelf solvers in a fraction of their running time.
  arXiv  Detail & Related papers  (2020-02-24T17:55:10Z)

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.