神经网络是基于学习的软件系统的重要组成部分。但是，它们的高计算，内存和功率要求使在低资源域中使用它们具有挑战性。因此，在部署前通常对神经网络进行量化。现有的量化技术倾向于降低网络准确性。我们提出了反示例引导的神经网络量化改进（CEG4N）。该技术结合了基于搜索的量化和等效性验证：前者最小化了计算要求，而后者保证网络的输出在量化后不会改变。我们根据包括大型和小型网络在内的各种基准测试对CEG4N〜进行评估。我们的技术成功地量化了我们评估中的网络，同时生产的模型比最先进的技术高达72％。

作为神经网络（NNS）越来越多地引入安全关键域，在部署之前越来越需要在部署之前正式验证NNS。在这项工作中，我们专注于NN等效的正式验证问题，其旨在证明两个NNS（例如原件和压缩版本）显示等效行为。已经提出了两种方法：混合整数线性编程和间隔传播。虽然第一种方法缺乏可扩展性，但后者仅适用于结构性相似的NN，其重量变化很小。我们纸张的贡献有四个部分。首先，我们通过证明epsilon-andatience问题是突出的，我们表现出理论结果。其次，我们扩展了Tran等人。单个NN几何路径枚举算法以多个NN的设置。在第三步中，我们实现了扩展算法，用于等价验证，评估其实际使用所需的优化。最后，我们执行比较评估，显示我们的方法优于前一种最先进的现有技术，两者，用于等效验证以及反例查找。

在过去的十年中，神经网络（NNS）已被广泛用于许多应用程序，包括安全系统，例如自主系统。尽管采用了新兴的采用，但众所周知，NNS容易受到对抗攻击的影响。因此，提供确保此类系统正常工作的保证非常重要。为了解决这些问题，我们介绍了一个修复不安全NNS W.R.T.的框架。安全规范，即利用可满足的模型理论（SMT）求解器。我们的方法能够通过仅修改其重量值的一些重量值来搜索新的，安全的NN表示形式。此外，我们的技术试图最大程度地提高与原始网络在其决策边界方面的相似性。我们进行了广泛的实验，以证明我们提出的框架能够产生安全NNS W.R.T.的能力。对抗性的鲁棒性特性，只有轻度的准确性损失（就相似性而言）。此外，我们将我们的方法与天真的基线进行比较，以证明其有效性。总而言之，我们提供了一种算法以自动修复具有安全性的算法，并建议一些启发式方法以提高其计算性能。当前，通过遵循这种方法，我们能够产生由分段线性relu激活函数组成的小型（即具有多达数百个参数）的小型（即具有多达数百个参数）。然而，我们的框架是可以合成NNS W.R.T.的一般框架。一阶逻辑规范的任何可决定片段。

Fairness of machine learning (ML) software has become a major concern in the recent past. Although recent research on testing and improving fairness have demonstrated impact on real-world software, providing fairness guarantee in practice is still lacking. Certification of ML models is challenging because of the complex decision-making process of the models. In this paper, we proposed Fairify, an SMT-based approach to verify individual fairness property in neural network (NN) models. Individual fairness ensures that any two similar individuals get similar treatment irrespective of their protected attributes e.g., race, sex, age. Verifying this fairness property is hard because of the global checking and non-linear computation nodes in NN. We proposed sound approach to make individual fairness verification tractable for the developers. The key idea is that many neurons in the NN always remain inactive when a smaller part of the input domain is considered. So, Fairify leverages whitebox access to the models in production and then apply formal analysis based pruning. Our approach adopts input partitioning and then prunes the NN for each partition to provide fairness certification or counterexample. We leveraged interval arithmetic and activation heuristic of the neurons to perform the pruning as necessary. We evaluated Fairify on 25 real-world neural networks collected from four different sources, and demonstrated the effectiveness, scalability and performance over baseline and closely related work. Fairify is also configurable based on the domain and size of the NN. Our novel formulation of the problem can answer targeted verification queries with relaxations and counterexamples, which have practical implications.

We study the problem of training and certifying adversarially robust quantized neural networks (QNNs). Quantization is a technique for making neural networks more efficient by running them using low-bit integer arithmetic and is therefore commonly adopted in industry. Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization, and certification of the quantized representation is necessary to guarantee robustness. In this work, we present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs. Inspired by advances in robust learning of non-quantized networks, our training algorithm computes the gradient of an abstract representation of the actual network. Unlike existing approaches, our method can handle the discrete semantics of QNNs. Based on QA-IBP, we also develop a complete verification procedure for verifying the adversarial robustness of QNNs, which is guaranteed to terminate and produce a correct answer. Compared to existing approaches, the key advantage of our verification procedure is that it runs entirely on GPU or other accelerator devices. We demonstrate experimentally that our approach significantly outperforms existing methods and establish the new state-of-the-art for training and certifying the robustness of QNNs.

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.

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

由于神经网络变得更加强大，因此在现实世界中部署它们的愿望是一个上升的愿望;然而，神经网络的功率和准确性主要是由于它们的深度和复杂性，使得它们难以部署，尤其是在资源受限的设备中。最近出现了神经网络量化，以满足这种需求通过降低网络的精度来降低神经网络的大小和复杂性。具有较小和更简单的网络，可以在目标硬件的约束中运行神经网络。本文调查了在过去十年中开发的许多神经网络量化技术。基于该调查和神经网络量化技术的比较，我们提出了该地区的未来研究方向。

This report summarizes the 3rd International Verification of Neural Networks Competition (VNN-COMP 2022), held as a part of the 5th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS), which was collocated with the 34th International Conference on Computer-Aided Verification (CAV). VNN-COMP is held annually to facilitate the fair and objective comparison of state-of-the-art neural network verification tools, encourage the standardization of tool interfaces, and bring together the neural network verification community. To this end, standardized formats for networks (ONNX) and specification (VNN-LIB) were defined, tools were evaluated on equal-cost hardware (using an automatic evaluation pipeline based on AWS instances), and tool parameters were chosen by the participants before the final test sets were made public. In the 2022 iteration, 11 teams participated on a diverse set of 12 scored benchmarks. This report summarizes the rules, benchmarks, participating tools, results, and lessons learned from this iteration of this competition.

深入学习模型的压缩在将这些模型部署到边缘设备方面具有根本重要性。在压缩期间，在压缩期间结合硬件模型和应用限制可以最大限度地提高优势，但使其专为一种情况而设计。因此，压缩需要自动化。搜索最佳压缩方法参数被认为是一个优化问题。本文介绍了一种多目标硬件感知量化（MohaQ）方法，其将硬件效率和推理误差视为混合精度量化的目标。该方法通过依赖于两个步骤，在很大的搜索空间中评估候选解决方案。首先，应用训练后量化以进行快速解决方案评估。其次，我们提出了一个名为“基于信标的搜索”的搜索技术，仅在搜索空间中重新选出所选解决方案，并将其用作信标以了解刷新对其他解决方案的影响。为了评估优化潜力，我们使用Timit DataSet选择语音识别模型。该模型基于简单的复发单元（SRU），由于其相当大的加速在其他复发单元上。我们应用了我们在两个平台上运行的方法：SILAGO和BETFUSION。实验评估表明，SRU通过训练后量化可以压缩高达8倍，而误差的任何显着增加，误差只有1.5个百分点增加。在Silago上，唯一的搜索发现解决方案分别实现了最大可能加速和节能的80 \％和64 \％，错误的误差增加了0.5个百分点。在BETFUSION上，对于小SRAM尺寸的约束，基于信标的搜索将推断搜索的错误增益减少4个百分点，并且与BitFusion基线相比，可能的达到的加速度增加到47倍。

我们向开放的神经网络交换（ONNX）中间表示格式提出扩展，以表示任意量化的量化神经网络。我们首先通过利用整数剪辑来引入对现有基于ONX的量化格式低精度量化的支持，从而产生了两个新的向后兼容的变体：带有剪辑和量化clip-dequantize（QCDQ）格式的量化运算符格式。然后，我们引入了一种新型的高级ONNX格式，称为量化ONNX（QONNX），该格式介绍了三个新运算符 - Quant，Biporlquant和Trunc，以表示均匀的量化。通过保持QONNX IR高级和灵活性，我们可以针对更广泛的平台。我们还介绍了与QONNX合作的实用程序，以及其在FINN和HLS4ML工具链中使用的示例。最后，我们介绍了QONNX模型动物园，以共享低精确的量化神经网络。

Neural networks are increasingly applied in safety critical domains, their verification thus is gaining importance. A large class of recent algorithms for proving input-output relations of feed-forward neural networks are based on linear relaxations and symbolic interval propagation. However, due to variable dependencies, the approximations deteriorate with increasing depth of the network. In this paper we present DPNeurifyFV, a novel branch-and-bound solver for ReLU networks with low dimensional input-space that is based on symbolic interval propagation with fresh variables and input-splitting. A new heuristic for choosing the fresh variables allows to ameliorate the dependency problem, while our novel splitting heuristic, in combination with several other improvements, speeds up the branch-and-bound procedure. We evaluate our approach on the airborne collision avoidance networks ACAS Xu and demonstrate runtime improvements compared to state-of-the-art tools.

背景信息：在过去几年中，机器学习（ML）一直是许多创新的核心。然而，包括在所谓的“安全关键”系统中，例如汽车或航空的系统已经被证明是非常具有挑战性的，因为ML的范式转变为ML带来完全改变传统认证方法。目的：本文旨在阐明与ML为基础的安全关键系统认证有关的挑战，以及文献中提出的解决方案，以解决它们，回答问题的问题如何证明基于机器学习的安全关键系统？'方法：我们开展2015年至2020年至2020年之间发布的研究论文的系统文献综述（SLR），涵盖了与ML系统认证有关的主题。总共确定了217篇论文涵盖了主题，被认为是ML认证的主要支柱：鲁棒性，不确定性，解释性，验证，安全强化学习和直接认证。我们分析了每个子场的主要趋势和问题，并提取了提取的论文的总结。结果：单反结果突出了社区对该主题的热情，以及在数据集和模型类型方面缺乏多样性。它还强调需要进一步发展学术界和行业之间的联系，以加深域名研究。最后，它还说明了必须在上面提到的主要支柱之间建立连接的必要性，这些主要柱主要主要研究。结论：我们强调了目前部署的努力，以实现ML基于ML的软件系统，并讨论了一些未来的研究方向。

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

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

神经网络越来越依赖于复杂安全系统（例如自动驾驶汽车）的组成部分。对在更大的验证周期中嵌入神经网络验证的工具和方法的需求很高。但是，由于关注的广泛验证属性，很难进行神经网络验证，通常每个验证属性仅适用于专用求解器中的验证。在本文中，我们展示了最初设计用于验证，验证和仿真金融基础架构的功能编程语言的Imandra如何为神经网络验证提供整体基础架构。我们开发了一个新颖的图书馆Checkinn，该图书馆在Imandra的神经网络上形式化，并涵盖了神经网络验证的不同重要方面。

在本文中，我们提供了一种系统的方法来评估和比较数字信号处理中神经网络层的计算复杂性。我们提供并链接四个软件到硬件的复杂性度量，定义了不同的复杂度指标与层的超参数的关系。本文解释了如何计算这四个指标以进行馈送和经常性层，并定义在这种情况下，我们应该根据我们是否表征了面向更软件或硬件的应用程序来使用特定的度量。新引入的四个指标之一，称为“添加和位移位数（NAB）”，用于异质量化。 NABS不仅表征了操作中使用的位宽的影响，还表征了算术操作中使用的量化类型。我们打算这项工作作为与神经网络在实时数字信号处理中应用相关的复杂性估计级别（目的）的基线，旨在统一计算复杂性估计。

QNNVerifier是第一个用于验证神经网络实现的开源工具，以考虑其操作数的有限字长（即量化）。通过采用最先进的软件模型检查（SMC）技术来实现对量化的新颖支持。它将神经网络的实现基于可满足模数理论（SMT）来将神经网络的实现到一阶逻辑的可解除片段。通过给定硬件确定的精度，通过直接实现来表示固定和浮点操作的影响。此外，Qnnverifier允许指定定制安全性能，并使用不同的验证策略（增量和K-Incuction）和SMT求解器来验证所产生的模型。最后，QNNVerifier是第一个通过间隔分析和非线性激活功能的离散化来组合不变推论的工具，以加快级别验证神经网络的级数。 qnnverifier的视频呈现可在https://youtu.be/7jmgol41zty中获得

我们研究了通过具有整流线性单元（Relu）激活的前馈神经网络建模目标函数的优化问题。最近的文献已经探讨了单一神经网络的使用来模拟目标函数内的不确定或复杂元素。然而，众所周知，神经网络的集合产生更稳定的预测，并且具有比具有单个神经网络的模型更好的普遍性，这表明在决策管道中应用神经网络的集合。我们研究如何将神经网络集合纳入优化模型的客观函数，并探索随后的问题的计算方法。我们基于现有流行的大量M $配方提供了一种混合整数线性程序，以优化单个神经网络。我们为我们的模型开发了两个加速技术，首先是一种预处理程序，用于拧紧神经网络中的关键神经元的界限，而第二个是基于弯曲分解的一组有效的不等式。我们解决方案方法的实验评估在一个全球优化问题和两个现实世界数据集中进行;结果表明，我们的优化算法在计算时间和最优性间隙方面优于最先进的方法的适应。

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