实现S型激活函数用于形式化验证的最紧松弛
Achieving the Tightest Relaxation of Sigmoids for Formal Verification
AI总结：
针对形式化验证中S型激活函数常见松弛过于宽松拖慢验证的问题，提出$α$-sig方法，利用可调超平面实现最紧的逐元素凸松弛，在大型验证任务中表现出优于LiRPA和$α$-CROWN的性能。
摘要：
在形式化验证领域，神经网络（NN）通常被转化为等效的数学规划进行优化。为克服这些转化固有的非凸性，通常使用非线性激活函数的凸松弛。然而，“S型”激活函数的常见松弛（即静态线性切割）可能过于宽松，从而拖慢整体验证过程。本文推导了可调超平面，对sigmoid激活函数进行上下界界定。在双空间中调参时，这些仿射界围绕sigmoid激活函数的非线性流形平滑旋转。该方法称为$α$-sig，使我们能将尽可能紧的逐元素凸松弛纳入形式化验证框架。我们将这些松弛嵌入大型验证任务中，并将其性能与LiRPA和$α$-CROWN这一最先进的验证组合进行比较。
英文摘要：
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 $α$-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 $α$-CROWN, a state-of-the-art verification duo.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
