We recently presented the following paper on the robustness verification of object detectors at ECCV 2026:
Brueckner, B., Mercado, A. J., Zhang, Y., Kouvaros, P., Lomuscio, A. (2026), 19th European Conference on Computer Vision (ECCV 2026), Lecture Notes in Computer Science, vol. 17021, doi.org/10.1007/978-3-032-37574-2_20
This blog post summarises our contributions and visualises the advantages of our proposed method.
Object detectors are used in many safety-critical systems such as autonomous vehicles or aircraft that use a camera to find the runway on approach. Empirical testing shows that a detector works on the images it was tested on, but does not provide any robustness guarantees for the model under slight changes of its input, for example when the light changes or the camera shakes. Formal verification, on the other hand, can provide such guarantees: it proves that a model behaves correctly across a range of input perturbations. So far, verifiers could only handle image classifiers and simplified detection models. IoUCert enables formal robustness verification for anchor-based object detectors such as SSD and YOLO. It proves that a detector still finds the object, with the right class and in the right place, under changes in brightness, contrast and motion blur. When identifying vulnerabilities, IoUCert returns concrete robustness counterexamples which can be used to understand and fix the weaknesses of the model.
Summary
Object detectors are more complicated than image classifiers since they need to not only classify the object but to also localise it by drawing a bounding box around it. A detection is considered to be correct if the box prediction overlaps with the true bounding box by a certain amount. The standard measure of that overlap is the Intersection over Union (IoU): the intersection area between both boxes divided by the area they cover together. Verifying the robustness of a detector therefore means proving that for every perturbed version of an image, the detector picks the right class with sufficient confidence and that their IoU is above a user-defined threshold (in our case we pick a threshold of 0.5).
This is much harder than verifying a classifier. Detectors such as SSD and YOLO do not output boxes, but start from a fixed grid of template boxes, called anchors, and predict for each anchor how to shift and stretch it. This is done using non-linear functions such as sigmoid and exponential functions which pose difficulties to verifiers. The IoU itself is also a non-linear function of the box corners, and the final prediction is the candidate box which scores highest. Existing verification tools either cannot handle these steps or approximate them so loosely that they often do not arrive at a definitive conclusion.
IoUCert solves these problems. It reformulates the problem in terms of the box corners, which removes the need to approximate the box decoding functions. It then computes the exact range of IoU values over all boxes that are consistent with the bounds on the network’s outputs by checking a fixed set of 169 candidate points. For YOLOv3, which uses LeakyReLU activations, it also uses the tightest possible linear approximation of that activation. Implemented in the Venus verifier, IoUCert is able to verify the robustness verification of anchor-based detectors for the first time. We use versions of SSD, YOLOv2 and YOLOv3 that have been adapted for verification, on images that contain a single object.
A small change to the image, a big change to the box
Switch between the original image and a perturbed version that IoUCert found. The detector is YOLOv3-tiny, trained on runway images from the LARD dataset at 128×128 pixels.
Main contributions
- We derive optimal IoU bounds for anchor-based detectors within Interval Bound Propagation. The lowest and highest possible IoU always occur at one of 169 candidate points, so the exact bounds can be computed in constant time. We find that they are 50 to 65% tighter than those of the previous method by Cohen et al.
- We introduce a coordinate transformation for the box decoding step. Because the decoding functions are strictly monotonic, IoUCert can work with the box corners directly and never has to approximate the sigmoid and exponential functions that turn network outputs into boxes.
- We derive linear relaxations for YOLOv3’s LeakyReLU activations which minimise the relaxation error.
- We integrate IoUCert into the Venus verifier and use it to verify SSD, YOLOv2 and YOLOv3 models trained on runway images (LARD) as well as the Pascal VOC and COCO datasets, considering brightness, contrast and motion blur perturbations.
A closer look
How verification works, and why detectors are challenging
Verifiers such as Venus answer questions of the form: does the network behave correctly for every image in a given set? The set contains all perturbed variants of an image within a certain perturbation range. The verifier propagates bounds through the network. Starting from the range of possible inputs, it computes a range of possible values for every neuron, layer by layer, until it reaches the output layer. For non-linear network components, the verifier uses linear approximations of the operation, so every approximation introduces additional relaxation errors. If the final ranges are too wide to make a decision, the verifier branches and checks robustness for each branch separately, a strategy known as branch and bound.
Object detectors are challenging for three reasons.
- Boxes are decoded, not predicted. For each anchor, the network outputs offsets, and a fixed formula turns them into a box. The centre moves according to a sigmoid of one offset, and the width and height are scaled through an exponential (or, in YOLOv3, a squared sigmoid) of the others. Propagating bounds through relaxations of these nonlinearities introduces large relaxation errors before the IoU is even computed.
- The IoU is awkward to bound. It is a ratio of areas that involves the minimum and maximum of box coordinates, so it is neither convex nor smooth. Bounding it from separate ranges for the four box corners gives very wide ranges.
- The detector considers many boxes simultaneously. A detector scores every anchor and keeps the box with the highest confidence. When the scores are only known up to a range, several boxes could end up on top, and the verifier has to check all of them.
Which box comes out on top?
Under a perturbation, the verifier only knows a range for each box’s confidence score. Every box whose range reaches above the best guaranteed score of any box could end up as the detector’s output, so all of them have to pass the IoU check. Drag the slider to widen the ranges.
Illustration with made-up scores. For simplicity each box’s IoU is fixed here. In the real check, IoUCert also bounds each candidate’s IoU and class scores over the whole perturbation range.
Working with box corners instead of offsets
The network does not output a box directly, only offsets that a fixed formula turns into a box. A verifier would normally push its bounds through this formula, and because the formula is curved, it has to approximate it, which loosens the bounds. IoUCert skips this step. Each part of the formula moves in one direction only: a larger offset always gives a larger shift or a larger box. So the limits on the offsets translate exactly into limits on where the centre of the box can be and how large the box can be. IoUCert then reasons about the box itself within these limits, without approximating anything.
Exact IoU bounds from 169 points
To prove that a detection stays correct, IoUCert needs the lowest IoU that any box within these limits can have. There are infinitely many such boxes, but we prove that the lowest and the highest IoU are always reached by one of a small set of special boxes: those at the extremes of the allowed position and size, and those with an edge exactly on an edge of the true box. There are 13 such cases for the left and right edges and 13 for the top and bottom edges, so IoUCert only has to check 13 × 13 = 169 boxes to get the exact range of the IoU, which takes a fixed and very short time. Because the limits on centre and size keep track of how the corners of the box belong together, these ranges are also much tighter than those of earlier methods, which bound each corner separately.
A tighter approximation for LeakyReLU
YOLOv3 uses the LeakyReLU activation, max(αx, x), which lets a small fraction α of negative inputs through, instead of the ReLU that most verifiers are built around. When the input range [l, u] of a neuron contains zero, the verifier has to enclose the activation between a lower and an upper line. The upper line is fixed, but any line α̃x with α̃ between α and 1 is a valid lower line, and existing verifiers always use αx. We prove that the approximation error, the area between the two lines, is smallest at one of the two extremes: x when u > |l|, and αx otherwise. Picking the better line costs nothing and, whenever u > |l|, reduces the error compared with the standard choice. In the example from our paper, with α = 0.1 and inputs between −2 and 5, the area shrinks from 15.75 to 6.3.
Choosing the lower line for LeakyReLU
Drag the ends l and u of the input range (on the plot or with the sliders). The shaded area is the approximation error of the lower line IoUCert picks. Existing verifiers always use αx.
Putting it together
IoUCert sits at the end of the network as a custom layer inside Venus. Venus computes bounds on the network’s outputs for the whole set of perturbed images. IoUCert takes every box that could have the highest confidence, bounds its confidence, class scores and IoU with the ground truth, and returns one of three answers. ROBUST means that every candidate box has the right class, a confidence above the threshold and an IoU of at least 0.5, for every allowed perturbation. NONROBUST means that the detector fails for some allowed perturbation, so a concrete counterexample can be produced. UNKNOWN means that the bounds are too loose to decide, and Venus splits the perturbation range and repeats the check on each part. In our experiments we observed no undecided results except for 3 timeouts on SSD.
Results
We evaluated IoUCert on five models across three architectures. We trained an SSD model with 11.3 million parameters on LARD (Landing Approach Runway Detection), a dataset of runway images for vision-based landing, at 128×128 pixels. We trained YOLOv3-tiny models with 8.7 to 8.9 million parameters on LARD at 64×64 and 128×128 pixels, and on single-object crops of COCO at 128×128 pixels. We also used a simplified YOLOv2-tiny model from the 2023 Verification of Neural Networks Competition (VNN-COMP), trained on Pascal VOC images. To make verification tractable, we replaced the max pooling layers of the models we trained with average pooling. For each model and perturbation, we verified 50 randomly chosen test images that the model detects correctly, at perturbation budgets ε from 0.01 to 1. The budget decides how strong the perturbation may be, and the verifier has to cover every perturbation up to that strength.
Verification results
50 test images per model and perturbation, all detected correctly without perturbation. Hover overTap the charts for the exact numbers.
Images verified robust, out of 50
Branches avoided thanks to the tighter bounds (%)
How much tighter the IoU bounds are (%)
The bounds are grouped by the IoU range they fall in. Tighter bounds save splitting where the threshold can be reached: for boxes whose IoU lies above 0.5 they avoided more than 95% of the branches that the looser bounds needed, and below 0.5 almost none. Because tighter bounds also take a little longer to compute, end-to-end verification times were similar for both methods.
YOLOv3-tiny on LARD at 64×64 pixels, trained once with average pooling (mAP@0.5 of 86.59%) and once with the original max pooling (86.88%).
Average pooling
Max pooling
Average time per query (log scale)
What the results show:
- Tighter bounds. For the SSD model under a brightness perturbation, we observe that IoUCert’s bounds are 50 to 65% tighter than those of Cohen et al. in every IoU range. For boxes whose IoU lies above the 0.5 threshold, the tighter bounds avoided more than 95% of the branches that the looser bounds would have had to explore. Tighter bounds take a little longer to compute, so end-to-end verification times were similar to those with the previous method.
- Accuracy is not robustness. The YOLOv3 model trained at 128×128 pixels detects runways more accurately than the one trained at 64×64 pixels (mAP@0.5 of 98.8% against 86.6%), but it is less robust. At the largest brightness budget, 12 of its 50 images are verified robust, against 28 of 50 for the smaller model.
- Dataset complexity affects verification. Trained on the more varied COCO data, the same architecture is less robust to brightness changes and motion blur than on LARD at the same resolution, for example 29 against 40 of 50 images verified robust under brightness at ε = 0.5. It is slightly more robust to moderate contrast changes.
- Motion blur is the mildest perturbation. Even at the largest budget, at least 43 of 50 LARD images and at least 30 of 50 COCO images are verified robust, for every blur direction. IoUCert still finds individual counterexamples, like the one at the top of this post.
- Average pooling makes verification practical. Max pooling layers require linear relaxations in the verification process, while average pooling is linear and exact. The swap changed the mAP@0.5 of our 64×64 YOLOv3-tiny model only from 86.88% to 86.59%, but made verification more than an order of magnitude faster. Under brightness with ε = 0.3, all 50 images of the average pooling model were verified robust in 56 seconds on average, while the max pooling model was verified robust on 15 images, with 33 timeouts and an average time of over 1,600 seconds.
Scope and limitations
IoUCert currently handles images that contain a single object. With several objects, correctness also depends on non-maximum suppression (NMS), the step that removes duplicate detections, and verifying it requires bounds on the overlap between pairs of predicted boxes. The models we verified use average instead of max pooling and inputs of up to 128×128 pixels, and the YOLO models are the compact tiny variants. However, our ideas are an important step towards the robustness verification of larger object detectors and apply to any detector whose box decoding can be inverted. Like all complete verification, IoUCert is meant for checking models before deployment rather than at run time.
