Applying deep learning to safety-critical tasks requires us to guarantee 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. My talk presents a new framework for trustworthy AI, relying on novel methods for formal verification and adversarial testing of DNNs. In particular, I will introduce a novel framework called “linear bound propagation methods” to enable efficient formal verification of DNNs, with an example of rigorously proving their safety and robustness. By exploiting the structure of this problem, my framework achieves up to three orders of magnitude speedup compared to traditional algorithms. My work led to the open-source α,β-CROWN verifier, with applications in computer vision, computer systems, non-linear control, and autonomous systems. Besides verification, I will also discuss the complementary problem of disproving the trustworthiness of AI-based systems using adversarial testing, including black-box adversarial attacks to computer vision, and a theoretically-principled attack to deep reinforcement learning.
Huan Zhang is an assistant professor in ECE at UIUC, joined recently in Fall 2023. 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.