Upcoming Seminars

Abstract: Safety is a fundamental requirement for deploying learning-based systems in the real world. From autonomous vehicles to large language model (LLM) based AI agents, guaranteeing that system trajectories remain within user-specified safety constraints, also known as forward invariance, is central to trustworthy AI and autonomy. Control Barrier Functions (CBFs) provide a principled mechanism for ensuring forward invariance in dynamical systems, but existing approaches face significant challenges in scalability and verifiability to complex or open-world dynamics due to the black-box nature of neural networks. In this talk, I will present my work on verified safety with neural barrier functions, a unified framework that enables provable safety guarantees from neural dynamical systems to modern foundation models. I will first show how to formally and efficiently verify if a learned neural network is a valid CBF, by introducing symbolic derivative bound propagation that tightly bounds the Lie derivative between the Jacobian of neural barrier functions and nonlinear system dynamics. I will then talk about how verification can be used to guide model training, enabling the synthesis of verifiable safety Q-filters even when the underlying system dynamics are parameterized by neural networks. Through verification-in-the-loop training, the well-trained Q-filters can be formally verified based on Hamilton-Jacobi reachability analysis. Finally, I will present our recent advances in open-world safety, where I extend CBF ideas beyond physical dynamical systems. I will show how we model LLM conversation as dynamical systems and use neural barrier functions to defend against multi-turn jailbreak attacks. Overall, the talk unifies these contributions to build a principled and scalable foundation for provably safe AI and autonomy, from classical dynamical systems to modern LLM-based agents.

Abstract: Encrypted control offers a promising solution for enhancing security in networked control systems, enabling direct control operations over encrypted data. However, its implementation is often challenged by the constraints of homomorphic encryption, particularly the requirement that linear dynamic controllers should ``have integer coefficients.’’ This talk explores the rationale behind this requirement and addresses the problem of designing such controllers. Specifically, I will present a recent finding that a stabilizing controller with integer coefficients always exists for any given discrete-time linear time-invariant (LTI) plant, along with a constructive method to find one. Furthermore, I will discuss the problem of converting a pre-designed controller into one with integer coefficients, while preserving the original performance.