Benchmarking provable resilience in convolutional neural networks: A study with Beta-CROWN and ERAN

Robust verification of neural networks is a critical property, particularly in the context of safety-critical applications. Despite its importance, achieving both accurate and efficient verification remains a significant challenge. This study focuses on the robustness of convolutional neural networks (CNNs), which are widely deployed in domains such as autonomous driving and medical diagnostics, where failure is not an option. We explored two state-of-the-art verification techniques, namely Beta-CROWN and ERAN, that leverage linear approximation methods to handle the inherent non-linearity of neural networks. Both approaches approximate nonlinear constraints to enable tractable formal verification. A comparative analysis is conducted to evaluate their performance in terms of certification accuracy and computational efficiency. Our findings provide insights into the practical trade-offs between these techniques and guide future work in provable resilience of CNNs.