EqBaB：针对压缩深度神经网络（DNNs）的高效等价性验证方法，支持有界传播（bounded propagation）

《Neurocomputing》：EqBaB: Efficient equivalence verification for compressed DNNs with bound propagation

模型压缩后DNN等价性验证方法研究，提出EqBaB框架通过合并网络和分支限界技术高效计算最大输出偏差，验证压缩模型与原始模型的功能一致性。实验表明该方法在输入域扩大和深层网络场景下扩展性优于现有方法，验证时间仅增加11倍，且能准确评估量化、剪枝等压缩方法的影响。

　　

莫子豪|向伟明

美国乔治亚州奥古斯塔大学计算机与网络科学学院，15街1120号，邮编30912

摘要

在安全关键和资源受限的应用中对深度神经网络（DNNs）的需求不断增加，这突显了在边缘设备上部署模型压缩技术的重要性。然而，压缩可能会无意中降低性能，从而影响DNNs的可靠性。为了评估压缩后的DNNs是否与参考DNNs具有等效的行为，迫切需要开发正式的等效性验证方法。在这项研究中，我们提出了EqBaB，这是一个基于分支定界（BaB）的等效性验证框架，旨在正式评估参考DNN与其压缩版本之间的最大输出差异。我们提出了一种合并网络构建方法，该方法同时编码两个网络，并调整界限传播技术以计算它们输出差异的紧密区间界限。EqBaB将等效性验证定义为限制最坏情况下的输出差异，并确定其是否在用户定义的容忍度范围内。与其他等效性验证方法相比，EqBaB能够更有效地处理更大的输入域和更复杂的网络结构。例如，当输入复杂性增加超过170倍时，EqBaB的验证时间仅增加了11倍。我们进一步比较了八种不同的压缩方法，以展示EqBaB的性能，并全面分析了压缩带来的差异及其对模型等效性的影响。

引言

近年来，深度神经网络（DNNs）在各个行业中的应用迅速扩展，包括农业领域[1]、自然环境[2]和发电厂[3]。这些网络在感知和决策任务中表现出色。然而，在现实世界系统中部署DNNs，特别是在边缘或嵌入式设备上，由于计算能力、内存和能源预算等资源限制，仍然具有挑战性。为了解决这些限制，已经开发了许多模型压缩技术。诸如压缩感知[4]、剪枝[5]和量化[6]等方法旨在在保持预测性能的同时减少模型大小和推理成本。然而，这些压缩方法不可避免地会引入错误，可能导致模型行为的微妙或严重偏差[7]。在安全关键的应用中，参考模型和压缩模型输出之间的即使是微小差异也可能导致错误的决策或系统故障[7]、[8]。因此，确保参考DNN和压缩DNN之间的性能等效性已成为可信部署信息物理系统（CPS）的关键问题。

这提出了一个重要的研究问题：我们能否验证压缩后的DNN在给定的容忍度范围内保留了其参考模型的基本功能行为或“属性”？已经提出了几种验证工具来评估压缩DNN的性能，旨在验证是否满足给定的规范。早期的工作，如SAT/SMT求解器[9]和MILP求解器[10]，为验证算法奠定了基础，但在网络规模和非线性函数方面存在局限性。一些新的方法，如奖励鞅[11]和抽象方法[12]也被提出。一般来说，验证方法分为三类：优化、可达性和基于搜索的验证[13]。基于可达性的算法在精确计算可达集方面具有优势，但成本较高，例如Zonotope[14]和Star set[15]。VeriNet[16]、CROWN[17]和其他BaB方法被归类为基于搜索的算法，可以更快地验证，且保守性较低。这些传统的验证工具适用于分析单个DNN，但缺乏对等效性验证的支持。这些正式的验证方法确实可以有效地验证任何基于规定规范的DNN，但由于同时验证两个DNN需要更长的时间和更多资源，等效性验证相对被忽视了。等效性验证的价值在于，它可以揭示两个DNN之间的性能差异，更重要的是，它们的属性差异。在涉及DNN升级和部署的场景中，用户更感兴趣的是了解压缩后的DNN是否与参考DNN一致地表现，换句话说，是否保留了参考DNN的属性。如果压缩后的网络表现不佳，识别两个DNN之间的差异对于进一步改进至关重要，而这正是压缩DNN的正式验证所缺乏的。因此，等效性验证具有其独特的价值。

为了填补等效性验证的空白，已经提出了一些方法来解决等效性验证问题；例如，QEBVerif方法[18]深入研究了量化界限的计算和验证，而[19]基于可达性分析对网络压缩方法进行验证，并提供精确的输出可达集以指示两个DNN之间的差异。为了正式定义两个DNN之间的等效关系，提出了$$-等效性和top-1-等效性作为评估指标[20]。这些指标的目的是量化两个DNN之间行为函数的差异，这也解释了它们之间的属性差异。神经网络的属性通常反映在其特定任务上的性能上，例如图像识别或语音识别[21]。为了直观地描述网络属性的差异，$$-等效性和top-1-等效性提供了数值规范，以验证属性差异，并为等效性验证的定量比较提供了基础。基于这些指标，迄今为止已经提出了一些方法，如MILPEQUIV[22]、ReluDiff[23]和NNEQUIV[24]。这些开创性的等效性验证方法扩展了神经网络验证的范围。然而，作为先驱，这些方法仍然遵循传统验证方法的路径，往往只能提供DNN之间的定性比较，这不足以解决之前提出的问题。

为了推进等效性验证，我们将其重新定义为最大差异估计任务：对于给定的输入空间，我们计算参考DNN和压缩DNN输出之间的最坏情况偏差。然后，我们确定这种偏差是否在预定义的阈值范围内。在这项研究中，我们提出了EqBaB，这是一个高效且可扩展的基于BaB的压缩DNN等效性验证框架。EqBaB首先构建了一个合并网络，将参考DNN和压缩DNN编码到统一的架构中。该合并网络同步计算两个DNN的中间状态，并通过一个特殊层直接产生输出差异。然后，EqBaB应用紧密的界限传播来估计差异的上界和下界，并结合分支分割来在非线性存在的情况下细化结果。将最大差异与用户定义的容忍度进行比较，以确定两个DNN在扰动下是否等效。总之，本研究提供了以下贡献：

•

合并结构等效性验证框架。 通过将两个DNN嵌入到分支定界范式中的单个合并网络中，我们捕获了两个模型的所有信息，便于差异分析，并为迭代细化提供了定量验证结果。

•

高效的最大差异计算。 我们使用具有具体值的最大差异指标定义和形式化了$$-等效性，而不是定性结果，并在分段线性操作下证明了界限紧密性的理论保证，减少了近似次数，避免了暴力搜索，从而获得了更接近精确输出的验证结果。

•

全面的实验评估。 我们在多个DNN架构和数据集上对EqBaB进行了实证评估，并将其与现有的等效性验证方法进行了比较。我们的实验表明，EqBaB具有更高的验证率、更短的验证时间和更好的准确性，同时随着输入复杂性的增加而更有效地扩展。

本研究的其余部分结构如下：第2节介绍了一些关于DNN验证的相关研究。第3节提出了压缩DNN的问题表述，并介绍了我们的正式指标——最大差异，用于等效性验证。第4节介绍了我们提出的方法EqBaB，包括合并框架的定义和在合并框架下的界限传播的理论基础。第5节展示了一系列实验，证明了EqBaB的效率，第6节总结了本研究并提出了未来的工作方向。

章节片段

神经网络

神经网络的概念灵感来自人类神经系统，它通过神经元处理和传输信号。其优势在于能够以任意精度近似各种函数。它对每个神经元进行参数化并连接它们，然后通过多层信息传输模拟非线性函数。一般来说，深度神经网络$$模拟了一个变换$$，将输入$$映射为输出

初步介绍和问题表述

神经网络验证的目标是建立正式保证，确保给定的DNN在定义的输入集上满足指定的属性，通常由模拟操作环境的不等式来表征。为了满足边缘平台的严格内存、能源和延迟限制，大型网络通常会被压缩，只有当压缩模型在保持所需功能的同时满足这些资源限制时，部署才成为可能。

EqBaB对DNN压缩的验证

在前一节中，我们定义了$$-等效性验证问题，并提出了基于最大差异的压缩DNN的等效性。为了解决等效性验证问题并提供定量结果，我们引入了一种高效的等效性验证方法EqBaB，该方法采用分支定界策略进行推理，并将最大差异作为验证指标。EqBaB结合参考DNN和压缩DNN构建了一个合并网络

实验和评估

在前一节中，我们详细描述了我们的方法。为了证明其实用性和效率，我们在本实验部分进行了全面的比较和性能分析。我们进行了三项实验，将我们的方法与不同的方法和压缩方法进行了比较，并从多个角度展示了其优势。

•

与等效性验证工具的比较（第5.1节）。 在第一个实验中，我们主要将我们的EqBaB验证工具与

结论和进一步评论

本文介绍了EqBaB，这是一个高效且严谨的基于分支定界的框架，用于正式验证压缩深度神经网络（DNNs）与其原始验证对应物之间的等效性。鉴于神经网络在安全关键、资源受限环境中的使用日益增加，我们强调了确保压缩DNN与参考DNN一致表现的重要性，以避免在模型行为中引入有害错误并保持

CRediT作者贡献声明

莫子豪：写作——审稿与编辑，撰写——原始草稿，可视化，验证，软件，资源，项目管理，方法论，调查，形式分析，数据整理，概念化。向伟明：写作——审稿与编辑，监督，项目管理，资金获取，概念化。

利益冲突声明

作者声明以下可能被视为潜在利益冲突的财务利益/个人关系：

向伟明报告称获得了国家科学基金会的财务支持。如果有其他作者，他们声明没有已知的财务利益或个人关系可能影响本文中报告的工作。

莫子豪于2019年在中国广州的华南理工大学获得信息科学学士学位，2019年在美国密苏里州哥伦比亚市的密苏里大学获得电气工程学士学位，2021年在美国加利福尼亚州圣地亚哥的加州大学圣地亚哥分校获得电气与计算机工程硕士学位。他目前正在美国乔治亚州奥古斯塔大学攻读计算机与网络科学博士学位。他的研究兴趣是验证和