激活函数的凸包近似

《Proceedings of the ACM on Programming Languages》：Convex Hull Approximation for Activation Functions

针对安全关键领域深度学习模型验证中激活函数非线性带来的挑战，提出WraAct方法通过双线性分段函数近似凸包，在保持精度的同时大幅提升效率，实验显示其约束数量减少50%，单神经元验证速度提升400倍，且在ResNet等大规模网络验证中表现优异。

　　

摘要

深度学习在安全关键领域的广泛应用促使人们需要正式验证神经网络的鲁棒性。这一努力中的一个关键挑战在于处理激活函数固有的非线性问题。激活函数的凸包作为一种有前景的解决方案应运而生，因为它能有效缩小变量范围并提供多神经元约束，从而提高验证精度。然而，由于构建精确的凸包在计算上非常昂贵，且在大多数情况下甚至不可行，现有研究主要集中在对其进行过度近似。针对ReLU和Sigmoid等特定函数，已经设计出了一些专门的方法。尽管如此，在开发适用于一般激活函数的方法方面仍存在较大差距。

在这项工作中，我们提出了WraAct，这是一种高效构建激活函数凸包近似值的方法。其核心思想是通过引入线性约束来平滑目标函数中的波动，利用双线性分段（DLP）函数简化局部几何结构。这样一来，问题就转化为对DLP函数的过度近似，而DLP函数可以高效处理。我们将WraAct与SBLM+PDDM进行了对比评估，后者是一种基于将函数分解为多个段的最先进（SOTA）多神经元过度近似方法。在处理Sigmoid、Tanh和MaxPool等常用函数时，WraAct的表现更胜一筹，效率提高了400倍（平均快400倍），精度提高了150倍（平均高150倍），同时约束数量减少了50%（平均减少50%）。它能够在10秒内完成最多8个输入维度的计算。我们还将WraAct集成到神经网络验证器中，以评估其在验证任务中的能力。在100个基准样本上，WraAct将单神经元验证的通过率从不到10%提升到了超过40%，并且比多神经元验证器PRIMA多验证了20个样本。在像ResNets这样拥有22k个神经元的大型网络中，它可以在一分钟内完成一个样本的验证。