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

TL;DR

SimCert is a probabilistic framework that verifies behavioral similarity in compressed neural networks, providing scalable, quantitative safety guarantees for resource-constrained embedded systems.

Contribution

It introduces a dual-network symbolic propagation method and variance-aware bounding technique for scalable, probabilistic certification of compressed DNNs.

Findings

Outperforms state-of-the-art verification methods

Provides adjustable confidence safety guarantees

Effective on ACAS Xu and vision benchmarks

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.