Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

IoUCert: Robustness Verification for Anchor-based Object Detectors

Benedikt Brückner, Alejandro J. Mercado, Yanghao Zhang, Panagiotis Kouvaros, Alessio Lomuscio

TL;DR

Focusing on the object localisation component in single-object settings, a coordinate transformation is proposed that enables the algorithm to circumvent precision-degrading relaxations of non-linear box prediction functions and enables a novel Interval Bound Propagation method that derives optimal IoU bounds.

Abstract

While formal robustness verification has seen significant success in image classification, scaling these guarantees to object detection remains notoriously difficult due to complex non-linear coordinate transformations and Intersection-over-Union (IoU) metrics. We introduce {\sc \sf IoUCert}, a novel formal verification framework designed specifically to overcome these bottlenecks in foundational anchor-based object detection architectures. Focusing on the object localisation component in single-object settings, we propose a coordinate transformation that enables our algorithm to circumvent precision-degrading relaxations of non-linear box prediction functions. This allows us to optimise bounds directly with respect to the anchor box offsets which enables a novel Interval Bound Propagation method that derives optimal IoU bounds. We demonstrate that our method enables, for the first time, the robustness verification of realistic, anchor-based models including SSD, YOLOv2, and YOLOv3 variants against various input perturbations.

IoUCert: Robustness Verification for Anchor-based Object Detectors

TL;DR

Focusing on the object localisation component in single-object settings, a coordinate transformation is proposed that enables the algorithm to circumvent precision-degrading relaxations of non-linear box prediction functions and enables a novel Interval Bound Propagation method that derives optimal IoU bounds.

Abstract

While formal robustness verification has seen significant success in image classification, scaling these guarantees to object detection remains notoriously difficult due to complex non-linear coordinate transformations and Intersection-over-Union (IoU) metrics. We introduce {\sc \sf IoUCert}, a novel formal verification framework designed specifically to overcome these bottlenecks in foundational anchor-based object detection architectures. Focusing on the object localisation component in single-object settings, we propose a coordinate transformation that enables our algorithm to circumvent precision-degrading relaxations of non-linear box prediction functions. This allows us to optimise bounds directly with respect to the anchor box offsets which enables a novel Interval Bound Propagation method that derives optimal IoU bounds. We demonstrate that our method enables, for the first time, the robustness verification of realistic, anchor-based models including SSD, YOLOv2, and YOLOv3 variants against various input perturbations.
Paper Structure (34 sections, 4 theorems, 37 equations, 4 figures, 7 tables, 3 algorithms)

This paper contains 34 sections, 4 theorems, 37 equations, 4 figures, 7 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. Background
  4. Object detection
  5. Neural Network Verification
  6. Method
  7. Coordinate Transformation
  8. Optimal IoU IBP Bounds
  9. Robustness Verification Algorithm
  10. Optimal Relaxations for LeakyReLU Activations
  11. Evaluation
  12. Benchmarks
  13. Experimental Results
  14. Conclusion
  15. Proof: Without Loss of Generality on Single Highest-Confidence Box
  16. ...and 19 more sections

Key Result

proposition 1

Let $f: \mathbb{R} \to \mathbb{R}, g: \mathbb{R} \to \mathbb{R}$ be injective functions. Then their concatenation $f \circ g$ is also injective.

Figures (4)

  • Figure 1: A counterexample from robustness verification of a YOLOv3 model on a runway detection task. Left: original image; right: perturbed image. Green boxes: ground truth, blue box: original model prediction (IoU $=0.89$), red box: prediction on the perturbed image (IoU $=0.11$).
  • Figure 2: Pipeline of our object detection (OD) verification framework, combining verifier bounds, candidate selection, and optimal IoU bound derivation to reach ROBUSTNONROBUST or UNKNOWN conclusions.
  • Figure 3: Variation of the IoU function given its partial derivatives.
  • Figure 4: Visualisation of the lower and upper LeakyReLU bounding functions for a sample $\tilde{\alpha}=0.5$. The lower overapproximation area is shaded in red, the upper overapproximation area in blue.

Theorems & Definitions (12)

  • proposition 1
  • proof
  • theorem 1
  • proof
  • theorem 2
  • proof
  • theorem 3
  • proof
  • proof
  • proof
  • ...and 2 more