张民与刘静教授团队提出一种可证明最优的面向Sigmoid类激活函数的神经网络验证线性近似技术

深度神经网络的鲁棒性对于保障智能系统的安全可靠至关重要。形式化验证方法已经被证明是一种验证神经神经网络鲁棒性的有效方法，能从理论上证明模型在某个给定扰动下依然是鲁棒的。然而对于一般的神经网络模型来说，其验证问题已被证明是NP完全的，因此需要高效的算法以提高验证的效率。对神经网络中的激活函数进行上线性近似是一种高效的手段，尤其在带有Sigmoid一类激活函数的神经网络验证中被广泛采用。然而由于近似不可避免的引入误差，如何降低近似带来的误差是该方法的一个关键难题。

本工作首先通过实例说明了目前已经有很多工作定义的所谓“更优”的近似方法只适用于某些特定网络，并且没有给出适用的范围。基于此发现，我们从验证的角度定义了计算最优的线性近似问题本身是神经网络层面的多目标非凸优化问题，其难度等同于神经网络验证问题本身。团队提出了两个有效的、可证明“最优”的近似方法从单个神经元层面解决这个复杂的非凸优化问题，即通过每个神经元的最优实现整个网络的最优近似,如下图所示。从理论和实验上分别证明了在权重全都非负的情况下通过断点切线的近似是最优的近似方法。结果表明，本工作提出的方法相比最新的方法相比在验证的鲁棒性的精度上取得了显著的提升，最高可达 251.28%，此外，本方法在卷积网络上的提升更加明显。

本工作以“Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks”为题，被软件工程领域CCF-A类会议ASE2022接收，是实验室2021年发表在AAAI上的论文“Tightening Robustness Verification of Convolutional Neural Networks with Fine-Grained Linear Approximation”的延续。在该问题上，我们认为在单个神经元上考虑激活函数的近似不存在适用于所有网络的最优近似方法。该结论也将为后续研究更精确的近似方法提供了理论基础。