  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
