IoUCert: Robustness Verification for Anchor-based Object Detectors¶
Conference: ECCV 2026
Paper: ECCV 2026
Area: Object Detection
Keywords: formal robustness verification, object detection, IoU bounds, interval bound propagation, LeakyReLU relaxation
TL;DR¶
IoUCert casts "the IoU of a single-object detection stays above a threshold" as a verifiable property: a coordinate transformation removes the non-linear box-decoding map from the relaxation chain, and a proof that the IoU extremum can only sit at finitely many critical points turns the IoU bounds into an exact enumeration over at most 169 candidates, which together with optimal LeakyReLU relaxations yields the first formal robustness verification of real anchor-based detectors such as SSD, YOLOv2 and YOLOv3.
Background & Motivation¶
Neural network verification has matured considerably for image classification: IBP, the CROWN family, and symbolic interval propagation combined with branch-and-bound (BaB) can now handle ReLU networks at scale, and VNN-COMP has standardised both tools and benchmarks. Nearly all of that capability, however, is aimed at classifiers. Once the target becomes an object detection (OD) model, existing verifiers either do not support it at all or only produce very loose approximations: detectors contain logical components such as non-maximum suppression, the whole max/min/division-composite geometric metric that is IoU, and a non-linear decoding step that turns regression outputs into box coordinates, on top of multi-scale heads and anchors. Prior OD verification work is mostly evaluated on "toy regression models" that directly regress four corner coordinates, use shallow backbones, have no anchors and no multi-scale heads, and whose detection accuracy is itself low. Reference [19], for instance, bounds IoU by running IBP on the predicted corner coordinates, and reference [53] encodes IoU as a network layer handed to a general-purpose verifier but is limited by loose bounds on max, min and division; the scalability of both stops at toy models. A third line, the probabilistic verifier of [45], does cover the full YOLO pipeline including NMS, but its certificates are not sound even for small models.
The core tension is that lifting certificates from toy models to real detectors requires crossing two mathematical bottlenecks, and both of them are caused by non-linearity. The first is the box-decoding map \(\psi\circ\phi\): offset-to-corner is non-linear, and the usual recipe propagates bounds in offset space and then pushes them through that map before bounding IoU, so every crossing adds an over-approximation and the error compounds. The second is IoU itself: a piecewise function built from max, min and division, which linear relaxation inevitably bounds loosely — and once bounds are loose, branch-and-bound times out. Worse, "correct" for a detector is not a size comparison between two logits: it also involves the selection of which box ends up being the output, and bound propagation naturally leaves several boxes that could all be the top-scoring one.
This paper's angle is to stop relaxing both non-linearities and instead route around them. In the common anchor-based families the box-decoding map is invertible, which makes the very step of "bound offsets first, then cross the decoder" redundant: substituting the variables into corner space and rewriting the offset box constraints as equivalent linear constraints on the corners introduces no relaxation at all, and it splits the IoU feasible region into two decoupled two-dimensional planes. On that structure, the IoU extremum no longer has to be estimated by relaxation — it can be enumerated exactly. Core idea: use a coordinate transformation to turn the IoU bounds from a relaxed estimate into an exact enumeration of extrema over the feasible region, and use optimal linear LeakyReLU relaxations to remove the relaxation error contributed by the activations, thereby making the first formal verifier for real anchor-based detectors (SSD / YOLOv2 / YOLOv3) possible.
Method¶
Overall Architecture¶
IoUCert answers the question: given an image and input constraints \(\zeta_x\), does there exist an image inside the perturbation set on which the detector's output is "incorrect"? Here \(\zeta_x\) is a set of input constraints, expressible as an \(\ell_\infty\) ball, a brightness interval, a contrast interval, a blur-kernel parameter interval, or any other input-interval form; verification success (ROBUST) means the property holds for all inputs in \(\zeta_x\) (infinitely many), so this is complete verification rather than sampled testing. The scope is deliberately restricted to the single-object setting: an image has exactly one ground-truth box \(g=(z_0,z_1,z_2,z_3,g_c)\), the detector still emits many candidate boxes, but correctness depends only on the one box left by post-processing:
That is, the certificate has to cover three things at once: the selected box is "the right one" (selection), its class and confidence clear the thresholds, and its IoU with the ground-truth box clears the threshold. Keeping the confidence threshold \(\tau_{\text{class}}\) is intentional — it lets a detector abstain when every candidate scores below it, and abstention itself has to be covered by the verification.
The pipeline has three stages: first, existing bound-propagation frameworks (IBP or symbolic interval propagation with back-substitution) produce bounds on the network outputs, i.e. intervals on each anchor's offsets and logits (Line 4 of Algorithm 1); then candidate-box selection keeps every box that could possibly be the highest-scoring one (Line 5); finally, for each candidate the method computes bounds on its class scores and on its IoU with the ground-truth box, and issues a three-valued verdict of ROBUST / NONROBUST / UNKNOWN. UNKNOWN is not a failure but "the bounds are not tight enough yet", and it is handed to branch-and-bound (implemented on top of the Venus verifier) for further splitting. The technical content of the method lives in the third stage: making the IoU bound tight requires the coordinate transformation and the exact enumeration of extreme points, and making a YOLOv3-style backbone not leak tightness at the activations requires an optimal set of linear LeakyReLU relaxations.
Key Designs¶
1. Coordinate transformation: lifting the non-linear box decoding out of the relaxation chain
Start with the pain point. Each candidate box arises as follows: the model predicts offsets \(o\) for a fixed anchor \(p\), a model-specific decoding function \(\phi(o,p)=(c_x,c_y,w,h)\) converts them into centre-width-height format, and \(\psi\) maps that to corners \(z=(z_0,z_1,z_2,z_3)\). The recipe of [19] obtains an interval \([\underline{o},\overline{o}]\) in offset space, pushes that interval through \(\psi\circ\phi\) to get corner bounds, and only then bounds IoU — but \(\psi\circ\phi\) is non-linear, so each crossing loses tightness and the IoU bound ends up too wide to decide anything.
This paper does not cross at all. Because both \(\psi\) and \(\phi\) are injective (Appendix B), the inverse \(\phi^{-1}\circ\psi^{-1}\) is available, and the optimisation variable can be changed from offsets to corner coordinates: the objective becomes an extremum of \(\mathrm{IoU}(z,g)\) directly, while the original offset box constraints are transported equivalently into four linear constraints on the corners — the ground-truth box is fixed, so the problem becomes the following (the expansion of Problem 2 in the paper, where the constants \(L_i,U_i\) follow directly from the offset-bound endpoints through \(\phi^{-1}\)):
The lower bound is obtained by replacing max with min, and the derivation is fully symmetric. The whole step is a single invertible change of variables with no relaxation performed anywhere: the non-linearity is not "approximated away", it is moved into the coefficients of the constraints. This rewrite brings a decisive structural benefit — the first two constraints involve only \((z_0,z_2)\) (the width direction) and the last two only \((z_1,z_3)\) (the height direction), so the two directions decouple and the problem splits into two independent two-dimensional problems. That is exactly the precondition for the exact enumeration in the next design; staying in offset space would leave the three variables entangled through the decoder, and no such split would exist.
The requirement is that the decoding map \(\psi\circ\phi\) be strictly monotonic in each offset with a tractable inverse (Appendix B), which the dense anchor-based heads of SSD and the YOLO family satisfy. The authors stress that this is independent of training: label-assignment strategies such as ATSS, PAA or OTA change the training target, not the inference-time decoding map. Likewise, the region proposal network of Faster R-CNN and anchor-free heads that regress invertible offsets fall inside the same framework (Appendix H).
2. Optimal IoU bounds: enumerating 13 candidate points, with no relaxation at all
With a decoupled feasible region in hand, the remaining problem is the non-linearity of IoU itself. IoU is assembled from max, min and division, so a linear relaxation is very loose (reference [53] is stuck exactly here), and loose bounds make branch-and-bound explode. This paper instead computes the extremum exactly: over a feasible region defined by linear constraints, the extremum of a continuous function can only sit at one of three kinds of location — an interior point where the gradient vanishes, a corner of the region boundary, or a point where the function is non-differentiable. Following [19], the first kind is ruled out (the partial derivatives of IoU do not vanish inside the feasible region), leaving the latter two as sources of candidates.
For the stationary points on the boundary, Appendix E.2 proves that the gradient of IoU along each boundary is "either zero everywhere or non-zero everywhere": in the first case the value on that boundary equals the value at a corner of the region, and in the second case the extremum is attained at one of the endpoints of the corresponding corner segment. The second kind therefore needs no separate enumeration — it is already covered by the corners. The third kind is where IoU is non-differentiable, \(z_i=g_i\), i.e. the ground-truth coordinate lines; each such line (\(z_0=g_0\), \(z_2=g_2\) and the two height-direction counterparts) meets the four boundary lines, giving \(2\times 4=8\) intersections, plus the ground-truth corner \((g_0,g_2)\) when it falls inside the feasible region. The candidate set per 2D plane is thus "4 corners of the feasible region + 8 intersections + 1 ground-truth corner = 13 points", and Theorem 1 states that the maximum of the IoU function is attained at some combination of coordinates drawn from these points; combining both planes gives \(|\mathcal{C}_s|=13^2=169\) candidates. In practice one simply iterates over these 169 points, checks feasibility (whether the constraints hold and whether the box is valid with \(z_0<z_2\) and \(z_1<z_3\)), and updates the maximum and minimum.
The value of this construction has three layers. First, it returns the optimal bound under the given constraint set rather than the bound of some relaxation: the accuracy gain comes directly from not approximating. Second, the candidate count is the constant 169, so the algorithm is correct and terminates in constant time (Appendix F), independent of how wide the bounds are. Third, it states the cost honestly: compared with a single pass of linear relaxation, enumerating 169 points (each requiring an IoU evaluation and a feasibility check) is more expensive per call, and what it buys is a bound over 50% tighter — a trade-off that the experiments quantify explicitly (see Key Findings). Figure 3 of the paper depicts these 13 candidates in the \((z_0,z_2)\) plane, where half of the 8 intersections fall outside the feasible region and are pruned by the feasibility check, leaving 9 filled points.
3. Candidate selection and the three-valued verdict: folding "which box is chosen" into the certificate
Detector correctness contains a layer of selection semantics that cannot be ignored. Bound propagation naturally leaves several boxes that could all be the top-scoring one — the paper's own example is box 1 with confidence bounds \([0.5,0.9]\) and box 2 with \([0.7,0.8]\), where neither can be excluded. Judging only the bounds on the argmax would not be sound. IoUCert instead collects every box whose upper confidence bound exceeds the largest lower confidence bound over all boxes: only those can ever be top-1, so the rest can safely be ignored. For each candidate it then computes class-score bounds by bound propagation and IoU bounds against the ground-truth box using the enumeration above.
The verdict is three-valued. Only when all candidates have an IoU lower bound at or above \(\tau_{\text{iou}}\), a confidence lower bound at or above \(\tau_{\text{class}}\), and agree on the predicted class (equal to the ground-truth class) does the procedure return ROBUST — note that this is a universal statement over every possible top-1 selection, which is what makes the certificate sound. Conversely, if no candidate's IoU upper bound reaches \(\tau_{\text{iou}}\) (so no choice of top-1 can pass), or the highest confidence upper bound over all candidates is below \(\tau_{\text{class}}\), or all candidates predict a class different from the ground truth, it returns NONROBUST together with a counterexample. Everything else is UNKNOWN: the bounds are still too loose, or the candidates cannot even agree on a single class. Theorem 2 establishes correctness and shows that IoUCert is complete once combined with any branching framework — UNKNOWN means "not split enough yet", not undecidable.
4. Optimal linear relaxations for LeakyReLU
The first three designs route around non-linearities, but one place in the backbone must be handled head-on: YOLOv3 uses LeakyReLU while the theory behind mainstream verifiers is built on ReLU. With \(\mathrm{LeakyReLU}(x)=\max\{\alpha x,x\}\) and \(\alpha\in[0,1]\), the activation is linear — and exactly representable — whenever the interval \([l,u]\) lies entirely on the positive or the negative side; only unstable neurons with \(l<0<u\) need linear lower and upper bounds. The upper bound is the chord through \((l,\alpha l)\) and \((u,u)\); the lower bound is where the choice lies, and prior work (e.g. reference [48]) simply sets its slope to \(\alpha\), which is not optimal. In fact both \(\alpha x\) and \(x\) are valid lower bounds (\(x\le \mathrm{LeakyReLU}(x)\) holds on the whole interval, and \(\alpha x\) is exact on the negative half), and which one is tighter depends on which side the interval leans towards: using \(\alpha x\) puts all the error on the positive half, proportional to \(u^2\), whereas using \(x\) puts all of it on the negative half, proportional to \(|l|^2\). The optimal choice therefore compares \(u\) with \(|l|\):
Theorem 3 states precisely this result (⚠️ the LaTeX of this equation is corrupted in the cached full text; the direction of the inequality and the case split above are reconstructed from the paper's prose and from minimising the relaxation error — refer to the original paper). This relaxation matters because relaxation error is a primary source of looseness for branch-and-bound: in classification verification, replacing unstable-neuron relaxations with optimal ones directly reduces the number of branches, and YOLOv3 backbones contain many LeakyReLUs, so without this step high perturbation budgets would be hard to decide.
A Worked Example¶
Take a \(128\times128\) runway image from LARD and verify whether SSD's prediction is ROBUST under a brightness perturbation with \(\epsilon=0.3\). The set \(\zeta_x\) writes every pixel's brightness as an interval, and back-substitution yields confidence bounds for each anchor; suppose two boxes have the bounds used in the paper — box 1 with \([0.5,0.9]\) and box 2 with \([0.7,0.8]\) — while every other box has an upper bound below \(0.7\), so the candidate set shrinks to these two (the rest can never be top-1 and are ignored). For each candidate, its offset bounds are converted through \(\phi^{-1}\circ\psi^{-1}\) into the four corner-space constraints involving only \(z_0+z_2\), \(z_1+z_3\), \(z_2-z_0\) and \(z_3-z_1\). In the \((z_0,z_2)\) plane the procedure enumerates the 4 corners, the 8 intersections of the ground-truth lines \(z_0=g_0\) and \(z_2=g_2\) with the four boundary lines, and the ground-truth corner \((g_0,g_2)\) (half of which fall outside the feasible region and get pruned); the \((z_1,z_3)\) plane is analogous. Combining both planes gives \(13\times13=169\) points, and validating feasibility and box validity while taking the maximum and minimum yields the IoU bounds of that candidate. If both candidates have IoU lower bounds at or above \(\tau_{\text{iou}}\), confidence lower bounds at or above \(\tau_{\text{class}}\) and agree on the class, the image verifies as ROBUST; if some candidate's IoU upper bound does not even reach the threshold (no choice of top-1 can pass), or the highest confidence upper bound is below \(\tau_{\text{class}}\), the result is NONROBUST with a counterexample; and if one candidate passes while the other does not, the result is UNKNOWN and Venus resumes branch-and-bound splitting.
Key Experimental Results¶
Main Results¶
IoUCert is implemented as a custom layer on top of the Venus verifier, appended to the target model: it consumes the concrete bounds on the output logits obtained by back-substitution, computes bounds on IoU and on the confidence score, and integrates with Venus's branch-and-bound procedure. The evaluated detectors are: an SSD trained on the LARD runway detection task (Google Earth images, one runway per image) at \(128\times128\), whose MaxPool layers are replaced by linear AvgPool layers for verifiability, trained with SGD and the MultiBox loss with an NMS threshold of 0.5 and a confidence threshold of 0.15, with about 11.28M learnable parameters; the YOLOv2-tiny (TinyYOLO) benchmark from VNN-COMP 2023 (a Pascal VOC subset); and YOLOv3-tiny models trained on LARD (\(64\times64\) and \(128\times128\)) and on COCO (\(128\times128\), preprocessed into single-object crops), with 8.7–8.9M parameters. Each dataset contributes a verification subset of 50 correctly classified images, and the perturbations are brightness, contrast and motion blur (kernel size 5, angle 0°).
In Table 1 (SSD and YOLOv2 under brightness/contrast perturbations), R / NR / T are the counts of ROBUST / NONROBUST / timeout, and the time is the mean verification time in seconds over all cases of that setting.
| Model | \(\epsilon\) | Brightness R / NR / T | Brightness time (s) | Contrast R / NR / T | Contrast time (s) |
|---|---|---|---|---|---|
| SSD (LARD) | 0.01 | 48 / 2 / 0 | 29.06 | 49 / 1 / 0 | 24.21 |
| SSD (LARD) | 0.10 | 40 / 10 / 0 | 731.41 | 42 / 8 / 0 | 359.41 |
| SSD (LARD) | 0.30 | 9 / 41 / 0 | 458.21 | 30 / 20 / 0 | 885.51 |
| SSD (LARD) | 0.50 | 0 / 47 / 3 | 221.71 | 14 / 36 / 0 | 743.04 |
| SSD (LARD) | 1.00 | 0 / 50 / 0 | 5.79 | 0 / 50 / 0 | 3.90 |
| YOLOv2 (VOC) | 0.01 | 50 / 0 / 0 | 3.69 | 50 / 0 / 0 | 3.23 |
| YOLOv2 (VOC) | 0.10 | 47 / 3 / 0 | 23.81 | 50 / 0 / 0 | 9.23 |
| YOLOv2 (VOC) | 0.30 | 28 / 22 / 0 | 39.40 | 48 / 2 / 0 | 33.36 |
| YOLOv2 (VOC) | 0.50 | 4 / 46 / 0 | 9.99 | 36 / 14 / 0 | 35.86 |
| YOLOv2 (VOC) | 1.00 | 0 / 50 / 0 | 0.81 | 0 / 50 / 0 | 2.36 |
Table 2 (YOLOv3-tiny, with the optimal LeakyReLU relaxations; timeouts are 0 in every setting here and are therefore omitted, and the time column is the mean under brightness perturbation).
| Model | \(\epsilon\) | Brightness R / NR | Contrast R / NR | Motion blur (0°) R / NR | Brightness time (s) |
|---|---|---|---|---|---|
| LARD \(64\times64\) | 0.01 | 50 / 0 | 50 / 0 | 50 / 0 | 3.35 |
| LARD \(64\times64\) | 0.10 | 50 / 0 | 50 / 0 | 50 / 0 | 20.45 |
| LARD \(64\times64\) | 0.30 | 50 / 0 | 50 / 0 | 50 / 0 | 56.26 |
| LARD \(64\times64\) | 0.50 | 47 / 3 | 49 / 1 | 50 / 0 | 89.58 |
| LARD \(64\times64\) | 1.00 | 28 / 22 | 0 / 50 | 45 / 5 | 103.87 |
| LARD \(128\times128\) | 0.01 | 50 / 0 | 50 / 0 | 50 / 0 | 10.32 |
| LARD \(128\times128\) | 0.10 | 50 / 0 | 50 / 0 | 50 / 0 | 190.99 |
| LARD \(128\times128\) | 0.30 | 42 / 8 | 43 / 7 | 50 / 0 | 381.03 |
| LARD \(128\times128\) | 0.50 | 40 / 10 | 40 / 10 | 50 / 0 | 592.56 |
| LARD \(128\times128\) | 1.00 | 12 / 38 | 0 / 50 | 49 / 1 | 304.45 |
| COCO \(128\times128\) | 0.01 | 50 / 0 | 50 / 0 | 50 / 0 | 8.93 |
| COCO \(128\times128\) | 0.10 | 46 / 4 | 50 / 0 | 50 / 0 | 120.60 |
| COCO \(128\times128\) | 0.30 | 36 / 14 | 45 / 5 | 49 / 1 | 272.45 |
| COCO \(128\times128\) | 0.50 | 29 / 21 | 43 / 7 | 48 / 2 | 376.78 |
| COCO \(128\times128\) | 1.00 | 6 / 44 | 0 / 50 | 38 / 12 | 169.74 |
Ablation Study¶
The first analysis concerns bound tightness (Table 3, Table 2 of the paper). During a verification run on SSD under a brightness perturbation with \(\epsilon=0.02\), bounds are recorded for all boxes (not just the top-scoring one), reporting the tightness improvement over reference [19] and the fraction of branches whose exploration was avoided thanks to tighter bounds.
| IoU bound range | #Bounds | Tightness improvement (%) | Branches 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 |
| 0.60 – 0.70 | 2707 | 53.74 | 98.93 |
| 0.70 – 0.80 | 2336 | 53.14 | 97.60 |
| 0.80 – 0.90 | 1802 | 52.20 | 96.50 |
| 0.90 – 0.99 | 1374 | 52.30 | 95.92 |
The second analysis ablates the downsampling choice (swapping AvgPool back to the original MaxPool), on the 50-image subset of LARD \(64\times64\) under brightness \(\epsilon=0.3\):
| Config | Verification result (brightness \(\epsilon=0.3\)) | Clean accuracy (mAP\(_{0.5}\)) | Note |
|---|---|---|---|
| AvgPool (ours) | 50 / 50 ROBUST, 56 s on average | 86.59% (mAP\(_{0.5:0.95}\): 40.90%) | linear layer is exactly representable in bound propagation |
| MaxPool (original) | 15 / 50 ROBUST, 33 timeouts, over 1600 s total | 86.88% (mAP\(_{0.5:0.95}\): 41.67%) | piecewise-linear pooling is hard to relax tightly |
Key Findings¶
- Certified rates fall monotonically with the perturbation budget, and the pattern depends strongly on the perturbation type. All models are almost entirely ROBUST at small \(\epsilon\) (SSD is 48/50 under brightness at \(\epsilon=0.01\), and YOLOv2 is close to all-pass under brightness at 0.01–0.10); as \(\epsilon\) grows the ROBUST count falls monotonically and NONROBUST rises, showing that the verifier finds genuine vulnerabilities rather than merely failing to decide. The same SSD keeps only 9/50 under brightness at \(\epsilon=0.30\) while contrast still passes 30/50, indicating that brightness is the more effective perturbation direction; YOLOv2 keeps only 4/50 under brightness at \(\epsilon=0.50\) against 36/50 for contrast at the same budget. At large budgets (\(\epsilon\ge0.80\)) nearly every model turns NONROBUST, and verification then becomes fast (e.g. SSD averages only 5.79 s at \(\epsilon=1.00\)), because counterexamples are found early and no further splitting is needed.
- Bound tightness is the central payoff, and it shows up mainly as pruning. Compared with [19], IoUCert's IoU bounds are over 50% tighter in every range (50.67%–65.09%). The pruning gain, however, is sharply two-regime: across the five ranges from 0.01 to 0.50 the fraction of branches whose exploration is avoided never exceeds 0.59% and is essentially negligible, whereas across 0.50–0.99 it reaches 95.92%–99.66%. The paper attributes the latter to shallower depths where the bounds themselves are looser, i.e. the looser the bound, the larger the marginal gain from tightening it (⚠️ the first column of Table 3 is labelled "IoU bound range" in the caption while the prose describes it as shallower depths; the correspondence is somewhat ambiguous in the cached full text — the numbers are transcribed as-is, refer to the original paper for the exact convention).
- Tighter bounds are not free. Against a reimplementation of the looser method of [19], the two are comparable overall on complete verification: tighter bounds avoid many branches but cost more per call, while looser bounds branch more but process each branch faster. The paper presents this as an explicit design trade-off rather than claiming a one-sided win.
- Higher clean accuracy does not imply better certified robustness. On LARD, the \(128\times128\) YOLOv3 has higher clean accuracy than the \(64\times64\) one yet is less certifiably robust — higher input dimensionality yields looser bounds. At the same resolution, the multi-class COCO model is more vulnerable than LARD (29/50 vs 40/50 under brightness at \(\epsilon=0.50\)) but slightly more resilient to mid-range contrast.
- Motion blur is the hardest of the three perturbations to exploit. All YOLOv3 models are highly robust under 0° motion blur (COCO still passes 38/50 ROBUST at \(\epsilon=1.00\), and LARD \(128\times128\) is still 50/50 at \(\epsilon=0.80\)), yet edge cases yielding incorrect predictions are still found at high budgets, so the conclusion is "this perturbation matters less" rather than "it does not matter"; other blur angles appear in Table S3 of Appendix C.2.
- The AvgPool substitution is decisive for verifiability and costs little. Swapping MaxPool for AvgPool lowers mAP\(_{0.5}\) only from 86.88% to 86.59% (mAP\(_{0.5:0.95}\) from 41.67% to 40.90%), yet the same verification queries go from "15/50 passing, 33 timeouts, over 1600 s total" to "50/50 passing, 56 s on average", more than an order of magnitude faster. Verifiability has to be traded off against accuracy during design, not patched in after training.
Highlights & Insights¶
- The most elegant step is not tightening the bound but removing a relaxation that was never necessary. If the box-decoding map is invertible, there is no reason for bounds to cross it — substituting into corner space and letting the non-linearity enter the constraint coefficients costs zero accuracy. The idea transfers to any verification pipeline that "propagates first, then crosses a decoder": ask whether the non-linearity is invertible with a tractable inverse, and if so, move it into the constraints instead of relaxing it.
- The recipe for enumerating extreme points is directly reusable. "Rule out interior points by showing the gradient does not vanish → boundary stationary points are either covered by corners or land on segment endpoints → intersect the non-differentiable set with the boundary to get finitely many candidates" turns bound computation for a non-smooth metric into a constant number of evaluations. Natural transfer targets are GIoU / DIoU, which are built from the same max/min/division primitives, and the pairwise overlap bounds needed inside NMS.
- Folding "which output is selected" into the certificate is the essential difficulty that separates detector verification from classifier verification. When a box's score is an interval rather than a point value, the selection itself is uncertain, and IoUCert handles it with a universal statement over all possible winners. The same treatment applies to any model with post-hoc selection logic: top-k in classification, reranking in retrieval, multi-candidate generation.
- Stating the trade-offs plainly is what makes the claim stand. The paper explicitly defers multi-object and NMS to future work and prices the cost (pairwise box IoU bounds require up to \(O(n^2)\) certificates, and the verdict becomes ambiguous whenever the overlap bound straddles the NMS threshold). As a result the claim of "first formal verification of SSD / YOLOv3" is qualified and checkable rather than inflated.
Limitations & Future Work¶
- Limitations acknowledged by the authors: the scope is single-object only; multi-object detection requires pairwise box IoU bounds (up to \(O(n^2)\) certificates) and becomes ambiguous when overlap bounds straddle the NMS threshold, so NMS-aware verification of the full pipeline is only the next step; the method requires the box-decoding map \(\psi\circ\phi\) to be strictly monotonic in each offset with a solvable inverse, and DETR-style detectors with attention and set prediction remain difficult for current verifiers; verification is an offline pre-deployment procedure rather than a runtime one.
- Issues I see in the experimental design: only 50 correctly classified images per dataset are used, and only ROBUST / NONROBUST / timeout counts are reported, with no certified-accuracy-style metric directly comparable to clean accuracy, so cross-model and cross-dataset comparisons stay qualitative; there is also no comparison against empirical attacks (PGD / C&W style), so the NONROBUST counterexamples come from the verifier's own search and a reader cannot tell from this paper how much stronger the certificate is than an attack; replacing MaxPool with AvgPool, while necessary for verifiability and shown by the ablation to cost little, means what is verified is not strictly the original architecture; finally there is no head-to-head against [53] or [45] on the same models, though this is partly because they do not support SSD/YOLO-style architectures.
- Plausible improvement directions: derive the pairwise IoU bounds needed by NMS with the same critical-point enumeration (the tight candidate-box bounds are already provided by IoUCert, making this the most natural next step); use these IoU bounds for certified training so that detectors are verifiable by construction (IBP training has proven effective for classification, and no counterpart exists for detection yet); and generalise the optimal-LeakyReLU argument to other piecewise activations such as SiLU and GELU.
Related Work & Insights¶
- vs [19] (VerifIoU, DASC 2025; cited in the body as Cohen et al. while the reference entry lists Ducoffe, N.C.M. as first author — the two disagree, ⚠️ refer to the original paper): they bound IoU by running IBP on the predicted corner coordinates, which is equivalent to letting offset bounds cross the non-linear decoder before bounding IoU; this paper cancels that crossing with a coordinate transformation and enumerates extreme points in corner space, returning the optimal bound for the given constraint set. In the experiments the bounds here are uniformly over 50% tighter while the overall runtime is comparable (tighter bounds save branches, looser bounds save per-call cost). This paper's extra requirement is an invertible decoder, while their bottleneck is scalability.
- vs [53] (Raviv et al., 2024): they encode IoU as a network layer and hand it to a general-purpose verifier, which limits them to loose relaxations of max, min and division; this paper does not reuse generic layer relaxations but solves for the extremum analytically, so it can absorb multi-scale heads, anchors and confidence scores.
- vs [45] (Liu et al., ICLR 2026): their probabilistic verifier covers the complete YOLO pipeline including NMS, but already yields unsound certificates for small models; this paper is sound at the cost of covering only single-object scenes without NMS. The two are complementary in coverage versus reliability rather than substitutes.
- vs [15] (ImageStars set-based reachability) and [50] (branch-free IBP for certified runway detection): they too are evaluated only on small toy models and lack support for multi-scale heads, non-linear coordinate transformations and anchor structures; that architectural gap is exactly what this paper claims to close.
Rating¶
- Novelty: ⭐⭐⭐⭐⭐ The first to extend formal robustness verification to real anchor-based detectors such as SSD / YOLOv2 / YOLOv3, with three substantive technical contributions: the coordinate transformation, the optimal IoU extreme-point bounds, and the optimal LeakyReLU relaxations.
- Experimental Thoroughness: ⭐⭐⭐⭐ Three detector families, four model configurations, three perturbation types and three datasets including the safety-critical LARD; but only 50 images per dataset, no certified-accuracy metric, and no comparison against empirical attacks.
- Writing Quality: ⭐⭐⭐⭐ Clear structure with matching theorems and algorithms, complete proofs in the appendices, and an honest account of the three scoping decisions (single-object, no NMS, offline); some notation and table conventions are slightly ambiguous (e.g. the candidate enumeration and the first column of Table 3).
- Value: ⭐⭐⭐⭐⭐ Provides a reusable set of mathematical tools (constraint rewriting for invertible decoders + extreme-point enumeration + optimal activation relaxations) and takes a solid step on the road to end-to-end detector verification.