MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression

• URL: http://arxiv.org/abs/2506.04268v1
• Date: Tue, 03 Jun 2025 12:42:15 GMT
• Title: MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression
• Abstract summary: MUC-G4 is a novel framework for incremental verification of compressed deep neural networks.<n>It encodes both the original and compressed networks into SMT formulas, classifies changes, and use emphMinimal Unsat Cores (MUCs) from the original network to guide efficient verification for the compressed network.
• Score: 7.9569432009714145
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Reducing Storage of Pretrained Neural Networks by Rate-Constrained Quantization and Entropy Coding [56.066799081747845]
  The ever-growing size of neural networks poses serious challenges on resource-constrained devices.<n>We propose a novel post-training compression framework that combines rate-aware quantization with entropy coding.<n>Our method allows for very fast decoding and is compatible with arbitrary quantization grids.
  arXiv  Detail & Related papers  (2025-05-24T15:52:49Z)
• Accelerating Error Correction Code Transformers [56.75773430667148]
  We introduce a novel acceleration method for transformer-based decoders. We achieve a 90% compression ratio and reduce arithmetic operation energy consumption by at least 224 times on modern hardware.
  arXiv  Detail & Related papers  (2024-10-08T11:07:55Z)
• Automatic Network Adaptation for Ultra-Low Uniform-Precision Quantization [6.1664476076961146]
  Uniform-precision neural network quantization has gained popularity since it simplifies densely packed arithmetic unit for high computing capability. It ignores heterogeneous sensitivity to the impact of quantization errors across the layers, resulting in sub-optimal inference. This work proposes a novel neural architecture search called neural channel expansion that adjusts the network structure to alleviate accuracy degradation from ultra-low uniform-precision quantization.
  arXiv  Detail & Related papers  (2022-12-21T09:41:25Z)
• Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks [58.195261590442406]
  We study the problem of training and certifying adversarially robust quantized neural networks (QNNs) Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization. We present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs.
  arXiv  Detail & Related papers  (2022-11-29T13:32:38Z)
• A Faster Approach to Spiking Deep Convolutional Neural Networks [0.0]
  Spiking neural networks (SNNs) have closer dynamics to the brain than current deep neural networks. We propose a network structure based on previous work to improve network runtime and accuracy.
  arXiv  Detail & Related papers  (2022-10-31T16:13:15Z)
• CEG4N: Counter-Example Guided Neural Network Quantization Refinement [2.722899166098862]
  We propose Counter-Example Guided Neural Network Quantization Refinement (CEG4N) This technique combines search-based quantization and equivalence verification. We produce models with up to 72% better accuracy than state-of-the-art techniques.
  arXiv  Detail & Related papers  (2022-07-09T09:25:45Z)
• ZippyPoint: Fast Interest Point Detection, Description, and Matching through Mixed Precision Discretization [71.91942002659795]
  We investigate and adapt network quantization techniques to accelerate inference and enable its use on compute limited platforms. ZippyPoint, our efficient quantized network with binary descriptors, improves the network runtime speed, the descriptor matching speed, and the 3D model size. These improvements come at a minor performance degradation as evaluated on the tasks of homography estimation, visual localization, and map-free visual relocalization.
  arXiv  Detail & Related papers  (2022-03-07T18:59:03Z)
• Compact representations of convolutional neural networks via weight pruning and quantization [63.417651529192014]
  We propose a novel storage format for convolutional neural networks (CNNs) based on source coding and leveraging both weight pruning and quantization. We achieve a reduction of space occupancy up to 0.6% on fully connected layers and 5.44% on the whole network, while performing at least as competitive as the baseline.
  arXiv  Detail & Related papers  (2021-08-28T20:39:54Z)
• Scalable Verification of Quantized Neural Networks (Technical Report) [14.04927063847749]
  We show that bit-exact implementation of quantized neural networks with bit-vector specifications is PSPACE-hard. We propose three techniques for making SMT-based verification of quantized neural networks more scalable.
  arXiv  Detail & Related papers  (2020-12-15T10:05:37Z)
• Finite Versus Infinite Neural Networks: an Empirical Study [69.07049353209463]
  kernel methods outperform fully-connected finite-width networks. Centered and ensembled finite networks have reduced posterior variance. Weight decay and the use of a large learning rate break the correspondence between finite and infinite networks.
  arXiv  Detail & Related papers  (2020-07-31T01:57:47Z)
• Efficient Integer-Arithmetic-Only Convolutional Neural Networks [87.01739569518513]
  We replace conventional ReLU with Bounded ReLU and find that the decline is due to activation quantization. Our integer networks achieve equivalent performance as the corresponding FPN networks, but have only 1/4 memory cost and run 2x faster on modern GPU.
  arXiv  Detail & Related papers  (2020-06-21T08:23:03Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.