IoUCert: Robustness Verification for Anchor-based Object Detectors

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

cs.LGMar 3, 2026

IoUCert: Robustness Verification for Anchor-based Object Detectors

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

Organizations: Safe Intelligence · Imperial College London

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. As a fundamental step towards verifying complete detection pipelines, we introduce IoUCert, a novel formal verification framework designed specifically to overcome these core mathematical bottlenecks. By isolating the object localisation task in single-object settings, we propose a coordinate transformation that circumvents precision-degrading relaxations of non-linear box prediction functions. This approach allows us to optimise bounds directly with respect to anchor box offsets, enabling a novel Interval Bound Propagation method that derives optimal IoU bounds. We demonstrate that IoUCert enables, for the first time, the robustness verification of foundational, anchor-based architectures including tractable variants of SSD, YOLOv2, and YOLOv3 against various input perturbations, providing a rigorous theoretical basis for future end-to-end detector verification.

Figures & tables

Panel of Figure 1 — 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$ ).

Panel of Figure 2 — Figure 2: Pipeline of our object detection (OD) verification framework, combining verifier bounds, candidate selection, and optimal IoU bound derivation to reach ROBUST , NONROBUST or UNKNOWN conclusions.

Panel of Figure 3 — Figure 3: Geometric intuition for the IoU candidate set in the $(z_{0},z_{2})$ plane (the $(z_{1},z_{3})$ plane is analogous). The four constraints define a feasible region (blue) with four corners ( $\bullet$ , $P^{c}_{x}$ ), and the dashed ground truth coordinate lines $z_{0}=g_{0}$ , $z_{2}=g_{2}$ mark the non-differentiability of the IoU, crossing at the ground truth corner ( $\bullet$ , $P^{gt}_{x}$ ). Each ground truth line meets each of the four lines bounding the region, giving $2\times 4=8$ intersections ( $P^{\text{int}}_{x}$ ): those on the feasible boundary ( $\bullet$ ) are retained, while those outside it ( $\circ$ , where the ground truth lines meet the dashed boundary-line extensions) are pruned by the feasibility check. This gives $4+8+1=13$ enumerated candidates per plane (as used in Theorem 4.1 ). Here $4$ of the $8$ intersections are infeasible, leaving the $9$ filled points.

Model	$\epsilon$	Brightness				Contrast
Model	$\epsilon$	R	NR	T	Time	R	NR	T	Time
SSD	0.01	48	2	0	29.06	49	1	0	24.21
	0.05	45	5	0	404.54	47	3	0	171.49
	0.10	40	10	0	731.41	42	8	0	359.41
	0.30	9	41	0	458.21	30	20	0	885.51
	0.50	0	47	3	221.71	14	36	0	743.04

Table 1: IoUCert verification results on SSD (trained on LARD) and YOLOv2 (trained on Pascal VOC) for different perturbation sizes

\epsilon

and perturbations showing robust (R), non-robust (NR), and timeout (T) counts and mean time (all cases) in seconds.

Range	#Bounds	Improv. (%)	Avoided (%)
0.01 - 0.10	14642	50.67	0.59
0.10 - 0.20	8479	65.09	0.12
0.20 - 0.30	8084	58.54	0.11
0.30 - 0.40	6383	56.09	0.05
0.40 - 0.50	4440	55.32	0.14
0.50 - 0.60	3569	54.75	99.66

Table 2: Summary of IoU bound ranges, number of sampled bounds, average tightness improvement, and avoided subproblem exploration percentages.

Model	$\epsilon$	Brightness				Contrast				Motion Blur ( $0^{\circ}$ )
Model	$\epsilon$	R	NR	T	Time	R	NR	T	Time	R	NR	T	Time
LARD $64\times 64$	0.01	50	0	0	3.35	50	0	0	3.28	50	0	0	3.15
	0.05	50	0	0	9.72	50	0	0	8.06	50	0	0	3.30
	0.10	50	0	0	20.45	50	0	0	15.82	50	0	0	3.83
	0.30	50	0	0	56.26	50	0	0	39.25	50	0	0	16.89
	0.50	47	3	0	89.58	49	1	0	58.63	50	0	0	31.91

Table 3: IoUCert results on YOLOv3 for different perturbation sizes

\epsilon

and perturbations with robust (R), non-robust (NR), and timeout (T) counts shown alongside mean verification time in seconds.

	YOLOv3-tiny, 64 $\times$ 64	YOLOv3-tiny-maxpool, 64 $\times$ 64
Dataset	LARD	LARD
Weight Decay	$10^{-3}$	$10^{-3}$
Learning Rate	$5\cdot 10^{-3}$	$5\cdot 10^{-3}$
Epochs	400	800
Left-Right Flipping Probability	0.5	0.5
Mosaic Probability	0.5	0.5

Table 4: Optimal hyperparameters for the 64

\times

64 YOLOv3 training runs and resulting accuracy.

\text{mAP}_{0.5}

denotes the Mean Average Precision at an IoU threshold of

0.5

while

\text{mAP}_{0.5:0.95}

denotes the Mean Average Precision averaged over IoU thresholds between

0.5

and

0.95

in increments of

0.05

	YOLOv3-tiny, 128 $\times$ 128	YOLOv3-tiny, 128 $\times$ 128
Dataset	LARD	COCO
Weight Decay	$10^{-4}$	$5\cdot 10^{-4}$
Learning Rate	$5\cdot 10^{-3}$	$10^{-2}$
Epochs	2000	2000
Left-Right Flipping Probability	0.5	0.5
Mosaic Probability	0.5	0.5

Table 5: Optimal hyperparameters for the 128

\times

128 YOLOv3 training runs and resulting accuracy.

\text{mAP}_{0.5}

denotes the Mean Average Precision at an IoU threshold of

0.5

while

\text{mAP}_{0.5:0.95}

denotes the Mean Average Precision averaged over IoU thresholds between

0.5

and

0.95

in increments of

0.05

Model	$\epsilon$	Motion Blur ( $45^{\circ}$ )				Motion Blur ( $90^{\circ}$ )				Motion Blur ( $135^{\circ}$ )
Model	$\epsilon$	R	NR	T	Time	R	NR	T	Time	R	NR	T	Time
LARD $64\times 64$	0.01	50	0	0	3.15	50	0	0	3.15	50	0	0	3.16
	0.05	50	0	0	3.31	50	0	0	3.30	50	0	0	3.32
	0.10	50	0	0	3.90	50	0	0	3.72	50	0	0	4.00
	0.30	50	0	0	17.97	50	0	0	15.42	50	0	0	18.28
	0.50	50	0	0	34.83	49	1	0	28.24	49	1	0	33.59

Table 6: YOLOv3 results for motion blur perturbations with angles of

45,90

and

135

degrees and different epsilon values. The numbers of robust (R), non-robust (NR) and timeout (T) cases are shown together with the mean verification time in seconds. The timeout was set to

1800

seconds.

$z$	$-\infty$	$g_{0}$		$g_{2}$	$\infty$
$\frac{\partial\text{IoU}}{\partial z_{0}}$	$+$	$nd$	$-$	$-$	$-$
$\frac{\partial\text{IoU}}{\partial z_{2}}$	$+$	$+$	$+$	$nd$	$-$

Figure 4: Variation of the IoU function given its partial derivatives.

Panel of Figure 5 — Figure 5: 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.

Explore similar work

From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specifications
Mar 5, 2026Xusheng Luo, Changliu LiuCertified Robustness Keypoint Detection
Carnegie Mellon University, Pittsburgh, PA, USA
LipSSD: Lipschitz-Constrained Single-Shot Detection for Adversarially Robust Object Detection
Jul 6, 2026Vincent Lébé, Yannick Prudent, Corentin Friedrich +3Adversarial Robustness Object Detection
IRIT, DTIPG - SNCF, UT3 · IRT Saint-Exup´ery · Alstom +2
Probabilistic Object Detection with Conformal Prediction
May 8, 2026Christopher Ries, Moussa Kassem Sbeyti, Nicolas Bianco +1Autonomous Driving Perception Conformal Prediction
Karlsruhe Institute of Technology (KIT), Karlsruhe, Germany

Mar 5, 2026J/K move · Enter open · S save

From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specifications

Xusheng Luo, Changliu Liu

Carnegie Mellon University, Pittsburgh, PA, USA

Certified Robustness Keypoint Detection

Open paper AskPDF arXiv

Keypoint detection underpins many vision tasks, including pose estimation, viewpoint recovery, and 3D reconstruction, yet modern neural models remain vulnerable to small input perturbations. Despite its importance, formal robustness verification for keypoint detectors is largely unexplored due to high-dimensional inputs and continuous coordinate outputs. We propose the first coupled robustness verification framework for heatmap-based keypoint detectors that bounds the joint deviation across all keypoints, capturing their interdependencies and downstream task requirements. Unlike prior decoupled, classification-style approaches that verify each keypoint independently and yield conservative guarantees, our method verifies collective behavior. We formulate verification as a falsification problem using a mixed-integer linear program (MILP) that combines reachable heatmap sets with a polytope encoding joint deviation constraints. Infeasibility certifies robustness, while feasibility provides counterexamples, and we prove the method is sound: if it certifies the model as robust, then the keypoint detection model is guaranteed to be robust. Experiments show that our coupled approach achieves high verified rates and remains effective under strict error thresholds where decoupled methods fail.

Abstract

Explore similar work

From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specifications

LipSSD: Lipschitz-Constrained Single-Shot Detection for Adversarially Robust Object Detection

Probabilistic Object Detection with Conformal Prediction