Program and Invited Speakers

Abstract: With the rise of learned systems enabling embodied and human-centric domains such as robotics and driving, we can no longer rely on conventional techniques to verify the correctness of such systems. While it is commonly agreed that safety guarantees must be adhered to to avoid absolute harm, the precise ways in which robots can now interact with humans are both varied and extremely nuanced, making formal verification harder to frame formally and solve for the vast majority of tasks capable of being solved today. We discuss several recent planning and control approaches proposed toward bridging this gap. We begin by examining the role that formal specifications can play in serving as a basis for learning how to undertake a task, then use the specification to plan and account for various human-aware risk factors at execution time. We then examine the role of learned inference and assistance schemes in guiding a human away from unsafe outcomes, and how our approach can encourage human-robot fluency and combat undesirable “automation surprise” brought about by conventional safety shielding techniques. Throughout the talk, we highlight our work in the context of various full- and semi-autonomous driving case studies.

Abstract: As neural networks (NNs) increasingly govern safety-critical autonomous systems, ensuring formal guarantees like stability and safety remains a fundamental challenge. In this talk, I will present α,β-CROWN - an award-winning, GPU-accelerated verification framework designed to address scalability and flexibility challenges in neural network verification problems, such as the verification of NN-controlled systems. The framework is based on the principle of “linear bound propagation”, which exploits the problem structure by efficiently propagating linear inequalities on neural networks and dynamical systems. These linear inequalities can be strengthened with branch-and-bound to automatically prove various properties of a neural network controlled system with little manual derivations. I will showcase recent applications of the α,β-CROWN toolbox in control, including formal stability and contraction analysis of NN-controlled systems in both discrete and continuous-time settings.

Abstract: In recent years, neural networks have been increasingly deployed for decision-making in autonomous systems. While they offer substantial computational advantages, ensuring the safety and reliability of these learning-enabled components remains a significant challenge due to their high dimensionality and inherent nonlinearity. In this talk, I will present theoretical and algorithmic tools for certifying the safety of closed-loop systems with neural network controllers. I study safety from a reachability perspective and establish conditions for system safety based on the system’s reachable sets. To enable scalable analysis, I leverage concepts from monotone systems theory to develop computationally efficient over-approximations of reachable sets in nonlinear dynamical systems. By integrating this reachability framework with state-of-the-art neural network verification algorithms, I introduce an efficient reachability approach that provides rigorous safety guarantees for neural network-controlled systems. A key feature of this approach is its ability to capture the stabilizing effect of the neural network controller in the overall safety analysis.

Abstract: Accelerated by rapid advances in machine learning and AI, there has been tremendous success in the design of learning-enabled autonomous systems in areas such as autonomous driving, intelligent transportation, and robotics. However, these exciting developments are accompanied by new fundamental challenges that arise regarding the safety and reliability of these increasingly complex control systems in which sophisticated algorithms interact with unknown environments. In this talk, I will provide new insights and discuss exciting opportunities to address these challenges.

Imperfect learning algorithms, system unknowns, and uncertain environments require design techniques to rigorously account for uncertainties. I advocate for the use of conformal prediction (CP) — a statistical tool for uncertainty quantification — due to its simplicity, generality, and efficiency as opposed to existing optimization-based neural network verification techniques that are either conservative or not scalable. I first provide an introduction to CP for the non-expert who is interested in applying CP to address real-world engineering problems. My goal is then to show how we can use CP to solve the problem of predicting failures of learning-enabled systems during their operation. Particularly, we leverage CP and design two predictive runtime verification algorithms (an accurate and an interpretable version) that compute the probability that a high-level system specifications is violated. Finally, we will discuss how we can use robust versions of CP to deal with distribution shifts that arise when the deployed learning-enabled system is different from the system during design time.