Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound


Loading...

Date

2022

Publication Type

Conference Paper

ETH Bibliography

yes

Citations

Altmetric

Data

Abstract

State-of-the-art neural network verifiers are fundamentally based on one of two paradigms: encoding the whole problem via tight multi-neuron convex relaxations or applying a Branch-and-Bound (BaB) procedure which leverages imprecise but fast bounds on a large number of easier subproblems. The former can better capture complex multi-neuron dependencies but sacrifices completeness due to inherent precision limits of convex relaxations. The latter enables complete verification yet becomes increasingly ineffective on larger and more challenging networks. In this work, we present a novel complete verifier which combines the strengths of both paradigms: it leverages multi-neuron relaxations and an efficient, GPU-based dual optimizer to drastically reduce the number of subproblems generated during the BaB process. An extensive evaluation demonstrates that our verifier achieves new state-of-the-art results on both established benchmarks as well as networks with significantly higher accuracy than previously considered. The latter result (up to 26% certification gains) indicates meaningful progress towards creating verifiers that can handle practically relevant networks.

Publication status

published

Editor

Book title

The Tenth International Conference on Learning Representations (ICLR 2022)

Journal / series

Volume

Pages / Article No.

Publisher

OpenReview

Event

10th International Conference on Learning Representations (ICLR 2022)

Edition / version

Methods

Software

Geographic location

Date collected

Date created

Subject

Adversarial robustness; Certified Robustness; Neural Network Verification

Organisational unit

03948 - Vechev, Martin / Vechev, Martin check_circle

Notes

Poster presented on April 27, 2022.

Funding

Related publications and datasets