FocusBranch把ℓ0鲁棒性验证拆成可分支的节点：在13个网络上验证2799个候选实例，最强基线为375个
核心概要
针对只允许改动少量像素的ℓ0扰动，FocusBranch把“至多k个像素被扰动”的约束改写为由焦点像素集与层级组成的节点，使验证可以在不同层级上分支。它用覆盖设计生成超节点、用上影生成具体节点，并按采样估计选择起始层级。在13个网络、3189个候选实例上，它验证了2799个；在740个候选实例的对比中验证641个，而CoVerD+top-k-GP为375个。
深度剖析
FocusBranch把ℓ0鲁棒性验证从“固定一套分解方案”改为“按实例选择起始层级和分支策略”的分支定界过程，使同一框架既能做覆盖设计式分解，也能逐个固定被扰动像素的位置。 此前的CoVerD+top-k-GP总是从最大层级k的初始节点出发，等价于FocusBranch固定在k层起步的特例；Calzone与CoVerD则要求每个子问题把全部被扰动像素放进同一个集合。 在740个候选实例的对比中，FocusBranch验证641个，CoVerD+top-k-GP验证375个，CoVerD验证100个；其中全连接网络上三者分别为367、179和1个，卷积网络上分别为274、196和99个。
节点由焦点像素集和层级组成，层级规定焦点集之外至多还能有多少个像素被扰动，因此一个节点就对应一类受约束的扰动输入空间。 具体节点通过上影分支，即每次把一个额外像素位置固定进焦点集；超节点通过覆盖设计细化焦点集，用较少的子节点覆盖大量扰动情形。 在afc5、k=5的消融中，完整方法在70个实例里验证61个，只保留具体分支的变体验证49个，只保留超节点分支的变体验证56个。
对节点的安全判定沿用LiRPA式线性松弛，但每次具体化都在节点约束的ℓ0球上闭式求解，不需要枚举扰动子集。 全ℓ0球上的具体化只取全局贡献最大的k个像素；节点约束下则先在焦点集内取贡献最大的像素，再从焦点集外补足剩余预算。 在MNIST、Fashion-MNIST和CIFAR-10的13个网络上，k=3时验证952个候选实例，k=4时839个，k=5时641个，k=6时367个；全部验证实例中只有7.4%调用了MILP回退。
启示与展望
评估覆盖MNIST、Fashion-MNIST和CIFAR-10上的13个图像分类网络，扰动为像素级ℓ0预算；bcv4与bcv5因边界过松只在k=3下评估，所有工具统一使用1800秒超时（bcv4为3600秒）。作者把扩展到语言模型等领域的ℓ0验证列为未来工作。
作者指出精确验证本质上是组合问题且计算困难，因此在实用时间与内存预算内只评估到数千个神经元的网络；覆盖设计式超分支可能因不同子超节点覆盖重叠的扰动情形而重复计算边界；广度优先的节点管理会延迟对深层不可分支节点的探索，可能推迟MILP发现反例。