用最小不满足核心引导，高效验证压缩神经网络的正确性。
MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression
- 基于最小不满足核心，动态引导压缩后的网络验证。
- 验证速度比传统方法快，证明复用率高。
- 适合需要可靠压缩的边缘设备部署场景。
深度学习的快速发展带来了在边缘设备上部署神经网络的挑战，主要源于其高内存和运行时复杂度。网络压缩技术（如量化与剪枝）旨在降低复杂度的同时保持精度。然而，现有增量验证方法多仅关注量化，难以应对结构变化。本文提出MUC-G4（最小不满足核心引导的增量验证框架），将原始与压缩网络编码为SMT公式，分类变化并利用原始网络的最小不满足核心（MUCs）指导压缩网络的高效验证。实验表明，该方法在处理量化与剪枝时均有效，具有高证明复用率，并显著提升验证速度，相较传统方法有明显加速。MUC-G4为压缩神经网络在实际应用中的安全性与可靠性提供了可行方案。
原文摘要 · Abstract (English)
The rapid development of deep learning has led to challenges in deploying neural networks on edge devices, mainly due to their high memory and runtime complexity. Network compression techniques, such as quantization and pruning, aim to reduce this complexity while maintaining accuracy. However, existing incremental verification methods often focus only on quantization and struggle with structural changes. This paper presents MUC-G4 (Minimal Unsat Core-Guided Incremental Verification), a novel framework for incremental verification of compressed deep neural networks. It encodes both the original and compressed networks into SMT formulas, classifies changes, and use \emph{Minimal Unsat Cores (MUCs)} from the original network to guide efficient verification for the compressed network. Experimental results show its effectiveness in handling quantization and pruning, with high proof reuse rates and significant speedup in verification time compared to traditional methods. MUC-G4 hence offers a promising solution for ensuring the safety and reliability of compressed neural networks in practical applications.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。