English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We improve the scalability of Branch and Bound (BaB) algorithms for formallyproving input-output properties of neural networks. First, we propose novelbounding algorithms based on Lagrangian Decomposition. Previous works have usedoff-the-shelf solvers to solve relaxations at each node of the BaB tree, orconstructed weaker relaxations that can be solved efficiently, but lead tounnecessarily weak bounds. Our formulation restricts the optimization to asubspace of the dual domain that is guaranteed to contain the optimum,resulting in accelerated convergence. Furthermore, it allows for a massivelyparallel implementation, which is amenable to GPU acceleration via modern deeplearning frameworks. Second, we present a novel activation-based branchingstrategy. By coupling an inexpensive heuristic with fast dual bounding, ourbranching scheme greatly reduces the size of the BaB tree compared to previousheuristic methods. Moreover, it performs competitively with a recent strategybased on learning algorithms, without its large offline training cost. Finally,we design a BaB framework, named Branch and Dual Network Bound (BaDNB), basedon our novel bounding and branching algorithms. We show that BaDNB outperformsprevious complete verification systems by a large margin, cutting averageverification times by factors up to 50 on adversarial robustness properties.

Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition