Research Seminar by LI Jiaying | Selective Faces Assembly - A precise, efficient and scalable approximate method for neural network verification

While deep neural networks(DNNs) are increasingly integrated into real-world applications, their wide adoption into safety critical systems is still in the early stage, due to the lack of correctness guarantees. Ideally, DNNs should be formally verified before being deployed into critical scenarios.

The primary obstacle in DNN verification lies in the complexity posed by non-linear activation functions. Despite several studies to abstract these functions, the status quo is still unsatisfactory. In response, we propose Selective Faces Assembly (SFA), a novel technique that provides precise (albeit not exact), efficient, and scalable approximations, significantly advancing the performance of DNN verification. SFA leverages the interplay between the H- and V-representation of polytopes and creatively approximates a polytope through assembling a selective set of its faces. While initially designed for ReLU functions, the principles of SFA can be applicable to S-shaped functions, such as Sigmoid and Tanh.

In this talk, I will provide a comprehensive overview of the SFA method. After introducing the DNN verification problem and existing approaches, I will elucidate the SFA technique and illustrate how it works for ReLU functions. Next, I will generalise the method and adopt it to approximate S-shaped functions. Finally, I will discuss some potential research opportunities related to SFA. It is important to note that the audience is not expected to have prior knowledge of verification.