ML Security PapersMini-Batch Robustness Verification of Deep Neural Networks
Saar Tzour-Shaday , Dana Drachsler-Cohen
Published on arXiv
2508.15454
Input Manipulation Attack
OWASP ML Top 10 — ML01
Key Finding
BaVerLy achieves 2.3x average and up to 4.1x speedup over standard one-by-one ε-ball verification, cutting a 24-hour analysis to 6 hours on fully connected and convolutional networks
BaVerLy
Novel technique introduced
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.
Key Contributions
- Group local robustness verification: a new paradigm that exploits similarity of network computations across ε-balls to reduce total verification cost
- BaVerLy: a sound and complete verifier that dynamically identifies effective mini-batch sizes, constructs batches of similar ε-balls, and verifies them jointly with guided refinement on failures
- 2.3x average speedup (up to 4.1x) over one-by-one verification on MNIST and CIFAR-10, reducing a 24-hour analysis to 6 hours
🛡️ Threat Analysis
Proposes a sound-and-complete certified robustness verifier that formally proves a model's resistance to adversarial perturbations within ε-balls — a direct defense technique against input manipulation attacks at inference time.