Generate and Verify: Semantically Meaningful Formal Analysis of Neural Network Perception Systems

Testing remains the primary method to evaluate the accuracy of neural network\nperception systems. Prior work on the formal verification of neural network\nperception models has been limited to notions of local adversarial robustness\nfor classification with respect to individual image inputs. In this work, we\npropose a notion of global correctness for neural network perception models\nperforming regression with respect to a generative neural network with a\nsemantically meaningful latent space. That is, against an infinite set of\nimages produced by a generative model over an interval of its latent space, we\nemploy neural network verification to prove that the model will always produce\nestimates within some error bound of the ground truth. Where the perception\nmodel fails, we obtain semantically meaningful counter-examples which carry\ninformation on concrete states of the system of interest that can be used\nprogrammatically without human inspection of corresponding generated images.\nOur approach, Generate and Verify, provides a new technique to gather insight\ninto the failure cases of neural network perception systems and provide\nmeaningful guarantees of correct behavior in safety critical applications.\n