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

TL;DR

This paper introduces a new reachability analysis technique for neural networks that provides provable bounds on the Hessian, leveraging derivative-preserving abstractions and Taylor expansions for improved accuracy.

Contribution

The paper presents a novel method to compute analytical bounds on neural network derivatives, including the Hessian, using derivative-preserving abstractions and loop transformations.

Findings

Accurately bounds the Hessian of neural networks for small input sets.

Employs branch and bound for larger input sets to refine bounds.

Outperforms existing methods in numerical evaluations.

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.