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.

翻译：深度神经网络（DNN）的形式化验证对于安全关键应用至关重要，其应用范围涵盖从手术机器人到NASA喷气推进实验室（JPL）自主系统等多个领域。然而，验证大规模模型的计算成本仍然是实际应用中的一个主要障碍。本文研究了不同剪枝比例对形式化局部鲁棒性证明的影响。利用最先进的 $α,β$-CROWN 验证器，我们在MNIST数据集上，更重要的是在NASA JPL火星霜冻识别数据集上，评估了不同剪枝比例下的ResNet4模型。我们的研究结果揭示了一种非线性关系：在MNIST数据集上轻度剪枝（40%）以及在JPL数据集上重度剪枝（70%-90%）均能提升模型的可验证性，使得这些模型在已证明的 $L_\infty$ 鲁棒性属性上优于未剪枝的基线模型。这表明，减少网络连接简化了形式化求解器的搜索空间，并且最优剪枝比例在不同数据集间存在显著差异。本研究揭示了模型压缩的复杂性，为在高风险、可靠性不容妥协的环境中，选择最优剪枝比例以部署高效且经过形式化验证的DNN提供了关键见解。