Proof transfer for fast certification of multiple approximate neural networks
Proof transfer for fast certification of multiple approximate neural networks
复制标题
DOI：
10.1145/3527319
复制
发表时间：
2022-04
影响因子：
--
通讯作者：
Shubham Ugare;Gagandeep Singh
中科院分区：
文献类型：
--
作者：
Shubham Ugare;Gagandeep Singh
机器学习应用程序的开发人员经常应用训练后神经网络优化（例如量化和剪枝）来近似神经网络，以加快推理速度并降低能耗，同时保持高精度和鲁棒性。尽管最近用于神经网络鲁棒性验证的技术激增，但几乎所有最先进方法的一个主要限制是，每次网络稍微修改时，验证都需要从头开始运行。在许多使用或比较多个近似网络版本的场景中，为每个新网络从头开始运行精确的端到端验证是昂贵且不切实际的，并且需要有效验证所有网络的鲁棒性。我们提出了 FANC，这是第一个在给定网络及其多个近似版本之间传输证明而不影响验证器精度的通用技术。为了重用验证原始网络时获得的证明，FANC 生成一组模板——原始网络中间层连接的符号形状——捕获要验证的属性的证明。我们提出了用于生成和转换模板的新颖算法，该算法可推广到广泛的近似网络并降低验证成本。我们提出了全面的评估，证明了我们方法的有效性。我们考虑通过应用流行的近似技术（例如全连接和卷积架构上的量化和修剪）获得的一组不同的网络，并验证它们针对不同对抗性攻击（例如对抗性补丁、L0、旋转和增亮）的鲁棒性。我们的结果表明，FANC 可以将最先进的验证器 DeepZ 的验证速度显着提高高达 4.1 倍。
Developers of machine learning applications often apply post-training neural network optimizations, such as quantization and pruning, that approximate a neural network to speed up inference and reduce energy consumption, while maintaining high accuracy and robustness. Despite a recent surge in techniques for the robustness verification of neural networks, a major limitation of almost all state-of-the-art approaches is that the verification needs to be run from scratch every time the network is even slightly modified. Running precise end-to-end verification from scratch for every new network is expensive and impractical in many scenarios that use or compare multiple approximate network versions, and the robustness of all the networks needs to be verified efficiently. We present FANC, the first general technique for transferring proofs between a given network and its multiple approximate versions without compromising verifier precision. To reuse the proofs obtained when verifying the original network, FANC generates a set of templates – connected symbolic shapes at intermediate layers of the original network – that capture the proof of the property to be verified. We present novel algorithms for generating and transforming templates that generalize to a broad range of approximate networks and reduce the verification cost. We present a comprehensive evaluation demonstrating the effectiveness of our approach. We consider a diverse set of networks obtained by applying popular approximation techniques such as quantization and pruning on fully-connected and convolutional architectures and verify their robustness against different adversarial attacks such as adversarial patches, L0, rotation and brightening. Our results indicate that FANC can significantly speed up verification with state-of-the-art verifier, DeepZ by up to 4.1x.