Verification Properties in Neural Network Verification: Exploration of the Design Space

With neural networks' (NNs) rise in popularity, including in safety-critical areas such as autonomous navigation, verifying their safety has become an important field of research. Due to their "black-box" nature there is no universal method that can accomplish that as of yet; instead there is an assortment of methods for very specific problems using variety of properties and methods.

There is no single NN property universally used in determining its robustness, although some may be used more often then others.

A good example would be epsilon-ball verification, used to measure robustness against adversarial examples - entries that are very similar to ones classified correctly and yet given the wrong label by the NN. This property uses the radius (epsilon) of a ball around input data point that is safe - that is there are no adversary examples within it - as a measure.

A more geometrical approach has indicated connection between the adversarial robustness and the shape of manifold modelled from input data of a
NN. Another method that has gained interest is verification via reachability analysis - given an input estimation looking at the region of outputs that
can be returned. Then there exists a different vein of probabilistic verification that has recently gained popularity. This approach can work both with the worst-case scenario of adversarial robustness as well as analysis of input data with random uncertainties - its goal being the estimation of probability that the result will end up in the safe region. However as this is a relatively new field most of the solutions analyse only some known perturbation of an input that is known to be "safe".

In summary there is a broad array of verification methods that have been developed to work for specific NN types - from a whole category, for example applying to Recurrent NNs, to some very limited cases. Depending on the tool in question they use different parameters to give judgment on the quality of the network. The fragmented nature of available solutions makes it challenging to identify all the gaps in current state-of-the-art but with each small, specific solution we are getting closer to the remote goal of a universal tool of some kind.