Formal Verification of Deep Neural Networks for Object Detection

TL;DR

The ability of formal verification to uncover vulnerabilities in object detection models is highlighted, underscoring the need to extend verification efforts to this domain and laying the foundation for further research into formal verification across a broader range of computer vision applications.

Abstract

Deep neural networks (DNNs) are widely used in real-world applications, yet they remain vulnerable to errors and adversarial attacks. Formal verification offers a systematic approach to identify and mitigate these vulnerabilities, enhancing model robustness and reliability. While most existing verification methods focus on image classification models, this work extends formal verification to the more complex domain of emph{object detection} models. We propose a formulation for verifying the robustness of such models and demonstrate how state-of-the-art verification tools, originally developed for classification, can be adapted for this purpose. Our experiments, conducted on various datasets and networks, highlight the ability of formal verification to uncover vulnerabilities in object detection models, underscoring the need to extend verification efforts to this domain. This work lays the foundation for further research into formal verification across a broader range of computer vision applications.

Figures (5)

• Figure 1: Examples of attacked images. The rightmost column shows original images, while the others display attacked images with different noise levels (maximum allowed noise $\epsilon$). The top two rows illustrate misdetection (IoU > 0.5 is needed for correct detection, see Sec. \ref{['sec:prelim']}), and the bottom two rows show misclassification into class $C$ (class mapping is detailed in WeKa17).
• Figure 2: Encoding IoU operation; At first, the area of the intersection and the area of the union are extracted into couple of neurons. Then, the equivalent condition is encoded using a single neural layer, and the output $z$ is positive if and only if $\text{IoU}{}>\tau$.
• Figure 3: (Top) Misdetection results per epsilon. (Bottom) Misclassification results per epsilon.
• Figure 4: Misdetection examples on all datasets. Ground truth (green bounding boxes), with misdetected objects (red bounding boxes) under adversarial attacks of varying noise levels.
• Figure 5: Effect of $\tau$. The number of Unsafe results increases with $\tau$.

Theorems & Definitions (4)

• proposition 1
• proof
• proposition 2
• proof