Pith. sign in

REVIEW 3 major objections 6 minor 1 cited by

A coordinate change lets robustness of SSD, YOLOv2, and YOLOv3 detectors be certified by checking 169 candidate boxes per anchor.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-02 19:11 UTC pith:62LT75RB

load-bearing objection The coordinate-transformation and 169-point IoU enumeration are a real step forward, but the Appendix A 'WLOG' reduction to the top box is false for the paper's own correctness definition, so the certificates are for a modified post-processor, not the full detector. the 3 major comments →

arxiv 2603.03043 v3 pith:62LT75RB submitted 2026-03-03 cs.LG cs.AIcs.CRcs.CV

IoUCert: Robustness Verification for Anchor-based Object Detectors

Benedikt Br\"uckner , Alejandro J. Mercado , Yanghao Zhang , Panagiotis Kouvaros , Alessio Lomuscio This is my paper
classification cs.LG cs.AIcs.CRcs.CV
keywords neural network verificationobject detectionIntersection-over-UnionInterval Bound Propagationanchor-based detectorsYOLOSSDrobustness certification
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

IoUCert is a verification method that, for the first time, formally certifies the robustness of anchor-based object detectors such as SSD, YOLOv2, and YOLOv3 against input perturbations. Its central move is a coordinate transformation: because the mapping from predicted offsets to corner coordinates is injective, the hard problem of bounding a non-linear box-construction function is replaced by the simpler problem of bounding the IoU over a region described by four linear inequalities in corner space. The main theorem shows that the best and worst IoU over that region are always achieved at one of a fixed set of 169 candidate corner points, so the IoU bounds are optimal and computed in constant time per anchor box. Combined with standard bound propagation through the network and an optimal LeakyReLU relaxation, the method returns sound certificates, and complete ones when combined with branching. If correct, this closes the gap between formal verification and realistic detection architectures, at least in the single-object setting.

Core claim

The paper's core claim is that verifying an anchor-based detector's single-box output can be reduced to a finite enumeration. Given bounds on the network's predicted offsets for an anchor, IoUCert uses the injectivity of the map h∘ϕ to re-express the same constraints as inequalities on the four corner coordinates of the predicted box. Under those constraints, the extrema of the IoU with a fixed ground-truth box occur only at corners, at boundary points where the IoU is non-differentiable, or at ground-truth corners; combining the 13 candidate values on each of the two independent coordinate planes yields 13×13=169 candidate boxes (Theorem 1). The algorithm evaluates IoU at all 169 points, fi

What carries the argument

The central object is the injective coordinate map h∘ϕ, which converts anchor offsets into corner coordinates. Its injectivity (established componentwise for SSD, YOLOv2, and YOLOv3) allows the optimization to be re-expressed in corner space as linear constraints; the argument then rests on the finite candidate set C_s = ×_i P_{z_i} of 169 points defined by corners, boundary/ground-truth intersections, and non-differentiable points. The 169-point enumeration is what carries the proof: it turns a continuous non-convex optimization into a constant-time check. A secondary piece is the optimal slope choice for LeakyReLU lower bounds, which minimizes the over-approximation area.

Load-bearing premise

The certificate is for simplified post-processing that selects only a single highest-confidence box above a threshold, and the paper's 'without loss of generality' argument (Section 3.1, Appendix A) only shows that the highest-scoring box is always retained, not that correctness of the full post-processed output is equivalent, so if the deployed pipeline's output differs, the guarantee may not cover it.

What would settle it

Take a certified-robust image from the paper's SSD or YOLOv3 evaluation and apply a perturbation inside the certified input budget, but run the full detector with its real NMS and confidence filtering instead of the simplified top-box selection; if the final output has no box, more than one box, or a box violating the IoU/class thresholds while the single highest-confidence box satisfies them, the reduction is empirically violated. A second, more mathematical check: search for a pair of offset intervals where a point outside the 169 candidates attains a strictly larger IoU than every candidate

Watch this falsifier. Get emailed when new claim-graph text bears on it.

Share X Bluesky LinkedIn Reddit HN

If this is right

  • The first formal robustness certificates for anchor-based SSD, YOLOv2, and YOLOv3 models, under brightness, contrast, and motion-blur perturbations.
  • IoU bounds are optimal for the given offset intervals, so no precision is lost in the box-construction nonlinearity, and verification is branch-complete when paired with a branching framework.
  • The IoU bound computation is constant time per candidate box (169 points), independent of the number of anchors or the model size.
  • The optimal LeakyReLU relaxation reduces over-approximation area (up to 60% in the paper's example), tightening verification of YOLOv3.
  • The method scales to models trained on complex datasets such as COCO and to safety-critical runway detection, not just toy regressors.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same 169-point enumeration likely transfers to other piecewise box-quality metrics such as GIoU or DIoU, provided their extrema still occur at boundary or non-differentiable points, giving a recipe for certifying newer losses.
  • The strongest limitation is the reduction to a single highest-confidence box: a true end-to-end guarantee for multi-object scenes would need to account for NMS interactions among boxes, perhaps by branching over suppression order.
  • Because the bottleneck is no longer the IoU computation but the network bound propagation, tighter network relaxations or better splitting strategies should directly translate into larger certified perturbation budgets for detectors.
  • A testable next step is to apply IoUCert to modern attention-based YOLO variants; the coordinate transformation is architecture-agnostic, so the open obstacle is bounding attention layers, not the box construction.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper introduces IoUCert, a verification framework for single-object anchor-based object detectors. Its main contribution is a coordinate transformation that re-expresses offset-interval constraints as linear inequalities on corner coordinates, exploiting the injectivity of the box-construction map h∘φ. This allows the IoU optimization problem to be solved exactly by checking a fixed set of 169 candidate points, avoiding loose relaxations of the nonlinear box construction. The method is integrated with bound propagation and branch-and-bound, and evaluated on SSD, YOLOv2, and YOLOv3 variants under brightness, contrast, and motion-blur perturbations. The paper claims the first formal robustness verification of these architectures.

Significance. If the mathematical core holds, the coordinate transformation and exact IoU candidate enumeration are a useful step beyond prior toy-model verification, and the self-contained derivation with no fitted constants is a strength. The method's ability to give crisp IoU bounds over offset intervals is a clean, parameter-free contribution that could be reused in future end-to-end detection verification. However, the significance is currently limited by a load-bearing scope issue: the verified property is for a simplified post-processor that selects the single highest-confidence box, not for the full NMS-based detector defined in Def. 1. The reported 'first verification of SSD/YOLOv2/YOLOv3' is therefore for modified variants, and this must be stated precisely for the claims to be sound.

major comments (3)
  1. [§3.1, Step 3; Appendix A] The 'without loss of generality' reduction from full post-processing to the single highest-confidence box is false as stated. Def. 1 requires the post-processed output to contain exactly one correct box. For an NMS-based detector, the highest-confidence box above threshold is always retained, but NMS may also output additional boxes whose IoU with the top box is below the NMS threshold. In such a case the full output has |D|>1 and is incorrect under Def. 1, while the top-box-only output is correct. Appendix A itself acknowledges this in its second bullet when it says that in the multiple-box case the highest-scoring box 'could end up being correct.' Consequently, Algorithm 1 certifies a simplified detector whose post-processor selects the highest-confidence box, not the NMS-based detector defined in Def. 1. The experimental claims of 'first verification of SSD/YOLOv2/YOLOv3' must be expl
  2. [Theorem 2 / Appendix G] The proof of Theorem 2 only establishes that GetHighestBox correctly aggregates score bounds and selects candidate boxes whose score upper bound exceeds the maximum lower bound. It does not connect this bookkeeping to the correctness definition of Def. 1. In particular, the proof assumes the output is the single highest-confidence box, which is exactly the assumption challenged in the previous comment. The theorem as stated ('IoUCert is correct') is therefore not established for detectors with NMS post-processing. Please either restrict the theorem to the simplified top-box post-processor, or extend the verification to enforce the 'exactly one box' condition required by Def. 1.
  3. [Appendix F / Theorem 1] The proof of Theorem 1 is the mathematical core of the 169-point enumeration, but it is not written to a fully publishable standard. The text states that points where the gradient is zero need not be considered because the partial derivatives are 'never zero within the feasible region' (citing Cohen et al.), yet F.2 then analyses boundary derivatives that can vanish under conditions such as a(g)=(K−2g0)(z3−z1). The argument that these stationary points are already covered by P_c ∪ P_int ∪ P_gt relies on an unstated property that the derivative along a boundary segment is either identically zero or never zero. This is plausible but not demonstrated, and the phrase 'in an analysis we present after the proof' does not clearly separate the required analysis from the proof. Please provide a complete, self-contained proof, or a precise reference, for Theorem 1.
minor comments (6)
  1. [§4.2] Theorem 1 is stated only for the maximum, but Algorithm 2 uses the same candidate set for the minimum. Please state explicitly that the minimum is handled by an analogous argument.
  2. [Algorithm 1] GetHighestBox is not defined in the main text; it appears only in Appendix G. The returned predClass is also ambiguous when multiple candidate boxes have different classes. Please clarify the main-text presentation.
  3. [Appendix G, Algorithm 2] The return statement 'Return IoU, IoU' is a typesetting artifact; use distinct names for the lower and upper IoU bounds.
  4. [Table 2] The caption mentions 'baseline length ranges' without explaining what is being measured. Define the quantity and clarify what 'avoided subproblem exploration percentage' means.
  5. [Appendix F.1] The definitions c_i=(1−i) and k_i=(2−i) are only used for specific index sets. Explicitly restrict them to avoid confusion, e.g., i∈{0,2} for c_i and i∈{1,3} for k_i.
  6. [Evaluation / Reproducibility] No code or artifact link is provided. Releasing the implementation would strengthen the reproducibility of the experimental claims.

Circularity Check

0 steps flagged

No significant circularity: Theorem 1's IoU-optimum enumeration is derived from an exact variable substitution plus an independently attributed derivative analysis; the central claim does not reduce to its inputs.

full rationale

The derivation chain is self-contained with respect to circularity. Section 4.1 replaces the offset-constrained maximization of IoU(h∘φ(o), g) with an exactly equivalent corner-space problem via the inverse mapping (h∘φ)^{-1}, justified by injectivity of the coordinate maps (Proposition 1 and Appendix C); this is a variable substitution, not a fitted or predefined answer. Theorem 1's 169-point candidate set is justified by an extreme-point argument in Appendix F, using partial-derivative sign information attributed to Cohen et al. [19] (an external source, not the authors' own prior work), and the derivative analysis is reproduced in the appendix. The LeakyReLU relaxation in Theorem 3 is derived from the over-approximation area formula, not imported as an ansatz. Self-citations such as [36] and [38] provide the underlying bound-propagation engine (Venus) and prior verifier techniques, but they are not the load-bearing theoretical premise of the IoU bound. The questionable Appendix A 'without loss of generality' reduction from full NMS post-processing to the single highest-confidence box is a correctness/scope caveat about what property is certified, not a circular reuse of the verification conclusion as an input, so it does not raise the circularity score. Overall, no step equates a prediction with a fitted parameter or derives the target result from an unverified self-citation chain.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 0 invented entities

The central claim does not rest on fitted free parameters. It rests on domain assumptions: injectivity of box decoding, the highest-confidence-box reduction, soundness of the underlying verifier, and the equivalence of AvgPool-modified models to the detectors being certified. The LeakyReLU slope choice is a design heuristic presented as optimal, not a fitted parameter.

axioms (4)
  • domain assumption The mapping h∘ϕ from anchor offsets to corner coordinates is injective on the domain of interest (positive anchor priors, positive grid scales, positive variance).
    Needed for the change of variables o=ϕ^{-1}∘h^{-1}(z) in Eq. (2). Proven in Appendix C for SSD/YOLOv2/YOLOv3 under p_i, s, var > 0; if a detector uses a non-injective decoding, the transformation fails.
  • domain assumption Post-processing in single-object detection is equivalent to selecting the highest-confidence box above a confidence threshold.
    Stated in §3.1 as 'without loss of generality, see Appendix A'. Appendix A only shows the highest-scoring box is retained by NMS; it does not prove equivalence with full NMS outputs (zero/multiple boxes, suppression of overlapping boxes).
  • domain assumption Bound propagation through Venus yields sound interval bounds for the network's output offsets and logits.
    IoUCert consumes these bounds in Algorithm 1 (Line 4); the correctness theorem assumes the underlying verifier is sound.
  • domain assumption The models verified are faithful stand-ins for SSD/YOLOv2/YOLOv3 after replacing MaxPool with AvgPool and cropping COCO to single objects.
    Stated in §5.1 and Appendix D.3; the architectures verified are 'tractable variants', not the original released models.

pith-pipeline@v1.3.0-alltime-deepseek · 31502 in / 18937 out tokens · 183543 ms · 2026-08-02T19:11:10.999672+00:00 · methodology

0 comments
Cite this review

Pith. "Pith review of IoUCert: Robustness Verification for Anchor-based Object Detectors." pith.science (2026). https://pith.science/paper/62LT75RB

@misc{pith2026260303043,
  author       = {Pith},
  title        = {Pith review of: IoUCert: Robustness Verification for Anchor-based Object Detectors},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/62LT75RB}},
  note         = {Machine review of arXiv:2603.03043}
}
Share X Bluesky LinkedIn Reddit HN
read the original 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

Figures reproduced from arXiv: 2603.03043 by Alejandro J. Mercado, Alessio Lomuscio, Benedikt Br\"uckner, Panagiotis Kouvaros, Yanghao Zhang.

Figure 1
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). require robustness validation. A notable example of this are object detection (OD) models [43,53,73] which may exhibit vulnerabilities su… view at source ↗
Figure 2
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. predicted offsets to center-format bounding boxes), and then through h (which converts the predicted offsets into corner-format coordinates) before bounding the IoU function [19]. Our approach circumvents the over-ap… view at source ↗
Figure 3
Figure 3. Figure 3: Variation of the IoU function given its partial derivatives. F.2 Analysing ∂IoU ∂zk on the border of constraints We will consider the general case: \label {newconstraints} \begin {gathered} \max _{z_0,z_1,z_2,z_3} \text {IoU}((z_0,z_1,z_2,z_3),g) \\ \begin {aligned} \text {s.t.}\quad L^x_1 &\leq z_0 + z_2 \leq U^x_1 \ \text {(a)} \\ L^y_1 &\leq z_1 + z_3 \leq U^y_1 \ \text {(b)} \\ L^x_2 &\leq z_2 - z_0 \l… view at source ↗
Figure 4
Figure 4. Figure 4: Visualisation of the lower and upper LeakyReLU bounding functions for a sample α˜ = 0.5. The lower overapproximation area is shaded in red, the upper overap￾proximation area in blue. The total relaxation error is the difference between area enclosed by the relax￾ation and that enclosed by the actual function, i.e. e_{x<0}(\tilde {\alpha }) = a_2 - a_1 = \frac {1}{2} l^2 (\tilde {\alpha } - \alpha ). (26) R… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Certified Training for Convolutional Perturbations

    cs.CV 2026-07 conditional novelty 6.0

    A certified-training method using parameterized blur kernels and symbolic bound propagation gives provable robustness to motion blur and related convolutional perturbations, reaching over 80% verified accuracy on CIFAR10.

Reference graph

Works this paper leans on

74 extracted references · 13 linked inside Pith · cited by 1 Pith paper

  1. [1]

    In: Proceedings of the 1st and 2nd Workshop on Applied Verification for Continuous and Hybrid Systems

    Althoff, M.: An introduction to cora 2015. In: Proceedings of the 1st and 2nd Workshop on Applied Verification for Continuous and Hybrid Systems. pp. 120– IoUCert: Robustness Verification for Anchor-based Object Detectors 15

    2015

  2. [2]

    In: The Visual Computer

    Amirkhani, A., Karimi, M.P., Banitalebi-Dehkordi, A.: A survey on adversarial attacks and defenses for object detection and their applications in autonomous vehicles. In: The Visual Computer. Lecture Notes in Computer Science, vol. 39, p. 5293–5307. Springer (2023)

    2023

  3. [3]

    In: Integer Pro- gramming and Combinatorial Optimization

    Anderson,R.,Huchette,J.,Ma,W.,Tjandraatmadja,C.,Vielma,J.:Strongmixed- integer programming formulations for trained neural networks. In: Integer Pro- gramming and Combinatorial Optimization. LNCS, vol. 11480, pp. 27–42. Springer (2020)

    2020

  4. [4]

    In: Proceedings of the 13th International Symposium on NASA Formal Methods (NFM21)

    Bak, S.: nnenum: Verification of relu neural networks with optimized abstraction refinement. In: Proceedings of the 13th International Symposium on NASA Formal Methods (NFM21). Lecture Notes in Computer Science, vol. 12673, pp. 19–36. Springer (2021)

    2021

  5. [5]

    In: Proceedings of the 33rd Annual Conference on Neural Information Processing Systems (NeurIPS19), pp

    Balunovic, M., Baader, M., Singh, G., Gehr, T., Vechev, M.: Certifying geometric robustness of neural networks. In: Proceedings of the 33rd Annual Conference on Neural Information Processing Systems (NeurIPS19), pp. 15313–15323. Curran Associates, Inc. (2019)

    2019

  6. [6]

    In: Proceedings of the 27th European Conference on Artifi- cial Intelligence (ECAI24)

    Batten, B., Zheng, Y., De Palma, A., Kouvaros, P., Lomuscio, A.: Verification of geometric robustness of neural networks via piecewise linear approximation and lipschitz optimisation. In: Proceedings of the 27th European Conference on Artifi- cial Intelligence (ECAI24). pp. 2362–2369. IOS Press (2024)

    2024

  7. [7]

    arXiv preprint arXiv:2004.10934 (2020)

    Bochkovskiy, A., Wang, C.., Liao, H.Y.M.: Yolov4: Optimal speed and accuracy of object detection. arXiv preprint arXiv:2004.10934 (2020)

    Pith/arXiv arXiv 2004

  8. [8]

    In: Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI20)

    Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., Misener, R.: Efficient ver- ification of neural networks via dependency analysis. In: Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI20). pp. 3291–3299. AAAI Press (2020)

    2020

  9. [9]

    Cambridge University Press (2004)

    Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press (2004)

    2004

  10. [10]

    arXiv preprint arXiv:2412.19985 (2024)

    Brix, C., Bak, S., Johnson, T.T., Wu, H.: The fifth international verification of neu- ral networks competition (vnn-comp 2024): Summary and results. arXiv preprint arXiv:2412.19985 (2024)

    Pith/arXiv arXiv 2024

  11. [11]

    arXiv preprint arXiv:2301.05815 (2023)

    Brix, C., Müller, M.N., Bak, S., Johnson, T.T., Liu, C.: First three years of the in- ternational verification of neural networks competition (vnn-comp). arXiv preprint arXiv:2301.05815 (2023)

    Pith/arXiv arXiv 2023

  12. [12]

    In: Proceedings of the 39th AAAI Con- ference on Artificial Intelligence (AAAI25)

    Brückner, B., Lomuscio, A.: Verification of neural networks against convolutional perturbations via parameterised kernels. In: Proceedings of the 39th AAAI Con- ference on Artificial Intelligence (AAAI25). pp. 27215–27223. AAAI Press (2025)

    2025

  13. [13]

    In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS 2019)

    Cao, Y., Xiao, C., Cyr, B., Zhou, Y., Park, W., Rampazzi, S., Chen, Q.A., Fu, K., Mao, Z.M.: Adversarial sensor attack on lidar-based perception in autonomous driving. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS 2019). pp. 2267–2281. ACM (2019)

    2019

  14. [14]

    In: Proceedings of the 40th International Conference on Machine Learning (ICML23)

    Chiu, H.M., Zhang, R.Y.: Tight certification of adversarially trained neural net- works via nonconvex low-rank semidefinite relaxations. In: Proceedings of the 40th International Conference on Machine Learning (ICML23). vol. 202, pp. 5631–5660. PMLR (2023)

    2023

  15. [15]

    In: Proceedings of the 34th Interna- tional Conference on Artificial Neural Networks (ICANN25)

    Chowdhury, S., Khandelwal, H., D’Souza, M.: Robustness verification for object detectors using set-based reachability analysis. In: Proceedings of the 34th Interna- tional Conference on Artificial Neural Networks (ICANN25). pp. 481–492. Lecture Notes in Computer Science, Springer (2025) 16 B. Brückner et al

    2025

  16. [16]

    arXiv preprint arXiv:2104.06718 (2021)

    DePalma,A.,Bunel,R.,Desmaison,A.,Dvijotham,K.,Kohli,P.,Torr,P.,Kumar, M.P.: Improved branch and bound for neural network verification via lagrangian decomposition. arXiv preprint arXiv:2104.06718 (2021)

    Pith/arXiv arXiv 2021

  17. [17]

    Soft Computing28(19), 11647–11665 (2024)

    Demarchi, S., Guidotti, D., Pulina, L., Tacchella, A.: Never2: Learning and verifi- cation of neural networks. Soft Computing28(19), 11647–11665 (2024)

    2024

  18. [18]

    arXiv preprint arXiv:2304.09938 (2023)

    Ducoffe, M., Carrere, M., Féliers, L., Gauffriau, A., Mussot, V., Pagetti, C., Sam- mour, T.: Lard – landing approach runway detection – dataset for vision based landing. arXiv preprint arXiv:2304.09938 (2023)

    Pith/arXiv arXiv 2023

  19. [19]

    In: Proceedings of the 44th Digital Avionics Systems Conference (DASC25)

    Ducoffe, N.C.M., Boumazouza, R., Gabrea, C., Pagetti, C., Pucel, X., Galametz, A.: Verifiou – robustness of object detection to perturbations. In: Proceedings of the 44th Digital Avionics Systems Conference (DASC25). pp. 1–10 (2025)

    2025

  20. [20]

    arXiv preprint arXiv:2307.10266abs/2307.10266(2023)

    Duong, H., Li, L., Nguyen, T., Dwyer, M.B.: A dpll(t) framework for verifying deep neural networks. arXiv preprint arXiv:2307.10266abs/2307.10266(2023)

    Pith/arXiv arXiv 2023

  21. [21]

    In: Proceedings of the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA17)

    Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: Proceedings of the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA17). Lecture Notes in Computer Science, vol. 10482, pp. 269–286. Springer (2017)

    2017

  22. [22]

    International Journal of Computer Vision88(2), 303–338 (2010)

    Everingham, M., Gool, L.V., Williams, C.K.I., Winn, J.M., Zisserman, A.: The pascal visual object classes (voc) challenge. International Journal of Computer Vision88(2), 303–338 (2010)

    2010

  23. [23]

    IEEE Transactions on Automatic Control (2020)

    Fazlyab, M., Morari, M., Pappas, G.J.: Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming. IEEE Transactions on Automatic Control (2020)

    2020

  24. [24]

    In: Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control (HSCC22)

    Ferlez, J., Khedr, H., Shoukry, Y.: Fast batllnn: Fast box analysis of two-level lattice neural networks. In: Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control (HSCC22). pp. 23:1–23:11. ACM (2022)

    2022

  25. [25]

    In: Proceedings of the 10th Interna- tional Conference on Learning Representations (ICLR22)

    Ferrari,C.,Mueller,M.,Jovanović,N.,Vechev,M.:Completeverificationviamulti- neuron relaxation guided branch-and-bound. In: Proceedings of the 10th Interna- tional Conference on Learning Representations (ICLR22). Openreview.net (2022)

    2022

  26. [26]

    In: Proceedings of the 3rd International Conference on Learning Repre- sentations (ICLR15) (2015)

    Goodfellow, I., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial ex- amples. In: Proceedings of the 3rd International Conference on Learning Repre- sentations (ICLR15) (2015)

    2015

  27. [27]

    arXiv preprint arXiv:1810.12715 (2019)

    Gowal, S., Dvijotham, K., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arand- jelovic, R., Mann, T., Kohli, P.: On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint arXiv:1810.12715 (2019)

    Pith/arXiv arXiv 2019

  28. [28]

    In: Proceedings of the 19th International Conference on Software Engineering and Formal Methods (SEFM21)

    Hashemi, V., Kouvaros, P., Lomuscio, A.: Osip: Tightened bound propagation for the verification of relu neural networks. In: Proceedings of the 19th International Conference on Software Engineering and Formal Methods (SEFM21). pp. 463–480. IEEE Computer Society (2021)

    2021

  29. [29]

    In: Proceedings of the 32nd British Machine Vision Conference (BMVC21)

    Henriksen, P., Hammernik, K., Rueckert, D., Lomuscio, A.: Bias field robustness verification of large neural image classifiers. In: Proceedings of the 32nd British Machine Vision Conference (BMVC21). BMVA Press (2021)

    2021

  30. [30]

    In: Proceedings of the 30th In- ternational Joint Conference on Artificial Intelligence (IJCAI21)

    Henriksen, P., Lomuscio, A.: DEEPSPLIT: an efficient splitting method for neural network verification via indirect effect analysis. In: Proceedings of the 30th In- ternational Joint Conference on Artificial Intelligence (IJCAI21). pp. 2549–2555. ijcai.org (2021)

    2021

  31. [31]

    Jocher, G.: Yolov3 by ultralytics.https://github.com/ultralytics/yolov3 (2020) IoUCert: Robustness Verification for Anchor-based Object Detectors 17

    2020

  32. [32]

    In: Proceedings of the 29th Inter- national Conference on Computer Aided Verification (CAV17)

    Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: Proceedings of the 29th Inter- national Conference on Computer Aided Verification (CAV17). Lecture Notes in Computer Science, vol. 10426, pp. 97–117. Springer (2017)

    2017

  33. [33]

    In: Proceedings of the 31st International Conference on Computer Aided Verification (CAV19)

    Katz, G., Huang, D., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljic, A., Dill, D., Kochenderfer, M., Barrett, C.: The marabou framework for verification and analysis of deep neural networks. In: Proceedings of the 31st International Conference on Computer Aided Verification (CAV19). pp. 443–452 (2019)

    2019

  34. [34]

    arXiv preprint 2512.19007 (2025)

    Kaulen, K., Ladner, T., Bak, S., Brix, C., Duong, H., Flinkow, T., Johnson, T.T., Koller, L., Manino, E., Nguyen, T.H., Wu, H.: The 6th international verification of neural networks competition (vnn-comp 2025): Summary and results. arXiv preprint 2512.19007 (2025)

    arXiv 2025

  35. [35]

    In: 1st Workshop on Formal Verification of Machine Learning (WFVML22) (2022)

    Kern, P., Büning, M., Sinz, C.: Optimized symbolic interval propagation for neural network verification. In: 1st Workshop on Formal Verification of Machine Learning (WFVML22) (2022)

    2022

  36. [36]

    In: Proceed- ings of the 39th AAAI Conference on Artificial Intelligence (AAAI25)

    Kouvaros, P., Brückner, B., Henriksen, P., Lomuscio, A.: Dynamic back- substitution in bound-propagation-based neural network verification. In: Proceed- ings of the 39th AAAI Conference on Artificial Intelligence (AAAI25). pp. 27383– 27391. AAAI Press (2025)

    2025

  37. [37]

    In: Proceedings of the 24th International Symposium on Formal Methods (FM21)

    Kouvaros, P., Kyono, T., Leofante, F., Lomuscio, A., Margineantu, D., Osipychev, D., Zheng, Y.: Formal analysis of neural network-based systems in the aircraft domain. In: Proceedings of the 24th International Symposium on Formal Methods (FM21). Lecture Notes in Computer Science, vol. 13047, pp. 730–740. Springer (2021)

    2021

  38. [38]

    In: Proceedings of the 30th Interna- tional Joint Conference on Artificial Intelligence (IJCAI21)

    Kouvaros, P., Lomuscio, A.: Towards scalable complete verification of relu neural networks via dependency-based branching. In: Proceedings of the 30th Interna- tional Joint Conference on Artificial Intelligence (IJCAI21). pp. 2643–2650. ij- cai.org (2021)

    2021

  39. [39]

    In: Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23)

    Lan, J., Brückner, B., Lomuscio, A.: A semidefinite relaxation based branch-and- bound method for tight neural network verification. In: Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23). pp. 14946–14954. AAAI Press (2023)

    2023

  40. [40]

    arXiv preprint arXiv:2410.23903 (2024)

    Lemesle, A., Lehmann, J., Gall, T.L.: Neural network verification with pyrat. arXiv preprint arXiv:2410.23903 (2024)

    Pith/arXiv arXiv 2024

  41. [41]

    In: Proceedings of the 13th European Conference on Computer Vision (ECCV 2014)

    Lin, T.Y., Maire, M., Belongie, S., Hays, J., Perona, P., Ramanan, D., Dollár, P., Zitnick, C.L.: Microsoft coco: Common objects in context. In: Proceedings of the 13th European Conference on Computer Vision (ECCV 2014). pp. 740–755. Lecture Notes in Computer Science, Springer (2014)

    2014

  42. [42]

    Medical Image Analysis42, 60–88 (2017)

    Litjens,G.,Kooi,T.,Bejnordi,B.E.,Setio,A.A.,Ciompi,F.,Ghafoorian,M.,Laak, J.A.V.D., Ginneken, B.V., Sánchez, C.I.: A survey on deep learning in medical image analysis. Medical Image Analysis42, 60–88 (2017)

    2017

  43. [43]

    In: Proceedings of the 14th European Con- ference on Computer Vision (ECCV16)

    Liu, W., Anguelov, D., Erhan, D., Szegedy, C., Reed, S.E., Fu, C.Y., Berg, A.C.: Ssd: Single shot multibox detector. In: Proceedings of the 14th European Con- ference on Computer Vision (ECCV16). Lecture Notes in Computer Science, vol. 9905, pp. 21–37. Springer (2016)

    2016

  44. [44]

    In: Proceedings of the 14th International Conference on Learning Representations (ICLR26)

    Liu, Z., Yu, L., Lin, T., Chi, Z., Zhang, L.: Certifying the full YOLO pipeline: A probabilistic verification approach. In: Proceedings of the 14th International Conference on Learning Representations (ICLR26). OpenReview.net (2026)

    2026

  45. [45]

    arXiv preprint 1706.07351 (2017) 18 B

    Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint 1706.07351 (2017) 18 B. Brückner et al

    Pith/arXiv arXiv 2017

  46. [46]

    In: Proceedings of the 35th International Conference on Computer Aided Verification (CAV23)

    Lopez, D.M., Choi, S.W., Tran, H.D., Johnson, T.T.: Nnv 2.0: The neural network verification tool. In: Proceedings of the 35th International Conference on Computer Aided Verification (CAV23). Lecture Notes in Computer Science, vol. 13965, pp. 397–412. Springer (2023)

    2023

  47. [47]

    IEEE Access11, 33401–33413 (2023)

    Mellouki, O.E., Khedher, M.I., El-Yacoubi, M.A.: Abstract layer for leakyrelu for neural network verification based on abstract interpretation. IEEE Access11, 33401–33413 (2023)

    2023

  48. [48]

    In: Proceedings of the 14th International Conference on Agents and Artificial Intelligence (ICAART22)

    Mziou-Sallami, M., Adjed, F.: Towards a certification of deep image classifiers against convolutional attacks. In: Proceedings of the 14th International Conference on Agents and Artificial Intelligence (ICAART22). pp. 419–428 (2022)

    2022

  49. [49]

    In: Proceedings of the 2025 IEEE International Conference on Image Processing (ICIP25)

    Nirala, A.K., Sarkar, S.: Towards certified object detectors: Certified runway de- tection using yolo. In: Proceedings of the 2025 IEEE International Conference on Image Processing (ICIP25). pp. 827–832 (2025)

    2025

  50. [50]

    AI Communications25(2), 117–135 (2012)

    Pulina, L., Tacchella, A.: Challenging SMT solvers to verify neural networks. AI Communications25(2), 117–135 (2012)

    2012

  51. [51]

    In: Proceedings of the 32nd Annual Conference on Neural Information Processing Systems (NeurIPS18)

    Raghunathan, A., Steinhardt, J., Liang, P.S.: Semidefinite relaxations for certifying robustness to adversarial examples. In: Proceedings of the 32nd Annual Conference on Neural Information Processing Systems (NeurIPS18). pp. 10900–10910 (2018)

    2018

  52. [52]

    arXiv preprint arXiv:2407.01295 (2024)

    Raviv, A., Elboher, Y.Y., Aluf-Medina, M., Weiss, Y.L., Cohen, O., Assa, R., Katz, G., Kugler, H.: Formal verification of object detection. arXiv preprint arXiv:2407.01295 (2024)

    Pith/arXiv arXiv 2024

  53. [53]

    In: Proceedings of the 29th IEEE Conference on Computer Vision and Pattern Recognition (CVPR16)

    Redmon,J.,Divvala,S.,Girshick,R.,Farhadi,A.:Youonlylookonce:Unified,real- time object detection. In: Proceedings of the 29th IEEE Conference on Computer Vision and Pattern Recognition (CVPR16). pp. 779–788 (2016)

    2016

  54. [54]

    In: Proceedings of the 30th IEEE Conference on Computer Vision and Pattern Recognition (CVPR17)

    Redmon, J., Farhadi, A.: Yolo9000: Better, faster, stronger. In: Proceedings of the 30th IEEE Conference on Computer Vision and Pattern Recognition (CVPR17). pp. 6517–6525 (2017)

    2017

  55. [55]

    arXiv preprint 1804.02767 (2018)

    Redmon, J., Farhadi, A.: Yolov3: An incremental improvement. arXiv preprint 1804.02767 (2018)

    Pith/arXiv arXiv 2018

  56. [56]

    In: Proceedings of the 32nd Annual Conference on Neural Information Processing Systems (NeurIPS18)

    Singh, G., Gehr, T., Mirman, M., Püschel, M., Vechev, M.: Fast and effective robustness certification. In: Proceedings of the 32nd Annual Conference on Neural Information Processing Systems (NeurIPS18). pp. 10802–10813 (2018)

    2018

  57. [57]

    Proceedings of the ACM on Programming Languages3(POPL), 41 (2019)

    Singh, G., Gehr, T., Püschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages3(POPL), 41 (2019)

    2019

  58. [58]

    In: Proceedings of the 7th International Conference on Learning Representations (ICLR19)

    Singh, G., Gehr, T., Püschel, M., Vechev, M.: Boosting robustness certification of neural networks. In: Proceedings of the 7th International Conference on Learning Representations (ICLR19). OpenReview.net (2019)

    2019

  59. [59]

    In: Proceedings of the 7th International Conference on Learning Representations (ICLR19) (2019)

    Tjeng, V., Xiao, K., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: Proceedings of the 7th International Conference on Learning Representations (ICLR19) (2019)

    2019

  60. [60]

    In: Proceedings of the 32nd Annual Conference on Neural Information Processing Systems (NeurIPS18)

    Wang,S.,Pei,K.,Whitehouse,J.,Yang,J.,Jana,S.:Efficientformalsafetyanalysis of neural networks. In: Proceedings of the 32nd Annual Conference on Neural Information Processing Systems (NeurIPS18). pp. 6367–6377. Curran Associates, Inc. (2018)

    2018

  61. [61]

    In: Proceedings of the 27th USENIX Security Symposium (USENIX18) (2018)

    Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: Proceedings of the 27th USENIX Security Symposium (USENIX18) (2018)

    2018

  62. [62]

    arXiv preprint arXiv:2103.06624 (2021) IoUCert: Robustness Verification for Anchor-based Object Detectors 19

    Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C., Kolter, J.: Beta-crown: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. arXiv preprint arXiv:2103.06624 (2021) IoUCert: Robustness Verification for Anchor-based Object Detectors 19

    Pith/arXiv arXiv 2021

  63. [63]

    In: Computer Aided Verification

    Wu,H., Isac, O.,Zeljić, A.,Tagomori,T., Daggitt,M., Kokke,W.,Refaeli, I.,Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komen- dantskaya, E., Katz, G., Barrett, C.: Marabou 2.0: A versatile formal analyzer of neural networks. In: Computer Aided Verification. Lecture Notes in Computer Science, vol. 14682, pp. 249–264. Springer (2024)

    2024

  64. [64]

    Proceedings of the 34th Annual Conference on Neural Information Processing Systems (NeurIPS20)33, 1129–1141 (2020)

    Xu, K., Shi, ., Zhang, H., Wang, Y., Chang, K.W., Huang, M., Kailkhura, B., Lin, X., Hsieh, C.J.: Automatic perturbation analysis for scalable certified robustness and beyond. Proceedings of the 34th Annual Conference on Neural Information Processing Systems (NeurIPS20)33, 1129–1141 (2020)

    2020

  65. [65]

    In: Proceedings of the 9th International Conference on Learning Representations (ICLR21)

    Xu, K., Zhang, H., Wang, S., Wang, Y., Jana, S., Lin, X., Hsieh, C.J.: Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In: Proceedings of the 9th International Conference on Learning Representations (ICLR21). OpenReview.net (2021)

    2021

  66. [66]

    In: Proceedings of the 36th Conference on Neural Information Processing Systems (NeurIPS22)

    Zhang, H., Wang, S., Xu, K., Li, L., Li, B., Jana, S., Hsieh, C.J., Kolter, J.Z.: General cutting planes for bound-propagation-based neural network verification. In: Proceedings of the 36th Conference on Neural Information Processing Systems (NeurIPS22). pp. 1656–1670. Curran Associates, Inc. (2022)

    2022

  67. [67]

    In: Proceedings of the 32nd Annual Conference on Neural Information Processing Systems (NeurIPS18)

    Zhang, H., Weng, T., Chen, P., Hsieh, C., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Proceedings of the 32nd Annual Conference on Neural Information Processing Systems (NeurIPS18). pp. 4944–4953 (2018)

    2018

  68. [68]

    IEEE Transactions on Geoscience and Remote Sensing62, 1–15 (2024)

    Zhang, Y., Chen, J., Peng, Z., Dang, Y., Shi, Z., Zou, Z.: Physical adversarial attacks against aerial object detection with feature-aligned expandable textures. IEEE Transactions on Geoscience and Remote Sensing62, 1–15 (2024)

    2024

  69. [69]

    In: Proceedings of the 39th Annual Con- ference on Neural Information Processing Systems (NeurIPS25)

    Zhang, Y., Kouvaros, P., Lomuscio, A.: Scalable neural network geometric robust- ness validation via hölder optimisation. In: Proceedings of the 39th Annual Con- ference on Neural Information Processing Systems (NeurIPS25). OpenReview.net (2025)

    2025

  70. [70]

    arXiv preprint arXiv:2101.00989 (2021)

    Zhang, Y., Wang, F., Ruan, W.: Fooling object detectors: Adversarial attacks by half-neighbor masks. arXiv preprint arXiv:2101.00989 (2021)

    Pith/arXiv arXiv 2021

  71. [71]

    In: Proceedings of the 38th Annual Conference on Neural Information Processing Systems (NeurIPS24) (2024)

    Zhou, D., Brix, C., Hanasusanto, G.A., Zhang, H.: Scalable neural network verifi- cation with branch-and-bound inferred cutting planes. In: Proceedings of the 38th Annual Conference on Neural Information Processing Systems (NeurIPS24) (2024)

    2024

  72. [72]

    In: Proceedings of the 39th Annual Conference on Neural Information Pro- cessing Systems (NeurIPS25)

    Zhou, D., Chavez, J., Chen, H., Hanasusanto, G.A., Zhang, H.: Clip-and-verify: Linear constraint-driven domain clipping for accelerating neural network verifica- tion. In: Proceedings of the 39th Annual Conference on Neural Information Pro- cessing Systems (NeurIPS25). OpenReview.net (2025)

    2025

  73. [73]

    Zou, Z., K.Chen, Shi, Z., Guo, Y., Ye, J.: Object detection in 20 years: A survey. Proceedings of the IEEE111(3), 257–276 (2023) IoUCert: Robustness Verification for Anchor-based Object Detectors 1 A Proof: Without Loss of Generality on Single Highest-Confidence Box We restate the assumption made in the paper:Without loss of generality, we assume inferenc...

    2023

  74. [74]

    In the single-object case (m= 1), correctness reduces to having just one predicted box of the correct class matching the ground truth with sufficientIoU and score

    For eachg∈G, there exists ab∈Dsuch thatarg max i∈1,...,nc ci =g c with its class probability exceedingτclass andIoU(b, g)≥τ iou. In the single-object case (m= 1), correctness reduces to having just one predicted box of the correct class matching the ground truth with sufficientIoU and score. Recall that the OD pipeline includes a postprocessing stageP(e.g...

    2000