Benchmarking Formal Verification for Autonomous Driving in the Wild

The verification of the security of neural networks is cruicial, especially for the field of autonomous driving. Although there are currently benchmarks for the verification of the robustness of neural networks, there are hardly any benchmarks related to the field of autonomous driving, especially those related to object detection and semantic segmentation. Thus, a notable gap exists in formally verifying the robustness of semantic semantic segmentation and object detection tasks under complex, real-world conditions. To address this, we present an innovative approach to benchamark formal verification for autonomous driving perception tasks. Firstly, we propose robust verification benchmarks for semantic segmentation and object detection, supplementing existing methods. Secondly, and more significantly, we introduce a novel patch-level disturbance approach for object detection, providing a more realistic representation of real-world scenarios. By augmenting the current verification benchmarks with our novel proposals, our work contributes towards developing a more comprehensive, practical, and realistic benchmarking methodology for perception tasks in autonomous driving, thereby propelling the field towards improved safety and reliability.