Chao Huang
Wenchao Li
Abstract
Applying neural networks as controllers in dynamical systems has shown great promises. However, it is critical yet challenging to verify the safety of such control systems with neural-network controllers in the loop. Previous methods for verifying neural network controlled systems are limited to a few specific activation functions. In this work, we propose a new reachability analysis approach based on Bernstein polynomials that can verify neural-network controlled systems with a more general form of activation functions, i.e., as long as they ensure that the neural networks are Lipschitz continuous. Specifically, we consider abstracting feedforward neural networks with Bernstein polynomials for a small subset of inputs. To quantify the error introduced by abstraction, we provide both theoretical error bound estimation based on the theory of Bernstein polynomials and more practical sampling based error bound estimation, following a tight Lipschitz constant estimation approach based on forward reachability analysis. Compared with previous methods, our approach addresses a much broader set of neural networks, including heterogeneous neural networks that contain multiple types of activation functions. Experiment results on a variety of benchmarks show the effectiveness of our approach.
- M. Althoff. 2015. An introduction to CORA 2015. In Proc. of ARCH’15 (EPiC Series in Computer Science), Vol. 34. EasyChair, 120--151.Google Scholar
- R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. 1995. The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 1 (1995), 3--34.Google ScholarDigital Library
- Jimmy Ba and Rich Caruana. 2014. Do deep nets really need to be deep?. In Advances in Neural Information Processing Systems. 2654--2662.Google Scholar
- Randall D. Beer, Hillel J. Chiel, and Leon S. Sterling. 1989. Heterogeneous neural networks for adaptive behavior in dynamic environments. In Advances in Neural Information Processing Systems. 577--585.Google Scholar
- M. Berz and K. Makino. 1998. Verified integration of ODEs and flows using differential algebraic methods on high-order taylor models. Reliable Computing 4 (1998), 361--369. Issue 4.Google ScholarCross Ref
- B. M. Brown, D. Elliott, and D. F. Paget. 1987. Lipschitz constants for the Bernstein polynomials of a Lipschitz continuous function. Journal of Approximation Theory 49, 2 (1987), 196--199.Google ScholarDigital Library
- Cristian Bucilă, Rich Caruana, and Alexandru Niculescu-Mizil. 2006. Model compression. In Proceedings of the 12th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining. ACM, 535--541.Google ScholarDigital Library
- X. Chen. 2015. Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models. Ph.D. Dissertation. RWTH Aachen University.Google Scholar
- X. Chen, E. Ábrahám, and S. Sankaranarayanan. 2012. Taylor model flowpipe construction for non-linear hybrid systems. In Proc. of RTSS’12. IEEE Computer Society, 183--192.Google Scholar
- X. Chen, E. Ábrahám, and S. Sankaranarayanan. 2013. Flow*: An analyzer for non-linear hybrid systems. In Proc. of CAV’13 (LNCS), Vol. 8044. Springer, 258--263.Google Scholar
- X. Chen and S. Sankaranarayanan. 2016. Decomposed reachability analysis for nonlinear systems. In 2016 IEEE Real-Time Systems Symposium (RTSS). IEEE Press, 13--24.Google Scholar
- Louis De Branges. 1959. The stone-weierstrass theorem. Proc. Amer. Math. Soc. 10, 5 (1959), 822--824.Google ScholarCross Ref
- T. Dreossi, T. Dang, and C. Piazza. 2016. Parallelotope bundles for polynomial reachability. In HSCC. ACM, 297--306.Google Scholar
- P. S. Duggirala, S. Mitra, M. Viswanathan, and M. Potok. 2015. C2E2: A verification tool for stateflow models. In Proc. of TACAS’15 (LNCS), Vol. 9035. Springer, 68--82.Google Scholar
- S. Dutta, X. Chen, and S. Sankaranarayanan. 2019. Reachability analysis for neural feedback systems using regressive polynomial rule inference. In Hybrid Systems: Computation and Control (HSCC). ACM Press, 157--168.Google Scholar
- S. Dutta, S. Jha, S. Sankaranarayanan, and A. Tiwari. 2018. Output range analysis for deep feedforward neural networks. In NASA Formal Methods Symposium. Springer, 121--138.Google Scholar
- G. Frehse. 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech. In HSCC. Springer, 258--273.Google Scholar
- G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler. 2011. SpaceEx: Scalable verification of hybrid systems. In Proc. of CAV’11 (LNCS), Vol. 6806. Springer, 379--395.Google ScholarDigital Library
- Eduardo Gallestey and Peter Hokayem. 2019. Lecture notes in Nonlinear Systems and Control.Google Scholar
- T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya. 1998. What’s decidable about hybrid automata? Journal of Computer and System Sciences 57, 1 (1998), 94--124.Google ScholarDigital Library
- Geoffrey E. Hinton, Oriol Vinyals, and Jeffrey Dean. 2015. Distilling the knowledge in a neural network. CoRR abs/1503.02531 (2015).Google Scholar
- C. Huang, X. Chen, W. Lin, Z. Yang, and X. Li. 2017. Probabilistic safety verification of stochastic hybrid systems using barrier certificates. TECS 16, 5s (2017), 186.Google ScholarDigital Library
- X. Huang, M. Kwiatkowska, S. Wang, and M. Wu. 2017. Safety verification of deep neural networks. In International Conference on Computer Aided Verification. Springer, 3--29.Google Scholar
- Radoslav Ivanov, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. 2018. Verisig: Verifying safety properties of hybrid systems with neural network controllers. arXiv preprint arXiv:1811.01828 (2018).Google Scholar
- G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer. 2017. Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification. Springer, 97--117.Google Scholar
- S. Kong, S. Gao, W. Chen, and E. M. Clarke. 2015. dReach: Δ-reachability analysis for hybrid systems. In Proc. of TACAS’15 (LNCS), Vol. 9035. Springer, 200--205.Google Scholar
- Timothy P. Lillicrap, Jonathan J. Hunt, Alexander Pritzel, Nicolas Heess, Tom Erez, Yuval Tassa, David Silver, and Daan Wierstra. 2016. Continuous control with deep reinforcement learning. CoRR abs/1509.02971 (2016).Google Scholar
- George G. Lorentz. 2013. Bernstein Polynomials. American Mathematical Soc.Google Scholar
- J. Lygeros, C. Tomlin, and S. Sastry. 1999. Controllers for reachability specifications for hybrid systems. Automatica 35, 3 (1999), 349--370.Google ScholarDigital Library
- K. Makino and M. Berz. 2005. Verified global optimization with taylor model-based range bounders. Transactions on Computers 11, 4 (2005), 1611--1618.Google Scholar
- J. D. Meiss. 2007. Differential Dynamical Systems. SIAM publishers.Google Scholar
- Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Andrei A. Rusu, Joel Veness, Marc G. Bellemare, Alex Graves, Martin Riedmiller, Andreas K. Fidjeland, Georg Ostrovski, et al. 2015. Human-level control through deep reinforcement learning. Nature 518, 7540 (2015), 529.Google Scholar
- Yunpeng Pan, Ching-An Cheng, Kamil Saigol, Keuntaek Lee, Xinyan Yan, Evangelos Theodorou, and Byron Boots. 2018. Agile autonomous driving using end-to-end deep imitation learning. Proceedings of Robotics: Science and Systems. Pittsburgh, Pennsylvania (2018).Google ScholarCross Ref
- S. Prajna and A. Jadbabaie. 2004. Safety verification of hybrid systems using barrier certificates. In HSCC. Springer, 477--492.Google Scholar
- H. L. Royden. 1968. Real Analysis. Krishna Prakashan Media.Google Scholar
- W. Ruan, X. Huang, and M. Kwiatkowska. 2018. Reachability analysis of deep neural networks with provable guarantees. arXiv preprint arXiv:1805.02242 (2018).Google Scholar
- Georgi V. Smirnov. 2002. Introduction to the Theory of Differential Inclusions. Vol. 41. American Mathematical Soc.Google Scholar
- C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, and R. Fergus. 2013. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013).Google Scholar
- W. Xiang and T. T. Johnson. 2018. Reachability analysis and safety verification for neural network control systems. arXiv preprint arXiv:1805.09944 (2018).Google Scholar
- Z. Yang, C. Huang, X. Chen, W. Lin, and Z. Liu. 2016. A linear programming relaxation based approach for generating barrier certificates of hybrid systems. In FM. Springer, 721--738.Google Scholar
- Yuichi Yoshida and Takeru Miyato. 2017. Spectral norm regularization for improving the generalizability of deep learning. arXiv preprint arXiv:1705.10941 (2017).Google Scholar
- F. Zhao. 1992. Automatic Analysis and Synthesis of Controllers for Dynamical Systems Based on Phase-Space Knowledge. Ph.D. Dissertation. Massachusetts Institute of Technology.Google Scholar
Index Terms
- ReachNN: Reachability Analysis of Neural-Network Controlled Systems
Recommendations
A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning-enabled Control Systems
ICCPS '23: Proceedings of the ACM/IEEE 14th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2023)Signal Temporal Logic (STL) has become a popular tool for expressing formal requirements of Cyber-Physical Systems (CPS). The problem of verifying STL properties of neural network-controlled CPS remains a largely unexplored problem. In this paper, we ...
Model-Agnostic Reachability Analysis on Deep Neural Networks
Advances in Knowledge Discovery and Data MiningAbstractVerification plays an essential role in the formal analysis of safety-critical systems. Most current verification methods have specific requirements when working on Deep Neural Networks (DNNs). They either target one particular network category, ...
ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems
Automated Technology for Verification and AnalysisAbstractWe introduce ReachNN*, a tool for reachability analysis of neural-network controlled systems (NNCSs). The theoretical foundation of ReachNN* is the use of Bernstein polynomials to approximate any Lipschitz-continuous neural-network controller with ...
Comments