  In this paper, we present BERN-NN as an efficient tool to perform bound
propagation of Neural Networks (NNs). Bound propagation is a critical step in
wide range of NN model checkers and reachability analysis tools. Given a
bounded input set, bound propagation algorithms aim to compute tight bounds on
the output of the NN. So far, linear and convex optimizations have been used to
perform bound propagation. Since neural networks are highly non-convex,
state-of-the-art bound propagation techniques suffer from introducing large
errors. To circumvent such drawback, BERN-NN approximates the bounds of each
neuron using a class of polynomials called Bernstein polynomials. Bernstein
polynomials enjoy several interesting properties that allow BERN-NN to obtain
tighter bounds compared to those relying on linear and convex approximations.
BERN-NN is efficiently parallelized on graphic processing units (GPUs).
Extensive numerical results show that bounds obtained by BERN-NN are orders of
magnitude tighter than those obtained by state-of-the-art verifiers such as
linear programming and linear interval arithmetic. Moreoveer, BERN-NN is both
faster and produces tighter outputs compared to convex programming approaches
like alpha-CROWN.
