Neural predictive monitoring and a comparison of frequentist and Bayesian approaches
Tóm tắt
Neural state classification (NSC) is a recently proposed method for runtime predictive monitoring of hybrid automata (HA) using deep neural networks (DNNs). NSC trains a DNN as an approximate reachability predictor that labels an HA state x as positive if an unsafe state is reachable from x within a given time bound, and labels x as negative otherwise. NSC predictors have very high accuracy, yet are prone to prediction errors that can negatively impact reliability. To overcome this limitation, we present neural predictive monitoring (NPM), a technique that complements NSC predictions with estimates of the predictive uncertainty. These measures yield principled criteria for the rejection of predictions likely to be incorrect, without knowing the true reachability values. We also present an active learning method that significantly reduces the NSC predictor’s error rate and the percentage of rejected predictions. We develop two versions of NPM based, respectively, on the use of frequentist and Bayesian techniques to learn the predictor and the rejection rule. Both versions are highly efficient, with computation times on the order of milliseconds, and effective, managing in our experimental evaluation to successfully reject almost all incorrect predictions. In our experiments on a benchmark suite of six hybrid systems, we found that the frequentist approach consistently outperforms the Bayesian one. We also observed that the Bayesian approach is less practical, requiring a careful and problem-specific choice of hyperparameters.
Tài liệu tham khảo
Alur, R.: Formal verification of hybrid systems. In Proceedings of the Ninth ACM International Conference on Embedded Software (EMSOFT), pages 273–278, Oct (2011)
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)
Chen, X. and Sankaranarayanan, S.: Model predictive real-time monitoring of linear systems. In Real-Time Systems Symposium (RTSS), 2017 IEEE, pages 297–306. IEEE, (2017)
Sha, L.: Using simplicity to control complexity. IEEE Softw. 18(4), 20–28 (2001)
Bartocci, E., Deshmukh, J., Donze, A., Fainekos, G., Maler, O., Nickovic, D. and Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In Lectures on Runtime Verification, pages 135–175. Springer, (2018)
Phan, D., Paoletti, N., Zhang, T., Grosu, R., Smolka, S.A. and Stoller, S.D.: Neural state classification for hybrid systems. In Automated Technology for Verification and Analysis, volume 11138 of Lecture Notes in Computer Science, pages 422–440, (2018)
Vovk, V., Gammerman, A., Shafer G.: Algorithmic learning in a random world. Springer Science & Business Media, Glenn (2005)
Neal, Radford M et al.: MCMC using Hamiltonian dynamics. Handbook of markov chain monte carlo, 2(11):2, (2011)
Jordan, M.I., Ghahramani, Z., Jaakkola, T.S., Saul, L.K.: An introduction to variational methods for graphical models. Mach. Learn. 37(2), 183–233 (1999)
Bortolussi, L., Cairoli, F., Paoletti, N., Smolka, S.A. and Stoller, S.D.: Neural predictive monitoring. In International Conference on Runtime Verification, pages 129–147. Springer, (2019)
Bak, S., Beg, O.A., Bogomolov, S., Johnson, T.T., Nguyen, L.V., Schilling, C.: Hybrid automata: from verification to implementation. Int. J. Softw. Tools Technol. Transf. 21(1), 87–104 (2019)
Gao, S., Kong, S. and Clarke, E.M.: dreal: An smt solver for nonlinear theories over the reals. In International conference on automated deduction, pages 208–214. Springer, (2013)
Chen, Xin, Ábrahám, Erika, Sankaranarayanan, Sriram: Flow*: An analyzer for non-linear hybrid systems. In International Conference on Computer Aided Verification, pages 258–263. Springer, (2013)
Althoff M.: An introduction to CORA 2015. In Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems, (2015)
Bogomolov, S., Forets, M., Frehse, G., Potomkin, K. and Schilling, C,: Juliareach: a toolbox for set-based reachability. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pages 39–44, (2019)
Hornik, K., Stinchcombe, M., White, H., et al.: Multilayer feedforward networks are universal approximators. Neural Netw. 2(5), 359–366 (1989)
Rumelhart, D.E., Hinton, G.E. and Williams, R.J.: Learning internal representations by error propagation. Technical report, California Univ San Diego La Jolla Inst for Cognitive Science, (1985)
Papadopoulos, H.: Inductive conformal prediction: Theory and application to neural networks. In Tools in artificial intelligence, InTech (2008)
Vineeth B., Shen-Shyang H., Vladimir V.: Conformal prediction for reliable machine learning: theory, adaptations and applications. Newnes (2014)
Christopher M Bishop. Pattern recognition and machine learning. Springer, 2006
Gal, Y.: Uncertainty in deep learning. PhD thesis, University of Cambridge, (2016)
MacKay, D.J.C.: A practical bayesian framework for backpropagation networks. Neural Comput. 4(3), 448–472 (1992)
Van der Vaart, A.W.: Asymptotic statistics. Cambridge University Press, Cambridge (2000)
Rasch, D., Pilz, J., Verdooren L.R., and Gebhardt A.: Chapman and Hall/CRC, Optimal experimental design with R (2011)
Massart, P.: The tight constant in the dvoretzky-kiefer-wolfowitz inequality. The annals of Probability, pages 1269–1283, (1990)
Deodato, G., Ball, C. and Zhang, X.: Bayesian neural networks for cellular image classification and uncertainty analysis. bioRxiv, page 824862, 2019
Jordaney, R., Sharad, K., Dash, S.K., Wang, Z., Papini, D., Nouretdinov, I. and Cavallaro, L.: Transcend: Detecting concept drift in malware classification models. In 26th USENIX Security Symposium (USENIX Security 17), pages 625–642, (2017)
Guo, C., Pleiss, G., Sun, Y. and Weinberger, K.Q: On calibration of modern neural networks. In Proceedings of the 34th International Conference on Machine Learning-Volume 70, pages 1321–1330. JMLR. org, (2017)
Bortolussi, L., Cairoli, F., Paoletti, N. and Stoller, S.D.: Conformal predictions for hybrid system state classification. In From Reactive Systems to Cyber-Physical Systems, pages 225–241. Springer, (2019)
Brefeld, U., Geibel, P. and Wysotzki, F.: Support vector machines with example dependent costs. In European Conference on Machine Learning, pages 23–34. Springer, (2003)
Batuwita, R., Palade, V.: Class imbalance learning methods for support vector machines, chapter 5, pages 83–99. John Wiley & Sons, Ltd, (2013)
Rasmussen, C.E., Williams, C.K.I: Gaussian processes for machine learning, volume 1. MIT press Cambridge, (2006)
Boughorbel, S., Jarray, F., El-Anbari, M.: Optimal classifier for imbalanced data using matthews correlation coefficient metric. PloS one 12(6), e0177678 (2017)
Paoletti, N., Liu, K.S., Smolka, S.A. and Lin, S.: Data-driven robust control for type 1 diabetes under meal and exercise uncertainties. In International Conference on Computational Methods in Systems Biology, pages 214–232. Springer, (2017)
Abadi M., Barham P., Chen J., Chen Z., Davis A., Dean J., Devin M., Ghemawat S., Irving G., Isard M., et al.: Tensorflow: A system for large-scale machine learning. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16), pages 265–283, (2016)
Paszke, A., Gross, S., Massa, F., Lerer, A., Bradbury, J., Chanan, G., Killeen, T., Lin, Z., Gimelshein, N., Antiga, L. and Desmaison, A. et al.: Pytorch: An imperative style, high-performance deep learning library. In Advances in Neural Information Processing Systems, pages 8024–8035, (2019)
Chollet, F. et al.: Keras: The Python deep learning library. Astrophysics Source Code Library, (2018)
Tran, D., Kucukelbir, A., Dieng, A.B., Rudolph, M., Liang, D. and Blei, D.M.: Edward: A library for probabilistic modeling, inference, and criticism. arXiv preprint arXiv:1610.09787, (2016)
Bingham, E., Chen, J.P., Jankowiak, M., Obermeyer, F., Pradhan, N., Karaletsos, T., Singh, R., Szerlip, P., Horsfall, P., Goodman, N.D.: Pyro: deep universal probabilistic programming. J. Mach. Learn. Res. 20(1), 973–978 (2019)
Yoon, H., Chou, Y., Chen, X., Frew, E. and Sankaranarayanan, S.: Predictive runtime monitoring for linear stochastic systems and applications to geofence enforcement for uavs. In International Conference on Runtime Verification, pages 349–367. Springer, (2019)
Stanley B., Taylor J.T., Marco C., Lui S.: Real-time reachability for verified simplex design. In Real-Time Systems Symposium (RTSS), 2014 IEEE, pages 138–148. IEEE, (2014)
Sauter, G., Dierks, H., Franzle, M. and Hansen, M.R.: Lightweight hybrid model checking facilitating online prediction of temporal properties. In Proceedings of the 21st Nordic Workshop on Programming Theory, pages 20–22, 2009
Djeridane, B. and Lygeros, J.: Neural approximation of PDE solutions: An application to reachability computations. In Proceedings of the 45th IEEE Conference on Decision and Control, pages 3034–3039. IEEE, (2006)
Royo, V.R., Fridovich-Keil, D., Herbert, S. and Tomlin, C.J.: Classification-based approximate reachability with guarantees applied to safe trajectory tracking. arXiv preprint arXiv:1803.03237, (2018)
Yel, E., Carpenter, T.J., Di Franco, C., Ivanov, R., Kantaros, Y., Lee, I., Weimer, J., Bezzo, N.: Assured runtime monitoring and planning: toward verification of neural networks for safe autonomous operations. IEEE Robotics Automation Magazine 27(2), 102–116 (2020)
Ivanov, R., Weimer, J., Alur, R., Pappas, G.J. and Lee, I.: Verisig: verifying safety properties of hybrid systems with neural network controllers. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pages 169–178, (2019)
Babaee R., Gurfinkel A., Fischmeister S.: Predictive run-time verification of discrete-time reachability properties in black-box systems using trace-level abstraction and statistical learning. In International Conference on Runtime Verification, pages 187–204. Springer, (2018)
Babaee R., Ganesh V., Sedwards S.: Accelerated learning of predictive runtime monitors for rare failure. In International Conference on Runtime Verification, pages 111–128. Springer, (2019)
Qin, X. and Deshmukh, J.V.: Predictive monitoring for signal temporal logic with probabilistic guarantees. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pages 266–267. ACM, (2019)
Dokhanchi, A., Hoxha, B. and Fainekos, G.: On-line monitoring for temporal logic robustness. In International Conference on Runtime Verification, pages 231–246. Springer, (2014)
Deshmukh J.V., Donze A., Ghosh S., Jin X., Juniwal G., Seshia S.A. (2017) Robust online monitoring of signal temporal logic. Formal Methods in System Design 51(1), 5–30
Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous-time Markov chains. Inf. Comput. 247, 235–253 (2016)
Pop, R. and Fulop, P.: Deep ensemble bayesian active learning: Addressing the mode collapse issue in monte carlo dropout via ensembles. arXiv preprint arXiv:1811.03897, (2018)
Gal, Y., Islam, R. and Ghahramani, Z.: Deep bayesian active learning with image data. In Proceedings of the 34th International Conference on Machine Learning-Volume 70, pages 1183–1192. JMLR. org, (2017)
Dayoub, F., Sunderhauf, N. and Corke, P.I.: Episode-based active learning with bayesian neural networks. In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition Workshops, pages 26–28, (2017)
Makili, Lázaro Emílio., Vega Sánchez, Jesús A., Dormido-Canto, Sebastián: Active learning using conformal predictors: application to image classification. Fusion Science and Technology 62(2), 347–355 (2012)
Toccaceli, P., Gammerman, A.: Combination of inductive mondrian conformal predictors. Mach. Learn. 108(3), 489–510 (2019)
Gammerman, A., Vovk, V.: Hedging predictions in machine learning. Comput. J. 50(2), 151–163 (2007)
Shafer, G., Vovk, V.: A tutorial on conformal prediction. J. Mach. Learn. Res. 9, 371–421 (2008)
Balasubramanian, V.N., Gouripeddi, R., Panchanathan, S., Vermillion, J., Bhaskaran, A., & Siegel, R. M.: Support vector machine based conformal predictors for risk of complications following a coronary drug eluting stent procedure. In 2009 36th Annual Computers in Cardiology Conference (CinC), pages 5–8. IEEE, (2009)
Phan, D., Paoletti, N., Zhang, T., Grosu, R., Smolka, S. A., Stoller, S. D.: Neural state classification for hybrid systems. ArXiv e-prints, July (2018)