Verifying Local Robustness of Pruned Safety-Critical Networks

TL;DR

The paper tackles the challenge of verifying local robustness for safety-critical neural networks under model pruning. It trains ResNet4 models on MNIST and NASA JPL Mars Frost Identification, applies magnitude-based pruning to convolutional layers with retraining to preserve accuracy, and uses the state‑of‑the‑art verifier $α,β$-CROWN to certify local $L_ inf$ robustness on 100 inputs within a 5‑minute budget per input. A key finding is a non‑linear, dataset-dependent effect of pruning: light pruning (≈40–50%) improves verifiability on MNIST, while heavy pruning (≈70–80%) yields the best provable robustness on Mars Frost, often outperforming unpruned baselines. This suggests pruning can simplify the search space for formal solvers, but the optimal pruning ratio varies with task and data, informing practical deployment of efficient yet certifiably robust DNNs in high-stakes contexts.

Abstract

Formal verification of Deep Neural Networks (DNNs) is essential for safety-critical applications, ranging from surgical robotics to NASA JPL autonomous systems. However, the computational cost of verifying large-scale models remains a significant barrier to adoption. This paper investigates the impact of pruning on formal local robustness certificates with different ratios. Using the state-of-the-art $α,β$-CROWN verifier, we evaluate ResNet4 models across varying pruning ratios on MNIST and, more importantly, on the NASA JPL Mars Frost Identification datasets. Our findings demonstrate a non-linear relationship: light pruning (40%) in MNIST and heavy pruning (70%-90%) in JPL improve verifiability, allowing models to outperform unpruned baselines in proven $L_\infty$ robustness properties. This suggests that reduced connectivity simplifies the search space for formal solvers and that the optimal pruning ratio varies significantly between datasets. This research highlights the complex nature of model compression, offering critical insights into selecting the optimal pruning ratio for deploying efficient, yet formally verified, DNNs in high-stakes environments where reliability is non-negotiable.