ML Security PapersVerifying Local Robustness of Pruned Safety-Critical Networks
Minh Le 1, Phuong Cao 2
Published on arXiv
2601.13303
Input Manipulation Attack
OWASP ML Top 10 — ML01
Key Finding
Heavy pruning (70–90%) improves provable L∞ robustness on the JPL Mars Frost dataset beyond unpruned baselines, while light pruning (40%) is optimal for MNIST, revealing that the optimal pruning ratio varies significantly by dataset.
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.
Key Contributions
- First empirical study of how varying pruning ratios (0–90%) affect formal local robustness certificates for safety-critical DNNs
- Demonstrates a non-linear, dataset-dependent relationship: 40% pruning optimizes verifiability on MNIST, while 70–90% pruning optimizes it on NASA JPL Mars Frost
- Provides practical guidance for deploying formally verified pruned networks in high-stakes domains (autonomous spacecraft, medical AI)
🛡️ Threat Analysis
Paper is fundamentally about certifying the absence of adversarial examples within an L∞ epsilon ball — formal verification is a defense against Input Manipulation Attacks. The contribution is understanding how magnitude-based pruning affects the verifiability of these certificates across different datasets.