Statistical model checking (SMC) is a simulation-based formal verification technique to deal with the scalability problem faced by traditional model checking. The main workflow of SMC is to perform iterative simulations. The number of simulations depends on users’ requirement for the verification results, which can be very large if users require a high level of confidence and precision. Therefore, how to perform as fewer simulations as possible while achieving the same level of confidence and precision is one of the core problems of SMC. In this paper, we consider the estimation problem of SMC. Most existing statistical model checkers use the Okamoto bound to decide the simulation number. Although the Okamoto bound is sound, it is well known to be overly conservative. The simulation number decided by the Okamoto bound is usually much higher than it actually needs, which leads to a waste of time and computation resources. To tackle this problem, we propose an efficient, sound and lightweight estimation algorithm using the Clopper-Pearson confidence interval. We perform comprehensive numerical experiments and case studies to evaluate the performance of our algorithm, and the results show that our algorithm uses 40%-60% fewer simulations than the Okamoto bound. Our algorithm can be directly integrated into existing model checkers to reduce the verification time of SMC estimation problems.

Since the discovery of adversarial examples, the local robustness of deep neural networks (DNNs) has received much attention. Moreover, researchers find that DNNs are also sensitive to semantic perturbations like fog, contrast and Gaussian noise. Due to the complexity of semantic perturbations, existing works only focus on local robustness towards some specific perturbations such as brightness and rotation. In this paper, we propose a statistics-based method to certify DNN’s local robustness towards general semantic perturbations. First, we give the formal definitions of semantic perturbations and local semantic robustness. Our definitions are general enough to cover almost all perturbations of concern. Then we develop a statistical certification algorithm. Our evaluations on CIFAR-10 and ImageNet show that compared with the state-of-the-art statistical certification algorithm, our method can provide the same theoretical guarantees using only 3.32%-6.55% of running time.

Measuring robustness of deep neural networks (DNNs) is an important topic for trustworthy AI. Existing methods for verifying local robustness of DNNs usually face the scalability problem and have difficulties to deal with non-linear activation functions and complex semantic perturbations. Existing methods for measuring global robustness usually rely on large datasets, so it is difficult for users without a large dataset to compare the global robustness of different networks. In this paper, we propose two algorithms to measure the local and global robustness of DNNs from the lens of statistical model checking. Compared with the local robustness estimation method using the Okamoto bound, our method can provide the same theoretical guarantee using only 48.6%-74.1% of running time. Our global robustness estimation algorithm can provide high-quality estimation using only 10 images for CIFAR-10 and 50 images for ImageNet, thus can be used in a wider range of scenarios.