SimCert: Probabilistic Certification for Behavioral Similarity in Deep Neural Network Compression

Abstract

Deploying Deep Neural Networks (DNNs) on resource-constrained embedded systems requires aggressive model compression techniques like quantization and pruning. However, ensuring that the compressed model preserves the behavioral fidelity of the original design is a critical challenge in the safety-critical system design flow. Existing verification methods often lack scalability or fail to handle the architectural heterogeneity introduced by pruning. In this work, we propose SimCert, a probabilistic certification framework for verifying the behavioral similarity of compressed neural networks. Unlike worst-case analysis, SimCert provides quantitative safety guarantees with adjustable confidence levels. Our framework features: (1) A dual-network symbolic propagation method supporting both quantization and pruning; (2) A variance-aware bounding technique using Bernstein's inequality to tighten safety certificates; and (3) An automated verification toolchain. Experimental results on ACAS Xu and computer vision benchmarks demonstrate that SimCert outperforms state-of-the-art baselines.

Figures (5)

• Figure 1: Diagram of network notations
• Figure 2: The pair of neural networks of the original one and the quantized one.
• Figure 3: Naive encoding to compute the difference of the two neural networks
• Figure 4: Conceptual illustration of Dual-Network Symbolic Error Propagation.
• Figure 5: Comparison of width reduction between Bernstein's (Our approach) and Hoeffding's (PROVEN) inequalities

Theorems & Definitions (12)

• definition 1: Qualitative $\epsilon$-Similarity Certification
• definition 2: $\epsilon$-$\gamma$ Similarity Certification
• definition 3
• remark 1: Structural Correlation vs. Naive Analysis
• lemma 1: Hoeffding's Inequality
• theorem 1: Hoeffding-Based Probabilistic Bound
• proof
• lemma 2: Bernstein's Inequality
• proposition 1: Tightness Condition
• proof