arXiv:2405.21063v3 公告类型: replace-cross 摘要: 分支界限法（BaB）是神经网络（NN）验证中最有效的技术之一。然而，现有的用于神经网络验证的分支界限法主要集中在具有分段线性激活的神经网络上，特别是ReLU网络。本文中，我们基于线性边界传播方法，开发了一个名为GenBaB的一般框架，以在具有通用架构的神经网络上执行分支界限法，以验证通用非线性。为了决定要分支的神经元，我们设计了一种新的分支启发式方法，利用线性边界作为捷径来高效估计分支后的潜在改进。为了为通用非线性函数确定非平凡的分支点，我们提出在验证过程中通过查找表高效利用预先优化的分支点。我们展示了GenBaB在验证各种神经网络的有效性，包括具有Sigmoid、Tanh、Sine和GeLU等激活函数的神经网络，以及涉及LSTMs和Vision Transformers等多维非线性操作的神经网络。我们的框架还允许验证通用非线性计算图，并使其能够在简单的神经网络之外的应用中发挥作用，特别是在AC Optimal Power Flow (ACOPF)方面。GenBaB是最新版的$\alpha$,$\beta$-CROWN的一部分，$\alpha$,$\beta$-CROWN是2023年和2024年国际神经网络验证竞赛（VNN-COMP）的获奖者。在GitHub上可以找到重复实验的代码：https://github.com/shizhouxing/GenBaB。