Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysis
This work addresses verification challenges for neural networks, offering a method with improved accuracy, though it appears incremental as it builds on existing reachability techniques.
The paper tackles the problem of verifying neural networks by proposing a reachability analysis method that computes analytical bounds on gradients and Hessians using Taylor expansions and loop transformations, achieving accurate bounds on small input sets and refining them for larger sets via branch and bound.
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.