BERN-NN: Tight Bound Propagation For Neural Networks Using Bernstein Polynomial Interval Arithmetic
This work addresses the challenge of large errors in bound propagation for neural networks, benefiting researchers and practitioners in formal verification and safety-critical AI applications, though it is an incremental improvement over existing methods.
The paper tackles the problem of computing tight output bounds for neural networks given bounded input sets, which is crucial for model checking and reachability analysis, by introducing BERN-NN, a method that uses Bernstein polynomial interval arithmetic to achieve orders of magnitude tighter bounds and faster performance compared to state-of-the-art verifiers like linear programming and alpha-CROWN.
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.