Benchmark: Formal Verification of Semantic Segmentation Neural Networks

Formal verification utilizes a rigorous approach to ensure the absence of critical errors and validate models against predefined properties. While significant progress has been made in verification methods for various deep neural networks (DNNs), such as feed-forward neural networks (FFNNs) and convolutional neural networks (CNNs), the application of these techniques to semantic segmentation remains largely unexplored. Semantic segmentation networks are vital in computer vision applications, where they assign semantic labels to individual pixels within an image. Given their deployment in safety-critical domains, ensuring the correctness of these networks becomes paramount. This paper presents a comprehensive benchmark study on applying formal verification techniques to semantic segmentation networks. We explore a diverse set of state-of-the-art semantic segmentation datasets and generate neural network models, including fully-convolutional networks and encoder-decoder architectures. Our investigation encompasses a wide range of verification properties, focusing on the robustness of these models against bounded adversarial vulnerabilities. To evaluate the networks’ performance, we employ set-based reachability algorithms to calculate the output reachable set(s) and some state-of-the-art performance measures for a comparative study among the networks. This benchmark paper aims to provide the formal verification community with several semantic segmentation networks and their robustness specifications for future use cases in different neural network verification competitions.