paperbot · PL 论文追踪

全部论文 待读 收藏

P1 Mini-Batch Robustness Verification of Deep Neural Networks

深度神经网络的 Mini-Batch 鲁棒性验证
OOPSLA 9(OOPSLA2)2025匹配度 5/10 · 该论文研究 DNN 局部鲁棒性的可靠且完备验证器,属于形式化验证/静态分析在机器学习系统上的应用,与用户“PL→AI”方向有部分交集;但它不涉及 Agentic 程序、LLM、浮点程序分析或贝叶斯程序分析,因此并非研究方向的核心。引用 1 inbox
Saar Tzour-Shaday, Dana Drachsler-Cohen
crossref: 2026-09-10

AI 速览

一句话:提出按 mini-batch 联合验证多个 ε-球的可靠且完备验证器 BaVerLy,加速 DNN 局部鲁棒性验证。

深度神经网络图像分类器易受对抗攻击,局部鲁棒性验证需分析大量 ε-球,但逐一验证耗时或精度损失大。本文提出分组局部鲁棒性验证,利用相似网络计算降低总时间,并实现可靠且完备的验证器 BaVerLy。它动态构造并联合验证 mini-batch,自适应选择大小,将计算相似的 ε-球分组;若通过则其中所有 ε-球均鲁棒,否则由疑似不鲁棒的 ε-球指导精化,并复用结果加速后续分析。在 MNIST 与 CIFAR-10 的全连接和卷积网络上,BaVerLy 相比逐一验证平均加速 2.3 倍、最高 4.1 倍,总时间从 24 小时降至 6 小时。

问题
安全攸关场景中的 DNN 图像分类器易受对抗攻击,而现有局部鲁棒性验证器逐一分析 ε-球,分析时间过长或精度损失过大,难以高效处理大量输入。
方法
提出分组局部鲁棒性验证,利用 ε-球间网络计算相似性,并由可靠且完备的验证器 BaVerLy 动态构造、联合验证 mini-batch,自适应选择 mini-batch 大小并用验证失败指导精化。
评估
在 MNIST 和 CIFAR-10 的全连接与卷积网络上评估,相比逐一验证平均加速 2.3 倍、最高 4.1 倍,总分析时间从 24 小时降至 6 小时。
原文摘要(Abstract)

Neural network image classifiers are ubiquitous in many safety-critical applications. However, they are susceptible to adversarial attacks. To understand their robustness to attacks, many local robustness verifiers have been proposed to analyze ϵ -balls of inputs. Yet, existing verifiers introduce a long analysis time or lose too much precision, making them less effective for a large set of inputs. In this work, we propose a new approach to local robustness: group local robustness verification. The key idea is to leverage the similarity of the network computations of certain ϵ -balls to reduce the overall analysis time. We propose BaVerLy , a sound and complete verifier that boosts the local robustness verification of a set of ϵ -balls by dynamically constructing and verifying mini-batches. BaVerLy adaptively identifies successful mini-batch sizes, accordingly constructs mini-batches of ϵ -balls that have similar network computations, and verifies them jointly. If a mini-batch is verified, all its ϵ -balls are proven robust. Otherwise, one ϵ -ball is suspected as not being robust, guiding the refinement. BaVerLy leverages the analysis results to expedite the analysis of that ϵ -ball as well as the analysis of the mini-batch with the other ϵ -balls. We evaluate BaVerLy on fully connected and convolutional networks for MNIST and CIFAR-10. Results show that BaVerLy scales the common one by one verification by 2.3x on average and up to 4.1x, in which case it reduces the total analysis time from 24 hours to 6 hours.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2878,
  title = {Mini-Batch Robustness Verification of Deep Neural Networks},
  author = {Saar Tzour-Shaday and Dana Drachsler-Cohen},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {OOPSLA2},
  year = {2025},
  doi = {10.1145/3763150}
}