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

TL;DR

This paper introduces extsc{HiTaB}, a novel hierarchical verification framework that leverages higher-order smoothness and curvature bounds to produce tighter safety guarantees for neural networks.

Contribution

It develops a unified hierarchy of bounds exploiting second-order information and introduces an efficient layerwise method to estimate curvature Lipschitz constants in neural networks.

Findings

The framework achieves tighter safety certificates compared to existing methods.

It effectively propagates curvature bounds through network layers.

The approach is applicable to both $ ext{l}_2$ and $ ext{l}_ extinfty$ input constraints.

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.