MUC-G4: Accelerating Incremental Verification of Compressed Neural Networks via Minimal UNSAT Core Reuse

The optimization of Deep Neural Networks (DNNs) for resource-constrained environments through quantization and pruning necessitates efficient re-verification to ensure safety. However, existing incremental verification methods are primarily designed for numerical parameter perturbations and often struggle to handle the discrete structural changes introduced by network pruning. Moreover, traditional approaches verify each model variant from scratch, discarding the significant computational effort invested in the original model’s proof. In this paper, we present MUC-G4 , an incremental verification framework that accelerates the certification of compressed DNNs via search space pruning. Inspired by the principles of residual reasoning and conflict-driven learning , MUC-G4 identifies Minimal UNSAT Cores (MUCs) as robust proof artifacts that capture the local logical reasons for safety. Our work is grounded in the insight of Locality of Conflicts : the logical contradictions that guarantee safety are often independent of the redundant neurons and connections targeted by compression algorithms. MUC-G4 extracts these MUCs from the original network’s proof and utilizes them as a warm-start mechanism to identify and prune stable infeasible regions in the compressed network’s search space. Experimental results on the ACAS Xu and MNIST benchmarks demonstrate that safety proofs exhibit high structural resilience. Crucially, the framework maintains full completeness through a residual solving phase, ensuring that all newly exposed search paths are rigorously verified. Our findings suggest that formal proofs can effectively evolve alongside optimized network variants, providing a scalable foundation for the continuous certification of safety-critical machine learning systems.