  This paper studies the problem of range analysis for feedforward neural
networks, which is a basic primitive for applications such as robustness of
neural networks, compliance to specifications and reachability analysis of
neural-network feedback systems. Our approach focuses on ReLU (rectified linear
unit) feedforward neural nets that present specific difficulties: approaches
that exploit derivatives do not apply in general, the number of patterns of
neuron activations can be quite large even for small networks, and convex
approximations are generally too coarse. In this paper, we employ set-based
methods and abstract interpretation that have been very successful in coping
with similar difficulties in classical program verification. We present an
approach that abstracts ReLU feedforward neural networks using tropical
polyhedra. We show that tropical polyhedra can efficiently abstract ReLU
activation function, while being able to control the loss of precision due to
linear computations. We show how the connection between ReLU networks and
tropical rational functions can provide approaches for range analysis of ReLU
neural networks.
