Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysis

Sina Sharifi; Mahyar Fazlyab

cs.LGJun 6, 2024

Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysis

Authors: Sina Sharifi, Mahyar Fazlyab

Organizations: Department of Electrical and Computer Engineering, Johns Hopkins University, 3400 North Charles Street Baltimore, MD 21218

Abstract

We propose a novel reachability analysis method tailored for neural networks with smooth activations. Our method relies on constructing an end-to-end first-order Taylor expansion of the network and bounding the remainder. To enable this, we develop a scalable algorithm for computing closed-form bounds on both the gradient norm and Hessian norm of the network. A key component is a loop transformation of the activation functions, which leverages their monotonicity to sharpen the bounds. This yields a local abstraction that preserves the network's value and gradient at the expansion point. For larger input domains, we integrate this local model into a branch-and-bound scheme, recursively refining the overapproximation. We validate our approach through extensive experiments and demonstrate scalability and accuracy improvements over state-of-the-art verification baselines.

Figures & tables

Figure 1: Overview of proposed abstraction.

Figure 2: Loop transformation on a two-layer neural network.

Figure 3: Architecture of the modified neural network. The yellow part is the sub-network consisting of the first $l$ layers, and the blue part is the sub-network consisting of the final $(L-l)$ layers.

Figure 4: Comparison of zeroth- and first-order bounds.

Figure 5: Closed-loop system reachability

Panel of Figure 6 — Figure 6: (Left) Lipschitz and (middle) Hessian upper bound calculated by different methods and (right) time spent to calculate the local Hessian bounds per number of layers.

Panel of Figure 7 — Figure 7: Reachable sets computed with zonotopes [ 48 ] (red), Taylor models [ 14 ] (purple), polynomial zonotopes [ 15 ] (blue), our method with coordinate directions (solid black), and 16 uniformly chosen directions (dashed black) for two randomly initialized $\tanh$ (left) and Sigmoid (right) networks.

Panel of Figure 8 — Figure 8: Reachable sets computed with zonotopes [ 48 ] (red), Taylor models [ 14 ] (purple), polynomial zonotopes [ 15 ] (blue), our method with 16 uniformly chosen directions (dashed black) for a single layer (left), two-layer (middle), three-layer (right) randomly initialized $\tanh$ networks.

	Zono. [ 48 ]	Taylor [ 14 ]	Poly. Zono. [ 15 ]	Ours
Sigmoid	0.01	0.4	0.37	0.16
Tanh	0.006	0.24	0.05	0.43
Tanh 1-hidden	0.002	0.02	0.01	0.05
Tanh 2-hidden	0.002	0.05	0.01	1.9
Tanh 3-hidden	0.003	0.13	0.17	47.5

Table 1: Runtime comparison for Figs. 7 and 8 .

Panel of Figure 9 — Figure 9: (a) Reachability analysis for the Double Integrator on a hexagon input set for five time-steps with $\varepsilon_{t}=10^{-3}$ . (b) Reachability analysis for the 6D Quadrotor system for 10 time-steps and comparing the results with ReachLipBnB with $\varepsilon_{t}=10^{-2}$ .

	$\varepsilon_{t}$	Method	Branches	Run Time
DI	$10^{-2}$	Zeroth	1.9k $\pm$ 0.1k	0.95 $\pm$ 0.25
DI	$10^{-2}$	First	0.6k $\pm$ 0.06k	0.4 $\pm$ 0.01
6Q	$10^{-2}$	Zeroth	4.89M $\pm$ 36k	678.5 $\pm$ 22.7
6Q	$10^{-2}$	First	0.93M $\pm$ 16k	385.8 $\pm$ 12

Table 2: Time and branch-count comparisons between the zeroth- and first-order bounding methods for networks with

\tanh

activation function.

	$\varepsilon_{t}$	Lipschitz	Branches	Run Time (Lip.)
DI	$10^{-2}$	Naive	2.4k $\pm$ 53	0.94 $\pm$ 0.26 (0.008)
		LipLT	0.67k $\pm$ 63	0.53 $\pm$ 0.26 (0.02)
		LipSDP	0.63k $\pm$ 33	1.36 $\pm$ 0.29 (0.8)
	$10^{-3}$	Naive	4.1k $\pm$ 0.1k	1.39 $\pm$ 0.27 (0.008)
		LipLT	2.2k $\pm$ 0.1k	1.03 $\pm$ 0.2 (0.02)
		LipSDP	2.2k $\pm$ 0.08k	1.83 $\pm$ 0.2 (0.8)

Table 3: Performance comparison between various Lipschitz calculation methods.

Bounding Method	Run Time (s)	Branches
IBP	15.6	8.5
CROWN	3.3	1
CROWN-IBP	3.2	1
Zeroth	0.12	4
First	0.04	3.5

Table 4: Run time and number of branches for a single iteration of the double integrator benchmark with

\varepsilon_{t}=10^{-2}

. The reported number of branches is averaged over the four subproblems.

	$\varepsilon_{t}$	Heuristic	Branches	Run Time
DI	$10^{-2}$	Max Length	678.8 $\pm$ 63	0.52 $\pm$ 0.26
	$10^{-2}$	Best UB	714 $\pm$ 53	1.74 $\pm$ 0.22
	$10^{-3}$	Max Length	2.25k $\pm$ 0.1k	1 $\pm$ 0.22
	$10^{-3}$	Best UB	2.24k $\pm$ 0.1k	5.01 $\pm$ 0.16

Table 5: Comparison between different branching heuristics.

Figure 10: Comparison between our first-order method with ReachMM on the double integrator with tanh activations.

Figure 11: Comparison of the resulting volumes versus the time budget of the methods.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Panel of Figure 12 — Figure 12: (Left): Visualization of the CROWN upper and lower bounds for the example with $\varepsilon=1$ . (Right): The progression of the CROWN upper bound of $\tanh(z)$ for $z\in[-\varepsilon,\varepsilon]$ .

Neural Network Verification

Neural network verification develops methods to prove whether networks satisfy properties such as robustness, safety, and bounded output behavior.

See all 125 papers

Hierarchical End-to-End Taylor Bounds for Complete Neural Network Verification
May 11, 2026Taha Entesari, Mahyar FazlyabNeural Network Verification Neural Network Robustness
Johns Hopkins University
Quadratic Characterizations for Reachability Analysis of Neural Networks
May 19, 2026Elias Khalife, Mazen Farhood, Pierre-Loic GarocheNeural Network Verification Reachability Analysis
Kevin T. Crofton Department of Aerospace and Ocean Engineering, Virginia Tech, Blacksburg, VA 24061, USA · Federation ENAC ISAE-SUPAERO ONERA, Universite de Toulouse, Toulouse, France
Neural Network Verification using Partial Multi-Neuron Relaxation
May 28, 2026Ido Shmuel, Guy KatzNeural Network Verification
The Hebrew University of Jerusalem, Jerusalem, Israel

May 11, 2026J/K move · Enter open · S save

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

Taha Entesari, Mahyar Fazlyab

Johns Hopkins University

Neural Network Verification Neural Network Robustness Certified Robustness

Open paper AskPDF 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 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.

Abstract

Neural Network Verification

Explore similar work

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

Quadratic Characterizations for Reachability Analysis of Neural Networks

Neural Network Verification using Partial Multi-Neuron Relaxation