实现Sigmoid函数的最紧凸松弛以用于形式化验证
机器学习
2024-08-23 v2 人工智能
摘要
在形式化验证领域，神经网络（NNs）通常被重新表述为等效的数学程序进行优化。为了克服这些重新表述固有的非凸性，通常对非线性激活函数使用凸松弛。然而，S形激活函数的常见松弛（即静态线性切割）可能过于宽松，减慢整体验证过程。在本文中，我们推导了可调节的超平面，用于上下界约束Sigmoid激活函数。当在対偶空间中调节时，这些仿射界围绕Sigmoid激活函数的非线性流形平滑旋转。这种方法称为α-sig，使我们能够将Sigmoid激活函数的最紧可能的逐元素凸松弛方便地融入形式化验证框架。我们将这些松弛嵌入大型验证任务中，并将其性能与LiRPA和α-CROWN（最先进的验证组合）进行了比较。
引用
@article{arxiv.2408.10491,
title = {Achieving the Tightest Relaxation of Sigmoids for Formal Verification},
author = {Samuel Chevalier and Duncan Starkenburg and Krishnamurthy Dvijotham},
journal= {arXiv preprint arXiv:2408.10491},
year = {2024}
}