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.

翻译：尽管形式化鲁棒性验证在图像分类领域取得了显著成功，但由于复杂的非线性坐标变换和交并比（IoU）度量，将这些保证扩展到目标检测领域仍然极具挑战。我们提出了IoUCert，这是一种专门设计用于克服基础性基于锚框的目标检测架构中这些瓶颈的新型形式化验证框架。聚焦于单目标场景下的目标定位组件，我们提出了一种坐标变换方法，使我们的算法能够规避非线性边界框预测函数中导致精度下降的松弛处理。这使我们能够直接针对锚框偏移量优化边界，从而启用一种新颖的区间边界传播方法，以推导最优IoU边界。我们证明了我们的方法首次实现了对包括SSD、YOLOv2和YOLOv3变体在内的现实基于锚框模型，针对各种输入扰动的鲁棒性验证。