一句话：提出 FANC，首次在原始网络与多个近似版本间迁移鲁棒性验证证明，显著加速认证。
后训练量化、剪枝等近似优化在加速推理的同时改变了神经网络，若对每个近似版本从头进行鲁棒性验证，代价高昂且不切实际。本文提出 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, L 0 , 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.
@article{paperbot1512,
title = {Proof transfer for fast certification of multiple approximate neural networks},
author = {Shubham Ugare and Gagandeep Singh and Sasa Misailovic},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA1},
year = {2022},
doi = {10.1145/3527319}
}