Neural networks are increasingly deployed in real-world safety-critical
domains such as autonomous driving, aircraft collision avoidance, and malware
detection. However, these networks have been shown to often mispredict on
inputs with minor adversarial or even accidental perturbations. Consequences of
such errors can be disastrous and even potentially fatal as shown by the recent
Tesla autopilot crash. Thus, there is an urgent need for formal analysis
systems that can rigorously check neural networks for violations of different
safety properties such as robustness against adversarial perturbations within a
certain $L$-norm of a given image. An effective safety analysis system for a
neural network must be able to either ensure that a safety property is
satisfied by the network or find a counterexample, i.e., an input for which the
network will violate the property. Unfortunately, most existing techniques for
performing such analysis struggle to scale beyond very small networks and the
ones that can scale to larger networks suffer from high false positives and
cannot produce concrete counterexamples in case of a property violation. In
this paper, we present a new efficient approach for rigorously checking
different safety properties of neural networks that significantly outperforms
existing approaches by multiple orders of magnitude. Our approach can check
different safety properties and find concrete counterexamples for networks that
are 10$\times$ larger than the ones supported by existing analysis techniques.
We believe that our approach to estimating tight output bounds of a network for
a given input range can also help improve the explainability of neural networks
and guide the training process of more robust neural networks.

本文提出了一种有效的方法来严格检查神经网络的不同安全属性，可以检查不同的安全属性并找到具体的反例，比现有方法的性能提高了数个数量级，这种方法也有助于提高神经网络的可解释性并指导训练更加稳健的神经网络。