Certifying the Full YOLO Pipeline: A Probabilistic Verification Approach
Authors: Zongxin Liu
Lijia Yu
Tao Lin
Zhiming Chi
Lijun Zhang
Venue: ICLR 2026 Poster (2026)
Keywords: Probabilistic Verification
Formal Verification
Object Detection
Safety Guaranteen
Primary area: alignment, fairness, safety, privacy, and societal considerations
TL;DR: This paper presents a probabilistic framework to verify the entire YOLO pipeline against perturbations, uniquely incorporating a formal analysis of  previously under-explored Non-Maximum Suppression (NMS) post-processing stage.

Abstract: Object detection systems are essential in safety-critical applications, but they are vulnerable to object disappearance (OD) threats, in which valid objects become undetected under small input perturbations, creating serious risks. This paper addresses the problem of verifying the robustness of YOLO (You Only Look Once) networks against OD by proposing a three-step probabilistic verification framework: (1) estimating output ranges under a distribution of input perturbations, (2) formally verifying the Non-Maximum Suppression (NMS) process within these ranges, and (3) iteratively refining the results to reduce over-approximation. The framework scales to practical YOLO models. Both theoretical analysis and experimental results demonstrate that our method achieves comparable probabilistic guarantees and provides tighter Intersection-over-Union (IoU) lower bounds while requiring significantly fewer samples than existing methods.

Published as a conference paper at ICLR 2026
CERTIFYING THE FULL YOLO PIPELINE: A PROBA- BILISTIC VERIFICATION APPROACH
Zongxin Liu Lijia Yu², Tao Lin Zhiming Chi Lijun Zhang 1.33+
Key Laboratory of System Software (Chinese Academy of Sciences), Institute of Software, Chinese Academy of Sciences
University of Chinese Academy of Sciences
Institute of AI for Industries, Chinese Academy of Sciences liuzxlics ac. en, jyuuiailiiii aac en, {lintao, chi cmizm, shanglj iioss. acc cn
ABSTRACT
Object detection systems are essential in safety-critical applications, but they are vulnerable to object disappearance (OD) threats, in which valid objects become undetected under small input perturbations, creating serious risks. This paper ad- dresses the problem of verifying the robustness of YOLO (You Only Look Once) networks against OD by proposing three-step probabilistic verification frame- work: (1) estimating output ranges under distribution of input perturbations, (2) formally verifying the Non-Maximum Suppression (NMS) process within these ranges, and (3) iteratively refining the results to reduce over-approximation. The framework scales to practical YOLO models. Both theoretical analysis and ex- perimental results demonstrate that our method achieves comparable probabilistic guarantees and provides tighter Intersection-owe Union (IoU) lower bounds while requiring significantly fewer samples than existing methods.
INTRODUCTION
Object detection (Zhao et al. 2019 Zou et al. 2023 is a fundamental computer vision task that
combines object localization and classification. Neural network architectures, including YOLO
(You Only Look Once) Redmon 2016: Redmon & Farhadi 2017 Farhadi & Redmon, 2018
Bochkooskiy et al.) 2020), Fast R-CNN [Girshick and SSD (Liu et al. 2016; Li et al. 2017
have achieved significant progress in both accuracy and computational efficiency, enabling their widespread deployment in real-world applications. Despite these advances, neural network-based detection systems remain vulnerable to minute, often imperceptible, input perturbations (e.g., sensor noise) (Im Choi & Tian. 2022 Lin et al. 2025 Goodfellow et al. [2113] Madry et al.) 2018 Dong (ct al. 2018 Carlini & Wagner 2017). Of particular concern is the object disappearance (OD) prob- Tem, in which minor input perturbations suppress the detection of valid objects. Such perturbations pose substantial risks in safety-critical domains, potentially leading to catastrophic consequences due detection failures. Consequently, verifying the safety of object detection systems crucial for their reliable deployment.
To measure network robustness, verification methods commonly employed. For given network F, an input æ, and property function é. verification methods can be grouped into three categories:
Formal Verification. The goal is verify whether the property preserved for all perturbed inputs satisfying a given input constraint set C: Va' E C, (F (x')) = (()())). Here C' can en- code norm-bounded perturbations, polyhedral constraints, or application-speecfii semantic con- straints. Equivalently, one can search for a counterexample x' E C that violates the property. However, exact formal verification for ReLU networks is NP-complete (Katz et 2017), mak- ing it infeasible for large-scale networks.
2. Probabilistic Verification. Given a radius and a tolerance a, the goal is to verify whether (ecDD(o(((<)))))) ((F(x))) a. where a distribution over inputs in C. Although this approach leverages probabilistic guarantees to reduce verification time and memory, its reliance
*Corresponding author.

---

Published as a conference paper at ICLR 2026
on processing internal network nodes prevents it from scaling to larger network architectures. Representative works include (Weng et al. 2019 Boetius et al. 2025).
3. Probably Approximately Correct (PAC) Verification. Given E, a, and B. the goal verify (())))) 2 1 - a holds with confidence at least 1 - 5. PAC
whether Pe (=>~D(o(((xz) methods rely on sampling and do not require access to internal network nodes, which allows them to scale further to larger models and datasets. Representative works include (Tran et al.)
2023
Park et al. 2020 ei al. 2022 Blohm al. 2025).
Verifying object detection networks with these methods, however, presents additional challenges beyond the large parameter scales:
1. Post-Processing Stage: Critical post-processing steps, such Non-Maximum Suppression (NMS) (Neubeck & Van Gool 2006), generally fall outside the scope of current formal veri- fication methods (Cohen et al.) [024] Elboher et al. 2024);
2. Large Input-Output Spaces: The dimensionality of the detection inputs and outputs renders cimension-dependentt PAC-based methods (Li al. 2022 Blohm et al. 2025 Haussler & Welzll
1987) computationally infeasible.
Due to these limitations, even recent verification methods specifically designed for object detec- tion (Cohen et al. 2024, Elboher et al. 2024) are restricted to simplified models or do not account for complex operations such as NMS. To address this gap, we propose PAC-based Object Detection Probabilistic Verification (ODPV) framework for YOLO networks under OD threats. To our knowl- edge, this the first framework that effectively verifies the robustness of original object de- tection networks at practical scale. Although PAC-based methods cannot provide deterministic guarantees, they currently offer the most practical means to verify YOLO in a reasonable time.
Our methodology includes three main components: (1) estimating output ranges under input pertur- bations, (2) formally verifying NMS within the estimated output space, and (3) iteratively refining verification results. We implement our approach and evaluate it standard benchmarks. Our main contributions are as follows:
We formally define the PAC verification problem of the OD threat in object detection and propose a novel verification approach to address it.
We implement a complete verification process that includes the NMS step, which has been under- explored in previous work, and provide probabilistic guarantees for each step.
We conduct experiments on widely used networks and datasets to evaluate our proposed method. We demonstrate that our method requires fewer samples to achieve comparable probabilistic guarantees and tighter certified coarsection-ove-Uniii (IoU) bounds.
In summary, we are the first to address the challenges of verifying large-scale detection networks and to provide an efficient probabilistic verification method.
Remark 1. We emphasize an important distinction: Our work differs from randomized smoothing in the type of guarantee it provides (Cohen et al.) 2019 Yang et al. (2200. Randomized smoothing establishes robustness for modified, "smoothed" classifiers, not the original detector. In contrast, we leave the network unchanged and provide statistical guarantees for the original model.
2 RELATED WORK
Object detection. Early detectors relied on hand-crafted features such as Histogram of Oriented
Gradients (HOG) (Dalal& Triggs adaptability. Convolutional Neural Network based approaches transformed feature extraction; R-
2005> and sliding windows (Viola & Jones) 200T). but lacked
CNN variants (Girshick et al. 2014 4 Ren 2015)) combined region proposals with deep learning meth- ods. More recent approaches such as YOLO (Redmon) 2016 Redmon & Farhadi [007], Farhadi &
Redmon 2018 Bochkovskiy et al. 2020) and SSD (Liu et al. 2016 2017) achieved real-time de- tection in complex scenarios.
Verification techniques for Neural Networks. Formal verification determines whether a property
holds under given input constraints. State-of-the the-art tools (Katz al. 2017 2019
Zhang et al.
2022 2018) employ Branch-an
combining relaxations (Singh et al.
2019
Bak 2021)
bound propagation (Wang et al. 2018b Weng et al. 2018 Wang al. 2018a
Gowal al. 2019
2

---

Published as a conference paper at ICLR 2026
person 0.70
stop sign 0.94
STOP STOP
POP S
STOP
struck Ostppp sign 0.84
car 0.65
Figure I: (First Stage) The net- work tries to find all boxes that may contain objects. A subset of these boxes is shown here.
Figure 2: (Second Stage) Final output boxes selected by NMS along with their corresponding labels and confidence scores.
Figure 3: Under imperceptible input perturbations, YOLO no longer recognize these ob- jects.
and constraint solving (Khedr al., 2021 Ehlers 2017 Henriksen & Lomuscio 2020 Kouvaros & Lomuscio 2021). However, for large networks such as YOLO (with 640 x 640 x 3 inputs), even
basic bound propagation may require more than 5000 GB of memory, rendering formal verification infeasible in practice. To address scalability, probabilistic verification estimates the likelihood of property satisfaction. Sampling- based methods (Webb al.) 2019) Cardelli et al., 2019 Mangal
et al. 2019 Anderson & Sojoudi] (023) provide probabilistic estimates, but may miss rare cases, thereby creating gaps between analy ysis and actual robustness. DeepPAC (Li et al. 2022] approxi-
mates local network behavior with linear equations and high-confidence eтror bounds, but it requires prohibitively large sample sizes for models such as YOLO. Techniques like median smoothing (Chi- ang et al. 2020) certify robustness for a modified, "smoothed" detector, whereas our approach di- rectly verifies the original network.
Verification of Object Detection. Current efforts mainly focus small or simplified detectors. Cohen et al. (2024) propagate bounds to certify IoU, while Elboher et al. (2024) encode IoU into networks for existing verifiers. Both approaches ignore the NMS step and fail to scale to real-world detectors. Comprehensive verification of complete detection pipelines remains an open problem.
PRELIMINARIES
This section outlines the key stages of YOLO object detection, as shown Figs. 3 with an image from the COCO validation dataset (Lin et al. 2014) and defines the threat of OD.
3.1 KEY STAGES OF YOLO OBJECT DETECTION
Bounding Box Prediction (First Stage). The YOLO network F Rddo > Rdd processes an input (with dimension do) to generate an output y F(x) (with dimension dz). The output y can be reformulated as a set of bounding boxes {boz, },me where The is a constant determined by the fixed input dimension. Each bounding box box; represented as (Ia, ys. w,, h4s Cs Pi. Pizy.... Pin...) ) Here, (r,, yt) denotes the box's center coordinates, (w;, 14.) its width and height, 6 its confidence score, and pi, the probability of the object belonging to class j (for number of classes). The class of box; is assigned as Class(box;) = arg max (ma.)) Pi, These boxes collectively identify possible object locations in the input image, Figure Illlustaats....
[Metss, where Rets is the total
Mon-Maximum Suppression (Second Stage). Let y = F(x) be the first-stage output tensor. The second stage applies an operator N to y. which yields index set S(y) S [. The selected boxes
are (boz,, hi, ES(y) C {boz, 1h which form the final YOLO output (Figure 2). The standard operator N is NMS (Neubeck & Van Gool 2006) in YOLO, which uses y and predefined thresholds 7. E (0, 1) to select the final output. For simplicity, we denote this as N(y); since and are fixed,
omit them. NMS selects boxes based on the following three rules:
(n1) ig E [ng]] and box.,, E N(y), then must satisfy Ci 2 4
3

---

Published as a conference paper at ICLR 2026
bon N)
Safe Exists one always detect correct
Unsafe
d sx
OutputA pproximaion
NMS Verification
d d=min
F(x)
3ll,
Bounds Refinement
Suspect
Figure 4: Overview of our verification framework for object detection. The green cube denotes the true but unknown output set under input constraints. The yellow cube is the probabilistically guaranteed over-approximmtion computed by method. Refinement iteratively removes regions that do not intersect the true output set, progressively tightening the bound.
(n2) If iy E [nm] satisfies boz; & Nyy) and ci, 2 4, then there must exist bor;, N(y) such that Class(box,, Class(boo;, and Ci I Cig (box,, box.,) 2 y)
(n3) ig. is E [n=e] such that box;, bor:s Nyy and Class(bor;;) ) Class(boz;,)) ) then must satisfy (oU(bo, box;;) ) <
The loU(bo boxr)) = Area(hozy (ibong))
Area boury Liborrg) measures overlap between two boxes, where Area(borr n
boxz) and Arca U boxz) denote the areas of the intersection and union, respectively. We focus on the properties of the unique NMS-selected subset, omitting implementation details.
3.2 OBJECT DISAPPEARANCE THREAT IN OBJECT DETECTION
An object detection model successfully detects object O in the image æ if there exists at least one box; (x())) satisfying: Class(box;;) = Class(boxgg) and (boz, boxgg)) 2 т, where 7 is predefined IoU threshold and bozgt is O's ground truth box. We define the OD threat as follows:
OD Threat Definition. Given ground truth box bozgt, input constraints C, IoU threshold t, and class Class(borg)) OD occurs if there exists input C such that:
max box, (=x)) [ToU(box; borgg)) II (Class(hoxz;) Class(hoxzg.) <T,
where I(+) denotes an indicator function (returns if true, otherwise). assume max(0) = 0.
VERIFICATION FRAMEWORK FOR OBJECT DETECTION
In this section, we introduce the verification target and our verification approach.
First, we formally define the OD Verifiiiiiintoon problem.
Definition (OD PAC- Verificiiinntion Problem). Given input constraints IoU threshold r, error rate [0, 1], significance level 3 [0, 1], and ground truth box boagtt verify whether with confidence
at least 1 - B, the following holds:
IP P (3boz; E N(F(z)) s.t. [loU(bor; boxg.) 2 7 A Class(bor;) = Class(bor,g:)) ))) 2 1
If true, the system is deemed PAC-safe in C under Here from a distribution over the inputs in the constraint set C.
C to denote that is sampled
Then, we propose a three-part verification framework (see Alg. and Fig. to solve this problem:
Part 1: Network Output Approximation. For input x (9) and constraint C. approximate the output set (()))))ee of the network F with a regular region Z (initially a hyperrectangle; refined by removing hyperspherical exclusion zones) satisfying (me C Z.

---

Published as a conference paper at ICLR 2026
Algorithm 1 Verification framework for the OD
problem
Require:
The network F; the input constraints C; the threshold OD verification problem r; the threshold for Part Three k;; the number of refinement steps 7; the ground truth bounding box boxggg-
Ensure:
Whether YOLO is safe under OD threat. Compute 2 that probabilistically over-approximates {F(x))
1:
b Part
2: repeat
3:
if Vy E 2, Bbor; E Ny)) such that Ubox,, boxgt) 2 A Class(box;; then
4: return Safe.
q = Class(boz) Part Two
5: else
6:
Find a y violating the specified property
Part
7:
dmin = mingee [[F(x) y'll2
> Part
8:
2 2 Byyy dmin)
b Part
9:
end if
10:
until dmai S or T refinement steps have been performed
11:
return Unsafe
>> Part
Part 2: NMS Verification. Verify whether, for all y 2, there exists box; N(y) that satisfies
the OD safety property (Definition[) []. If this holds, the detector is safe. Otherwise, identify a that violates the loU or class-matching condition.
Part 3: Counterexample Validation and Refinement. Compute dmin millaec [[[(x) y ||2- If dmin S (with
0 tolerance). the system unsafe. Otherwise, refine Z by excluding B2 dmin) = { yy - y < ] because the regular region we obtained may be larger than the actual output space (F(x)) and then go back to Part Note that we limit the number of Part 3 iterations for high- nigh-dimensional outputs to prevent computational overload.
Remark 2. Since our goal is PAC verification, Part and Part 3 are implemented using probabilistic methods with guarantees, rather than exact computation, as detailed in the next section.
VERIFICATION METHOD FOR YOLO OBJECT DETECTION
We illustrate the application of the verification framework from Section 4o YOLO object detection. Because of YOLO's complexity and scale, formal verification becomes intractable; therefore, we adopt PAC verification, i.e., black-box verification via sampling. Proofs for Propositions, Lemmas, and Theorems are provided in the Appendix.
We define the input constraint as = (æ ||0 a0 lp < $} for a given sample x (0), norm p Zt (20), and perturbation radius the input set C, and write æ ~ C to denote that æ is a sample drawn from this distribution. For convenience, we define the comparison < & for vectors a, 6 E E to mean Vj [k] a; S by. where a; is the j-th component of a. Similarly, scalar-vector multiplication is defined element-wise.
(0, 1). We consider probability distribution
5.1 NETWORK OUTPUT APPROXIMATION (PART 1)
Consider a network dR + Rd and an input constraint C. In Part I of our approach, we aim to determine the range of [F(x)) JaEC with probabilistic guarantee. We first find a constant e₁ E R+ and vector Umax dd such that Vo C, C,c1% Umaa |((x) ()) holds element- wise. Then let Z [F(x(()) + |e| S (1uma which implies
C Z.
As shown in Algorithm 2 we first randomly select N1 samples from C, and define (Umax); max max, max(max, [| (zx -(x))(())))) (0)),)}><) <}. where Ç > 0 is a small constant to ensure all components are positive. When finding C1. directly solving the problem c₁ = min.20 s.t. [F(x) - F F(x <
CUmaxi Vo is infeasible. Since each constraint is convex for c, by the RCPx n (Campi al.
2009), get er by randomly selecting N₂ samples (1)( ) from C, then calculate by
5

---

Published as a conference paper at ICLR 2026
Algorithm 2 Network Output Approximation (Part 1)
Require:
The neural network F; the input constraints C, N2 Zt, threshold Ç, original input (0)),
Ensure:
The output over-approximmtiio region Z.
1: (x(() N
Jim] -anddomy select N1 points in C.
Find the Umax Find the mmax
2: for JE [dz] do
3:
(Umax)y < mmx { (IF()()) ((z)))))))))
> Use to prevent division by
4: end for
5: (1))) Randomly select N2 points in C.
Find the c
-F((=
6: C1 F maxig(Nal.e((d..
Find the cj
(Amax))
7: return Z + (F(x!")) + le CIUmx]
Algorithm NMS Verification (Part 2)
Require:
{[boz Me likA derived from 2; IoU threshold т; ground truth bounding box boxgt.
Ensure:
Either non-empty safe set Q(2, boxg:)) or an unsafe witness E 2.
Q x-
2: for i [næ] do
3: Calculate (i, 2, boxgt) and r2(1, Z, boogg)
B Appendix Lemma Lemma
4: 2,, boorge) min(r1 (i, Z, boxgt) 12 2, bozg))
5: i 2, boxgt) > r then Q + Q U {i}
6: end if
7: end for
8: if Q o then return (Safe, Q)
9: else f arg ma [T(j', Z, boxge) }: +- unsafe witness that leads to T(j, Z, boxg:)
end if
11: return (Unsafe, 2)
the following optimization problem:
C1 min
s.t. (F(((() F(x) S comax: Vi [Na).
e20
let Umax be vector with positive components (e.g., as estimated from N1 samples in Algorithm ( If cf is computed based
Proposition (probabilistic guarantee for Part 1). For any N1
21n(2/a)] samples described in Algorithm 2 then on this Umax using N2 > 221n(1/8) 2 +
with probability 1 we have: Pawe (F((x) ((x S c1 Umax) 2 a, which implies
Panc (F(x)) 1 l-a.
Remark 3. The probabilistic guarantee imposes no special requirements on N1. We select Umax in this way because a larger N₁ yields a tighter approximation of the true output range (Appendix D)
5.2 NMS VERIFICATION (PART 2)
To better illustrate the NMS verification, we use an infinite index set A to enumerate all possible values in 2, i.e., 2 {2 Jees, where each zt E Z possible output vector. Each z* can be interpreted as set of boxes (box) korking 1n according to the YOLO output format. We assume that bozt can be written as boz = (af ... w/ N cf Pf, define the safe Q r, boxgg)) which contains indices of boxes that satisfy the NMS conditions. Definition (Safe Set). The safe set Q(Z, T, boxgt) S [næ] and i E Q(Z, r, boxgt) if and only if:
.P. pf.......
P ). To verify the NMS, we first
(1) Vk E A, Class(bou?)) = Class(boxgg)) ), & 2 i and loU booggt) 2 T:
(2) Ōk E A, [nzd] {i) such that &t 4, Class(bout)) Class(bougg)) ci 2 c. [bo(bo boort) n7, and ToUuro box

---

Published as a conference paper at ICLR 2026
Then soundly verify the NMS by checking whether the safe set is empty.
Proposition 2 (NMS Soundness Verification), For given 2, T, and bozgt, if (2, T, boxge)) # 0, then Ak E A, 3boz, E N(z*) such that [bor, boxggt 2 T Class(boz.) = Class(bozig
According to this proposition, verification reduces to calculating the safe set. To calculate the safe set, need the following key metric:
Definition 3 (Safe IoU Threshold). The Safe IoU Threshold r(i, 2, borggt) = inf(r' 1Jū ø ((2,7') where inf the infimum operator.
The following lemmas about ri,, Z, boxg:) can help us compute the safe set Q(2, T, boxg:))
Lemma (Threshold Properties). T(i, Z, borg:) = i Q,
We can obtain r(i, 2, bozgi) by solving the following optimization problem: Lemma (Threshold Computation). The threshold can be calculated as T(i, b.og)) = min(r (1, 2, borggt, (2,;; 2, bowggt)), where:
71 (i, 3, boxgg)
= min loU boxg)) I(Claas(box,)) = =q) I[c, 2 1).9 = Class(boo) KEA
A C ToU borgt)
min
if [k: n) s.t. Ckn =
(1,1, 2, borggt)
otherwise
where constraint Ckn = 11(c 2 2) 1(Cllass(bor))) = q)) [(loU(boo boo 2 n) 1(c ct)
Appendix I shows how we encode the optimization problem in line of Algorithm 3 as mixed- integer quadratically constrained program (MIQCP) and use the Gurobi solver to solve it.
5.3 COUNTEREXAMPLE VALIDATION AND REFINEMENT (PART
Part 3 of our framework refines the initial output approximation Z. When Part detects potential counterexample y E Z, in Part 3, we need to check whether y actually reachable by F for some E C. This is done by computing dmii minged [|F(x)) - -y112-
Due to the high dimensionality, even if y E (F(=)) the dmai derived from the sampled outputs converges 7ero very slowly as the sample size increases, directly estimating dmin simply by taking the minimum distance from set of sampled outputs (F() to y may be unreliable.
To address this, we introduce Algorithm two-step procedure for estimating dmin with proba- bilistic guarantees.
Step One (Estimating C): This step aims characterize the local variability of the function F within the input constraint set C. It computes a constant C = max X-- by repeatedly sam-
pling pairs of points and observing the ratio B X where A max [[)()))))))) ((x())))
and B = minje[[] [(+()())) - F(x
Step Two (Estimating dmin using C): Using the constant C' and new set of M2 samples, this step estimates dmin for the specific target vector y. The formula dmin max B.,, (a.-C(4, -Bm),, 0} lever-
Bm))
1-20 ages C to provide more conservative estimate of the minimum distance than B,, (the minimum observed distance from the M2 samples) alone.
Let V(y, dmii) = Pare (F(x) Be(y, dmuin), and V(y, O. We use V(y, dmii) to measure the intersection between B2 dmin) and [F(x))=Ec. We show that with high probability, V(y, dmii) very small.
Theorem 1 (Probabilistic Guarantee for Part 3). Consider Algorithm 4 Here N is the number of outer samples [N in Step One, M is the number of samples {xl and M2 is the number of samples used in Step Two.
LM M ) drawn each (t)
(1-2c) Mc) > 2/ (n( with Algorithm 4 for any y, with probability least B 2(1 M2 over steps one and two, have V(y, dunin) a.
For any a, B,C E 10 satisfying e < 1
2 and N. ((1 -
7

---

Published as a conference paper at ICLR 2026
Algorithm 4 Counterexample Validation and Refinement (Part 3)
Require:
The neural network F; the input constraints C, N, M, M2 Zt, vector y.
Ensure:
Estimate dmin = mingec |1y - F22))l2.
1: C < 0; [x(") Ji= - Randomly select N samples from
Step One
2: for i E [N] do
3:
{ar (((6))) 1=1 < Randomly select M samples from C again
Step One
4: A f maxje[M] (IF(x(()) (l2 Bi + minzelM] [[F(x((1)) F(x |
5:
C+ [C x
Step One
6: end for
7: ) + Randomly select M2 samples from
Step Two
8: Let Am f max]e[[M]] [F(x(()) (1) yl22; Bn +- mingg(Ms) [IF(x((1) - -y112
Step Two
9: return dminn max B. C(Am Bm)) 0}
Step Two
1+20
Remark 4. Take N = 3000, M = 10, M2 = 2000, and e = 1/200, a, 3 0.0099, then 1 - B 2
0.99 and 3 2(1 e)aa2 2 0.99.
We also provide sound refinement algorithm for small networks, shown in Appendix K
5.4 THE PROBABILISTIC GUARANTEE FOR THE ENTIRE ALGORITHM
We prove that the whole algorithm implemented above has probabilistic guarantee by combining and Theorem
Proposition Proposition 2
Theorem 2. (Probabilisttic Guarantee for the Entire Algorithmm Using the notation and definitions from Algorithms
4 Given a, B, E (0,1) satisfying < N ((1- (1)-2e) 2e) (n(})) and
N₂ 2 228(11/8) 2 2lm(2/a) Then, after executing the algorithms defined above, for any k used in Algorishm [ if these algorithms output "Safe" after at most T refinement iterations, then with probability at least - [ + 2(1 - M2) ) 3 over Algorithm (Part 1) and Algorithm (Part 3), we have e is safe)
a
(1 (1+T))
If we take N₁ 30,000, N₂ 5,000, N 3,000, M = 10, M2 2,000, c = 1 1/200, T = 1, we can achieve a 98% probabilistic guarantee with 98% confidence using only 37,000 samples (reuse Part 1 samples in Part 3 Step One), which means with at least 98% confidence, the probability of an OD threat occurring under the given perturbation distribution is at most 2%.
0.0099,
Remark& 5. Note all our theoretical guarantees depend only on the i.i.d. ussumption and hold for any sampling distribution, not just uniform.
EXPERIMENTS
Our experiments evaluate bound accuracy and safety guarantees. Detailed experimental settings and additional results are provided Appendices No
the medium and large versions of the YOLOv3, YOLOv5. YOLOv8 and YOLO11 I models by Ultralytics (oocher et al. 2023). We conduct verification on the COCO dataset (Lin et 2014), widely used benchmark for object detection, and randomly select 100 validation images containing more than 520 objects in total. We use a uniform distribution for sampling, which is common choice in the literature (Li al. 2022 Cohen al. 2024) The IoU threshold is set to 7 E {0.5, 0.7). and the NMS constants are = 0.45 and & 0.25. which are commonly used in object detection tasks. In Appendix X we also evaluate our method under other perturbation distributions (c.g., Gaussian and salt-and-peppe -eppeer noise) and different threat models (e.g.. False Appearance). We set Ç 0.001 (Alg. 2 and 0.01 (Alg. The perturbation radius is set to 255 or 255 Larger radii make the network overly fragile, enabling counterexamples to be found with very few samples, and thus eliminating meaningful differences between methods.
Basic setting. Our experiments
8

---

Published as a conference paper at ICLR 2026
Table Comparison with RCP APGD denotes the mean absolute difference of IoU lower bounds relative to Projected Gradient Descent (PGD) attack. Bold values indicate the best performance.
APGD
PPGD T
8 method
model
time
model
time
0.5
r 0.7
Ours RCPN
109.0
0.49
0.45
50.7
0.48
0.44
255
563.5
0.55
0.53
455.0
0.52
0.52
v3spp
v8m
Ours
106.3
0.48
0.41
49.6
0.53
0,45
2
RCPN
562.9
0.58
0.54
454.7
0.59
0.55
Ours RCP n
108.5
0.52
0.46
132.3
0.49
0.46
255
561.0
0.57
0.55
591.3
0.55
0.54
v3
v8x
Ours RCPN
105.0
0.48
0.42
129.0
0.51
0.44
255
560.3
0.60
0.55
590.6
0.61
0.57
Ours RCPN n
43.6
0.42
0.39
59.1
0.48
0.43
445.5
0.47
0.47
468.8
0.53
0.52
v5m
11m
Ours
42.8
0.48
0.42
58.0
0.50
0.43
2
255
RCPN N
444.4
0.55
0.50
467.8
0.57
0.53
Ours RCPM n
131.5
0.48
0.44
147.2
0.49
0.45
255
593.8
0.54
0.54
618.1
0.54
0.54
v5x
11x
Ours
128.4
0.52
0.45
141.9
0.50
0.44
RCPN
593.2
0.60
0.57
616.5
0.62
0.57
Table 2: Guarantee evaluation of our method with т = 0.5 and & 253 255 under 10 uniform perturbations. TPR/FPR: True/False Positive Rate. TNR/ENR: True/False Negative Rate. A detec- tion is considered positive verified robust by our method, and negative otherwise. Certified Robust Accuracy (CRA): percentage of detections verified robust that indeed robust. Average Bounds Improvement (ABI): mean improvement of certified IoU lower bounds without refinement.
model
8
TPR (%)
FPR (%)
TNR (%)
FNR (%)
CRA (%)
ABI
1/255
94.9
2.9
97.1
5.1
98.9
0.10
yolollx
2/255
85.2
1.4
98.6
14.8
99.4
0.17
1/255
95.0
3.0
97.0
5.0
98.6
0.10
yolo
2/255
93.1
1.1
98.9
6.9
99.4
0.11
1/255
95.1
0.0
100.0
4.9
100.0
0.09
yolov8x
2/255
89.7
0.6
99.4
10.3
99.7
0.14
1/255
97.3
2.6
97.4
2.7
98.9
0.08
yolov8m
2/255
93.9
2.4
97.6
6.1
98.8
0.11
1/255
94.8
0.7
99.3
5.2
99.7
0.09
yolov5xu
2/255
90.6
0.6
99.4
9.4
99.7
0.13
1/255
96.0
2.9
97.1
4.0
98.6
0.10
yolov5mu
2/255
92,4
0.5
99.5
7.6
99.7
0.11
1/255
95.6
0.0
100.0
4.4
100.0
0.08
yolov3-sppu
2/255
87.4
0.0
100.0
12.6
100.0
0.15
1/255
95.7
1.3
98.7
4.3
99.4
0.09
yolov3u
2/255
85.8
0.0
100.0
14.2
100.0
0.16
Baseline Selection. By Theorem our method achieves 98% probabilistic guarantee with 98% confidence using only 37,000 samples. contrast, RCP v requires over 11,000,000 samples, while DeepPAC (Li et al.) 2022) requires over 100,000,000 samples and needs to solve linear programs (LPs) with more than 10 variables to achieve the same guarantee (see Appendix N), making both

---

Published as a conference paper at ICLR 2026
Vectzalton tiuumus
Sparn stak
0.8
FCD aback
Verticaton (Oue))
BCR
0.6
10 11
24 30
34 37 38 40
Figure 5: Lower bounds IoU between detected boxes and their ground-truth counterparts under our method, RCPN, the square attack, and PGD. Results are reported for YOLOI with e 255 and 0.5. Each x-axis tick represents one object COCO.
approaches impractical. Formal verification methods also infeasible: existing tools (Cohen al. 2024 Elboher et al.] 2024) handle only 2-3 convolutional layers with 2-3 linear layers, far below the scale of YOLO, and cannot address its complex architecture or NMS. Therefore, full-guarantee direct comparisons with DeepPAC, RCP n. and formal verification are not feasible. Instead, we weaker-guarantee empirical baseline.
report RCP N with 10th samples
Bounds Accuracy. Table compares our method with RCP N. showing that our approach both faster and more accurate. particular, achieves smaller mean absolute difference between IoU lower bounds and the worst-case input found by the PGD attack (APgD), indicating tighter certified bounds. Figure 5 further confirms this, our bounds remain consistently closer those PGD.
Safety Guarantee. Table 2 further shows results under 106 uniform perturbations: the certified robust accuracy (CRA) exceeds 98%, and the false positive rate (FPR) remains very low, consistent with theory. The true positive rate (TPR) is lower, as expected since our certification is stricter than empirical robustness. Finally, the average bounds improvement (ABI) confirms that our method yields tighter certified IoU lower bounds.
We further evaluate (i) the effect of Part (Appendix Pb. (ii) an ablation study on hyperparameters (Appendix[T) (iii) real-world applications (Appendix R), and (iv) com- parison with median smoothing (Appendix S). All results confirm the effectiveness of our method and its strong probabilistic guarantees.
Additional Experiments.
CONCLUSION
This paper presents new verification framework that provides provable probabilistic guarantees for YOLO-based object detection systems under specific threat models (c.g., object disappearance, false appearance), across range of perturbation distributions. The framework applies to any distribution from which we can draw independent and identically distributed (i.i..) samples, and can be extended other threat models by changing the definition and encoding of the safety property in the NMS verification stage. Our contributions are threefold: (i) we give a formal definition of the object detection verification problem; (ii) we propose a practical three-stage methodology that explicitly includes formal analysis of non-maximum suppression; and (iii) we derive strong probabilistic guarantees for the full detection pipeline. We further show that adapting the method to other threat models only requires modifying the NMS verification condition, while keeping the other stages unchanged. Experiments on multiple YOLO architectures, perturbation distributions, and threat models demonstrate that our approach provides reliable safety assurances and achieves tighter certified IoU bounds with much higher sample efficiency than prior methods.
Limitations and Future Directions: Our method relies on assumed distribution of input per- turbations, a limitation inherent to the PAC framework. Developing verification methods for other types of attacks remains important direction for future work. Another valuable direction involves leveraging adversarial attack strategies to further refine Part 1 and Part 3, alongside investigating more efficient methods for interval estimation and refinement.
10

---

Published as a conference paper at ICLR 2026
ACKNOWLEDGMENTS
This work is supported by the Chinese Academy of Sciences (CAS) Project for Young Scientists in Basic Research, Grant No. YSBR-040, the Institute of Software, Chinese Academy of Sciences (ISCAS) New Cultivation Project ISCAS-PYTX-202201 and ISCAS Basic Research ISCAS-ICZD- 202302. The authors thank anonymous referees for their valuable comments.
REFERENCES
Brendon G. Anderson and Somayeh Sojoudi. Data-driven certification of neural networks with random input noise. IEEE Transactions on Control of Network Systems, 10(1):249-22) 260, 2023. doi: 10. N0.1199/CNSS.222.199999
Stanley Bak. nnenum: Verification of ReLU neural networks with optimized abstraction refinement. In Proceedings the 13th International Symposium NASA Formal Methods (NFM), pp. 19-36. Springer, 2021.
Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel, and Prateek Saxena. Scalable quantitative verification for deep neural networks. In 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE), pp. 312-323, 2021. doi: 10.1 10.1109/CSA499902222..0000 202000009.
Peter Blohm, Patrick Indri, Thomas Gärtner, and SAGAR MALHOTRA. Probably approximately global robustness certification. In Forty-second International Conference on Machine Learning, 2025. |tttsssts////peeeee http://pwwaeeeeeeeeeeeeerraaaaap wwt.
Alexey Bochkovskiy, Yai Wang, and Hong- Yuan Mark Liao.
Yolov4: Optimal speed and
accuracy of object detection. CoRR, 2ax/2004.103344 2020. URL attps://arxiy: org/
0/s/2004.10934
David Boetius, Stefan Leue, and Tobias Sutter. Solving probabilistic verification problems of neural networks using branch and bound. In Forty-second International Conference on Machine Learn- ing, 2025. URL httpt/ttts//pepeeeeeeeps
wttp://ntt/oouumeeeeee forum? wttprrrmmmmnssuiaaaaae pNddkkV
Marco Campi, Simone Garatti, and Maria Prandini. The scenario approach for systems and control design. Annual Reviews in Control, 33(2):1199155 2009.
Luca Cardelli, Marta Kwiatkowska, Luca Laurenti, and Andrea Patane. Robustness guarantees for bayesian inference with gaussian processes. In Proceedings of the AAAI conference on artificial intelligence, volume 33, pp. 7759-7768, 2019.
Nicholas Carlini and David Wagner. Towards evaluating the robustness of neural networks. In 2017 IEEE Symposium Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017, pp. 39-57. IEEE Computer Society, 2017. doi: 10. 2..11099...217..9. URL httpp:: : //o.i
org 20g/100.10 10.1109/11111111 2017.45
Yanbo Chen and Weiwei Liu. A theory of transfer-based black-box attacks: explanation and impli- cations. Advances in Neural Information Processing Systems, 36, 2024.
Ping-yeh Chiang, Michael Curry, Ahmed Abdelkader, Aounon Kumar, John Dickerson, and Tom Goldstein. Detection as regression: Certified object detection with median smoothing. Advances in Neural Information Processing Systems, 33:1275-1222 2020.
Jung Im Choi and Qing Tian. Adversarial attack and defense of yolo detectors in autonomous driving scenarios. In 2022 IEEE Intelligent Vehicles Symposium (IV), pp. 1011-1017, 2022. doi: 10.1109/VV51971.2222. 2022
Jeremy Cohen, Elan Rosenfeld, and Zico Kolter. Certified adversarial robustness via randomized smoothing. In international conference on machine learning, pp. 1310-1320. PMLR, 2019.
Noémic Cohen, Mélanie Ducoffe, Ryma Boumazouza, Christophe Gabreau, Claire Pagetti, Xavier Pucel, and Audrey Galametz. Verification for object detection-ibp iou. arXiv preprint 003.022003.88888, 2024.
11

---

Published as a conference paper at ICLR 2026
N. Dalal and B. Triggs. Histograms of oriented gradients for human detection. In 2005 IEEE Com- puter Society Conference on Computer Vision and Pattern Recognition (CVPR'OS) volume 1, pp. 886-895 vol. 1, 2005. doi: 10.1 ww.11999VVR..200..77..
Yinpeng Dong, Fangzhou Liao, Tianyu Pang. Hang Su, Jun Zhu, Xiaolin Hu, and Jianguo Li. Boost- ing adversarial attacks with momentum. In 2018 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2018, Salt Lake City, UT. USA, June 18-22, 2018, pp. 9185-9193. Computer Vision Foundation IEEE Computer Society, 2018. doi: 10. 00.1109/CVPR.2211800099
Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In Au- tomated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings 15, pp. 269-286 Springer, 2017.
Yizhak Y. Elboher, Avraham Raviv, Yael Leibovich Weiss, Omer Cohen, Roy Assa, Guy Katz, and Hillel Kugler. Formal verification of deep neural networks for object detection, 2024. URL
www/ http://bb//24000 01295
Ali Farhadi and Joseph Redmon. Yolov3: An incremental improvement. In Computer vision and pattern recognition, volume 1804, pp. 1-6. Springer Berlin/Heidelherg, Germany, 2018.
Ross Girshick. Fast r-cnn. In 2015 IEEE International Conference Computer Vision (ICCV), pp- 1440-1448, 2015. doi: 10. 10.100C....221..1
Ross Girshick, Jeff Donahue, Trevor Darrell, and Jitendra Malik. Rich feature hierarchies for ac- curate object detection and semantic segmentation. In Proceedings of the IEEE conference on computer vision and pattern recognition, pp. 580-587, 2014.
Ian J. Goodfellow. Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. In Yoshua Bengio and Yann LeCun (eds.). 3rd International Conference on Learning Representations, ICLR 2015, San Diego CA, USA, May 7-9, 2015, Conference Track Proceed- ings, 2015. URL http: /aw.iv.iviv..///.a//.aaa/aaaaav. www./gg/bbaa.a......e 1412. 6572
Sven Gowal, Krishnamurthy Dj Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovie, Timothy Mann, and Pushmeet Kohli. Scalable verified training for provably robust image classification. In Proceedings of the IEEE/CVF International Conference on Computer Vision, pp. 4842-4851, 2019.
David Haussler and Emo Welzl. s-nets and simplex range queries. Discrete Computational Geometry, 2: 1987. URL. wwtptttt:///// //apps::/ap... semant cccho ar Barg/CorpusTD)
27638326
Patrick Henriksen and Alessio Lomuscio. Efficient neural network verification via adaptive refine- ment and adversarial search. In ECAI 2020, pp. 2513-2521 IOS Press, 2020.
Jung Im Choi and Qing Tian. Adversarial attack and defense of yolo detectors in autonomous driving scenarios. In 2022 IEEE Intelligent Vehicles Symposium (IV), pp. 1011-1017. IEEE, 2022.
Glenn Jocher, Jing Qiu, and Ayush Chaurasia. Ultralytics YOLO. In github, January 2023. URL https:///ithhi: com/ httppultallllle http://aaaallt.tcetaaaaaaa//////
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV), pp. 97-117. Springer, 2017.
Guy Katz, Derek A. Huang, Duligur lbeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Alcksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, and Clark W. Barrett. The marabou framework for verification and analysis of deep neural net- works. In Isil Dillig and Serdar Tasiran (eds.), Computer Aided Verification 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, vol- ume 11561 of Lecture Notes in Computer Science, pp- 443 452. Springer, 2019. doi: 10. 030 25540-4
978-3-030-25540-4
URL https: /ooi org 10t.:////1.1111/09900 0-00888333000--------11
26
12

---

Published as a conference paper at ICLR 2026
Haitham Khedr, James Ferlez, and Yasser Shoukry. Peregrinn: Penalized-relaxation greedy neural network verifier. In Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part 1 33, pp. 287-300. Springer, 2021.
Suhas Kotha, Christopher Brix, Zico Kolter, Krishnamurthy Dvijotham, and Huan Zhang. Provably bounding neural network preimages. Advances in Neural Information Processing Systems, 36: 80270-80290, 2023.
Panagiotis Kouvaros and Alessio Lomuscio. Towards scalable complete verification of ReLU neural networks via dependency-basse -based branching. In IJCAI, pp. 2643-2650, 2021.
Huichen Li, Xiaojun Xu, Xiaolu Zhang, Shuang Yang. and Bo Li. Qeba: Query-efficient boundary- based blackbox attack. In Proceedings of the IEEE/CVF conference on computer vision and pattern recognition, pp. 1221-1230, 2020.
Renjue Li, Pengfei Yang, Cheng-Chao Huang, Youcheng Sun, Bai Xue, and Lijun Zhang. Towards practical robustness analysis for dans based on pac-model learning. In Proceedings of the 44th International Conference on Software Engineering, pp. 2189-2201, 2022.
Zuoxin Li, Lu Yang, and Fuqiang Zhou. Fssd: feature fusion single shot multibox detector. arXiv 2017.
preprint arXiv:1712.0000
Tao Lin, Lijia Yu, Gaojie Jin, Renjue Li, Peng Wu, and Lijun Zhang. Out- nut-of-bouuddig--bee triggers: A stealthy approach to cheat object detectors. In Aleš Leonardis, Elisa Ricci, Stefan Roth, Olga Russakovsky, Torsten Sattler, and Güil Varol (eds.), Computer Vision ECCV 2024, pp. 269-287, Cham, 2025. Springer Nature Switzerland. ISBN 978-3-031-72848-1
Tsung- Yi Lin, Michael Maire, Serge Belongie, James Hays, Pietro Perona, Deva Ramanan, Piotr Dollár, and C Lawrence Zitnick. Microsoft coco: Common objects context. In Computer Vision-ECCV 2014: 13th European Conference, Zurich, Switzerland, September 6-12, 2014, Proceedings, Part V 13, pp. 740-755. Springer, 2014.
Wei Liu, Dragomir Anguelov, Dumitru Erhan, Christian Szegedy, Scott Reed, Cheng- Yang Fu, and Alexander C Berg. Ssd: Single shot multibox detector. In Computer Vision-ECCV 2016: 14th European Conference, Amsterdam, The Netherlands, October / 11-14, 2016, Proceedings, Part I 14, pp. 21-37. Springer, 2016.
Yanpei Liu, Xinyun Chen, Chang Liu, and Dawn Song. Delving into transferable adversarial exam- ples and black-box attacks. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. OpenReview.net, 2017. URL
net hwtp:/eee///uunnt/eeeeee forum id wwd.dyyysssaa SGJqxlxx11
Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. In 6th International Conference Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30 May 3, 2018, Conference Track Proceedings. OpenReview.net, 2018. htllhtttps//openeeeet
net/
Forum?id-rJzz
Ravi Mangal, Aditya V. Nori, and Alessandro Orso. Robustness of neural networks: a probabilis- tic and practical approach. In Proceedings of the 4/st International Conference on Software Engineering: New Ideas and Emerging Results, ICSE-NIER '19, pp. 93-96. IEEE Press, 2019. URL /tt.attps::/bii.orgg/ee org/ 1109 ICSE IIIIIIIIISEEEEE.R...E NIER.
doi: 10. 10.110000
2019 00032
P. Massart. The Tight Constant in the Bieerzky-Kiefer-Woor Inequality The Annals of Prob- ability, 1863):1269 1283, 1990. doi: 10. / URL https:tpp/. //o... org/
Michael Naaman. On the tight constant in the multivariate dvorezzAy-Kieffe-wollov inequal- ity. Statistics Probability Letters, 173:109088, 2021. ISSN 0167-7152. doi: https://doi. org/10. 111.000001111sp122221000090000 URL https: wwwww//wwww/.../////////////wt.. sci wwc.ieeeedrrrt............. wtw.:reetttccteeeeeeeeeeeeeeeeee www.sccenccee...c.cccccmccmp.pee
Atticle/ss1/000177122200000
13

---

Published as a conference paper at ICLR 2026
Alexander Neubeck and Luc Van Gool. Efficient non-maxinum suppression. In 18th international conference on pattern recognition (ICPR '66, volume 3, pp. 150-855. IEEE, 2006.
Sangdon Park, Osbert Bastani, Nikolai Matni, and Insup Lee. PAC confidence sets for deep neural networks via calibrated prediction. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020, OpenReview.net, 2020. URL https:
//openzeview.. wwt.:orrumii-BBB.IIOA.A..
J Redmon. You only look once: Unified, real-time object detection. Proceedings of the IEEE conference on computer vision and pattern recognition, 2016.
Joseph Redmon and Ali Farhadi. Yolo9000: better, faster, stronger. In Proceedings of the IEEE conference on computer vision and pattern recognition, pp. 7263-7271, 2017.
Shaoqing Ren. Faster r-cnn: Towards real-time object detection with region proposal networks.
arXiv preprint arXiv:1506.0m SEt.::1506.01197,, 2015.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for cer- tifying neural networks. Proceedings of the ACM on Programming Languages, 3PP... 2019.
Mloag-Dungg Tran, Sungwoo Choi, Hideki Okamoto, Bardh Hoxha, Georgios Fainekos, and Danil Prokhorov. Quantitative verification for neural networks using probstars. In Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, HSCC '23, New York, NY, USA, 2023. Association for Computing Machinery. ISBN 9798400700330. doi:
10.1145/375870.3587111 12. URL [RLl:ttss://ool 1ttp////...11111111111111 358 7112
Paul Viola and Michael Jones. Rapid object detection using boosted cascade of simple features. In Proceedings of the 2001 IEFE computer society conference on computer vision and pattern recognition. CVPR 2001, volume 1, pp. lee, 2001.
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang. and Suman Jana. Efficient formal safety analysis of neural networks. Advances in neural information processing systems, 31, 201 8a.
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. In 27th USENIX Security Symposium (USENIX Security 18), pp. 1599-1614, 2018b.
Stefan Webb, Tom Rainforth, Yee Whye Teh, and M. Pawan Kumar. Statistical verification of neural networks. International Conference on Learning Representations, 2019. URL https:
7/peeneeieww
Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards fast computation of certified robustness for ReLu networks. In International Conference on Machine Learning, pp. 5276-5285. PMLR, 2018.
Lily Weng, Pun-Yu Chen, Lam Nguyen, Mark Squillante, Akhilan Boopathy, Ivan Oseledets, and Luca Daniel. Proven: Verifying robustness of neural networks with a probabilistic approach. In International Conference on Machine Learning, pp. 6727-6736. PMLR, 2019.
Kaidi Xu, Huan Zhang, Shiqi Wang. Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsich. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. httpstts::///peeeeeee nnt:/forum? dit.nntdndVBBBBBBB. 66N
Greg Yang, Tony Duan, J Edward Hu, Hadi Salman, Ilya Razenshteyn, and Jerry Li. Randomized smoothing of all shapes and sizes. International conference on machine learning, pp. 10693- 10705. PMLR, 2020.
Huan Zhang, Tsui-Wor Weng, Pin- Yu Chen, Cho-Jui Hsich, and Luca Daniel. Efficient neural network robustness certification with general activation functions. Advances in neural information processing systems, 31, 2018.
14

---

Published as a conference paper at ICLR 2026
Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsich, and J. Zico Kolter. General cutting planes for bound-pret poaondd-ooggtion-aaae neural network verification. In NeurIPS, 2022.
Zhong-Qiu Zhao, Peng Zheng, Shou-tao Xu, and Xindong Wu. Object detection with deep learning: A review. IEEE transactions on neural networks and learning systems, 30(11):3212-3232, 2019.
Zhengxia Zou, Keyan Chen, Zhenwei Shi, Yuhong Guo, and Jieping Ye. Object detection in 20 years: survey. Proceedings of the IEEE, 111(3)2557-276 2023.
15

---

Published as a conference paper at ICLR 2026
A APPENDIX
This appendix provides more related work, supplementary discussions, proofs, and experiments to support the main text. We organize the appendix as follows:
Section
B
Summarizes additional related work.
Section
Provides proof Proposition (probabilisti guarantee for part 1).
Section
Explains the role of sample size Part Step and its effect on mmax-
Section E
Gives the proof of Proposition 2
(NMS Soundness Verification).
Section
Proves Lemma (threshold properties).
Section
Proves Lemma (explicit threshold computation formulas).
Section
Defines and estimates the verification bound for object detection and provides proofs
for Lemmas 4
5
Section !
Details the verification procedure for Non-Maximum Suppression, including abstract box construction and IoU bound computation.
Section
J
Proves Theorem (probabilistic guarantee for Part 3).
Section
Proposes strict sound gradient-based refinement algorithm implement Part Three
on small scale networks (Theorem
Section
Provides the proof of Theorem based on dual formulations.
Section
M
Gives proof of Theorem 2
combining probabilistic guarantees across parts.
Section
Reports detailed experimental settings, sample number calculations, and server con-
figuration.
Section
Discusses the efficiency of the NMS verification process.
Section
Shows effectiveness of Part refinement for YOLO CNNs.
Section
Shows verification time comparison between our method and RCP N.
Section
Demonstrates method's effectiveness real-world images.
Section
Compares our method against median smoothing under Gaussian noise.
Section
Presents an ablation study on parameters and
Section
Discusses the broader impact of our verification method.
Section
LLM Usage Statement.
Section W
Lists and explains all hyperparameters used in algorithms.
Section
Provides details how adapt method to other attacks beyond OD.
B ADDITIONAL RELATED WORK
Adversarial attacks. Adversarial methods induce misclassification through imperceptible pertur-
bations. White- box attacks exploit gradient information (Goodfellow et al. [0115] Madry et al. 2018
Carlini & Wagner 2017) and be adapted to OD attacks (Choi & Tian 2022 Li et al.) 2020
Black-box attacks use transferability (Chen & Liu 2024 or query-hased optimization (Li et al.
2020 these are more practical but may be computationally costly. Using adversarial attacks in iso- lation only demonstrates non-robustness if the attack is successful, whereas our method provides rigorous probabilistic certificate of robustness. A network that is robust with high probability under common perturbations (e.g., sensor noise) is acceptable for practical deployment, whereas the strict requirement of complete robustness in a neighborhood often leads significant drop network performance. Thus, our focus is on providing probabilistic robustness under realistic perturbations such as sensor noise rather than adversarial attacks (which often represent worst-case scenarios).
16

---

Published as a conference paper at ICLR 2026
Bound Estimation Methods. There several classical methods for estimating probabilistic out- put bounds of neural networks, including DKW- Waseeseed confidence regions (Massart 1990 Naa-
man 2021,, ERM-based hyper-rectangles, and e-nets (Haussler & Welzi 1987 Blohm al. (025).
While these methods are theoretically robust, their sample complexity typically scales with the out-
put dimension dz (e.g.. ((d2/c) for c-nets). Given the extremely high-dimensional output space of YOLO networks, dimension-dependenn bounds like those from e-nets DKW would be computa- tionally infeasible. We therefore focus on dimension-independent PAC bounds, making estimation feasible even for high-dimensional outputs.
PAC with Attack. There are several PAC verification methods that incorporate adversarial attacks to refine the estimated output bounds (Blohm et al. 2025 ei ct al. 2022 [aluta et al. 2021). For ex- ample, Blohm al. (2025) evaluates the robustness of individual points via a local robustness oracle (such as PGD or LiRPA) and leverages e-net sampling methods to provide high probbbbbbbbiltty statis- tical guarantees for global robustness. Combining attacks with PAC verification is an interesting direction, and we will explore this in future work.
C THE PROOF OF PROPOSITION
I
Proposition (probabilistic guarantee for part 1), For any N₁ > 1, let Omax be a vector with positive components (e.g., as estimated from N₁ samples in Algorithm 2 If computed based
on this Umax using N₂ 2 [2ln(1/0)
4 2lm(2/a) samples as described in Algorithm 2 then a
a
with probability 1 - 3, we have: Pewc (IF(x) F(x(0)) & c1 Umax) 2 1 - a. which implies
Pawe (F(x) E 2) 2 1 a
This proposition can be directly obtained by the classic method RCP N. which is introduced below.
C.I CLASSIC METHOD FOR PROBABILISTIC SAMPLING.
We begin by introducing a well-known result from the RCP method (Campi et al., 2009). which forms the basis of our approach in this section. Consider the following optimization problem with an infinite number of constraints:
min a x + s.L. x E n Xs, wERd
where A is an index set, and X C Rd denotes the constraint set corresponding to the index ó.
Since there are infinitely many constraints, we cannot solve the problem directly. Thus sample the constraints { from A according to a probability distribution Q on A, and consider the sampled problem equation We are interested in quantifying how likely it is that the optimal solution of the sampled problem is (almost) feasible for the original problem.
min a Tax b s.t. a E EN Xx: #ERd
(E(N]
When Xss is convex for every 8 A. we have the following result. If Q is distribution defined on A, and
N 2m + 2d
2d 2dl//2
then, with probability least 3 over the i..d. samples {6,) QN if the optimization problem equation has a unique solution Emin. this solution Emii satisfies
Po~e (Fmin E Xs) 21
classic application of RCPN is to compute a probabiii upper bound of function f(t) over domain A. This can be formulated (i.e., dimension d = 1):
optimization problem with decision variable R
min x
s.t. > f(),, W A.
#EB
17

---

Published as a conference paper at ICLR 2026
By applying the RCPN result with d 1, we know that if we draw N samples {ta) from A according to Q, where
N 2 1
2+ 2l((2/a)
a
then, with probability at least 1 1 3 over the sampling, we have PPr (1(1) & maxi NN f(4)) 2
1
D ANALYSIS OF THE SAMPLE SIZE EFFECT IN PART STEP
In this section, we justify the choice of Umax as presented in Algorithm The main objective is to ensure that the range obtained by Algorithm 2 does not significantly exceed the actual range [[())=<c)
Algorithm 2 guarantees this property under certain assumptions, as detailed in the following propo- sition.
Proposition 3. Let (((())); (F(x(())), N₁ when C, and Us R4 is the minimum value such that P Pm~N.(x I U/) =
a < 0 and B1, B2 satissyy that: Pa aqv,) 31 and PENN S agv,) = $2 any E [dz.).
Let 2, (e1 (maxx) where er and Umax are obtained by algorithm
2 then we have that: S
max,
o jorfor any E [dz] with probability 1 - dr PN
3 d1 + B/ gNa).
Proof. Observe that for any coordinate E [dz]. given the N₁ randomly selected points {xx) from in Algorithm we have:
P aB2; max((r=); af 2 3 -
Applying the union bound, with probability 1 1- 1-dz d1 (g)) - 1) = d1 8 1, the condition abn; 2 max; (Ir)); 2 of holds for all E [dz].
Similarly, for the N₂ points {at}} randomly selected in Algorithm with probability - (1 + 3/ 12 the condition ahv; 2 max; (z(,)= 2 a n holds for all E [dz]-
Consequently, based on the construction in Algorithm 2 if the above events occur, we have c₁ S (ax//a//ai), Therefore, for any j E [dz,], implies:
(c) Um)xm) S max
which completes the proof.
Based on our observations of numerous neural network outputs, we find that the output values are highly likely to be concentrated within specific region. An example provided in Figure 6 Based on this observation, it is possible that di 02 while Bn s 1 and B1 < 1. Consequently, since on a2, we can infer that each dimension of will not extend significantly beyond vi- Furthermore, since B2 x 1 and B1 1, the probability term satisfies:
dr (1 3 3. d (1 + 8N== 32 11
However, in practice, we cannot accurately estimate a and B,. Therefore, the choice of Ni is primarily determined empirically. The proposition above serves to theoretically justify the accuracy of the region Z obtained when N₁ is sufficiently large.
18

---

Published as a conference paper at ICLR 2026
around
100
80
Frequency
60
40
20
0
Value
Figure 6: This picture shows the distribution around sample When we take a₁ 2.33/3.5 and
02 = 2.8/3.5, from this figure, we have that B1 I 0.99 but 32 Thus (a2/as (2/a))ay = 0.97.
Hence, N1 = N₂ = 3000, then - (1 + 8iN. - (.N.) - d1 + B - B) ) 2 0.99 when
dz S 107.
E THE PROOF OF PROPOSITION 2
Proposition (NMS Soundness Verification). For given Z, and bongt. if Q(2, T, boxg)) + 0, then for all k A, there exists box, E [(z²) such that IoU(, bozgt) 2 T and (lass(bor;)) = Class(boxgg0
We first present a lemma.
Lemma 3. For a given E Z, if there is no box; E N(z) that satisfies loU(box, bexre)) T and Class (ox;; Class(bburgg) then:
For any boz; E z with C 2 4, Class(bor,) = Class(borgg)) and (bU(,, boxg:) ) 2 T, there exists another boz, z such that ej 2 Class(bor,) Class (boz;), c cy. Loli boxrgt T, and (box; box,)) 2
Proof. Assume that there exists bor, 2 with C; 2 4, Class(box:) Class(bozgi) and loU(b bozg)) 2 r. By the assumption of the lemma, it implies that box; & N(z).
According to non-maximum suppression condition (n2) in Section 3.1 there must exist a box, N(z) such that ToU(box; box,)) 17, G S Cy. and Class(borr;) = Class = Class(bor)g)) By condition (nl) in Section 3.1 box, E N(z) implies that Cj 2
However, by the assumptions, there is no box, N(z) that satisfies Class(bor,,) = Class(boz,)) and (bu boxrg)) 2 т. Since we have shown that Class(boz,) Class(bougg)) above, follows that TbU(r,, boxgs) < r. This completes the proof.
Using this lemma, we can directly prove Proposition
2
Proof. Assume that Q(Z, r, boxggt) # but for some A, the stated result does not hold.
Based on condition (1) of the definition of Q(2, b,borg:), let E Q(2, r, boxg:)). Then, based on Lemma we know that there exists another boo E z² such that of 2 Class(bor))) = Class bowt of S ct. LoU boxgt) < r, and lbU book)) 1). This contradicts condition (2) of the definition of Q(Z, r, boog).
Thus, the assumption leads to a contradiction, and the result follows.
19

---

Published as a conference paper at ICLR 2026
F
THE PROOF OF LEMMA 1
Lemma (Threshold Properties). т < T(i, 2, boxgg:) )= = i Q(2, boxgge)
Proof. First, we demonstrate that for any >'> T, the inclusion Q boxgt) ) C 22 boxxt)
holds. Indeed, if an index i satisfies Condition (1) in Definition 2 with threshold T', it neces- sarily satisfies Condition (1) with any lower threshold т < T'. assuming the input constraints and ground truth remain unchanged. A similar argument applies to Condition (2) in Definition 2 This establishes the monotonicity result.
Now, suppose for the sake of contradiction that < r(i, Z, boxgt) and i & Q r, boxg). By the monotonicity established above, this implies that i E Q(2, r', boxg) ) for any r' > т. According to the definition of T(è, 2, boxg)), this entails hypothesis that < T(i, 2, boxgt). Thus, the assumption leads to contradiction, which completes the proof.
7(i, 2, boxgt), which contradicts the initial
G THE PROOF OF LEMMA 2
Lemma (Threshold Computation).
The threshold can be calculated as T(i, Z, boxgt) = muin(ri(d 2, boxgg), T2 Z, boxg))) where:
Ti (i, Z, boorgg)) = min IoU (box, boorg)) Class((box)? = I(c 2 1), q Class(boxgg)) KEA
min KEA.
loU(box boxgi)
( n) s.t. Ckn =
(2 2, boxtgt))
otherwise
where constraint Cun I1c 2 1) [(Cllass(boxt) = q) [IlloU(boz,, boo 2 1)) 1(c ct)
Proof. We prove the equality by showing both directions of the inequality.
Part 1: Proof of r(i, 2, boxxx) S 721,
Observe that if x' > Ti (V, 2, boxg:), index is not contained in the safe set Q(2, (',,"' boxgr) because
it violates Condition (1) in Definition 2 Similarly, if 7' (1, 2, boxgt). index excluded
from the safe set Q(2, rr, boxg.) because it violates Condition (2), even if Condition (1) is satisfied. Consequently, the threshold must satisfy:
r(i, Z, boxgt) S min(Ti Z, boxg),, 12(1, Z, boxg))}
Part 2: Proof of 7(1, 2, ) 2 min(r1.
Note that when 7' Ti (i, 2, boxg)), index must satisfy Condition (1) in Definition Likewise, when r' < T2 Z, boxg)). index must satisfy Condition (2). Therefore, if we choose a threshold min (i, Z, boxgt), r2 2, boxg))). index i satisfies both conditions, which implies i Q22,7, r, b. By the definition of the threshold T(i, 2, boxg)). ), this implies:
Ti, 2, boxg:) 2 min(71 (i, 2, boxg:), (2 2, boxg))).
Combining the results from Part and Part 2, the equality holds.
H COMPUTING THE VERIFICATION BOUND
In this section, we show how to Calculate the verification bound for NMS.
We first define the verification bounds:
Definition 4 (OD Verification Bound). For constraints and box define:
min #EC
max IoU(bor, bozg)) - [(Class(bor;)) Class(booxg:) (x))
the OD verification bound. This quantifies robustness against OD attacks.
20

---

Published as a conference paper at ICLR 2026
We need to estimate the verification bound min maX (bor,, box gt Class(boz)) Class borg:)) )) under output over-approximation region 2 and ground truth boxgt, according to def- inition
To estimate such bound, we first need the following lemma: Lemma 4. For any T, bougg, there is:
min max [bu(, boxgg)I(((laaa (IIaIIIICCssbii = Class(borgg)) 2 =I(1)Q(2,T, boxge)) 2 1})
ZEZ (Nz,)((=)
So try find the maximum such that Q(2, boetgt)) O, but this maximum may exist in some cases (it may only be approached arbitrarily), so we consider the following value instead:
min 0
T s.t. IQ(2,T', bozggt = O, V12T>T
(5)
We use the following lemma to calculate such minimum value: Lemma 5. The solution of problem 5 is equal to: maX4e[na] T (i,, 2, boorg))
Using this lemma, we only need to calculate 7(1, 2, boxgs) as described above, and then we can estimate the verification bound.
H.1 THE PROOF OF LEMMA 4
Proof. By Proposition 2 if Q(2, boxgt) 2 1, then for any 2 E Z, there exists box, E N(2) and (loxs) Class(boxg)) This implies that the value of
such that LoU(, boxgt) min 2 maXpox. (N Io Ubo(, boxgt) I(Class(box,) = Class(box.:)) greater than or equal to 7, which yields the desired result.
H.2 THE PROOF OF LEMMA 5
Proof. We have shown that when 7' > T, we have Q(Z,'', boxg:) C Q(Z, boxgt) ) in Lemma
By the definition of T (i,, Z, boorg)) and above result, we know that the safe set Q T', boxrg) is for at most max r(i, 2, boxg)).
any 7' > max;c[==] [(,, 2, boxgg)) so the solution of problem 5
If r is the solution of problem then for any E [n=)]. there must be Q(2, ('o.gg) for any 7' > so 2 max;e(ma] (i,, 2, boxggt).
This completes the proof of the lemma.
I VERIFICATION PROCESS OF NMS
To illustrate Non- Mon-Maximum Suppression (NMS) verification, define constraints as H. S. Here, H. constrains the neural network output y. and S constrains bounding box parameters. This formulation equivalent to the original. A 5 details the NMS verification process.
Next we show how construct the abstract box box and how calculate the lower and upper bounds of IoU.
Let B be the 'box space' (space of individual box structures). An interpretation function G RRd {S C B S] ne) } maps y to a set {bozz)?" of nw bounding boxes, where ng is a constant determined by the fixed input dimension. A function S - P([1.... dr}) (where P is the power set) maps each distinct boor, E BB (that could form part of an output set) to its source indices y. We then define the regular region& as follows:
Definition (Regular Region). A regular region is a subset C RR defined as Z = H'S. S, where:
H. is an axis-aligned hyperrectangle centered at F(x:(0)) with component-wise perturbations bounded by Ci Umaxi
H { (((x + +EER" Rd. VVj fl,...,,h leal S (cI (Cmmmaa)))))
21

---

Published as a conference paper at ICLR 2026
Algorithm 5 Sound Object-Disappearance Threat Verification for NMS
Require: Constraints Z 7. S; ground truth bozgti confidence threshold IoU threshold IoU
suppression threshold f)-
Ensure: Calculate T1 -2-
1: B Beand Bother < 0.0
2: {boz; | Uh
[= CONSTRUCT_ABSTRACTI
3: for all box; E {bor, 1== do
4: Ti (i) < 0, 72 -
5:
if 7k E [Mras] (Class(bexrg)) Pt, Clasa(bougs)
S 2. then
6:
continue
> Skip boxes that cannot match boxge class
7:
end
8:
if 2 then
b Ensure indicator I(e: 2 t)
9:
(i) WWW.LLOEERRBUUUEE
boxrgt) if v E [ncal \\ [Class(bozgl H. La Classss(bo)
10:
2 Pi. then
11:
Bannd Beand {boz,
Box must match boxigg class
12:
else
13:
end Bother t Bother [bor,
Box may match borgtt class
14:
end if
16: end for
for all box, E Brand do
for all box, E Bother do
19: if cj < C; then
b Ensure box, may suppress box;
continue
b Skip boxes that cannot suppress bor;
21:
end if
22:
ub +- WWW__UPPE.BUUUUDE
box
23:
if ub 2 17 then
Ensure box; may be suppressed by boxy
24:
1b lOU LOWER BouNDs bourgt)
25:
(1) min(r2(1),
26: end
end for
28:
end for
return (r20))(00)))))))))
S is union of & hyperspherical zones. Each zone S; B(c,, d,) is defined by center e; and radius d,, where is the center of the exclusion zone and d; is the radius. The union of these zones is given by:
U i=1
B(e, d),, B(c, d.) { Rd 11
cil3 s df
i=1
Note, sometimes we just need part dimension of S,. Thus we can extend B to B(c;, di, Ix), where I is the index set of dimensions in S:- Then have:
B(c,, di I,) {y dd
|1yT, - c; df
where C,I,, is the component of c; for index set Iz,
I.1 ABSTRACT BOUNDING Box CONSTRUCTION AND IOU BOUND COMPUTATION
We use to represent that a Gurobi variable, i to represent real number Gurobi variable space. Let ý d be the Gurobi variable vector.
Then encode the regular region Z as set of constraints. To encode H. need to ob- tain the lower and upper bounds of each parameter of each bounding box. Suppose H (F(x(")) + Ed VAj (I....,dr.), leyl S (c)umax) }. where e₁ and Umax (Note Umax 0)
22

---

Published as a conference paper at ICLR 2026
obtained from Part 1. Let = F(x!")) + maa and y F(x(")) C1 Umax- Then add the
following constraints to the Gurobi model:
Here, is the component-wise less than equal to operator.
Next, we need to add the exclusion zone constraints. For each exclusion zone Si, we need to add the following constraints:
Σ (
JET
where (c:) the component of G; for index j.
CONSTRUCT BASSTRUCTABSTRACTT.E ( adds these constraints to the Gurobi model, then reorganizes ÿ as an abstract bounding box set {box; 1 where fz is the number of bounding boxes. Each bounding box boz, = (T,, it, W; his o, {Pi.) (P.)))=): where nels is the number of classes. Note all the parameters of box; are from ý thus have constraints on them.
IoU bounds for abstract boxes involve:
Geometric Constraints: Box i coordinates are:
5; W/ Fmax
min Tj J max
hi
hi 2
Pmin Ui 2
01 +
2. Intersection/Union Area
L = ma min(F mmax F(max) max (# minn Fmmnn) )),
In max(0, min( (Fmaxx Fmax) max Fminn), )),
Ant Tw Tb.
Aunion = ( Fiiin) (Fmax Fmin)) + (# x ( (D
Aint-
We use big-M constraints to encode max(0,-) -) and min(.s-) operations in Gurobi. For example, to encode Aexpr max(0, E), where E is an expression, we introduce an auxiliary binary variable b E {0, 1} and sufficiently large constant M. The variable Auxpe is then constrained by:
Aexppr 2 E
Aexpr 2 0
Aexpr E + M b
Aexpr S M (1 b)
where Āexpr a Gurobi variable representing the maximum. The inner terms of Iw and In, such as min( F(ax)) are handled similarly using appropriate big-M formulations Gurobi's built-in functions. The constant must be chosen such that M 2 max(Ur. - LL), where Up and L are known upper and lower bounds for the expression E.
If E 2 O, the objective of minimizing Ams (or other constraints) will force = 0. The constraints become Amt 2 E, Amt 2 0, Aut & E, and Aus I M. This correctly sets Am = E.
If < 0, the objective will force 1. The constraints become Ame 2 E, Aus 2 0.
Amt I M, and Am < 0. This correctly sets Ams 0.
3. Binary Search for loU bounds: To find IoU (lower bound of loU):
1: < 0, Tub + 1, Csearh f- 10
2: while (Tub Tial Ceearch do
23

---

Published as a conference paper at ICLR 2026
3: Tmid f- (Ti /2
4: Solve Leheck = min (Aint Auiio)) by Gurobi
5: if' Leheck 2 0 then Tis Tmid
6: elseT < Tmid
7: end if
8: end while
9: return 726
Checking loU bounds against value r is often done via optimizing Aint -int-TAh Aunion as direct interval ratio optimization Aint/ A Aunion is complex for solvers (e.g.. Gurobi) without reformulation. For instance, to check if (boz,, bozgt) 2 T is possible, one can check if max(Ain - Aunioon) 2 0.
It is straightforward to extend the above algorithm to find Tub (the upper bound of IoU).
The Gurobi solver, when minimizing or maximizing an objective subject to these constraints, returns an assignment for ý (which corresponds to specific point 2). If a particular optimization (e.g., a step in the binary search showing Leheck < 0) demonstrates a property violation, the returned ÿ is the concrete instance that exhibits this violation.
J THE PROOF OF THEOREM 1
Theorem (probabilistic guarantee for Part 3). Consider Algorithm 4 Here N is the number of outer samples {x(()) in Step One, M is the number of samples (a(0-)) I drawn for each ( and M2 the number of samples used in Step Two.
For any a. B, e (0, 1) satisfying
and N ((1 26)M) > à In( with Alg. 4 for any y.
with probability at least
2(11 - -) 3) over steps one and two, we have V(y, dmin) S a.
Proof. For any given o' F(x'), ) let Ay satisfy that ( 1lll2 A.)) = let By satisfy that IP FF - y' 2 By) = Let Sy A B.
By
For convenience, we denote Step in Algorithm 4 by P1, and Step 2 by P2.
Part One: For any with probability (1 2 of Pl, we have [[(((+)) F(ol00)22
[Be (yy) for all j E [M]
Based on the definition of BF(a()) and AF(=()), know that:
P P (I ((((tt))) - F(x I|| E [Br(at)), AF()))))) 2 - 2
(6)
by union bound. Because each selection of (1.)) independent, we have:
P(Vj E [M], (F((())))))) - (1) E [Bp( AF(a(1))) 2 (1 (1-26)
Part Two: With probability 1 1- of P1, have P Pn-c(SP(e)) SC)
Firstly, if E [N] such that ([F(x((.)) 1 F(x [Br( AF(aU))) for all E [M], then there must be:
B
C A B
> Sp(a(o).
(8)
Here, B = minje[M] (())) F F(x (z)) )| and A = maxje M / (((()()))) - ((x(
Let p satisfy that (SF())) $ p) 1 a, then we have P ( 2 p) 2a.
Then, we define the witness event W; as: W. = (St(w()) 2 p} n (((F(()(())) F(x(1))l2 E [Br(a()), Ap(a(t))) for all j E [M]]
24

---

Published as a conference paper at ICLR 2026
Using equation
we have that:
P(W.) = E 1s p(o(t)) 2P P(IIF(x( )(x [B(at()) Ap(atty) for all j E [M] x0(1))
2 1B 1 (()( (1), 2p (1 22)
a (1 2c)
(9)
Since each sample (1) is independent, thus each event W; is independent, then we have that:
P(Vi [M] W; does not occur) (1 (1 (1- 2c) M <e-0-(1- (1-)
(10)
From the theorem's 's sample-size condition, condiitonnnonniiio we have N-((1-2c)M) M) > 2/4 In( () hence ((112c)
In( ( so a
a. (1 22) 2c) N > In (3) e-11(1_ < 3.
This means that with probability least 1- 3, there exists such that W3 occurs, which means we have [[F(x(()))) F(a E [Br( ( for all [M] and Sp(n(0) 2 p. Fix such an index i, from equation 8 we have
B
B
Bp(a(9)
C = max NEIN
2
2 SF(2 =
2 p.
A
BB
A
B
Ar(1()) BF(a(9)
So, with probability at least B, we obtain C 2 p. according to the definition of we have:
Parc(Sr(z) S C) 2 P (Sp(z)) p) = =
(11)
Part Three: For any y, with probability at least have V(y, dmiin) S a.
3- c) Md over steps one and two,
Let Q {x E C. SF(w) S p). By the definition of p. have Pawe Q) 2 1
Consider the M2 i..dd samples {M M2 ~ C in Step Two of the algorithm. Fix any x' E Q, by the definition of BF(w)) and AF(="), we have ((F(<(((F((()"))) - F(x')l12 I BF(m)) 2 so the probability that none of the M2 samples satisfies this is at most (1 c)M², Similarly, each draw satisfies IP mmlF - F(x')ll2 2 AF(w)) 2 e, so the probability that none satisfies it is at most (1 M2, By union bound, with probability at least 1 - 2(1 M), there exist:
B(x') min [|F(x') - F(x - Br(ay):
(12)
Á(x') max [IF(x') - F(x 2 AF(w)) ve[Ma]
Then for a given y, let
(4) = arg min | - F(x)ll2, t= lly (
(13)
=EQ
Then, we have Am = maxie[Ma] lv (( 2 maxie|Ma ([(()()) F(x
- |1y F(x( = A(x(1) f, similar, we have Bn < ((x(v)) +t. So, we have Bn, C(Am Bm) S
B(x(() - ((A(x(1)) - B(x())) + f(1 + 2C).
As shown in the Part Two, with probability - 8 of Pl, there C 2 p. and then, using ( E Q. we have (Bz(((((()) C (A(x(()) (1) - B ()) < 0) > 1 2(1 - M2 which can imply that Prz(B Bm CC(Am B.n) (11 20)) 2 1 2(1
Ma by the above result.
And when Bnn C(Am Bm) S ((1 +1+12 2C') holds, we have 2 max(
B., C(A. B..). 0) dmin- (1+20)
Because (2) is an open ball, hence B, (y. dmna) n F( = ( by the definition of t, which implies that:
V(y, dmin) Pawc (xx) E B2(y, dmin)) S Pa P & Q) S
(14)
25

---

Published as a conference paper at ICLR 2026
Putting probabilities together. From equation I1 we have 1 - percent of z C such that SF()) C. For fixed x/9) chosen above, the algorithm succeeds with probability at least 1
2(1 M2, A union bound gives
P(V(y. dmii) S sa) 2 2(1 c)Ma
This completes the proof.
K PART THREE FOR SMALL NETWORKS
To demonstrate the superiority of our method in Section 4 and compare it with existing approaches, we show how we can apply Part Three on scall-scale object detection based on the forwafo ReLU neural networks. In this case, the problem in Part Three can be formulated as follows:
ming. y x (111/2
s.t. ii a C, x(0) = x;;
(ii) x( - bb(,, ie [L] 200 max (0, (0,)()), i [L 1]
Where W is the weight matrix of i-th layer in network, ((6) is the bias vector of i-th layer in network. Unfortunately, finding an exact solution to this problem NP-complete(Katte
al. 2017). (/9) - 2 S _; -Based on these bounds,
So, we consider bounds on the outputs of hidden-layers:
let (-) = {j 2 s 0}, (+) = (j 1 0} and Z- = :i: < u }. the
(1) J
condition (iii) can be replaced by the following constraints: // 2 0,
0,4 (0)
2 22, (u,
19) S
(i) I- ==,0 = - E I (0 = 0, j E I-()) To solve this problem, we prove that such minimum value is equal to the maximum value of the square root of d(a v) which is defined the following theorem. So, we can use the gradient estimate the maximum of d(a, v), and use it to be the minimum distance in the part three.
(2) (6) 1 3
uj 2j
Theorem 3. Under the setting in this section, we have that:
min #EC
[[((x) y112 max Vdla,v) aE(0,11
which is defined as below:
DLL)T D(L) -1 (LDTw(1)44)) + [ (
d(a.v) v) -y -T (L)
1-1
(1 1
(15)
(()) +
u (2) (0)
jE
where
1/00
(+11) W ( (i+1)
-(00 = 10/01 - -b ViE -1,
(1)
1)E+(()
0
-
Wi (1,,,.....L
(0 - 10
( EII4()
L THE PROOF OF THEOREM 3
We mainly follow the proof idea in Kotha et al. 2023).
26

---

Published as a conference paper at ICLR 2026
Proof. Consider the I- [i: : uj < 03. I+(0
03..
:;:19 00 and I+ -i:15 <0<
(i) nj ], such optimization problem tends the:
min (a (4) y) (x (z) y)
1 100) S (0
x = W (1-1)) +b" (1,,2,, D}
2/ 2 0: jE I+(1))
(16)
8) 2 rj jE I
(1)
(u) 10 19)
(1)
(1) (8)
(0) 10
(0)
8) = -,
Then we use the Lagrange dual of the optimization problem to solve the Lagrange dual of the optimization problem is given by:
(x) - -y) T (2x yy)
min max 2. A.p.T.
D()T (a (6 b(0)
(-
jEI+()
(a
(17)
5EI+G)
Σ Σ
jEZ
( < (0) S "))
s.t.
8/00 0, I (0, 10 - -.j
(1)
(
# #20 12:0200 A20;
27

---

Published as a conference paper at ICLR 2026
According to its strong duality, the solution of the dual problem is the same as that of the primal problem. The dual problem is given by:
max min (x!44) 2y + Ell1) T 111 + yo (v w()))(00)
(1)) D w
jEI+())
(1) (1) 2j
JEI-
(
(0
1n (1) (
1 zj
(18)
JEIZ())
+(
w
(6-1)
(
( + (u)
- 1 )0
L-1
Σ DOT 6(0)
Σ
Σ
1 10
i= JCT+())
( v 2 (0) < u (0); (1)
5j = 0, J.j =, 1 = -af.jer
s.t.
0; 0; X 0;
Here, we adjust the order of each term in the formula and directly incorporate the constraints a/0 0,j E =0 = (1)
jj I+() into the objective function. Then can minimize
-(DU)) T (() subject to [0) - (0)) S (0))) according to the each dimension of (1)) If (2(IT) w(), > 0, then $)0)) ,, Otherwise, 2000) 110) Since no additional constraints
(0)
applied to (T)), we can minimize (x 2y + v(1)) (1.) by setting x!!)_ = 2 ( Then we get:
max min y TT()) u(L)T(()) A, 2,
(WOT (0 + (((0) w('))
4
Σ (v/00)
((+l)
w
jEI+()
Σ
JEI-() (1)
(19)
(0) (1
--- - 100 210
(6)
((11
(i+1))
(
19
11
1--1
Σ BOT
Σ
1
s.t.
M 0, T
0;
X2 0;
Since variables x, are unconstrained, any nonzero coefficients would drive their values to -o- in the inner minimization. Therefore, the outer maximization requires setting all coefficients of az / to zero. Then we get:
28

---

Published as a conference paper at ICLR 2026
y v vlLT vlL)
max M.
- [2(1) )220) + [p w()
1-1
LOOTT (00) + Σ Σ 1
JEI+())
(20)
s.L.
# # 0: 0,120 0;
1 D (HI W (641)
0, E I
11 ( E
o0 + +T) ( - -100 (0) 0 II
D6tH W (+11) = (u) 1 1/) - - -11) +,,")) E I+(
Define D/0) (++1T w (141) Then, we define (u ( 1290 =1o/0 and p1 =1000|
we get the following bound propagation procedure:
v(I)T(())
max y v
(U)
w (0) + ( 1
1
1-1
5j 1 10
Σ
(T b
+
"/ -700
==1
1= jEI
s.t.
5 ((-1) w(+
(++1) o000)
= -100
10,0
{1,2, ..., ..,, L L-13
(21)
E (1, --1
+ aa 10/00
, =
5 /
1, E ++0
(4) Here a is the optimizable parameter controlling the relaxation of neuron j in layer i introduced in Xu al. 2021). This completes the proof.
M THE PROOF OF THEOREM 2
4 Given a, B, E (0, 1) satisfy- ing c < N (()- > 1 In( 3) and N₂ 2 22l +2+ In(2/a) Then, after executing the algorithms defined above, for any k used in Algorithm 7 if these algorithms oulput "Safe" after at most T refinement iterations, then with probability at least - T(3 + 2(1 <) M2) 3
Theorem. Using the notation and definitions from Algorithms
over Algorithm (Part 1) and Algorithm (Part 3), we have P Pa~c(# is safe) 1 (1 T)a.
Proof. We use the simple fact that (PA n B) Z P(A) + - to obtain the following result:
From Theorem 1 after T refinement steps, the reduction in the probability of the system being certifiably safe due to these refinements at most Ta. This statement holds with a confidence of at least T (1 - (3 + 2(1 e) (T 1) 1 T (3 + 2(1 M2).
According to Proposition I. we obtain that the probability of the box being safe is 1 - Ta - a with
probability 1 - [ 2(I M2) (1 3) 1 = T(3 2(1 e) Ma) 3.
Then we obtain (2 safe) > 1 - (1 + T with probability - T 2(1 -) M2) B.
This yields the final result.
29

---

Published as a conference paper at ICLR 2026
Remark 6. Note we do not assume that Part I and Part 3 are independent, reuse the samples in Part 1 to Part
N EXPERIMENT DETAILS
Detailed Setting: We use N1 30000, N₂ 5000, N 3000, M 10, M2 2000, 0.0099, = 0.0099 and 1/200 as our default setting. As we do not assume that Part and Part 3 are independent, samples from Part (Algorithm 2 can also be used in Part (Algorithm{)) so we only need to sample N1 + 22 + M2 = 37000 samples in total (Nı N2 can cover the sample number N N. M). We use one refinement turn (T 1) for experiments.
Attack Setting: We use the square attack with 5000 iterations for each box. For PGD, we use 20 iterations with step sizes 1/255 and 2/255. In each iteration, we find the box with the highest loU and the same class as the ground-truth box, then use its GloU as the loss function. Each step may attack a different box. We find this to be strong attack for YOLO networks.
Server Setting: We use a server with 8 NVIDIA V100 32G GPUs, 40 Intel(R) Xeon(R) Gold 5215 CPUs at 2.50GHz and 503GB memory. The code is implemented in Python with Gurobi and PyTorch.
Sample Calculation: According to Theorem 2 the sample number N1 + N2 + M2 = 37, 000 for each box. Note that this is the sample number of the full algorithm.
Our work (Part 1) aims to find a tight becea-rectangle bound Z for the d, dimmensnio vector output space {F(x)] In this context, more appropriate application of RCPN a baseline for this task would be to directly estimate an upper bound for each dimension in this d, di-dimensio space. The Recision-variable dimension for this problem would be d = d2 (i.e., the network output dimension), corresponding to finding a vector u E Rdd such that, for all inputs æ E C, the network output F(x) element-wise. Based this, the required sample count would be:
N 22l(1133 + 2d,, + 2d,. In(2/ar)
R 10
Alternatively, if one were to use the RCPx method to directly verify the entire problem, this could be framed as computing an loU lower bound for each predicted box against its corre- sponding ground-truth (GT) box. The decision variable dimension in this case would be d (80 x 80 + 40 x 40 + 20 x 20) x 3 = 25, 200 (i.c., the number of bounding boxes). Based on this, the required sample count would be:
2m1(1/3)
2d/n(2/a) zs 10
+2d
a
The order of magnitude of the sample size under either estimation is still prohibitively large for any practical application.
For the PAC-based methods, according to Li et al. 2022). to achieve - probability with - confidence, we need that N satisfies:
N
log do 122880391.
Here also 0.02, 0.02.
In terms randomized smoothing (Chnen et al. 2019). the number of samples required is strongly correlated with the standard deviation (a) and the certified radius. For example, certify radius of 2/255 against noise with a standard deviation of a 255x3 the randomized smoothing method would require impractical number of samples (approximately 3.9 x 109). This severely limits its application in real-world scenarios.
Our method, by introducing Vmax and the scalar C1 reduces the entire verification problem to d scalar optimization (for ej) plus constrained optimization (MIQCP). Thus the required sample size significantly reduced manageable level, making it feasible for practical applications.
30

---

Published as a conference paper at ICLR 2026
Table 3: Ground Truth Information for Table
#RB: Number of robust boxes; #NRB: Number of
non-robust boxes
Model
#RB (T 0.5)
#NRB(T = 0.5)
#RB (T = 0.7)
#NRB(T 0.7)
yolollm
363
164
335
192
255
yolollm
346
181
315
212
255
yolollx
390
137
348
179
255
yolo11x
379
148
335
192
2/5
yolov3-sppu
364
163
332
195
255
yolov3-sppu
356
171
320
207
255
yolov3u
374
153
338
189
2
yolov3u
365
162
327
200
265
yolov5mu
354
173
316
211
255
yolov5mu
344
183
301
226
21
yolovSxu
387
140
354
173
255
yolov5xu
372
155
337
190
255
yolov8m
376
151
342
185
255
yolov8m
361
166
327
200
yolov8x 2G5
385
142
348
179
255
yolov8x 255
370
157
337
190
Remark 7. Note that without refinement (only Part and Part 2), our method can achieve 99% confidence and 99% probability with a 0.0099, 3 = 0.0099. After refinement, the true confidence and probability are both 98%. For the other methods, we use an error rale of 0.02 and significance level of 0.02 to obtain the same confidence and probability.
Clarification on Sample Complexity There are two distinct sampling procedures used in our ex- periments, which serve different purposes:
Verification Samples (37,000): This is the sample budget used by our algorithm to issue the 37,00 37,000 samples (N₃ N₂ + M2) to construct Z
certificate. For each ground truth box, and the refinement constant C, as prescribed by Theorem
For the RCP baseline Table 1, we also use 10 samples to compute empirical robustness, but this does not yield comparable theoretical guaran- tees. To achieve our target (98% robustness, 98% confidence). RCP, x would theoretically require about 11.6 million samples. With only 10 samples, RCP can only provide 86% robustness guarantee at 98% confidence.
RCP N Baseline Samples (10% in Table I
Evaluation Samples (106 Table Independently the verification algorithm, we draw 106 additional uniform perturbations to empirically estimate the "ground truth" robustness. These samples are only used to calculate evaluation metrics (TPR, FPR, TNR, FNR, and CRA) and do not inform the certificate itself.
Ground Truth information of Table 2 Table shows the ground truth information Table Here, #RB means the number of robust boxes, and #NRB means the number of non-robust boxes. The ground truth is calculated by 10 uniform perturbations for each box.
O THE EFFICIENCY OF NMS VERIFICATION
The NMS optimization step is highly efficient. Verifying one ground truth box against all candidate boxes takes average of only 4.9 seconds. This efficiency arises because only perform sound verification: boxes that could potentially cause unsafe hehavior are filtered out advance, leaving only small number of boxes be verified.
31

---

Published as a conference paper at ICLR 2026
Lowas Boand Improvements
Boad
Prequeney
100-
100
10:
10
1.8
0.00
0.02
0.04
0.06
0.08
0.10
0.12
0.00 0.02 0.04 0.06 0.68 0.10 0.12 0.14
Lower bound improves
Lower bound improves
Ineage Number
(a) Improvements
(b) Improvements with &
(c)
Improvements in CNNS (Cohen
255
al. 2024
Figure 7: Verification bound improvement after Part 3
Ground Truth
Iol:: 0.3975
Tol: 0.4777
Image 378
(b) Image 397
Figure 8: The effect of Part 3 in small object detection. The middle panel shows the bound from prior methods; the right panel shows our improved bound.
P THE EFFECT OF PART 3
This section shows that Part in Section 4 and Appendix Kiss effective for both large-scale networks (YOLO) and small-scale CNNs. For the LARD dataset, we use a six-layer CNN network provided in (Cohen al. 2024). As seen in Figure 7c with Part 3, the IoU lower bound obtain is higher than the bound obtained without using Part 3. This improvement occurs because Part 3 reduces the over-approximation of the network's output, implying that we use sound formal verification on small object detection, instead of probabilistic verification, that the network can indeed achieve such bound. For YOLO, we also show the effect of Part in Fig. 7 and Fig. [7b After refinement, most of the lower bounds are improved, which means Part is also helpful in YOLO networks.
bound is closer to the true bound. Note
We observe that the first iteration yields the most significant gains. Since further refinement linearly accumulates confidence loss as described in Theorem 2, employing T 1 represents favorable trade-off in most cases.
TIME COMPARISON
Fig. shows the detailed time comparison of our method and RCP different YOLO models with 255 and e 255
The results show that our method significantly faster than RCP, N in
all images.
R REAL-WORLD EXAMPLES
We take 40 images from sensors our autonomous vehicles and annotate the ground truth manually. Table 4 shows the results of our method on these images. The results show that our method also works well in real-world scenarios. Our method still uses less time and achieves better bounds than RCP N. CRA high on these images, which means most boxes verified as robust by our method indeed robust.
32

---

Published as a conference paper at ICLR 2026
19255
740
340
270
Figure 9; Verification time comparison
Table 4: Real-world examples of our method.
APGD
CRA
model
method
time
== 0.5
= 0.7
== 0.5
7 0.7
RCP ODPV
571.0
0.53
0.52
1.00
1.00
1/(3 255)
32.1
0.47
0.44
1.00
1.00
yolol
RCP N ODPV
569.6 32.1
0.57
0.55
1.00
1.00
2/(3 * 255)
0.43
0.37
1.00
1.00
COMPARED WITH MEDIAN SMOOTHING
Table compares our method with median smoothing (MS) (Chiang et al.] 2020) under normal distribution on 50 images from the COCO dataset. We set the standard deviation as 255x3 and
255x3' The results show that our method achieves smaller mean absolute difference of IoU lower bounds relative to the worst-case input found by the PGD attack (APGD). indicating more precise loU lower bounds. most cases, the CRA of our method is higher than that of median smoothing. This also proves that our method works well across different distributions.
ABLATION STUDY OF PARAMETERS
Fig. shows the ablation study of parameters 7) and c. The results show that our method maintains more accurate bounds than RCPN n under different parameters.
U BROADER IMPACT
Our method focuses on verifying the safety of the object detection model, which may help people better understand the model and give safety metric. We do not think there is negative social impact of our method as our method is not used to attack the model.
V LLM USAGE STATEMENT
In the preparation of this manuscript, a Large Language Model (LLM) was utilized as writing assistance tool. use was strictly confined to language polishing, which includes proofreading for grammatical errors, improving sentence structure, and enhancing the overall clarity and readability of the text.
All core intellectual contributions the research ideation, paper structure, and the initial drafting of the content-are the original work of authors. The LLM not contribute to formulation of any hypotheses, experimental results, or conclusions presented herein. The authors have reviewed all Al-generated suggestions and take full responsibility for the final content this paper.
33

---

Published as a conference paper at ICLR 2026
Table 5: Comparison of our method with median smoothing. ÂPGD denotes the mean absolute dif- ference of IoU lower bounds relative to the PGD attack. Bold values indicate the best performance.
PGGD
CRA
model
method
0.5
0.7
0.5
0.7
RCP N
0.45
0.47
1.00
1.00
1/255
ODPV
0.42
0.40
0.99
0.98
MS
0.44
0.45
0.99
0.98
yololIx
RCPw N
0.59
0.56
1.00
1.00
2/255
ODPV
0.54
0.47
1.00
1.00
MS
0.59
0.53
0.96
0.97
RCTy-AAu (5)0
02N (0ur)) Anco frm00.5
oo Trenddt
0-465
11:90
11:7766
0.115
0.122
0.104
9.25
-3.2
-G20
0.321
0.377
1.599
0.087
0.081
0,065
0.2
8:45
NCNy-fese
0.45
CAC
0.473
0.472
0.472
3
0.105
0.105
0,105
0.40
-33
Contere Th Trando
Coffern
0.101
11361
03376
0.08K
0,081
0.065
Figure 10: Ablation study parameters 17,
W DESCRIPTION OF HYPERPARAMETERS
Our framework consists of three parts, implemented by Algorithms 1 Part (Output Approxi- mation). Part 2 (NMS Verification), and Part 3 (Counterexample- Based Refinement). Only Parts and 3 are probabilistic; Part 2 is based on sound MIQCP constraints and introduces no additional probabilistic error.
W.I ROLE OF PARAMETERS AND FAILURE EVENTS
We now describe the role of the three key parameters a, 3, used in theoretical guarantees and experiments.
(Error Rate)
Appears in Definition (OD PAC- PAC-ffrifiaation) Proposition (Part 1), Theorem | (Part 3),
and Theorem (Overal Guarantee).
34

---

Published as a conference paper at ICLR 2026
Controls the allowable violation probability of the OD property under the imput distribution: Theorem if the algorithm returns "safe" after at most refinement steps, we guarantee
P Pa (a safe) > (1 7)
our experiments, we set a 0.0099, so with we obtain a lower bound on the safety probability for each certified box of approximately 1 0.0198 se 0.98.
3 (Significance Confidence)
Used for the scenario-type bounds in Part (Prop. and Part 3 (Thm. and combined in Theorem
Controls the confidence with which the above probabilistic claim holds, i.c., the probability that the incquality regarding P(w is safe) is valid under the randomness of our sampling process. Theorem gives the overall confidence:
P (( is safe) > 1 (1 ()+ 2 1 2(1 c)) B.
We B 0.0099; with our default N, M2, and T 1, this lower bound is 0.98 (reported in Appendix ND.
e (width of the local uncertainty interval in Part 3)
Used Theorem to define the probability mass of the local distance interval [Br(=)- AF(w))- For each æ, at least
2e fraction of the M local perturbations fall into this interval. The term 2(1 e) Ma in Theorem bounds the probability that the empirical estimation of this interval fails.
We set 1/200 in all experiments.
In practice, one needs to select appropriate a, B, e based on the desired probability thresholds and then calculate the sample sizes N1. N2, N, M, M2. Below we discuss the relationship between sample sizes and these parameters.
W.2 SAMPLE SIZE RELATIONSHIPS
The main sample size constraints appear Theorem 2
Part Sampling:
N₂ 2 2ln(1/3)
21n(2/0)
+2
a
α
For fixed B. we have N₂ = ( log 4). Importantly, there is no explicit dependency on the output dimension dj in this bound.
Part 3 Sampling: With fixed M, the bound on N can be written as
( In ))
N 2 (1 2c
Thus, for fixed M, we again have N = 2 log }) In the experiments, we instantiate these quantities with the following values:
N1 30,000, N2 = 5,000, N 3,000, = = 10,
M2 = 2,000,
and a 0.0099, 1/200 (Appendix N). Because the samples from Part reused in Part 3 (Remark 6). the total number of samples per box is:
Nuaai = N₁ + N₂ + M₂ = 37,000
This quantity is independent of d, and forms the basis for the claim "achieving 98% guarantee 98% confidence with 77,000 samples" in Section 6
35

---

Published as a conference paper at ICLR 2026
W.3 NOTATION FOR SAMPLING PARAMETERS
Throughout Proposition Theorem the symbols NI, N2, N. M. M2, A₁, Bi, Am Bn and C inherited from Algorithms 2 and as follows. In Algorithm 2 N, denotes the number of sam- ples used to estimate the per-coordinate scale vector Umax. and N2 is the number of samples used to compute the smallest scaling factor ej the optimization problem equation which yields the
output hyper-rectangle 2. In Algorithm 4 N is the number of reference points {a(0) Ti=l drawn from C. in Step One, and M is the number of auxiliary samples (axlf-)) drawn for each ref-
N
Ji=!
erence point. For each é E [N], we define A = maxxe[M] [[ - F(x()))l2 and B minje[M]] [[F(z(())) - F(x((() l|2 and the constant C is updated as C' +- max B B())- In Step Two of Algorithm 4 M2 denotes the number of additional samples (ax(1) J;=l drawn from C to estimate the distance from candidate output y to the true output set {F(a)) with Am = max |I((x:()) yl12 and B,, min [[F(x(()) -yll2. These quantities are then combined to form the estimator dmin- = max C(Am - Bm))/(1 + 20), 0} used in Part
X EXTENDING OUR METHOD
We acknowledge that different architectures and threat models may necessitate distinct verification strategies, making a universal solution challenging. Nonetheless, for many common threats, our proposed method can be adapted by modifying only the encoding in Part 2, while keeping Parts and unchanged. The following describes how to adapt our method to verify two additional threats: class misidentification and false appearances.
X.1 EXTENDING TO CLASS MISIDENTIFICATION
Algorithm 6 Sound Verification of Class Misidentification
Require: Constraints 2 H \ S; ground truth bo.gt: confidence threshold
Ensure: Calculate per-box upper bounds {Tiis (1) for class misidentification.
1: (box;) 18 + BAASTRRUCT.BSSTRATTBBOO.O
2: for all box; E (boz, \== do
Initialize upper bound for misidentification IoU of box 4: if vkk E [Mate]] \ {Class(bor Pi Classs(boorg))) 2 P,, then
3:
Tmis
5:
continue Skip boxes that must match borge class (never misclassified w.r.t. this GT)
6: end if
Box may pass the confidence threshold in some realization 8: (i) + IOU UPPER (bo,, boxg)) b> Worst-case IoU boxge when box, is
7: if C
2 then
potentially of a wrong class
9: end if
10: end for
11: return {Tmis (T)
Formalization of the Property (Bad Event): Given an input constraint set C, if there exists an input æ E C' such that after processing by the network F and NMS module, the output set (F)))) contains a predicted box boz; that has an IoU 2 T with some GT box boxge, but their predicted and GT classes do not match, we consider this a class misidentification. Formally:
Ba C, Abox; E N(F(x))) 3bougt E G (CClass(box;) * Class ToU(bo boxgt) 2
We want to prove that class misidentificationn does not occur, which is the negation of the bad event, equivalently written as:
Vax Ybor; E N(F(=))), Ybougt E G ICClass(box.)) # Class(borrg))) Tou boxggt) T.
To this end, we can define worst-case function:
+ (2)x())
max
(I( [I(Class(bor)) * Class( (b)ss))) LoU(bo boxg)))
boz,eN (F))) borge EG
36

---

Published as a conference paper at ICLR 2026
The property holds if and only if: sup Pab(z) <.
Let Z be the over-approximation of the pre-NMS network output range {F( obtained in Part
1. Since our NMS analysis in Part 2 is applied uniformly over all y E Z. compute upper bound of II( (Class (loxs(box;) * Class(boz) (boz,, bozgt) on over all possible predicted boxes and GT pairs:
Ucls
sup
(llas((boor * Class(bor.g)) lbox,, bozg)))
ye Z, b (v), b
If we can prove Uels < then it is impossible for any æ E C and any prediction/GT pair to have an IoU 2 and class mismatch. Thus, we can certify that class misidentification occurs within C, and the property is verified.
Algorithm shows how compute per-box upper bounds on the misidentification IoU Part 2.
X.2 EXTENDING TO FALSE APPEARANCES
Algorithm Sound Verification of False Appearance
Require: Constraints Z H \ S; set of ground truth boxes G; confidence threshold 6.
Ensure: Calculate per-box lower bounds {TEA (1)) on maXboxg: loU(boz,, bozgt).
18 | f CONSTRUCT ABSTRIATTTTTTTTTBBOAOA
2: for all box, E (bor, /m do
3:
TFA (7)
0
Initialize lower bound for maximal IoU to GTs of box i
4:
if C < ( then
5: continue
Box i never become high-confidence detection, ignore it for False
Appearance
6: end if
7:
lb +0
D- Lower bound on mäXbor Eg IoU (bori, borgt)
8:
for all boxge E g do
9:
1bgt f IOU SOU_LLWER_BBOUE BOUNDS borgg)
10:
lb max(b,,,, lbga) Aggregate lower bounds to obtain conservative lower bound of
maXboz
IoU
11: end for
12: TEA (i) <b lb
13:
end for
14: return (TEA
Formalization of the Property (Bad Event): Given input constraint C, if there exists input æ E C and predicted box boo; & N(F(x))) whose loU with all GT boxes is less than т, we consider this False Appearance:
Fx E C, 3box, E N(F(x))), Yborg E G, (bo borgg) <
Equivalently, define the maximum IoU for each predicted box with all GT boxes:
loU NoUmax(bor; (bor,, x) = max loU boxgt),
boaggi
The bad event can be written as:
Ex E C, Bbox; E N(F(x))) IoU (bozi; x) T.
We want to prove "no false appearances occur", which is the negation of the bad event:
Vx C, Vbox, N(F(x)) IoU (box, x) т.
We can further define:
(F)(
min ToU max (boxi; 2)), FN(())
and the property holds if and only if inf @ (ar) r.
37

---

Published as a conference paper at ICLR 2026
Algorithm shows how to compute per-box lower bounds on the maximum IoU to GT boxes in Part
For any given property, first formalize the attack and verification objective described in Section and the process above. Then, as in Section and above, we adapt Part the algorithm (c.g., by adjusting the MIQCP constraints) based the specific verification objective.
X.3 EVALUATION
To assess the effectiveness of our proposed method under diverse noise conditions and threat types, we conduct experiments using three distinct noise models and verify the False Appearance (FA) detection performance of our YOLO1 Ix model. We define noise tensor N₂ and set the perturba- tion magnitude to & = 1/255. The specific noise distributions and their corresponding real-world motivations are outlined below:
Uniform: Nr ~ ((-e,e) (Quantization/Unccttaan))
Gaussian: N ~ (O, (E/3)²) (Sensor Readout Noise).
Salt-and-Pepper: =e impulse noise with p 0.05 (Transmission Faults).
We randomly select 10 images from the COCO validation set and apply each noise model with 1/255 generate noisy inputs. We then evaluate the FA detection verification performance of our YOLO1 1x model on these perturbed images. For each input, we draw 10 samples from the corresponding noise distribution to approximate the ground truth. The results are summarized in the table below:
Table 6: FA Detection Verification Performance under Diverse Noise Models
Model
Noise type
CRAAA
TPRFA
TNRFA
FPRFA
FNRFA
yolol1x 1x
gaussian
100.00%
92.31%
100.00%
0.00%
7.69%
yolollx Ix
salt and pepper
100.00%
85.71%
100.00%
0.00%
14.29%
yolollx
uniform
100.00%
92.31%
100.00%
0.00%
7.69%
A detection is considered positive if it remains robust under the corresponding noise model and negative otherwise. The results indicate that method sustains high Certified Robust Accuracy (CRA) across different noise types, demonstrating that provides reliable guarantees under diverse real-world noise conditions and threat types. Moreover, the True Positive Rate (TPR) and True Neg- ative Rate (TNR) remain consistently high, while the False Positive Rate (FPR) and False Negative Rate (FNR) stay low, underscoring the method's effectiveness in distinguishing between robust and non-robust detections.
Overall, these results demonstrate that our method remains reliable across heterogeneous noise dis- tributions and diverse threat types. This confirms that the proposed framework is broadly applicable and provides trustworthy robustness guarantees under a wide range of real- colld noise conditions.
38


Reviews:
[{"review_id": "T64KFDdifI", "reviewer": "Reviewer_Es96", "summary": "The paper proposes a new method for PAC-based verification of the YOLO object detection network. Importantly, the method accounts for the Non-Maximum Suppression (NMS) post-processing step that is often used in practice. The first contribution is formalizing the verification problem. The second contribution is a certification pipeline based on the sample-based scenario approach [Campi, 2009]. Results show certification results that are faster than baselines and not too conservative.", "questions": "- Please clarify the sample complexity of the $RCP_N$ method.\n\n- Please revise the appendix and its proofs that are sometimes unclear or suffer from poor grammar.", "limitations": "", "rating": 4, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "- The paper tackles an ambitious problem, as YOLO is a large object detection model.\n- The method accounts for the NMS post-processing stage, which appears to be novel and practically useful.\n- By using a PAC-based sample-based analysis, the proposed verification method is less conservative and more practical than deterministic formal verification techniques (at the expense of weaker guarantees).\n- The method is substantiated with a theoretical analysis.\n- Results show that the error bounds are not too conservative.", "weaknesses": "- The sample complexity derived for the $RCP_N$ method (Appendix C.1) is incorrect: It should be computed with $d=1$ and not with $d_0=640 \\times 640 \\times 3$ (Appendix N), so $RCP_N$ likely requires fewer than 560'000'000 samples. The dimension $d$ corresponds to the optimization variable dimension, which is scalar for $RCP_N$, see (4). This error affects the sample efficiency and speedup claims.\n\n- The appendix and proofs of the theoretical results are long, yet they are sometimes not polished, unclear, and have typos. Given the emphasis on theoretical results, this is a serious limitation. In particular:\n1) Section D would greatly benefit from clearer exposition, e.g. \"Then main result\" (line 788). Also, \"by algorithm should not far beyond\" (line 789) does not specify what algorithm is considered and misses a verb.\n2) Section G (proof of lemma 2) is unclear and not rigorous: The proof starts with \"There are ...\", but how it leads to the conclusion is unclear, the sentences on lines 903-905 and 909-910 are unclear and miss verbs and nouns.\n3) In Section J.1., the proof relies on the sets $\\mathcal{Q}_k$ and $\\mathcal{T}$ whose definitions are unclear (the $\\mathcal{Q}_k$ are only subsets of $2^{\\mathcal{C}}$, and the definition of $\\mathcal{T}$ is not rigorously written), and on an independence assumption of the events $\\mathcal{T}\\in\\mathcal{Q}_k$ that is unclear.\n\n- In Definition 1, $P_{x\\sim\\mathcal{C}}$ is unclear. The probability distribution $P$ is undefined. Also, $\\mathcal{C}$ is a set, not a distribution, so $x\\sim\\mathcal{C}$ is unclear. This notation should be clarified before Section 5.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "HMh84diuuI", "reviewer": "Reviewer_UDS2", "summary": "This paper presents a probabilistic method to verify the full YOLO pipeline, from a specified input set C (a hypersphere of images around a nominal image) through non-maximum suppression (NMS). The goal is to check that, for all x in C, the post-NMS output y does not exhibit object disappearance: there is no perturbation such that,   after NMS on x, the best box with the correct class has the IoU below a fixed detection threshold.\n\nThe procedure has three parts. First, over-approximate the detector outputs F(C) by building Z. In practice, Z is an axis-aligned hyperrectangle estimated from samples x ~ C, with a PAC guarantee: with probability at least 1 - beta over the construction, a random x ~ C satisfies F(x) in Z with probability at least 1 - alpha. Second,  verify NMS over all y in Z. This is framed via a safe set Q that identifies boxes which, across Z, both meet the IoU and class requirements and cannot be suppressed into failure by NMS; if Q is nonempty, disappearance cannot occur. Third, if a candidate y in Z appears to violate safety, refine Z by trimming unreachable regions until either a real counterexample is confirmed or the candidate is shown unreachable. Then they provide the end-to-end probabilistic guarantee: for the chosen perturbation set C, object disappearance does not occur with the specified confidence and coverage parameters.", "questions": "1. For a deployment like traffic monitoring, where the scene evolves continuously (new vehicles appear, others leave), how tractable is it to verify formal robustness guarantees over a short temporal horizon (multiple frames)?\n\n2. What shape would C take on to make such guarantees meaningful? For instance, naively stretching the hypersphere C would begin to include semantically broken images that always invalidate safety.\n\n3. Is it possible for verification to work with weaker supervision? E.g., rather than having complete ground truth bounding boxes, you have some sort of a priori map over time.", "limitations": "", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "- The paper addresses the difficult and relevant problem of assuring end-to-end robustness of YOLO under perception noise, including the NMS stage. This is especially relevant to safety-critical systems that employ these black box detectors at runtime.\n\n- The formalism encodes object disappearance but is general enough to express other anomaly types (e.g., misclassification, spurious appearances, duplicate suppression)\n\n- Synthesizing Z only requires the ability to draw samples from C and does not assume a parametric form for the perturbations\n\n- The PAC-style guarantees are nice because they provide calibrated confidence and coverage claims as opposed to simple binary claims, so the guarantees are generally more interpretable and can help inform upstream design decisions.\n\n- The paper states definitions precisely, proves lemmas and propositions (including the soundness of the NMS safe set argument), and relates the algorithms to the formal guarantees they provide.", "weaknesses": "- The method certifies robustness only within a small epsilon-ball around a single image, and doesn't necessarily reflect practical YOLO deployments (e.g., traffic monitoring) where scenes change continuously and unpredictably across frames.\n\n- If ground truth is already available for the target image, the value of verifying that the detector recovers it is questionable; this makes the result feel more like a labeled-scene sanity check than a deployment-relevant guarantee.\n\n- The safety specification is narrow and ignores other important failure modes under perturbations, such as false appearances (spurious detections), class misidentification, or other anomalies.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "XHAVlJZ3Dv", "reviewer": "Reviewer_HJ5S", "summary": "This paper proposes a probabilistic verification framework (ODPV) to certify YOLO object detectors against the Object Disappearance (OD) problem. The framework consists of three modules: output range approximation, NMS verification, and probabilistic refinement, providing experiments on multiple YOLO variants showing strong robustness.", "questions": "NA", "limitations": "", "rating": 4, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "1.\tThe work presents a scalable verification framework for YOLO object detectors, incorporating the non-differentiable NMS post-processing into the certification process.\n2.\tThe method requires far fewer samples to achieve strong probabilistic guarantees, enabling the verification of large-scale models.\n3.\tThe experimental evaluation is comprehensive, covering diverse YOLO object detectors and testing robustness under various configurations. Results demonstrate the effectiveness and superiority of ODPV compared to existing probabilistic baselines, establishing a solid empirical foundation for detection verification research.", "weaknesses": "1.\tThe PAC guarantees rely on a uniform sampling distribution over the perturbation set. However, the paper does not explore how this assumption might affect the robustness of the guarantees in more realistic scenarios with non-uniform perturbations.\n2.\tThis framework is developed and evaluated only on the YOLO family of detectors, and its robustness certification is limited to the OD threat. The generality of the approach to other detection architectures or to other robustness concerns remains unverified.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "u5BBTfTzV4", "reviewer": "Reviewer_YCar", "summary": "The paper introduces a PAC-based local verification procedure for YOLO networks---object detection networks that produce annotation boxes---specially for object disappearance (OD) threats (see, e.g., [Eykholt et al., 2018](https://www.usenix.org/conference/woot18/presentation/eykholt)).\nThese networks have very high-dimensional input and especially output spaces and use non-trivial post-processing, which makes verification with off-the-shelf methods difficult.\n\nThe approach combines multiple sampling-based probabilistic techniques to solve the task in multiple steps.\n1. Approximate (from a sample) a hyper-rectangle as a high probability output \"bounding box\" for the relevant region in the input space.\n2. (Repeatedly):\n    - Detect unsafe output points $\\mathbf y$ with Quadratic programming, if none found, return **safe**.\n    - Attempt (with random sampling) to find inputs $\\mathbf x$ such that $\\lVert F(\\mathbf x) - \\mathbf y\\rVert$ is minimal\n    - If no close enough input found, refine output space, else return unsafe\nThe resulting guarantees are relaxed depending on multiple probabilistic hyperparameters, that dictate various sample sizes.", "questions": "I would appreciate it if the authors briefly addressed my concerns in **$W2$** as well as answered my questions below to address the remaining weaknesses.\n\n - **(Q1) Initial Approximation of Output Domain**:\nMany methods exist to give an \\(\\alpha,\\beta\\) guarantee on estimating a hyper-rectangle. How does your Part 1 method compare in terms of the tightness of the obtained rectangle? How much of an issue do over-approximations of the output domain present in practice?\n\n   There is established theory for estimating non-parametric confidence regions from samples, e.g., the **DKW inequality** ([Dvoretzky–Kiefer–Wolfowitz, 1956](https://projecteuclid.org/journals/annals-of-mathematical-statistics/volume-27/issue-3/Asymptotic-Minimax-Character-of-the-Sample-Distribution-Function-and-of/10.1214/aoms/1177728174.full); [Massart, 1990](https://projecteuclid.org/journals/annals-of-probability/volume-18/issue-3/The-Tight-Constant-in-the-Dvoretzky-Kiefer-Wolfowitz-Inequality/10.1214/aop/1176990746.full); for multivariate exact constants, see [Naaman, 2021](https://www.sciencedirect.com/science/article/pii/S016771522100050X)). \n   Similarly, one can learn the smallest hyper-rectangle with empirical risk minimization (ERM).\n\n   Alternatively, there exist dimension-dependent bounds with **$\\epsilon$-nets**—see [Haussler & Welzl, 1987](https://link.springer.com/article/10.1007/BF02187876) and the standard reference [Mitzenmacher & Upfal, 2017](https://www.cambridge.org/core/books/probability-and-computing/3A5B47DB315FC64B9256C5C8131C5EFA). One could consider the class of *inverse* (half-)hyperrectangles with VC-dimension $d$. After a sample of size $\\tilde{O}(\\frac{d}{\\epsilon})$, one could use $\\mathbf v_{\\max}$ directly as a bound, without the need to scale by a constant. \n   These alternatives trade dimension-independence for transparency; a short discussion comparing your scaling heuristic to empirical rectangles/$\\epsilon$-nets would help position your choice.\n\n- **(Q2) Counterexample Refinement with MIQP**: From reading the manuscript, it is not obvious that refinement steps significantly reduce the volume of the output domain (i.e., that the produced $\\mathbf y$ will be far from the actual codomain of $F$). Consequently, refinement might weaken the probabilistic guarantees in Theorem 2 without real advantage. Why eliminate an $L_2$ neighborhood of each counterexample rather than, for example, an $L_\\infty$ hypercube (or hyper-rectangles)? \nWouldn’t that allow eliminating much larger volumes in high dimensions, especially for images?\n\n   It would be very useful to investigate how much each successive refinement step not only increases the bounds but actually decreases the size of the output domain, as well as how much it relaxes the resulting bounds. A discussion of when further refinement is “not worth it” in terms of cost in confidence would be valuable.\n\n- **(Q3) Counterexample Validation and Refinement**: The theoretical idea of Theorem 1 is opaque from the main text. A brief mention of the probabilistic idea behind the “more conservative estimates” in §5.3 (with a citation or name of the invoked bound/inequality) would help communicate the approach. \n  The proof of Theorem 1 in the appendix mentions Hoeffding’s inequality; explaining its role in one sentence in the main text would help.\n\n- **(Q4) Motivation versus PGD**: If I understand correctly, Figure 5 shows that PGD often finds tighter lower bounds than probabilistic verification. \n   Is this an issue for the motivation of the procedure? \n\n   With an attack that is presumably cheaper than the proposed method, one can seemingly get tighter bounds. \n   What advantage does the proposed method offer over performing a PGD attack over an \\(\\tilde{O}(1/\\epsilon)\\) sample and reporting the tightest counterexample as a bound (cf. [Blohm et al., 2025](https://openreview.net/forum?id=UKHlXpiFMy))?\n\n   In general, can adversarial methods be integrated into the approach instead of relying on uniform random samples? If such integration is out of scope, a motivation for using a probabilistic procedure when a cheap attack can immediately provide a counterexample would help.\n\n- **(Q5)Clarification of Experimental Setup**:\n  - What is the precise sample complexity of the results in Table 2---37,000 or $10^6$?\n  - What is the precise certificate that the procedure issues for the instances, in terms of the probabilistic bounds and their interpretation?\n  - Which column in the table reflects actual robustness behaviour?\n  - Approximately, what is the certificate (confidence) provided by $\\mathrm{RCP}_N$ at the used sample complexity?\n\n---\n\n## Minor Recommendations\n\n**Self-Contained Theorems** In §5.3–5.4, including Theorems 1–2, some notation is not reintroduced (e.g., $A', B', C$). In the theorems, restate the meanings of $N, M, M_2$ for self-containment. In Theorem 2, “the algorithms defined above” should be referenced specifically (reffing Algorithm 1 might suffice if others are subroutines).\n\n**Naming of Subroutines.** The manuscript would be easier to follow if “Part 1/2/3” were replaced by names (e.g., *Output-Box Estimation*, *Unsafe-$\\mathbf y$ Search*, *Counterexample Validation/Refinement*). The algorithm captions would read more cleanly without the repeated “Part Y” phrasing.\n\n**Typos.** One of the OpenReview keywords reads “guaranteen.” In Algorithm 4, use $\\mathbb{Z}^+$ rather than $Z^+$.\n\n---\n\n## References\n\n- Blohm, P.; Indri, P.; Gärtner, T.; Malhotra, S. (2025). *Probably Approximately Global Robustness Certification.* ICML 2025. OpenReview: <https://openreview.net/forum?id=UKHlXpiFMy>  \n- Baluta, T.; Chua, Z. L.; Meel, K. S.; Saxena, P. (2021). “Scalable Quantitative Verification for Deep Neural Networks.” Proceedings of the 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE), 312–323. <https://doi.org/10.1109/ICSE43902.2021.00039>  \n- Dvoretzky, A.; Kiefer, J.; Wolfowitz, J. (1956). “Asymptotic Minimax Character of the Sample Distribution Function and of the Classical Multinomial Estimator.” *Annals of Mathematical Statistics*, 27(3), 642–669. <https://projecteuclid.org/journals/annals-of-mathematical-statistics/volume-27/issue-3/Asymptotic-Minimax-Character-of-the-Sample-Distribution-Function-and-of/10.1214/aoms/1177728174.full>  \n- Massart, P. (1990). “The Tight Constant in the Dvoretzky–Kiefer–Wolfowitz Inequality.” *Annals of Probability*, 18(3), 1269–1283. <https://projecteuclid.org/journals/annals-of-probability/volume-18/issue-3/The-Tight-Constant-in-the-Dvoretzky-Kiefer-Wolfowitz-Inequality/10.1214/aop/1176990746.full>  \n- Naaman, M. (2021). “On the Tight Constant in the Multivariate Dvoretzky–Kiefer–Wolfowitz Inequality.” *Statistics & Probability Letters*, 173, 109088. <https://www.sciencedirect.com/science/article/pii/S016771522100050X>  \n- Haussler, D.; Welzl, E. (1987). “\\(\\varepsilon\\)-nets and Simplex Range Queries.” *Discrete & Computational Geometry*, 2, 127–151. <https://link.springer.com/article/10.1007/BF02187876>  \n- Mitzenmacher, M.; Upfal, E. (2017). *Probability and Computing: Randomization and Probabilistic Techniques in Algorithms and Data Analysis* (2nd ed.). Cambridge University Press. <https://www.cambridge.org/core/books/probability-and-computing/3A5B47DB315FC64B9256C5C8131C5EFA>", "limitations": "", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "- **(S1) Significance and Motivation**\n    - The problem is important for gauging the robustness of YOLO networks, and existing methods cannot be trivially adapted to this domain.\n    - The Introduction and Related Work motivate the work well and give a nice overview of the neural net verification landscape, although some additional sources for more scalable PAC approaches can be discussed (e.g., [Baluta et.al., 2021](https://ieeexplore.ieee.org/abstract/document/9402111), [Blohm et al., 2025](https://openreview.net/forum?id=UKHlXpiFMy)).\n\n- **(S2) Theoretical Contribution**\n    - The obtained sample complexities are realistic, and proofs of the main results seem correct after surface-level checks.\n    - Neural network verification with PAC methods has been widely explored, yet the unique output modality and post-processing seem to require more involved methods for verification.\n    - The authors leverage multiple probabilistic techniques in tandem, leading to low sample complexity for the overall procedure; samples appear quasi-independent of the network dimensionality.\n    - The general idea of integrating PAC methods with counterexample-guided refinement in verification is interesting and implemented in a novel way.\n\n- **(S3) Empirical Results**\n    - The procedure seems able to deal with model sizes common in related literature and issues robustness certificates that are close to the results of adversarial methods.\n\nWhile I have several questions regarding the details of the procedure, I think they can be addressed, and their inclusion in the manuscript would strengthen the contribution.\n\n I would be happy to see a refined version of this submission accepted.", "weaknesses": "The main weakness of this manuscript is the complicated presentation of an already complex procedure.\nImportant details of the probabilistic procedure are difficult to gauge from the manuscript. \n\nMany theoretical issues may be easily clarified or adapted by the authors and do not greatly impact the theoretical contribution. \nHowever, a clear statement of the limitations and failure modes is necessary for a probabilistic procedure like this.\n\n- **(W1) Readability and Notation**: The notation is very dense, which is partially difficult to avoid in this output modality. \nWhile not the main concern of the manuscript, the readability of the manuscript would improve a lot if:\n  - Abbreviations were introduced more consistently (e.g., YOLO, RCP, PGD, ...).\n  - Citations were wrapped in parentheses when they are not part of a sentence (i.e., use `\\citep{}`-style formatting if you use LaTeX/natbib).\n  - Tables avoided heavy rules and used a cleaner booktabs style, as is typical for ML conferences like ICLR.\n\n- **(W2) Opaque Sample Complexity**: The procedure combines sampling-based approaches in a “nested” way, resulting in four hyperparameters $\\alpha,\\beta,\\delta,\\epsilon$, as well as empirically chosen sample sizes for parts of the procedure. \nThis makes it difficult to gauge how precisely the sample complexity and runtime scale with each parameter, and what trade-offs different choices bring to the overall procedure. \n\n  The fact that the likelihoods of failure events depend on multiple parameters amplifies this, as multiple choices of different parameters can lead to the same sample sizes.\n\n  **Actionable request:** Can you provide a mapping of each parameter to its failure event, sample complexity (big-O), or its impact on the overall runtime?\n  This might not be necessary to include in the main text, but it potentially gives a nice overview of the procedure.\n\n- **(W3) Partially Empirical Network Output Approximation**: The output domain of the network is estimated by scaling $\\mathbf v_{\\max}$, which, in my understanding, is essentially an empirically chosen proposal vector.\n  The scaling coefficient is chosen with a probabilistic guarantee with $O(\\frac{1}{\\alpha} (\\ln \\frac{1}{\\beta}+\\ln\\frac{1}{\\alpha}))$ samples. \n  While this scaling coefficient is chosen optimally, the proposal vector seems to be chosen based on a heuristic, with the statement in Proposition 3 in Appendix D being opaque.\n\n  There is a lot of established theory on obtaining bounding rectangles (see alternatives below). \n  These methods do not give the dimension-independent sample complexities that are presented here.\n  However, the presented method consequently relies on a scaling trick and might overapproximate the tightest bounding rectangle if the proposal vector was not chosen well.\n\n  The potential looseness of the initial output-space approximation is amplified by eliminating $L\\_2$ balls from counterexamples, instead of using $L_\\infty$.\n   Over-approximations in a single dimension may require many refinement steps to eliminate, especially in very high-dimensional spaces.\n  **Actionable request:** see **(Q1)**\n\n - **(W4) $L_2$ Counterexample Refinement and MIQP Runtime in Higher Dimensions**: Refinement steps of the output space are performed with a Mixed Quadratic Integer Program. \n  While this idea is novel and interesting, it is unclear how effective the refinement steps are, and whether the found counterexamples, in general, significantly shrink the output domain to be searched.\nA discussion/investigation of this seems important, as each refinement step brings the cost of increased uncertainty.\n- **(W5) Unclear Empirical Results in Table 2 and Figure 5**:\n\n  - It is unclear what results precisely are presented in Table 2. The Baseline Selection and Appendix N state that 37,000 samples are used to certify the proposed method, with the baseline $\\mathrm{RCP}_N$ on $10^6$ samples. However, the caption of Table 2, as well as *Safety Guarantee*, states $10^6$ uniform perturbations. In either scenario, the results are presented in a slightly confusing manner: either the runtime is compared to a method using significantly more samples (clarify in Table 1), or Table 2 shows results for significantly larger sample complexity (and thus tighter parameters).  \n  - The caption states $\\epsilon = 1/255$, yet $\\epsilon$ is varied in the table.  \n  - The false negative rate appears high (up to 15%). It is not stated on how many robust/non-robust boxes these results were computed; standard deviations are also missing.  \n  - Figure 5’s x-axis is not labelled; it is not stated which model/experiment produced this data. Code does not appear to be available, so details cannot be checked.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "xThfxE4dlr", "reviewer": "Reviewer_ji71", "summary": "This paper proposes a three-step probabilistic verification framework to assess the robustness of YOLO object detection systems against object disappearance attacks. By estimating output ranges, verifying NMS, and refining results, the method provides strong probabilistic guarantees and tighter IoU lower bounds with fewer samples, scaling effectively to practical models.", "questions": "1. How does the method generalize under different perturbation distributions?\n2. Could this verification framework be integrated with robustness training methods to further improve security?", "limitations": "", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The authors propose the first scalable probabilistic verification framework for YOLO models, effectively addressing the object disappearance threat in safety-critical scenarios.\n2. Combines solid theoretical analysis with comprehensive experiments, showing tighter IoU lower bounds and improved robustness.\n3. Achieves strong probabilistic guarantees with significantly fewer samples compared to existing methods.", "weaknesses": "1. The method is very focused on object disappearance, which is an important threat, but also a pretty narrow one. It’s not clear how well the framework would generalize to other attack scenarios or tasks.\n\n2. The experimental comparison feels a bit limited. Most of the analysis is against one baseline (RCPN), and a broader set of baselines would make the claims more convincing.\n\n3. There’s little discussion on actual computational cost. While the paper shows faster verification times, it doesn’t really explain how the method would scale in a real deployment or resource-constrained setting.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)