Formal Verification of Neural Networks

With the increasing popularity of neural networks, it is also important to make sure that at least some properties can be guaranteed for neural networks, especially if safety is a major concern for their applications. In this work, techniques and tools for formal verification specifically made for neural networks are studied. The tools are top performers in the VNN-COMP 2022, which is a competition specifically for formally verifying neural networks. By providing a neural network model in the ONNX format, and a specification in the VNNLIB format, the tools can find whether there exists a case where the specification is satisfied, given the model. With this result, several properties can be verified for different applications of neural networks.