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.

我们提出了一种针对具有可微激活函数的神经网络的新型可达性分析方法。我们的想法依赖于基于一阶泰勒展开的神经网络映射的有声抽象，并对余项进行边界约束。为此，我们提出了一种计算网络一阶导数（梯度）和二阶导数（海森矩阵）的解析上界的方法。我们的方法的一个关键方面是通过循环变换激活函数，以有效利用它们的单调性。由此产生的端到端抽象在局部保留了导数信息，从而对小的输入集提供精确的上界。最后，我们使用分支界限框架来递归地完善较大的输入集的抽象。我们通过不同的例子对我们的方法进行了数值评估，并将结果与相关的最新方法进行了比较。

神经网络海森矩阵的可证界：导数保持可达性分析