 |
Center for Nonlinear Studies |
Formal verification methods for deep neural networks (DNNs) aim to rigorously guarantee the trustworthiness of DNNs, ensuring properties like safety, security, robustness, and correctness even under malicious scenarios. These guarantees are essential for applying DNNs in mission-critical applications, such as autonomous systems and medical devices. In this talk, I will first introduce the concept of DNN verification and the problem formulation. Then, I will discuss a novel framework called "linear bound propagation methods" to enable efficient formal verification of large deep neural networks. By exploiting the structure of this problem, this framework achieves up to three orders of magnitude speedup compared to traditional algorithms and leads to the award-winning α,β-CROWN neural network verifier. Finally, I will discuss a few applications and potential usage of DNN verification, such as autonomous systems, non-linear control, and computer systems.
Bio: : Huan Zhang is an assistant professor in the Department of Electrical and Computer Engineering at the University of Illinois Urbana-Champaign (UIUC). Huan's work aims to build trustworthy AI systems that can be safely and reliably used in mission-critical tasks, with a focus on using formal verification techniques to give provable performance guarantees for machine learning. He leads a multi-institutional team developing the α,β-CROWN neural network verifier, which won VNN-COMP 2021, 2022, and 2023. He has received several awards, including an IBM Ph.D. fellowship, the 2021 Adversarial Machine Learning Rising Star Award, and a Schmidt Futures AI2050 Early Career Fellowship.
Host: Wenting Li