In the field of formal verification, Neural Networks (NNs) are typically reformulated into equivalent mathematical programs which are optimized over. To overcome the inherent non-convexity of these reformulations, convex relaxations of nonlinear activation functions are typically utilized. Common relaxations (i.e., static linear cuts) of "S-shaped" activation functions, however, can be overly loose, slowing down the overall verification process. In this paper, we derive tuneable hyperplanes which upper and lower bound the sigmoid activation function. When tuned in the dual space, these affine bounds smoothly rotate around the nonlinear manifold of the sigmoid activation function. This approach, termed $\alpha$-sig, allows us to tractably incorporate the tightest possible, element-wise convex relaxation of the sigmoid activation function into a formal verification framework. We embed these relaxations inside of large verification tasks and compare their performance to LiRPA and $\alpha$-CROWN, a state-of-the-art verification duo.

本研究针对形式验证中深度神经网络的非凸性问题，提出了一种新的方法，通过调整超平面紧密地包围sigmoid激活函数。该方法称为α-sig，可以有效地在形式验证框架中引入sigmoid函数的紧凑凸放松，显著提高了验证效率。实验结果显示其优于现有的LiRPA和α-CROWN方法。

实现Sigmoid函数在形式验证中的紧致放松