Computer Science Department Seminar: Huan Zhang

Title: “Trustworthy AI via Formal Verification and Adversarial Testing”
Abstract: To apply deep learning to safety-critical tasks, we need to formally verify their trustworthiness, ensuring properties like safety, security, robustness, and correctness. Unfortunately, modern deep neural networks (DNNs) are largely “black boxes”, and existing tools can hardly formally reason about them. In this talk, I will present a new framework for trustworthy AI, relying on novel methods for formal verification and adversarial testing of DNNs. In particular, I will first introduce a novel framework called “linear bound propagation methods” to enable efficient formal verification of deep neural networks, with an example of rigorously proving their safety and robustness. This framework exploits the structure of this NP-hard verification problem to solve it efficiently, and achieves up to three orders of magnitude speedup compared to traditional verification algorithms. My work leads to the open-source α,β-CROWN verifier, the winners of the 2021 and 2022 International Verification of Neural Networks Competitions (VNN-COMP), with applications including image classification, image segmentation, reinforcement learning, and computer systems. Besides verification, I will discuss the complementary problem of disproving the trustworthiness of AI-based systems using adversarial testing, including black-box adversarial attacks to DNNs, and theoretically-principled attacks to deep reinforcement learning. Finally, I will conclude my talk with an outlook on verifying AI models as building blocks for complex systems in various applications, and addressing challenging engineering problems using the bound propagation-based verification framework.
Bio: Huan Zhang is a postdoctoral researcher at Carnegie Mellon University, working with Prof. Zico Kolter. He obtained his Ph.D. in Computer Science at UCLA in 2020, advised by Prof. Cho-Jui Hsieh. Huan’s research 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 on machine learning systems. He is the leader of a multi-institutional team developing the α,β-CROWN neural network verifier, which won VNN-COMP 2022 and VNN-COMP 2021. 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.
Seminar Zoom Link
Additional details: https://www.cs.jhu.edu/department-seminars.