Understanding ReLU Network Robustness Through Test Set Certification Performance

Neural networks can be vulnerable to small changes in input within their learning distribution, and this vulnerability increases for distributional shifts or input completely outside their training distribution. To ensure networks are used safely, robustness certificates offer formal assurances about the stability of their predictions in a pre-defined range around the input. However, the relationship between correctness and certified robustness remains unclear. In this work, we investigate the unexpected outcomes of verification methods applied to piecewise linear classifiers for clean, perturbed, in- and out-of-distribution samples. In our experiments focused on image classification, we observed that introducing a modest stability margin around the input sample leads to an important reduction in misclassified samples - approximately a 75% decrease - compared to the roughly 11% for samples that are correctly classified. This finding emphasizes the value of formal verification methods as an extra layer of safety, illustrating their effectiveness in enhancing accuracy for data that falls within the distribution. On the other hand, we provide a theoretical demonstration that formal verification methods robustly certify samples sufficiently far from the training distribution. These results are integrated with an experimental analysis and demonstrate their limitations compared to standard out-of-distribution detection methods.