| _version_ | 1866902114811248640 |
|---|---|
| author | DenBleyker, Bennett Davis, Mason Smith, Joshua Swaminathan, Viswanathan Zhang, Zhen |
| author_facet | DenBleyker, Bennett Davis, Mason Smith, Joshua Swaminathan, Viswanathan Zhang, Zhen |
| contents | <p>Formally verifying and improving the adversarial robustness of deep neural networks is extremely challenging. Existing verification tools face a fundamental tradeoff: abstract interpretation scales to large networks but sacrifices completeness, while SMT solvers are complete but do not scale; and both frequently return <code>UNKNOWN</code> on large or complex input regions, leaving users with no actionable result. Improving the adversarial robustness of deep neural networks requires retraining on counterexamples representative of the full range of unsafe behavior, but generating such counterexamples is computationally expensive. We present <span>VeRAPAk</span> (Verification for Robust neural<br>networks through Abstraction, Partitioning and Attack methods), an adversarial robustness verification framework that resolves both problems through iterative refinement combined with targeted falsification. Rather than verifying a region in a single pass, <span>VeRAPAk </span>progressively subdivides uncertain regions into smaller subproblems where verification eventually succeeds; this enables incomplete tools to achieve practical completeness where they would otherwise fail. At each subdivision, <span>VeRAPAk</span> also searches for counterexamples using RFGSM: a novel, randomized variant of the Fast Gradient Sign Method. Unlike FGSM, which generates counterexamples along a single gradient direction, RFGSM spans an <em>m</em>-dimensional hyperplane. Combined with the iterative subdivision, this produces a <em>covering set</em> of adversarial examples distributed approximately uniformly across the unsafe subregion. Covering sets are experimentally shown to yield improved adversarial retraining outcomes compared to standard single-point gradient methods and unpartitioned baselines. Beyond these contributions, <span>VeRAPAk</span>'s engines are fully interchangeable, making the framework compatible with any existing or future verification, falsification, or partitioning strategy.</p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_20060113 |
| institution | Zenodo |
| language | |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | VeRAPAk: Distributed Counterexample Generation via Iterative Neural Network Verification and Falsification DenBleyker, Bennett Davis, Mason Smith, Joshua Swaminathan, Viswanathan Zhang, Zhen <p>Formally verifying and improving the adversarial robustness of deep neural networks is extremely challenging. Existing verification tools face a fundamental tradeoff: abstract interpretation scales to large networks but sacrifices completeness, while SMT solvers are complete but do not scale; and both frequently return <code>UNKNOWN</code> on large or complex input regions, leaving users with no actionable result. Improving the adversarial robustness of deep neural networks requires retraining on counterexamples representative of the full range of unsafe behavior, but generating such counterexamples is computationally expensive. We present <span>VeRAPAk</span> (Verification for Robust neural<br>networks through Abstraction, Partitioning and Attack methods), an adversarial robustness verification framework that resolves both problems through iterative refinement combined with targeted falsification. Rather than verifying a region in a single pass, <span>VeRAPAk </span>progressively subdivides uncertain regions into smaller subproblems where verification eventually succeeds; this enables incomplete tools to achieve practical completeness where they would otherwise fail. At each subdivision, <span>VeRAPAk</span> also searches for counterexamples using RFGSM: a novel, randomized variant of the Fast Gradient Sign Method. Unlike FGSM, which generates counterexamples along a single gradient direction, RFGSM spans an <em>m</em>-dimensional hyperplane. Combined with the iterative subdivision, this produces a <em>covering set</em> of adversarial examples distributed approximately uniformly across the unsafe subregion. Covering sets are experimentally shown to yield improved adversarial retraining outcomes compared to standard single-point gradient methods and unpartitioned baselines. Beyond these contributions, <span>VeRAPAk</span>'s engines are fully interchangeable, making the framework compatible with any existing or future verification, falsification, or partitioning strategy.</p> |
| title | VeRAPAk: Distributed Counterexample Generation via Iterative Neural Network Verification and Falsification |
| url | https://doi.org/10.5281/zenodo.20060113 |