Deep Neural Networks (DNNs) are ubiquitous in real-world applications, yet they remain vulnerable to errors and adversarial attacks. This work tackles the challenge of applying formal verification to ensure the safety of computer vision models, extending verification beyond image classification to object detection. We propose a general formulation for certifying the robustness of object detection models using formal verification and outline implementation strategies compatible with state-of-the-art verification tools. Our approach enables the application of these tools, originally designed for verifying classification models, to object detection. We define various attacks for object detection, illustrating the diverse ways adversarial inputs can compromise neural network outputs. Our experiments, conducted on several common datasets and networks, reveal potential errors in object detection models, highlighting system vulnerabilities and emphasizing the need for expanding formal verification to these new domains. This work paves the way for further research in integrating formal verification across a broader range of computer vision applications.

翻译：深度神经网络（DNNs）在现实世界应用中无处不在，然而它们仍然容易受到错误和对抗性攻击的影响。本研究致力于应对应用形式化验证以确保计算机视觉模型安全性的挑战，将验证范围从图像分类扩展到目标检测。我们提出了一种利用形式化验证来认证目标检测模型鲁棒性的通用框架，并概述了与最先进验证工具兼容的实现策略。我们的方法使得这些最初为验证分类模型而设计的工具能够应用于目标检测。我们定义了针对目标检测的各种攻击，阐明了对抗性输入可能损害神经网络输出的多种方式。我们在多个常用数据集和网络上进行的实验揭示了目标检测模型中潜在的错误，突显了系统漏洞，并强调了将形式化验证扩展到这些新领域的必要性。这项工作为进一步研究将形式化验证整合到更广泛的计算机视觉应用中铺平了道路。