A challenge in verifying a closed-loop system with a neural network controller is to be able to approximate the image of a net within a given error bound. We propose an abstract algorithm, to this end, using rational approximations for activation functions and taking advantage of Bernstein expansion. Furthermore, by exploiting monotonicity of activation functions, we propose a fast approximation that can be used for parts of the net which do not require accurate approximation for property verification.
