Formal Verification for Counting Unsafe Inputs in Deep Neural Networks

Traditionally, Formal Verification (FV) of Deep Neural Networks (DNN) can be employed to check whether a DNN is unsafe w.r.t. some given property (i.e., whether there is at least one unsafe input configuration). However, the binary answer typically returned could be not informative enough for other purposes, such as shielding, model selection, or training improvements. In this paper, we introduce the #DNN-Verification problem, which involves counting the number of input configurations of a DNN that result in a violation of a particular safety property. We analyze the complexity of this problem and propose a novel approach that returns the exact count of violations. Due to the #P-completeness of the problem, we also propose a randomized, approximate method that provides a provable probabilistic bound of the correct count while significantly reducing computational requirements tested on a set of safety-critical benchmarks.