  Bound propagation based incomplete neural network verifiers such as CROWN are
very efficient and can significantly accelerate branch-and-bound (BaB) based
complete verification of neural networks. However, bound propagation cannot
fully handle the neuron split constraints introduced by BaB commonly handled by
expensive linear programming (LP) solvers, leading to loose bounds and hurting
verification efficiency. In this work, we develop $\beta$-CROWN, a new bound
propagation based method that can fully encode neuron splits via optimizable
parameters $\beta$ constructed from either primal or dual space. When jointly
optimized in intermediate layers, $\beta$-CROWN generally produces better
bounds than typical LP verifiers with neuron split constraints, while being as
efficient and parallelizable as CROWN on GPUs. Applied to complete robustness
verification benchmarks, $\beta$-CROWN with BaB is up to three orders of
magnitude faster than LP-based BaB methods, and is notably faster than all
existing approaches while producing lower timeout rates. By terminating BaB
early, our method can also be used for efficient incomplete verification. We
consistently achieve higher verified accuracy in many settings compared to
powerful incomplete verifiers, including those based on convex barrier breaking
techniques. Compared to the typically tightest but very costly semidefinite
programming (SDP) based incomplete verifiers, we obtain higher verified
accuracy with three orders of magnitudes less verification time. Our algorithm
empowered the $\alpha,\!\beta$-CROWN (alpha-beta-CROWN) verifier, the winning
tool in VNN-COMP 2021. Our code is available at http://PaperCode.cc/BetaCROWN
