Abstract

With the wide application of artificial intelligence (AI) systems, how to strictly ensure the correctness and safety of AI in key applications is an important research topic. Due to the complexity and specificity of AI systems, it is often challenging to adopt traditional formal verification methods in AI systems. In this lecture, I will introduce a methodological and theoretical framework specifically for the formal verification of deep neural networks. It makes use of the special structure of neural network problems, efficiently transmits linear inequalities on neural networks, avoids the high complexity of traditional solving methods, and can realize GPU acceleration for formal verification problems. Based on the neural network verifier α implemented by the framework, β-CROWN has achieved three orders of magnitude faster speedups than traditional algorithms in some formal verification problems, and has won the championship of the International Neural Network Verification Competition (VNN-COMP) for three consecutive years. Finally, I will discuss the recent applications of neural network algorithms in some engineering fields, such as autonomous systems, nonlinear control, computer systems, etc.

Lecturer

Huan Zhang is currently an assistant professor in the Department of Electrical and Computer Engineering at the University of Illinois at Urbana-Champaign (UIUC). Prof. Huan received his B.S. from Zhejiang University in 2012 and his Ph.D. from the University of California, Los Angeles (UCLA) in 2020. His main research interests are the construction of trustworthy AI systems, especially the use of formal verification methods to rigorously prove the security and robustness of deep neural networks. He led the team to develop the α, β-CROWN Neural Network Verifier (https://abcrown.org), which won the first place in the 2021, 2022, and 2023 International Neural Network Verification Competition (VNN-COMP). His awards include IBM Ph.D. fellowship, 2022 Adversarial Machine Learning Rising Star Award, and Schmidt Futures AI2050 Early Career Fellowship.