Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2506.04268 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915326988386304 |
|---|---|
| author | Li, Jingyang Li, Guoqiang |
| author_facet | Li, Jingyang Li, Guoqiang |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_04268 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression Li, Jingyang Li, Guoqiang Machine Learning Artificial Intelligence 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. |
| title | MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression |
| topic | Machine Learning Artificial Intelligence |
| url | https://arxiv.org/abs/2506.04268 |