Recent works in neural network verification show that cheap incomplete verifiers such as CROWN, based upon bound propagations, can effectively be used in Branch-and-Bound (BaB) methods to accelerate complete verification, achieving significant speedups compared to expensive linear programming (LP) based techniques. However, they cannot fully handle the per-neuron split constraints introduced by BaB like LP verifiers do, leading to looser bounds and hurting their verification efficiency. In this work, we develop $\beta$-CROWN, a new bound propagation based method that can fully encode per-neuron splits via optimizable parameters $\beta$. When the optimizable parameters are jointly optimized in intermediate layers, $\beta$-CROWN has the potential of producing better bounds than typical LP verifiers with neuron split constraints, while being efficiently parallelizable on GPUs. Applied to the complete verification setting, $\beta$-CROWN is close to three orders of magnitude faster than LP-based BaB methods for robustness verification, and also over twice faster than state-of-the-art GPU-based complete verifiers with similar timeout rates. By terminating BaB early, our method can also be used for incomplete verification. Compared to the state-of-the-art semidefinite-programming (SDP) based verifier, we show a substantial leap forward by greatly reducing the gap between verified accuracy and empirical adversarial attack accuracy, from 35% (SDP) to 12% on an adversarially trained MNIST network ($\epsilon=0.3$), while being 47 times faster. Our code is available at https://github.com/KaidiXu/Beta-CROWN
翻译:神经网络核查的近期工程表明,基于定线传播的CROWN等廉价的不完全的校验器可以有效地用于分流和分流(BAB)方法,以加速完整的核查,实现与昂贵线性编程(LP)基于技术相比的大幅加速。然而,它们无法完全处理像LP核查员那样的BAB(BAB)引入的每中子分解限制,导致松散,损害其核查效率。在这项工作中,我们开发了美元(Beta$-CROWN),这是一种基于调频的基于新调频传输的基于新调频度的基于新调频度的传播方法,能够通过可优化参数($\beta$-Ceta)来充分编码每中中中中子的分解。当可选参数在中间层联合优化时,$(Beta-C-CROWN)就有可能比典型的LP(LP-DFRI)更精确的校验系统,同时可以显示我们目前使用的GPU=Qral-ral-r-ral-ral-r