深度神经网络的鲁棒性对于现代AI支持系统至关重要，应正式验证。在广泛的应用中采用了类似乙状结肠的神经网络。由于它们的非线性，通常会过度评估乙状结肠样激活功能，以进行有效的验证，这不可避免地引入了不精确度。已大量的努力致力于找到所谓的更紧密的近似值，以获得更精确的验证结果。但是，现有的紧密定义是启发式的，缺乏理论基础。我们对现有神经元的紧密表征进行了彻底的经验分析，并揭示它们仅在特定的神经网络上是优越的。然后，我们将网络紧密度的概念介绍为统一的紧密度定义，并表明计算网络紧密度是一个复杂的非convex优化问题。我们通过两个有效的，最紧密的近似值从不同的角度绕过复杂性。结果表明，我们在艺术状态下的方法实现了有希望的表现：（i）达到高达251.28％的改善，以提高认证的较低鲁棒性界限； （ii）在卷积网络上表现出更为精确的验证结果。

神经网络已广泛应用于垃圾邮件和网络钓鱼检测，入侵预防和恶意软件检测等安全应用程序。但是，这种黑盒方法通常在应用中具有不确定性和不良的解释性。此外，神经网络本身通常容易受到对抗攻击的影响。由于这些原因，人们对可信赖和严格的方法有很高的需求来验证神经网络模型的鲁棒性。对抗性的鲁棒性在处理恶意操纵输入时涉及神经网络的可靠性，是安全和机器学习中最热门的主题之一。在这项工作中，我们在神经网络的对抗性鲁棒性验证中调查了现有文献，并在机器学习，安全和软件工程领域收集了39项多元化研究工作。我们系统地分析了它们的方法，包括如何制定鲁棒性，使用哪种验证技术以及每种技术的优势和局限性。我们从正式验证的角度提供分类学，以全面理解该主题。我们根据财产规范，减少问题和推理策略对现有技术进行分类。我们还展示了使用样本模型在现有研究中应用的代表性技术。最后，我们讨论了未来研究的开放问题。

随着深度学习在关键任务系统中的越来越多的应用，越来越需要对神经网络的行为进行正式保证。确实，最近提出了许多用于验证神经网络的方法，但是这些方法通常以有限的可伸缩性或不足的精度而挣扎。许多最先进的验证方案中的关键组成部分是在网络中可以为特定输入域获得的神经元获得的值计算下限和上限 - 并且这些界限更紧密，验证的可能性越大，验证的可能性就越大。成功。计算这些边界的许多常见算法是符号结合传播方法的变化。其中，利用一种称为后替代的过程的方法特别成功。在本文中，我们提出了一种使背部替代产生更严格的界限的方法。为了实现这一目标，我们制定并最大程度地减少背部固定过程中发生的不精确错误。我们的技术是一般的，从某种意义上说，它可以将其集成到许多现有的符号结合的传播技术中，并且只有较小的修改。我们将方法作为概念验证工具实施，并且与执行背部替代的最先进的验证者相比，取得了有利的结果。

While deep neural networks (DNNs) have demonstrated impressive performance in solving many challenging tasks, they are limited to resource-constrained devices owing to their demand for computation power and storage space. Quantization is one of the most promising techniques to address this issue by quantizing the weights and/or activation tensors of a DNN into lower bit-width fixed-point numbers. While quantization has been empirically shown to introduce minor accuracy loss, it lacks formal guarantees on that, especially when the resulting quantized neural networks (QNNs) are deployed in safety-critical applications. A majority of existing verification methods focus exclusively on individual neural networks, either DNNs or QNNs. While promising attempts have been made to verify the quantization error bound between DNNs and their quantized counterparts, they are not complete and more importantly do not support fully quantified neural networks, namely, only weights are quantized. To fill this gap, in this work, we propose a quantization error bound verification method (QEBVerif), where both weights and activation tensors are quantized. QEBVerif consists of two analyses: a differential reachability analysis (DRA) and a mixed-integer linear programming (MILP) based verification method. DRA performs difference analysis between the DNN and its quantized counterpart layer-by-layer to efficiently compute a tight quantization error interval. If it fails to prove the error bound, then we encode the verification problem into an equivalent MILP problem which can be solved by off-the-shelf solvers. Thus, QEBVerif is sound, complete, and arguably efficient. We implement QEBVerif in a tool and conduct extensive experiments, showing its effectiveness and efficiency.

作为一个新的编程范式，深度神经网络（DNN）在实践中越来越多地部署，但是缺乏鲁棒性阻碍了他们在安全至关重要的领域中的应用。尽管有用于正式保证的DNN验证DNN的技术，但它们的可伸缩性和准确性有限。在本文中，我们提出了一种新颖的抽象方法，用于可扩展和精确的DNN验证。具体而言，我们提出了一种新颖的抽象来通过过度透明度分解DNN的大小。如果未报告任何虚假反例，验证抽象DNN的结果始终是结论性的。为了消除抽象提出的虚假反例，我们提出了一种新颖的反例引导的改进，该精炼精炼了抽象的DNN，以排除给定的虚假反例，同时仍然过分欣赏原始示例。我们的方法是正交的，并且可以与许多现有的验证技术集成。为了进行演示，我们使用两个有前途和确切的工具Marabou和Planet作为基础验证引擎实施我们的方法，并对广泛使用的基准ACAS XU，MNIST和CIFAR-10进行评估。结果表明，我们的方法可以通过解决更多问题并分别减少86.3％和78.0％的验证时间来提高他们的绩效。与最相关的抽象方法相比，我们的方法是11.6-26.6倍。

Verifying the robustness property of a general Rectified Linear Unit (ReLU) network is an NPcomplete problem. Although finding the exact minimum adversarial distortion is hard, giving a certified lower bound of the minimum distortion is possible. Current available methods of computing such a bound are either time-consuming or deliver low quality bounds that are too loose to be useful. In this paper, we exploit the special structure of ReLU networks and provide two computationally efficient algorithms (Fast-Lin,Fast-Lip) that are able to certify non-trivial lower bounds of minimum adversarial distortions. Experiments show that (1) our methods deliver bounds close to (the gap is 2-3X) exact minimum distortions found by Reluplex in small networks while our algorithms are more than 10,000 times faster; (2) our methods deliver similar quality of bounds (the gap is within 35% and usually around 10%; sometimes our bounds are even better) for larger networks compared to the methods based on solving linear programming problems but our algorithms are 33-14,000 times faster; (3) our method is capable of solving large MNIST and CIFAR networks up to 7 layers with more than 10,000 neurons within tens of seconds on a single CPU core. In addition, we show that there is no polynomial time algorithm that can approximately find the minimum 1 adversarial distortion of a ReLU network with a 0.99 ln n approximation ratio unless NP=P, where n is the number of neurons in the network.

基于基于不完整的神经网络验证如冠的绑定传播非常有效，可以显着加速基于神经网络的分支和绑定（BAB）。然而，绑定的传播不能完全处理由昂贵的线性编程（LP）求解器的BAB常规引入的神经元分割限制，导致界限和损伤验证效率。在这项工作中，我们开发了一种基于$ \ beta $ -cra所做的，一种基于新的绑定传播方法，可以通过从原始或双空间构造的可优化参数$ \ beta $完全编码神经元分割。当在中间层中联合优化时，$ \ Beta $ -CROWN通常会产生比具有神经元分裂约束的典型LP验证更好的界限，同时像GPU上的皇冠一样高效且并行化。适用于完全稳健的验证基准，使用BAB的$ \ Beta $ -CROWN比基于LP的BAB方法快三个数量级，并且比所有现有方法更快，同时产生较低的超时率。通过早期终止BAB，我们的方法也可用于有效的不完整验证。与强大的不完整验证者相比，我们始终如一地在许多设置中获得更高的验证准确性，包括基于凸屏障破碎技术的验证技术。与最严重但非常昂贵的Semidefinite编程（SDP）的不完整验证者相比，我们获得了更高的验证精度，验证时间较少三个级。我们的算法授权$ \ alpha，\ \β$ -craft（Alpha-Beta-Crown）验证者，VNN-Comp 2021中的获胜工具。我们的代码可在http://papercode.cc/betacrown提供

To rigorously certify the robustness of neural networks to adversarial perturbations, most state-of-the-art techniques rely on a triangle-shaped linear programming (LP) relaxation of the ReLU activation. While the LP relaxation is exact for a single neuron, recent results suggest that it faces an inherent "convex relaxation barrier" as additional activations are added, and as the attack budget is increased. In this paper, we propose a nonconvex relaxation for the ReLU relaxation, based on a low-rank restriction of a semidefinite programming (SDP) relaxation. We show that the nonconvex relaxation has a similar complexity to the LP relaxation, but enjoys improved tightness that is comparable to the much more expensive SDP relaxation. Despite nonconvexity, we prove that the verification problem satisfies constraint qualification, and therefore a Riemannian staircase approach is guaranteed to compute a near-globally optimal solution in polynomial time. Our experiments provide evidence that our nonconvex relaxation almost completely overcome the "convex relaxation barrier" faced by the LP relaxation.

本文提出了一种新的可达性分析工具，用于计算给定输入不确定性下的前馈神经网络的输出集的间隔过度近似。所提出的方法适应神经网络的现有混合单调性方法，用于可动力分析的动态系统，并将其应用于给定神经网络内的所有可能的部分网络。这确保了所获得的结果的交叉点是可以使用混合单调性获得的每层输出的最紧密的间隔过度近似。与文献中的其他工具相比，专注于小类分段 - 仿射或单调激活功能，我们方法的主要优势是其普遍性，它可以处理具有任何嘴唇智能连续激活功能的神经网络。此外，所提出的框架的简单性允许用户通过简单地提供函数，衍生和全局极值以及衍生物的相应参数来非常容易地添加未实现的激活功能。我们的算法经过测试，并将其与1000个随机生成的神经网络上的五个基于间隔的工具进行了比较，用于四个激活功能（Relu，Tanh，Elu，Silu）。我们表明我们的工具总是优于间隔绑定的传播方法，并且我们获得比Reluval，神经化，Verinet和Crown（适用于案件的时）更严格的输出界限。

我们考虑了认证深神经网络对现实分布变化的鲁棒性的问题。为此，我们通过提出一个新型的神经符号验证框架来弥合手工制作的规格和现实部署设置之间的差距模型。这种环境引起的一个独特的挑战是，现有的验证者不能紧密地近似sigmoid激活，这对于许多最新的生成模型至关重要。为了应对这一挑战，我们提出了一个通用的元算象来处理乙状结肠激活，该乙状结激素利用反示例引导的抽象细化的经典概念。关键思想是“懒惰地”完善Sigmoid函数的抽象，以排除先前抽象中发现的虚假反示例，从而确保验证过程中的进展，同时保持状态空间较小。 MNIST和CIFAR-10数据集的实验表明，我们的框架在一系列具有挑战性的分配变化方面大大优于现有方法。

经认证的稳健性是安全关键应用中的深度神经网络的理想性质，流行的训练算法可以通过计算其Lipschitz常数的全球界限来认证神经网络的鲁棒性。然而，这种界限往往松动：它倾向于过度规范神经网络并降低其自然精度。绑定的Lipschitz绑定可以在自然和认证的准确性之间提供更好的权衡，但通常很难根据网络的非凸起计算。在这项工作中，我们通过考虑激活函数（例如Relu）和权重矩阵之间的相互作用，提出了一种有效和培训的\ emph {本地} Lipschitz上限。具体地，当计算权重矩阵的诱发标准时，我们消除了相应的行和列，其中保证激活函数在每个给定数据点的邻域中是常数，它提供比全局Lipschitz常数的可怕更严格的绑定神经网络。我们的方法可用作插入式模块，以拧紧在许多可认证的训练算法中绑定的Lipschitz。此外，我们建议夹住激活功能（例如，Relu和Maxmin），具有可读的上限阈值和稀疏性损失，以帮助网络实现甚至更严格的本地嘴唇尖端。在实验上，我们表明我们的方法始终如一地优于Mnist，CiFar-10和Tinyimagenet数据集的清洁和认证准确性，具有各种网络架构的清洁和认证的准确性。

There has been a rapid development and interest in adversarial training and defenses in the machine learning community in the recent years. One line of research focuses on improving the performance and efficiency of adversarial robustness certificates for neural networks \cite{gowal:19, wong_zico:18, raghunathan:18, WengTowardsFC:18, wong:scalable:18, singh:convex_barrier:19, Huang_etal:19, single-neuron-relax:20, Zhang2020TowardsSA}. While each providing a certification to lower (or upper) bound the true distortion under adversarial attacks via relaxation, less studied was the tightness of relaxation. In this paper, we analyze a family of linear outer approximation based certificate methods via a meta algorithm, IBP-Lin. The aforementioned works often lack quantitative analysis to answer questions such as how does the performance of the certificate method depend on the network configuration and the choice of approximation parameters. Under our framework, we make a first attempt at answering these questions, which reveals that the tightness of linear approximation based certification can depend heavily on the configuration of the trained networks.

多项式网络（PNS）最近在面部和图像识别方面表现出了有希望的表现。但是，PNS的鲁棒性尚不清楚，因此获得证书对于使其在现实世界应用中的采用至关重要。基于分支和绑定（BAB）技术的Relu神经网络（NNS）上的现有验证算法不能微不足道地应用于PN验证。在这项工作中，我们设计了一种新的边界方法，该方法配备了BAB，用于全球融合保证，称为VPN。一个关键的见解是，我们获得的边界比间隔结合的传播基线更紧密。这可以通过MNIST，CIFAR10和STL10数据集的经验验证进行声音和完整的PN验证。我们认为我们的方法对NN验证具有自身的兴趣。

深度神经网络（DNN）的巨大进步导致了各种任务的最先进的性能。然而，最近的研究表明，DNNS容易受到对抗的攻击，这在将这些模型部署到自动驾驶等安全关键型应用时，这使得非常关注。已经提出了不同的防御方法，包括：a）经验防御，通常可以在不提供稳健性认证的情况下再次再次攻击; b）可认真的稳健方法，由稳健性验证组成，提供了在某些条件下的任何攻击和相应的强大培训方法中的稳健准确性的下限。在本文中，我们系统化了可认真的稳健方法和相关的实用和理论意义和调查结果。我们还提供了在不同数据集上现有的稳健验证和培训方法的第一个全面基准。特别是，我们1）为稳健性验证和培训方法提供分类，以及总结代表性算法的方法，2）揭示这些方法中的特征，优势，局限性和基本联系，3）讨论当前的研究进展情况TNN和4的可信稳健方法的理论障碍，主要挑战和未来方向提供了一个开放的统一平台，以评估超过20种代表可认真的稳健方法，用于各种DNN。

许多最先进的对抗性培训方法利用对抗性损失的上限来提供安全保障。然而，这些方法需要在每个训练步骤中计算，该步骤不能包含在梯度中的梯度以进行反向化。我们基于封闭形式的对抗性损失的封闭溶液引入了一种新的更具内容性的对抗性培训，可以有效地培养了背部衰退。通过稳健优化的最先进的工具促进了这一界限。我们使用我们的方法推出了两种新方法。第一种方法（近似稳健的上限或arub）使用网络的第一阶近似以及来自线性鲁棒优化的基本工具，以获得可以容易地实现的对抗丢失的近似偏置。第二种方法（鲁棒上限或摩擦）计算对抗性损失的精确上限。在各种表格和视觉数据集中，我们展示了我们更加原则的方法的有效性 - 摩擦比最先进的方法更强大，而是较大的扰动的最新方法，而谷会匹配的性能 - 小扰动的艺术方法。此外，摩擦和灌注速度比标准对抗性培训快（以牺牲内存增加）。重现结果的所有代码都可以在https://github.com/kimvc7/trobustness找到。

由于它们在计算机视觉，图像处理和其他人领域的优异性能，卷积神经网络具有极大的普及。不幸的是，现在众所周知，卷积网络通常产生错误的结果 - 例如，这些网络的输入的小扰动可能导致严重的分类错误。近年来提出了许多验证方法，以证明没有此类错误，但这些通常用于完全连接的网络，并且在应用于卷积网络时遭受加剧的可扩展性问题。为了解决这一差距，我们在这里介绍了CNN-ABS框架，特别是旨在验证卷积网络。 CNN-ABS的核心是一种抽象细化技术，它通过拆除卷积连接，以便在这种方式创造原始问题的过度逼近来简化验证问题;如果产生的问题变得过于抽象，它会恢复这些连接。 CNN-ABS旨在使用现有的验证引擎作为后端，我们的评估表明它可以显着提高最先进的DNN验证引擎的性能，平均降低运行时间15.7％。

We consider the algorithmic problem of finding the optimal weights and biases for a two-layer fully connected neural network to fit a given set of data points. This problem is known as empirical risk minimization in the machine learning community. We show that the problem is $\exists\mathbb{R}$-complete. This complexity class can be defined as the set of algorithmic problems that are polynomial-time equivalent to finding real roots of a polynomial with integer coefficients. Furthermore, we show that arbitrary algebraic numbers are required as weights to be able to train some instances to optimality, even if all data points are rational. Our results hold even if the following restrictions are all added simultaneously. $\bullet$ There are exactly two output neurons. $\bullet$ There are exactly two input neurons. $\bullet$ The data has only 13 different labels. $\bullet$ The number of hidden neurons is a constant fraction of the number of data points. $\bullet$ The target training error is zero. $\bullet$ The ReLU activation function is used. This shows that even very simple networks are difficult to train. The result explains why typical methods for $\mathsf{NP}$-complete problems, like mixed-integer programming or SAT-solving, cannot train neural networks to global optimality, unless $\mathsf{NP}=\exists\mathbb{R}$. We strengthen a recent result by Abrahamsen, Kleist and Miltzow [NeurIPS 2021].

Learning monotonic models with respect to a subset of the inputs is a desirable feature to effectively address the fairness, interpretability, and generalization issues in practice. Existing methods for learning monotonic neural networks either require specifically designed model structures to ensure monotonicity, which can be too restrictive/complicated, or enforce monotonicity by adjusting the learning process, which cannot provably guarantee the learned model is monotonic on selected features. In this work, we propose to certify the monotonicity of the general piece-wise linear neural networks by solving a mixed integer linear programming problem.This provides a new general approach for learning monotonic neural networks with arbitrary model structures. Our method allows us to train neural networks with heuristic monotonicity regularizations, and we can gradually increase the regularization magnitude until the learned network is certified monotonic. Compared to prior works, our approach does not require human-designed constraints on the weight space and also yields more accurate approximation. Empirical studies on various datasets demonstrate the efficiency of our approach over the state-of-the-art methods, such as Deep Lattice Networks.

深度神经网络已被证明容易受到基于语义特征扰动输入的对抗性攻击。现有的鲁棒性分析仪可以建议语义特征社区提高网络的可靠性。但是，尽管这些技术取得了重大进展，但他们仍然很难扩展到深层网络和大型社区。在这项工作中，我们介绍了VEEP，这是一种主动学习方法，将验证过程分为一系列较小的验证步骤，每个验证步骤都会提交给现有的鲁棒性分析仪。关键想法是基于先前的步骤来预测下一个最佳步骤。通过参数回归估算认证速度和灵敏度来预测最佳步骤。我们评估了MNIST，时尚摄影师，CIFAR-10和Imagenet的VEEP，并表明它可以分析各种特征的邻域：亮度，对比度，色相，饱和度和轻度。我们表明，平均而言，鉴于90分钟的超时，VEEP在29分钟内验证了96％的最大认证社区，而现有的拆分接近近距离验证，平均在58分钟内验证了73％的最大认证社区的73％。

We introduce a scalable method for training robust neural networks based on abstract interpretation. We present several abstract transformers which balance efficiency with precision and show these can be used to train large neural networks that are certifiably robust to adversarial perturbations.