  The most scalable approaches to certifying neural network robustness depend
on computing sound linear lower and upper bounds for the network's activation
functions. Current approaches are limited in that the linear bounds must be
handcrafted by an expert, and can be sub-optimal, especially when the network's
architecture composes operations using, for example, multiplication such as in
LSTMs and the recently popular Swish activation. The dependence on an expert
prevents the application of robustness certification to developments in the
state-of-the-art of activation functions, and furthermore the lack of tightness
guarantees may give a false sense of insecurity about a particular model. To
the best of our knowledge, we are the first to consider the problem of
automatically computing tight linear bounds for arbitrary n-dimensional
activation functions. We propose LinSyn, the first approach that achieves tight
bounds for any arbitrary activation function, while only leveraging the
mathematical definition of the activation function itself. Our approach
leverages an efficient heuristic approach to synthesize bounds that are tight
and usually sound, and then verifies the soundness (and adjusts the bounds if
necessary) using the highly optimized branch-and-bound SMT solver, dReal. Even
though our approach depends on an SMT solver, we show that the runtime is
reasonable in practice, and, compared with state of the art, our approach often
achieves 2-5X tighter final output bounds and more than quadruple certified
robustness.
