Saved in:
Bibliographic Details
Main Authors: Shapira, Yuval, Wiesel, Naor, Shabelman, Shahar, Drachsler-Cohen, Dana
Format: Preprint
Published: 2024
Subjects:
Online Access:https://arxiv.org/abs/2405.10924
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866912050982158336
author Shapira, Yuval
Wiesel, Naor
Shabelman, Shahar
Drachsler-Cohen, Dana
author_facet Shapira, Yuval
Wiesel, Naor
Shabelman, Shahar
Drachsler-Cohen, Dana
contents Proving local robustness is crucial to increase the reliability of neural networks. While many verifiers prove robustness in $L_\infty$ $ε$-balls, very little work deals with robustness verification in $L_0$ $ε$-balls, capturing robustness to few pixel attacks. This verification introduces a combinatorial challenge, because the space of pixels to perturb is discrete and of exponential size. A previous work relies on covering designs to identify sets for defining $L_\infty$ neighborhoods, which if proven robust imply that the $L_0$ $ε$-ball is robust. However, the number of neighborhoods to verify remains very high, leading to a high analysis time. We propose covering verification designs, a combinatorial design that tailors effective but analysis-incompatible coverings to $L_0$ robustness verification. The challenge is that computing a covering verification design introduces a high time and memory overhead, which is intensified in our setting, where multiple candidate coverings are required to identify how to reduce the overall analysis time. We introduce CoVerD, an $L_0$ robustness verifier that selects between different candidate coverings without constructing them, but by predicting their block size distribution. This prediction relies on a theorem providing closed-form expressions for the mean and variance of this distribution. CoVerD constructs the chosen covering verification design on-the-fly, while keeping the memory consumption minimal and enabling to parallelize the analysis. The experimental results show that CoVerD reduces the verification time on average by up to 5.1x compared to prior work and that it scales to larger $L_0$ $ε$-balls.
format Preprint
id arxiv_https___arxiv_org_abs_2405_10924
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Boosting Few-Pixel Robustness Verification via Covering Verification Designs
Shapira, Yuval
Wiesel, Naor
Shabelman, Shahar
Drachsler-Cohen, Dana
Machine Learning
Logic in Computer Science
Programming Languages
Proving local robustness is crucial to increase the reliability of neural networks. While many verifiers prove robustness in $L_\infty$ $ε$-balls, very little work deals with robustness verification in $L_0$ $ε$-balls, capturing robustness to few pixel attacks. This verification introduces a combinatorial challenge, because the space of pixels to perturb is discrete and of exponential size. A previous work relies on covering designs to identify sets for defining $L_\infty$ neighborhoods, which if proven robust imply that the $L_0$ $ε$-ball is robust. However, the number of neighborhoods to verify remains very high, leading to a high analysis time. We propose covering verification designs, a combinatorial design that tailors effective but analysis-incompatible coverings to $L_0$ robustness verification. The challenge is that computing a covering verification design introduces a high time and memory overhead, which is intensified in our setting, where multiple candidate coverings are required to identify how to reduce the overall analysis time. We introduce CoVerD, an $L_0$ robustness verifier that selects between different candidate coverings without constructing them, but by predicting their block size distribution. This prediction relies on a theorem providing closed-form expressions for the mean and variance of this distribution. CoVerD constructs the chosen covering verification design on-the-fly, while keeping the memory consumption minimal and enabling to parallelize the analysis. The experimental results show that CoVerD reduces the verification time on average by up to 5.1x compared to prior work and that it scales to larger $L_0$ $ε$-balls.
title Boosting Few-Pixel Robustness Verification via Covering Verification Designs
topic Machine Learning
Logic in Computer Science
Programming Languages
url https://arxiv.org/abs/2405.10924