Resumen
Among recent publications containing an overview and systematization of algorithms for formal verification of neural networks, a classification of algorithms is proposed which is based on three following properties: reachability, optimization, and search. Reachability-based methods select data from a range of input values based on predefined constraints on the input values, and approximate this set using symbolic mathematical constructs. The main problem of this approach is overapproximation, i.e., the output set is too wide. Another big problem is preservation of linearity after applying the ReLU activation function, which is necessary for applying the backpropagation algorithm. In present article we analyze, compare, and sistemathize mathematical constructions and attempts to approximate the point data by flat continuous sets with the least possible approximation. We also discuss the most effective methods of solving the problem of applying the ReLU activation function to symbolic elements.