Analyzing neural network behavior through deep statistical model checking

Abstract

Neural networks (NN) are taking over ever more decisions thus far taken by humans, even though verifiable system-level guarantees are far out of reach. Neither is the verification technology available, nor is it even understood what a formal, meaningful, extensible, and scalable testbed might look like for such a technology. The present paper is an attempt to improve on both the above aspects. We present a family of formal models that contain basic features of automated decision-making contexts and which can be extended with further orthogonal features, ultimately encompassing the scope of autonomous driving. Due to the possibility to model random noise in the decision actuation, each model instance induces a Markov decision process (MDP) as verification object. The NN in this context has the duty to actuate (near-optimal) decisions. From the verification perspective, the externally learnt NN serves as a …

@article{grosAnalyzingNeuralNetworkBehavior2023,
 author = {Timo P. Gros and Holger Hermanns and Jörg Hoffmann and Michaela Klauck and Marcel Steinmetz},
 journal = {International Journal on Software Tools for Technology Transfer (STTT)},
 number = {3},
 pages = {407-426},
 publisher = {Springer Berlin Heidelberg Berlin/Heidelberg},
 title = {Analyzing neural network behavior through deep statistical model checking},
 volume = {25},
 year = {2023}
}