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

arXiv: https://arxiv.org/abs/2605.10621 · HTML: https://mlsanity.com/paper/2605.10621/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 28 references that are in the map.
- First posted on arXiv 11 May 2026.

## Builds on (most cited first, 6 of 6)

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [A Unified Algebraic Perspective on Lipschitz Neural Networks](https://mlsanity.com/paper/2303.03169/) (2023)
- [Novel Quadratic Constraints for Extending LipSDP beyond Slope-Restricted Activations](https://mlsanity.com/paper/2401.14033/) (2024)
- [Compositional Curvature Bounds for Deep Neural Networks](https://mlsanity.com/paper/2406.05119/) (2024)
- [Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysis](https://mlsanity.com/paper/2406.04476/) (2024)

## Abstract (arXiv)

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 textscHiTaB, a novel verification framework that exploits second-order smoothness through both the Hessian, nabla2 f, and its Lipschitz constant, Lnabla2 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 Lnabla2 f in deep neural networks via layerwise propagation of curvature bounds. We extend the framework to both ℓ2- and ℓ_∞-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.