IoUCert: Robustness Verification for Anchor-based Object Detectors¶
会议: ECCV 2026
论文: ECCV 2026
领域: 目标检测
关键词: 形式化鲁棒性验证、目标检测、IoU 界、区间界传播、LeakyReLU 松弛
一句话总结¶
IoUCert 把「单目标检测的 IoU 不低于阈值」写成一个可验证的性质：先用坐标变换把框解码的非线性映射从松弛链里摘出去，再证明 IoU 的极值只可能落在有限个临界点上，从而用最多 169 个候选点解析地给出最优 IoU 上下界，配合 LeakyReLU 的最优线性松弛，首次在 SSD、YOLOv2、YOLOv3 这类真实 anchor-based 检测器上完成形式化鲁棒性验证。
研究背景与动机¶
神经网络验证在图像分类上已经相当成熟：IBP、CROWN 一族、符号区间传播加分支定界（BaB）已经能把 ReLU 网络的鲁棒性判定做到大规模，VNN-COMP 也把工具与基准标准化了。但这套能力几乎全部落在分类器上，一旦目标变成目标检测（OD）模型，现有验证器要么根本不支持、要么只能给出极松的近似：检测器里有非极大值抑制这类逻辑组件、有 IoU 这一整套 max/min/乘除复合的几何指标、还有把回归输出变成框坐标的非线性解码，以及多尺度 head 与 anchor 结构。已有的 OD 验证工作大多在"玩具回归模型"上评估——网络直接回归四个角点坐标、浅 backbone、没有 anchor、没有多尺度 head，而且这些模型本身的检测精度就很低。例如文献 [19] 在预测的角点坐标上做 IBP 来界 IoU，文献 [53] 把 IoU 编码成网络层交给通用验证器、却卡在 max/min/除法上的松散界；两者的可扩展性都止步于玩具模型。还有一条路是概率验证器 [45]，它能覆盖完整的 YOLO 管线（含 NMS），但给出的证书本身不 sound，即便对小模型也不成立。
这里的核心矛盾是：要把证书从玩具模型抬到真实检测器，必须跨过两个数学瓶颈，而这两个瓶颈恰好都是"非线性"造成的。第一个是框解码 \(\psi\circ\phi\)——offset 到角点是非线性映射，常规做法先在 offset 上做界传播、再让界穿过这层映射去界 IoU，每穿一层就多一次过近似，误差被逐级放大；第二个是 IoU 本身——它是 max/min/除法复合出的分段函数，直接线性松弛必然很松，界一松，分支定界就会超时。更麻烦的是，检测器的"正确"不是单个 logit 的大小关系：它同时包含"最终输出的是哪一个框"这一层选择逻辑，而界传播天然会让多个框都"可能成为最高分"。
本文的切入角度是：与其把这两处非线性都拿去松弛，不如想办法绕开它们。检测器的框解码映射在常见的 anchor-based 家族里是可逆的，那么"先在 offset 上得界、再穿过解码"这件事本身就是多余的——把变量替换到角点空间、把 offset 上的盒约束等价地写成角点上的线性约束，既没有引入松弛，又让 IoU 的可行域变成两个互相解耦的二维平面；在这个结构上，IoU 的极值不再需要用松弛去估计，而是可以精确枚举。核心 idea：用坐标变换把 IoU 的界从"松弛估计"变成"可行域上的精确极值枚举"，再用最优的 LeakyReLU 线性松弛压掉激活层贡献的松弛误差，从而让首个面向真实 anchor-based 检测器（SSD / YOLOv2 / YOLOv3）的形式化验证器成为可能。
方法详解¶
整体框架¶
IoUCert 回答的问题是：给定一张图和扰动约束 \(\zeta_x\)，是否存在扰动范围内的某张图使检测器的输出"不正确"。这里的 \(\zeta_x\) 是输入上的约束集合，可以写成 \(\ell_\infty\) 球、亮度区间、对比度区间、模糊核参数区间等任意可表达为输入区间的形式；验证通过（ROBUST）意味着对 \(\zeta_x\) 中的所有输入（无限多个）都成立，因此它是完整验证而非采样测试。作者把场景限制在单目标设定：一张图只有一个真值框 \(g=(z_0,z_1,z_2,z_3,g_c)\)，检测器仍会输出大量候选框，但正确性只取决于后处理留下的那一个框：
也就是说，证书要同时覆盖三件事：选出来的框是"对的那个"（选择）、它的类别与置信度过阈、并且它与真值框的 IoU 过阈。保留置信度阈值 \(\tau_{\text{class}}\) 是有意的——它让检测器在全部候选都低于阈值时可以弃权，而弃权本身也要被验证覆盖。
算法的整体流程是三段：先用既有的界传播框架（IBP 或符号区间传播/回代）得到网络输出上的界，即每个 anchor 的 offset 与 logits 的区间（对应 Algorithm 1 的 Line 4）；然后做候选框选择，筛出所有"有可能成为最高分"的框（Line 5）；最后对每个候选框计算其类别分数界与和真值框之间的 IoU 界，据此给出 ROBUST / NONROBUST / UNKNOWN 三值判定。UNKNOWN 不是失败，而是"界还不够紧"，交给分支定界（论文把它接在 Venus 验证器上）继续切分空间来收紧。整篇方法的技术含量集中在第三段：为了让 IoU 界够紧，需要前面的坐标变换，以及一套精确的极值点枚举；为了让 YOLOv3 这类用 LeakyReLU 的骨干不在激活层上漏掉紧度，还需要一组最优的 LeakyReLU 线性松弛。
关键设计¶
1. 坐标变换：把框解码的非线性从松弛链里摘出去
先看痛点。每个候选框是这样产生的：模型对固定 anchor \(p\) 预测 offset \(o\)，再用模型特定的解码函数 \(\phi(o,p)=(c_x,c_y,w,h)\) 变成中心宽高格式，最后用 \(\psi\) 转成角点 \(z=(z_0,z_1,z_2,z_3)\)。文献 [19] 的做法是在 offset 上得到区间 \([\underline{o},\overline{o}]\) 之后，让这个区间穿过 \(\psi\circ\phi\) 得到角点的界，再去界 IoU——但 \(\psi\circ\phi\) 是非线性的，穿一次就松一次，IoU 界被放大到难以判定。
本文的做法是干脆不穿。由于 \(\psi\) 与 \(\phi\) 都是单射（附录 B），可以定义逆映射 \(\phi^{-1}\circ\psi^{-1}\)，把优化变量从 offset 换成角点坐标：目标函数变成直接对 \(\mathrm{IoU}(z,g)\) 求极值，而原先 offset 上的盒约束被等价地搬运成角点上的四个线性约束——真值框固定不动，于是问题被改写成下面的形式（论文 Problem 2 的展开，\(L_i,U_i\) 由 offset 界的端点经 \(\phi^{-1}\) 直接算出）：
求下界只需把 max 换成 min，推导完全对称。整个过程只做了一次可逆的变量替换，没有经过任何松弛操作：非线性没有被"近似掉"，而是被搬进了约束的系数里。这个改写带来一个关键的结构性好处——前两条约束只含 \((z_0,z_2)\)（宽度方向），后两条只含 \((z_1,z_3)\)（高度方向），两个方向天然解耦，原问题于是分裂成两个独立的二维问题。这正是下一节能够精确枚举极值的前提；如果还在 offset 空间里，三个变量会通过解码函数互相纠缠，拆不开。
适用条件是解码映射 \(\psi\circ\phi\) 在每个 offset 上严格单调、逆映射可解（附录 B），SSD 与 YOLO 家族的 dense anchor head 都满足。作者特别强调这与训练无关：ATSS、PAA、OTA 这类标签分配策略改变的是训练目标，不改变推理期的解码映射；同理，Faster R-CNN 的 RPN、以及回归可逆 offset 的 anchor-free head 也落在同一框架内（附录 H）。
2. 最优 IoU 界：枚举 13 个候选点，不做任何松弛
有了凸性之外的可解结构，接下来要解决的是 IoU 本身的非线性。IoU 由 max/min 与乘除复合而成，线性松弛会非常松（文献 [53] 正是卡在这一点上），界一松，分支定界就会指数爆炸。本文选择的路线是精确求极值：在一个由线性约束定义的可行域上，连续函数的极值只可能出现在三类位置——梯度为零的内点、可行域边界的角点、以及函数不可导处。论文沿用 [19] 的结论排除了第一类（IoU 的偏导在可行域内不为零），于是只剩后两类可以产生候选。
对边界上的驻点，附录 E.2 证明了 IoU 沿每条边界的梯度"要么处处为零、要么处处非零"：前者意味着边界上的值与区域角点的值相同，后者意味着极值落在角点之间的某一段端点上。因此第二类点不需要单独枚举，已经被角点覆盖。第三类是 IoU 的不可导点 \(z_i=g_i\)，即真值坐标线；每条真值坐标线（\(z_0=g_0\)、\(z_2=g_2\) 以及高度方向的对应两条）与四条边界线相交，给出 \(2\times 4=8\) 个交点，再加上真值框角点 \((g_0,g_2)\)（若落在可行域内）。于是每个二维平面的候选集就是"4 个可行域角点 + 8 个交点 + 1 个真值角点 = 13 个点"，Theorem 1 断言 IoU 的最大值一定在这些点的某个坐标组合上取到，两个平面的候选组合起来给出 \(|\mathcal{C}_s|=13^2=169\) 个候选。实现上只需遍历这 169 个点，逐个检查是否满足约束、是否构成合法框（\(z_0<z_2\) 且 \(z_1<z_3\)），再更新最大最小值即可。
这个方案的价值有三层。第一，它给出的是该约束集合下的最优界，而不是某个松弛的界：精度提升直接来自"不再近似"。第二，候选数是常数 169，算法正确且常数时间终止（附录 F），计算量与界有多宽无关。第三，它把工作量的代价说清楚了：相比一次线性松弛传播，枚举 169 个点（每个都要算 IoU 与可行性）每调用一次更贵，换来的是紧 50% 以上的界——这个 trade-off 在实验里被明确量化（见"关键发现"）。论文的 Figure 3 用 \((z_0,z_2)\) 平面画出了这 13 个候选点，其中 8 个交点里落在可行域外的一半会被可行性检查剪掉，最终留下 9 个实心点。
3. 候选框选择与三值判定：把"选中哪个框"也纳入证书
检测器的正确性里有一层"选择"语义不能忽略。界传播天然会让多个框都可能成为最高分——论文给的例子是 box 1 的置信度界为 \([0.5,0.9]\)、box 2 为 \([0.7,0.8]\)，此时谁当选都无法排除。只对 argmax 的界做判断是不 sound 的。IoUCert 的处理是：把所有"置信度上界超过全体框置信度下界之最大值"的框都收进候选集——只有这些框才有可能成为 top-1，其余框不可能被选中，可以被安全忽略。对每个候选框，分别用界传播算类别分数界、用上一节的枚举算与真值框的 IoU 界。
有了这些界，判定规则是三值的：只有当所有候选框的 IoU 下界都不低于 \(\tau_{\text{iou}}\)、置信度下界不低于 \(\tau_{\text{class}}\)、且所有候选框预测的类别一致（等于真值类别）时，才返回 ROBUST——注意这是对"所有可能的 top-1 选择"的全称判断，所以证书是 sound 的。反过来，只要没有任何一个候选框的 IoU 上界能到 \(\tau_{\text{iou}}\)（也就是无论选中谁都不合格），或所有候选的最高置信度上界都低于 \(\tau_{\text{class}}\)，或所有候选预测的类别都与真值不同，就返回 NONROBUST，并给出反例。剩下的情况返回 UNKNOWN：界还不够紧，或者候选框之间连类别都没法统一。Theorem 2 给出正确性，并说明 IoUCert 与任意分支定界框架结合后是完备的——UNKNOWN 只是"还没切够"，不是不可判定。
4. LeakyReLU 的最优线性松弛
前面三步都在绕开非线性，但骨干网络里还有一处必须正面处理：YOLOv3 用的是 LeakyReLU，而主流验证器的理论都建立在 ReLU 上。\(\mathrm{LeakyReLU}(x)=\max\{\alpha x,x\}\)，\(\alpha\in[0,1]\)，当区间 \([l,u]\) 完全落在正半轴或负半轴时它是线性的、可以被精确表示；只有 \(l<0<u\) 的不稳定神经元需要线性上下界。上界取连接 \((l,\alpha l)\) 与 \((u,u)\) 的弦即可，关键在下界：已有工作（如文献 [48]）直接令下界斜率取 \(\alpha\)，但这并非最优。事实上 \(\alpha x\) 与 \(x\) 都是合法下界（\(x\le \mathrm{LeakyReLU}(x)\) 在整个区间上成立，\(\alpha x\) 在负半轴逐点精确），选哪一条更紧取决于区间往哪边偏：用 \(\alpha x\) 时误差全部落在正半轴、大小正比于 \(u^2\)，用 \(x\) 时误差全部落在负半轴、大小正比于 \(|l|^2\)。因此最优选择是比较 \(u\) 与 \(|l|\) 谁大：
Theorem 3 给出的正是这一结论（⚠️ 该式在缓存全文中的 LaTeX 已损坏，上式的不等号方向与分段形式是按论文文字描述与"最小化松弛误差"的推导复述的，以原文为准）。这条松弛之所以重要，是因为松弛误差是分支定界紧度的主要来源：在分类验证里，把不稳定神经元的松弛换成最优松弛可以直接降低分支数，而 YOLOv3 的骨干里 LeakyReLU 数量很多，不做这一步就很难在高扰动预算下判定。
一个完整示例¶
以 LARD 上一张 \(128\times128\) 的跑道图为例，验证亮度扰动 \(\epsilon=0.3\) 下 SSD 的预测是否 ROBUST。\(\zeta_x\) 把每个像素的亮度写成一个区间，回代后得到各 anchor 的置信度界；设其中两个框的界是论文里的那组数字——box 1 为 \([0.5,0.9]\)、box 2 为 \([0.7,0.8]\)，其余框的上界都低于 \(0.7\)，于是候选集被筛成这两个框（第三类框不可能成为 top-1，直接忽略）。接着对每个候选框：把它的 offset 界用 \(\phi^{-1}\circ\psi^{-1}\) 换成角点空间上那四条只含 \(z_0+z_2\)、\(z_1+z_3\)、\(z_2-z_0\)、\(z_3-z_1\) 的约束；在 \((z_0,z_2)\) 平面上枚举 4 个角点、真值线 \(z_0=g_0\) 与 \(z_2=g_2\) 同四条边界线的 8 个交点、以及真值角点 \((g_0,g_2)\)（可行域外的一半被剪掉），\((z_1,z_3)\) 平面同理；两个平面的候选组合起来是 \(13\times13=169\) 个点，逐个校验可行性与合法性后取最大最小，就得到这个候选框的 IoU 界。若两个候选框的 IoU 下界都 \(\ge\tau_{\text{iou}}\)、置信度下界都 \(\ge\tau_{\text{class}}\) 且类别一致，整张图的验证返回 ROBUST；若某个候选框的 IoU 上界都到不了阈值（无论选谁都不合格），或最高置信度上界低于 \(\tau_{\text{class}}\)，返回 NONROBUST 并给出反例；若两个候选框一个过界一个不过界，就是 UNKNOWN，交给 Venus 的分支定界继续切分。
实验关键数据¶
主实验¶
IoUCert 实现为 Venus 验证器上的一个自定义层，接在目标模型之后：它吃回代得到的输出 logits 的具体界，算出 IoU 与置信度分数的界，并与 Venus 的分支定界过程联动。评估用的检测器包括：在 LARD 跑道检测任务（Google Earth 图像，每张图一条跑道）上训练的 SSD，输入 \(128\times128\)，为可验证性把 MaxPool 换成线性的 AvgPool，用 SGD 与 MultiBox loss 训练，NMS 阈值 0.5、置信度阈值 0.15，约 1128 万可学习参数；VNN-COMP 2023 提供的 YOLOv2-tiny（TinyYOLO，Pascal VOC 子集）基准；以及在 LARD（\(64\times64\) 与 \(128\times128\)）和 COCO（\(128\times128\)，预处理成单目标裁剪）上训练的 YOLOv3-tiny，参数量 870–890 万。每个数据集取 50 张正确分类的图像作为验证子集，扰动为亮度、对比度与运动模糊（核大小 5、角度 0°）。
表 1（SSD 与 YOLOv2，亮度/对比度扰动）中 R/NR/T 分别是 ROBUST/NONROBUST/超时 的计数，时间为该设置下所有案例的平均验证时间（秒）。
| 模型 | \(\epsilon\) | 亮度 R / NR / T | 亮度时间 (s) | 对比度 R / NR / T | 对比度时间 (s) |
|---|---|---|---|---|---|
| SSD (LARD) | 0.01 | 48 / 2 / 0 | 29.06 | 49 / 1 / 0 | 24.21 |
| SSD (LARD) | 0.10 | 40 / 10 / 0 | 731.41 | 42 / 8 / 0 | 359.41 |
| SSD (LARD) | 0.30 | 9 / 41 / 0 | 458.21 | 30 / 20 / 0 | 885.51 |
| SSD (LARD) | 0.50 | 0 / 47 / 3 | 221.71 | 14 / 36 / 0 | 743.04 |
| SSD (LARD) | 1.00 | 0 / 50 / 0 | 5.79 | 0 / 50 / 0 | 3.90 |
| YOLOv2 (VOC) | 0.01 | 50 / 0 / 0 | 3.69 | 50 / 0 / 0 | 3.23 |
| YOLOv2 (VOC) | 0.10 | 47 / 3 / 0 | 23.81 | 50 / 0 / 0 | 9.23 |
| YOLOv2 (VOC) | 0.30 | 28 / 22 / 0 | 39.40 | 48 / 2 / 0 | 33.36 |
| YOLOv2 (VOC) | 0.50 | 4 / 46 / 0 | 9.99 | 36 / 14 / 0 | 35.86 |
| YOLOv2 (VOC) | 1.00 | 0 / 50 / 0 | 0.81 | 0 / 50 / 0 | 2.36 |
表 2（YOLOv3-tiny，含 LeakyReLU 最优松弛；超时案例在全部设置下均为 0，故从表中省略，时间为亮度扰动下的平均验证时间）。
| 模型 | \(\epsilon\) | 亮度 R / NR | 对比度 R / NR | 运动模糊 (0°) R / NR | 亮度时间 (s) |
|---|---|---|---|---|---|
| LARD \(64\times64\) | 0.01 | 50 / 0 | 50 / 0 | 50 / 0 | 3.35 |
| LARD \(64\times64\) | 0.10 | 50 / 0 | 50 / 0 | 50 / 0 | 20.45 |
| LARD \(64\times64\) | 0.30 | 50 / 0 | 50 / 0 | 50 / 0 | 56.26 |
| LARD \(64\times64\) | 0.50 | 47 / 3 | 49 / 1 | 50 / 0 | 89.58 |
| LARD \(64\times64\) | 1.00 | 28 / 22 | 0 / 50 | 45 / 5 | 103.87 |
| LARD \(128\times128\) | 0.01 | 50 / 0 | 50 / 0 | 50 / 0 | 10.32 |
| LARD \(128\times128\) | 0.10 | 50 / 0 | 50 / 0 | 50 / 0 | 190.99 |
| LARD \(128\times128\) | 0.30 | 42 / 8 | 43 / 7 | 50 / 0 | 381.03 |
| LARD \(128\times128\) | 0.50 | 40 / 10 | 40 / 10 | 50 / 0 | 592.56 |
| LARD \(128\times128\) | 1.00 | 12 / 38 | 0 / 50 | 49 / 1 | 304.45 |
| COCO \(128\times128\) | 0.01 | 50 / 0 | 50 / 0 | 50 / 0 | 8.93 |
| COCO \(128\times128\) | 0.10 | 46 / 4 | 50 / 0 | 50 / 0 | 120.60 |
| COCO \(128\times128\) | 0.30 | 36 / 14 | 45 / 5 | 49 / 1 | 272.45 |
| COCO \(128\times128\) | 0.50 | 29 / 21 | 43 / 7 | 48 / 2 | 376.78 |
| COCO \(128\times128\) | 1.00 | 6 / 44 | 0 / 50 | 38 / 12 | 169.74 |
消融实验¶
第一组分析是界的紧度（表 3，论文 Table 2）。在 SSD 上、亮度扰动 \(\epsilon=0.02\) 的一次验证运行中，记录所有框（不只最高分框）的 IoU 界，统计相对文献 [19] 的紧度提升，以及因界更紧而避免探索的分支比例。
| IoU 界所在区间 | 采样数 | 紧度提升 (%) | 避免探索的分支 (%) |
|---|---|---|---|
| 0.01 – 0.10 | 14642 | 50.67 | 0.59 |
| 0.10 – 0.20 | 8479 | 65.09 | 0.12 |
| 0.20 – 0.30 | 8084 | 58.54 | 0.11 |
| 0.30 – 0.40 | 6383 | 56.09 | 0.05 |
| 0.40 – 0.50 | 4440 | 55.32 | 0.14 |
| 0.50 – 0.60 | 3569 | 54.75 | 99.66 |
| 0.60 – 0.70 | 2707 | 53.74 | 98.93 |
| 0.70 – 0.80 | 2336 | 53.14 | 97.60 |
| 0.80 – 0.90 | 1802 | 52.20 | 96.50 |
| 0.90 – 0.99 | 1374 | 52.30 | 95.92 |
第二组是下采样方式的消融（把 AvgPool 换回原始 MaxPool），在 LARD \(64\times64\) 的 50 张子集、亮度 \(\epsilon=0.3\) 下：
| 配置 | 验证结果（亮度 \(\epsilon=0.3\)） | 干净精度 (mAP\(_{0.5}\)) | 说明 |
|---|---|---|---|
| AvgPool（本文） | 50 / 50 ROBUST，平均 56 s | 86.59%（mAP\(_{0.5:0.95}\): 40.90%） | 线性层可在界传播中精确表示 |
| MaxPool（原始） | 15 / 50 ROBUST，33 次超时，总耗时 > 1600 s | 86.88%（mAP\(_{0.5:0.95}\): 41.67%） | 分段线性池化层难以精确松弛 |
关键发现¶
- 认证率随扰动预算单调下降，并且下降方式与扰动类型强相关。 所有模型在小 \(\epsilon\) 上几乎全部 ROBUST（SSD 在 \(\epsilon=0.01\) 亮度下 48/50，YOLOv2 在 0.01–0.10 亮度下接近全过），随 \(\epsilon\) 增大 ROBUST 计数单调下降、NONROBUST 上升，验证器找到了真实的脆弱性而非仅仅"判不出来"。同一张 SSD 在 \(\epsilon=0.30\) 下亮度只剩 9/50 而对比度仍有 30/50，说明亮度是更有效的扰动方向；YOLOv2 在亮度 \(\epsilon=0.50\) 只剩 4/50，相比之下对比度同预算下还有 36/50。大预算下（\(\epsilon\ge0.80\)）几乎所有模型都变为 NONROBUST，此时验证反而很快（例如 SSD 在 \(\epsilon=1.00\) 时平均仅 5.79 s），因为反例很早就被找到、不需要继续切分。
- 界紧度是本方法的核心收益，且紧度收益集中体现在剪枝上。 相比 [19]，IoUCert 在所有区间上的 IoU 界都紧 50% 以上（50.67%–65.09%）。剪枝收益则呈现明显的两极：在 0.01–0.50 这五个区间内，"避免探索的分支"不超过 0.59%，几乎可以忽略；而在 0.50–0.99 区间内达到 95.92%–99.66%。原文把后者对应到"较浅的深度、界本身更松"的情形，即界越松的地方，收紧它的边际收益越大（⚠️ 表 3 第一列的语义在表题中写作"IoU 界区间"，正文又用 shallower depths 描述，两处的对应关系在缓存全文中略含糊，数字照录，具体口径以原文为准）。
- 更紧的界不是免费午餐。 与 [19] 的松散界重实现相比，两者在完整验证上的整体表现接近：紧界避免了大量分支，但每次调用更贵；松界分支更多、但每个分支处理更快。论文把这一点作为设计上的显式取舍交给使用者，而不是宣称单方面胜出。
- 干净精度更高不等于认证鲁棒性更好。 LARD 上 \(128\times128\) 的 YOLOv3 比 \(64\times64\) 的干净精度更高，但认证鲁棒性更差——输入维度更高导致界更松；同一分辨率下 COCO 模型（多类、场景更复杂）比 LARD 更脆弱（\(\epsilon=0.50\) 亮度下 29/50 vs 40/50），但对中等强度的对比度略更耐受。
- 运动模糊是这三类扰动里最难造成失效的。 0° 运动模糊下所有 YOLOv3 模型都高度鲁棒（COCO 在 \(\epsilon=1.00\) 仍有 38/50 ROBUST，LARD \(128\times128\) 在 \(\epsilon=0.80\) 仍 50/50），但高预算下仍能找到反例，说明结论是"该类扰动影响小"而不是"没有影响"；其他模糊角度见附录 C.2 的 Table S3。
- AvgPool 替换是可验证性的决定性因素，而代价很小。 把 MaxPool 换成 AvgPool 后 mAP\(_{0.5}\) 只从 86.88% 降到 86.59%（mAP\(_{0.5:0.95}\) 从 41.67% 到 40.90%），但同样的验证查询从"15/50 通过、33 次超时、总耗时超过 1600 s"变成"50/50 通过、平均 56 s"，快了一个数量级以上。可验证性与精度在设计上需要一起权衡，而不是先训好模型再想办法验证。
亮点与洞察¶
- 最漂亮的一步不是把界得更紧，而是取消了一次本不必要的松弛。 既然框解码映射可逆，就完全没有必要让界穿过它——把变量替换到角点空间、让非线性进入约束的系数，精度损失为零。这个思路可以迁移到任何"先传播再穿解码"的验证管线：先问一句"这个非线性是不是可逆、逆是不是好写"，如果是，就把它搬进约束而不是拿去松弛。
- 确定性枚举极值点的配方可以直接照搬。 "先排除内点（证梯度非零）→ 边界驻点要么被角点覆盖要么落在端点 → 不可导集合与边界相交得到有限候选"这条三步推理，把非光滑指标的界计算变成了常数次枚举。迁移对象很自然：GIoU / DIoU 这类同样由 max/min/乘除构成的检测指标，以及 NMS 里的成对重叠界。
- 把"选择哪一项输出"纳入证书，是检测器验证区别于分类器验证的本质难点。 一个框的分数界是区间而不是点值时，"谁当选"本身就是不确定的，IoUCert 用"所有可能当选者都要满足性质"的全称判断处理了它。这套处理对任何带后处理选择逻辑的模型（分类里的 top-k、检索里的 rerank、多候选生成）都适用。
- 取舍讲得很坦白，反而让 claim 站得住。 论文明确把多目标与 NMS 的组合复杂度留作 future work，并算清了代价（成对框的 IoU 界需要 \(O(n^2)\) 个证书，且界跨过 NMS 阈值时判定会变得模糊）。正因如此，"首个在 SSD / YOLOv3 上完成形式化验证"这一说法是有限定条件的、可检验的，而不是夸大的。
局限与展望¶
- 作者承认的局限：只覆盖单目标场景；多目标需要成对框的 IoU 界（最多 \(O(n^2)\) 个证书），且当重叠界跨过 NMS 阈值时判定会变得模糊，因此 NMS 感知的完整管线验证还只是下一步；方法要求框解码映射 \(\psi\circ\phi\) 逐 offset 严格单调、逆映射可解，含 attention 与 set prediction 的 DETR 类检测器对当前验证器仍然困难；验证是部署前的离线过程，不用于运行时。
- 我从实验设计看到的问题：每数据集只取 50 张正确分类图，且只报告 ROBUST / NONROBUST / 超时的计数，没有给出"认证精度"这类可与干净精度直接比较的指标，因此跨模型、跨数据集的强弱只能定性判断；此外论文没有与经验攻击（PGD / C&W 一类）做对照——NONROBUST 的反例来自验证器自身的搜索，读者无法从这篇知道"证书比攻击强多少"；把 MaxPool 换成 AvgPool 虽然是可验证性的必要手段且消融显示代价很小，但严格说被验证的并非原版架构；最后，论文没有与 [53]、[45] 在同模型上做 head-to-head，不过这也部分因为它们不支持 SSD/YOLO 这类架构。
- 可以想见的改进方向：把 NMS 的成对 IoU 界用同一套临界点枚举做出来（候选框的紧界已经由 IoUCert 提供，这是最自然的下一步）；把这里的 IoU 界用到 certified training 上，训练天然可验证的检测器（IBP 训练在分类上已被证明有效，检测侧还没有对应工作）；把最优 LeakyReLU 松弛的思路推广到 SiLU / GELU 等其他分段激活。
相关工作与启发¶
- vs [19]（VerifIoU，DASC 2025；正文引用为 Cohen et al.，参考文献条目首作者显示为 Ducoffe, N.C.M.，两处不一致，⚠️ 以原文为准）: 他们在预测的角点坐标上做 IBP 来界 IoU，等价于让 offset 界先穿过非线性解码再界 IoU；本文用坐标变换取消这次穿越，并在角点空间枚举极值点，得到该约束集合下的最优界。实验里本文的界一致紧 50% 以上，整体用时接近（紧界省分支、松界省单次开销）。本文的额外前提是解码可逆，他们的瓶颈是可扩展性。
- vs [53]（Raviv et al., 2024）: 他们把 IoU 编码成一个网络层，交给通用验证器去处理，于是受限于 max / min / 除法上的松散界；本文不复用通用层的松弛，而是解析求极值，因此能够吃下多尺度 head、anchor 与置信度分数这些真实结构。
- vs [45]（Liu et al., ICLR 2026）: 概率验证器能覆盖完整的 YOLO 管线（含 NMS），但对小模型也已给出不 sound 的证书；本文是 sound 的，代价是只覆盖单目标、不含 NMS。两者在"覆盖范围"与"可靠性"上互补，不是替代关系。
- vs [15]（ImageStars 集合可达性）与 [50]（branch-free IBP 的跑道检测认证）: 它们同样只在小规模玩具模型上评估，缺少多尺度 head、非线性坐标变换与 anchor 结构的支持；架构层面的这道差距正是本文声称填上的部分。
评分¶
- 新颖性: ⭐⭐⭐⭐⭐ 首次把形式化鲁棒性验证扩展到 SSD / YOLOv2 / YOLOv3 这类真实 anchor-based 检测器，坐标变换、最优 IoU 极值界、最优 LeakyReLU 松弛三项都是实打实的技术贡献。
- 实验充分度: ⭐⭐⭐⭐ 覆盖 3 个检测器家族、4 种模型配置、3 类扰动与 3 个数据集（含安全攸关的 LARD），但每数据集仅 50 张图、缺少认证精度指标、也缺少与经验攻击的对照。
- 写作质量: ⭐⭐⭐⭐ 结构与算法配套清楚，定理、算法与附录证明齐全，对单目标 / 无 NMS / 离线这三个取舍交代得诚实；部分符号与表格口径的表述略含糊（如候选点枚举与表 3 第一列的语义）。
- 价值: ⭐⭐⭐⭐⭐ 提供了一套可复用的数学工具（可逆解码的约束改写 + 极值点枚举 + 最优激活松弛），为"端到端检测器验证"这条路线打下了扎实的一步。