CISE Seminar: Morteza Lahijanian, Assistant Professor, University of Colorado Boulder

Verification and Control Synthesis for Stochastic Neural Network Dynamic Models

Neural networks (NNs) are emerging as powerful tools to represent the state evolution of complex dynamical systems with complicated physics or black-box components. Such models, referred to as NN dynamic models (NNDMs), use iterative noisy predictions of NN to estimate a distribution of system trajectories over time. Despite their accuracy, formal reasoning of NNDMs is known to be a challenging problem and remains largely unexplored.

In this talk, I present our recent work on verification and control synthesis for NNDMs with formal guarantees. I first show that safety verification of NNDMs can be performed efficiently by synthesizing a stochastic barrier function using a convex optimization problem, which in turn provides a lower bound on the system's safety probability. A key step in the method is the employment of the recent convex relaxation results for NNs. I also show that, by exploiting the convexity of such barrier functions, we can generate minimally-invasive controllers to maximize the safety probability via a linear program. Then, I introduce a generalization framework for formal reasoning about NNDMs by showing that NNDMs can be formally abstracted into Interval Markov Decision Processes (IMDPs). Therefore, their verification and control synthesis against complex specifications, such as linear temporal logic formulas, can simply be performed by using off-the-shelf tools for IMDPs. Finally, I illustrate the computational tractability and scalability of these approaches by presenting benchmarks on NNDMs with architectures of up to 5 hidden layers and hundreds of neurons per layer.

Morteza Lahijanian is an assistant professor in the Aerospace Engineering Sciences department, an affiliated faculty at the Computer Science department, and the director of the Assured, Reliable, and Interactive Autonomous (ARIA) Systems group at the University of Colorado Boulder. He received a B.S. in Bioengineering at the University of California, Berkeley and a PhD in Mechanical Engineering at Boston University. He served as a postdoctoral scholar in Computer Science at Rice University. Prior to joining CU Boulder, he was a research scientist in the department of Computer Science at the University of Oxford. His awards include Ella Mae Lawrence R. Quarles Physical Science Achievement Award, Jack White Engineering Physics Award, NSF GK-12 Fellowship, and Wadham College Research Fellowship. Dr. Lahijanian's research interests span the areas of control theory, stochastic hybrid systems, formal methods, machine learning, and game theory with applications in robotics, particularly, motion planning, strategy synthesis, model checking, and human-robot interaction. His lab develops novel theoretical foundations and computational frameworks to enable reliable and intelligent autonomy. The emphasis is especially on safe autonomy through correct-by-construction algorithmic approaches.

Faculty Host: Sean Andersson

Student Host: Ahmad Ghandi