Utilizing Testing-Based Formal Verification in Neural Networks: A Theoretical Approach *

Neural networks are widely applied across various computer applications, including many safety-critical systems. However, understanding the decision-making behavior of neural networks and verifying their reliability through formal specifications continues to be a topic of ongoing discussion. The first difficulty is to give the precondition and post-condition for neural networks, and the second difficulty also exists in traditional software, i.e., the problem of exploding execution paths. Fortunately, the output range of a neural network is easier to give and when an input is given, we can obtain the activation order of neurons in the neural network. Based on the above facts, we propose DeepTBFV, a method for pre-trained neural networks, which uses a testing-based formal verification algorithm to derive the precondition of the neural network on a specified path by post-condition. Preconditions can be used to verify that a neural network meets a given formal specification, and the behavior of the neural network can also be interpreted by analyzing its preconditions.