More Like this

1. Verifying the Safety of Autonomous Systems with Neural Network Controllers

   https://doi.org/10.1145/3419742  

   Ivanov, Radoslav; Carpenter, Taylor J.; Weimer, James; Alur, Rajeev; Pappas, George J.; Lee, Insup (January 2021, ACM Transactions on Embedded Computing Systems)

   This article addresses the problem of verifying the safety of autonomous systems with neural network (NN) controllers. We focus on NNs with sigmoid/tanh activations and use the fact that the sigmoid/tanh is the solution to a quadratic differential equation. This allows us to convert the NN into an equivalent hybrid system and cast the problem as a hybrid system verification problem, which can be solved by existing tools. Furthermore, we improve the scalability of the proposed method by approximating the sigmoid with a Taylor series with worst-case error bounds. Finally, we provide an evaluation over four benchmarks, including comparisons with alternative approaches based on mixed integer linear programming as well as on star sets. 

   more » « less
2. A Data-Driven Hybrid Automaton Framework to Modeling Complex Dynamical Systems

   https://doi.org/10.1109/ICIT58465.2023.10143031  

   Yang, Yejiang; Mo, Zihao; Xiang, Weiming (April 2023, 2023 IEEE International Conference on Industrial Technology (ICIT))

   In this paper, a computationally efficient data-driven hybrid automaton model is proposed to capture unknown complex dynamical system behaviors using multiple neural networks. The sampled data of the system is divided by valid partitions into groups corresponding to their topologies and based on which, transition guards are defined. Then, a collection of small-scale neural networks that are computationally efficient are trained as the local dynamical description for their corresponding topologies. After modeling the system with a neural-network-based hybrid automaton, the set-valued reachability analysis with low computation cost is provided based on interval analysis and a split and combined process. At last, a numerical example of the limit cycle is presented to illustrate that the developed models can significantly reduce the computational cost in reachable set computation without sacrificing any modeling precision. 

   more » « less
3. HyRNN: Hybrid Recurrent Neural Networks for Approximating Hybrid Dynamical Systems

   https://doi.org/10.1609/aaai.v40i30.39709  

   Sanfelice, Ricardo G (March 2026, Proceedings of the AAAI Conference on Artificial Intelligence)

   For a class of hybrid dynamical systems, we show that a recurrent neural network with hybrid dynamics, which we refer to as a hybrid dynamic recurrent neural network (HyRNN), can be constructed to approximate solutions to hybrid systems over bounded (hybrid) time horizons. Specifically, given a desired precision level, we show that a hybrid system with dynamics resembling those of recurrent neural networks for continuous-time and discrete-time systems can be designed so that, for each bounded hybrid time horizon, its solutions are close to the solutions to the given hybrid system. Through the use of universal approximation theorems, we show that the approximation result holds for traditional smooth activation functions, such as sigmoid and arctan, and that extensions to ReLU functions are possible, and characterize the complexity of the proposed HyRNN. 

   more » « less
4. Reachability Analysis of Sigmoidal Neural Networks

   https://doi.org/10.1145/3627991  

   Choi, Sung Woo; Ivashchenko, Michael; Nguyen, Luan V.; Tran, Hoang-Dung (October 2023, ACM Transactions on Embedded Computing Systems)

   This paper extends the star set reachability approach to verify the robustness of feed-forward neural networks (FNNs) with sigmoidal activation functions such as Sigmoid and TanH. The main drawbacks of the star set approach in Sigmoid/TanH FNN verification are scalability, feasibility, and optimality issues in some cases due to the linear programming solver usage. We overcome this challenge by proposing a relaxed star (RStar) with symbolic intervals, which allows the usage of the back-substitution technique in DeepPoly to find bounds when overapproximating activation functions while maintaining the valuable features of a star set. RStar can overapproximate a sigmoidal activation function using four linear constraints (RStar4) or two linear constraints (RStar2), or only the output bounds (RStar0). We implement our RStar reachability algorithms in NNV and compare them to DeepPoly via robustness verification of image classification DNNs benchmarks. The experimental results show that the original star approach (i.e., no relaxation) is the least conservative of all methods yet the slowest. RStar4 is computationally much faster than the original star method and is the second least conservative approach. It certifies up to 40% more images against adversarial attacks than DeepPoly and on average 51 times faster than the star set. Last but not least, RStar0 is the most conservative method, which could only verify two cases for the CIFAR10 small Sigmoid network,δ= 0.014. However, it is the fastest method that can verify neural networks up to 3528 times faster than the star set and up to 46 times faster than DeepPoly in our evaluation. 

   more » « less
5. 𝖲𝖼𝖾𝗇𝖾𝖢𝗁𝖾𝖼𝗄𝖾𝗋 : Boosting Scenario Verification Using Symmetry Abstractions

   Hussein Sibai and Yangge Li and Sayan Mitra (July 2021, Computer Aided Verification. CAV 2021. Lecture Notes in Computer Science(), vol. Springer, Cham)

   Silva, A. and (Ed.)

   We present 𝖲𝖼𝖾𝗇𝖾𝖢𝗁𝖾𝖼𝗄𝖾𝗋, a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. 𝖲𝖼𝖾𝗇𝖾𝖢𝗁𝖾𝖼𝗄𝖾𝗋 converts the scenario verification problem to a standard hybrid system verification problem, and solves it effectively by exploiting structural properties in the plan and the vehicle dynamics. 𝖲𝖼𝖾𝗇𝖾𝖢𝗁𝖾𝖼𝗄𝖾𝗋 uses symmetry abstractions, a novel refinement algorithm, and importantly, is built to boost the performance of any existing reachability analysis tool as a plug-in subroutine. We evaluated 𝖲𝖼𝖾𝗇𝖾𝖢𝗁𝖾𝖼𝗄𝖾𝗋 on several scenarios involving ground and aerial vehicles with nonlinear dynamics and neural network controllers, employing different kinds of symmetries, using different reachability subroutines, and following plans with hundreds of waypoints in complex workspaces. Compared to two leading tools, DryVR and Flow*, 𝖲𝖼𝖾𝗇𝖾𝖢𝗁𝖾𝖼𝗄𝖾𝗋 shows 14× average speedup in verification time, even while using those very tools as reachability subroutines. 

   more » « less