Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysis
Sina Sharifi, Mahyar Fazlyab
TL;DR
This work develops a derivative-preserving reachability framework for neural networks with differentiable activations by deriving analytical bounds on the gradient and Hessian through a Taylor-model abstraction. It leverages a loop-transformation of activations to tighten local Lipschitz constants (local LipLT) and couples these bounds with a branch-and-bound scheme to obtain provable reachability for general input sets, including zonotopes. The main contributions are scalable gradient and Hessian bounds, a derivative-informed bounding strategy, and a method that combines end-to-end Taylor approximations with curvature information to improve verification over ReLU-centric approaches. The approach yields tighter, less conservative certificates for both open-loop and closed-loop systems, demonstrated on control benchmarks, with public code released for broader use and extension to curvature-aware robustness and safety analyses.
Abstract
We propose a novel reachability analysis method tailored for neural networks with differentiable activations. Our idea hinges on a sound abstraction of the neural network map based on first-order Taylor expansion and bounding the remainder. To this end, we propose a method to compute analytical bounds on the network's first derivative (gradient) and second derivative (Hessian). A key aspect of our method is loop transformation on the activation functions to exploit their monotonicity effectively. The resulting end-to-end abstraction locally preserves the derivative information, yielding accurate bounds on small input sets. Finally, we employ a branch and bound framework for larger input sets to refine the abstraction recursively. We evaluate our method numerically via different examples and compare the results with relevant state-of-the-art methods.