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

随着神经网络（NN）的普及，包括在自主导航等安全关键领域，验证其安全性已成为一个重要的研究领域。由于它们的“黑箱”性质，目前还没有通用的方法可以实现这一点;相反，对于非常具体的问题，有各种各样的方法，使用各种属性和方法。没有一个单一的NN属性普遍用于确定其鲁棒性，尽管有些属性可能比其他属性使用得更频繁。一个很好的例子是ε球验证，用于测量对抗性示例的鲁棒性-条目与正确分类的条目非常相似，但NN给出了错误的标签。该属性使用安全的输入数据点周围的球的半径（λ）-也就是说其中没有对手的例子-作为度量。一种更具几何性的方法表明了对抗鲁棒性与从aNN的输入数据建模的流形形状之间的联系。另一种引起兴趣的方法是通过可达性分析进行验证-给定一个输入估计，查看可以返回的输出区域。然后，存在一种不同的概率验证方法，最近流行起来。这种方法既可以用于对抗鲁棒性的最坏情况，也可以用于分析具有随机不确定性的输入数据-其目标是估计结果最终处于安全区域的概率。然而，由于这是一个相对较新的领域，大多数解决方案仅分析已知为“安全”的输入的一些已知扰动。总之，已经开发了一系列广泛的验证方法，用于特定NN类型-从整个类别，例如应用于递归NN，到一些非常有限的情况。根据所讨论的工具，他们使用不同的参数来判断网络的质量。现有解决方案的分散性使得识别当前最先进技术中的所有差距变得非常具有挑战性，但是通过每个小的特定解决方案，我们正在接近某种通用工具的遥远目标。

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 aNN. Another method that has gained interest is verification via reachability analysis - given an input estimation looking at the region of outputs thatcan 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.