MUC-G4：面向深度神经网络压缩的极小不可满足核引导增量验证
机器学习
2025-06-06 v1 人工智能
摘要
深度学习的快速发展导致在边缘设备上部署神经网络面临挑战，这主要是由于其高内存和运行时复杂度。网络压缩技术，如量化和剪枝，旨在降低这种复杂性的同时保持准确率。然而，现有的增量验证方法通常只关注量化，并且难以处理结构变化。本文提出了MUC-G4（极小不可满足核引导增量验证），一种用于压缩深度神经网络增量验证的新颖框架。它将原始网络和压缩网络都编码为SMT公式，分类变化，并使用来自原始网络的极小不可满足核（MUC）来引导对压缩网络的高效验证。实验结果表明了其在处理量化和剪枝方面的有效性，与传统方法相比，具有高证明重用率和显著的验证时间加速。因此，MUC-G4为在实际应用中确保压缩神经网络的安全性和可靠性提供了一种有前景的解决方案。
引用
@article{arxiv.2506.04268,
title = {MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression},
author = {Jingyang Li and Guoqiang Li},
journal= {arXiv preprint arXiv:2506.04268},
year = {2025}
}