ASE 2023
Mon 11 - Fri 15 September 2023 Kirchberg, Luxembourg
Thu 14 Sep 2023 11:30 - 11:42 at Room E - Program Verification 2 Chair(s): Martin Kellogg

The rapid development of deep learning has significantly transformed the ecology of the software engineering field. As new data continues to grow and evolve at an explosive rate, the challenge of iteratively updating software built on neural networks has become a critical issue. While the continuous learning paradigm enables networks to incorporate new data and update accordingly without losing previous memories, resulting in a batch of new networks as candidates for software updating, these approaches merely select from these networks by empirically testing their accuracy; they lack formal guarantees for such a batch of networks, especially in the presence of adversarial samples. Existing verification techniques, based on constraint solving, interval propagation, and linear approximation, provide formal guarantees but are designed to verify the properties of individual networks rather than a batch of networks. To address this issue, we analyze the batch verification problem corresponding to several non-traditional machine learning paradigms and further propose a framework named HOBAT (BATch verification for HOmogeneous structural neural networks) to enhance batch verification under reasonable assumptions about the representation of homogeneous structure neural networks, increasing scalability in practical applications. Our method involves abstracting the neurons at the same position in a batch of networks into a single neuron, followed by an iterative refinement process on the abstracted neuron to restore the precision until the desired properties for verification are met. Our method is orthogonal to boundary propagation verification on a single neural network. To assess our methodology, we integrate it with boundary propagation verification and observe significant improvements compared to the vanilla approach. Our experiments demonstrate the enormous potential for verifying large batches of networks in the era of big data.

pdf of HOBAT: Batch Verification for Homogeneous Structural Neural Networks (HOBAT.pdf)421KiB

Thu 14 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:00
Program Verification 2Research Papers / Tool Demonstrations / NIER Track at Room E
Chair(s): Martin Kellogg New Jersey Institute of Technology
10:30
12m
Talk
Expediting Neural Network Verification via Network Reduction
Research Papers
Yuyi Zhong National University of Singapore, Singapore, Ruiwei Wang School of Computing, National University of Singapore, Siau-Cheng Khoo National University of Singapore
Pre-print File Attached
10:42
12m
Talk
SMT Solver Validation Empowered by Large Pre-trained Language Models
Research Papers
Maolin Sun Nanjing University, Yibiao Yang Nanjing University, Yang Wang National Key Laboratory for Novel Software Technology, Nanjing University, Ming Wen Huazhong University of Science and Technology, Haoxiang Jia Huazhong University of Science and Technology, Yuming Zhou Nanjing University
Pre-print File Attached
10:54
12m
Talk
LIV: Invariant Validation Using Straight-Line Programs
Tool Demonstrations
Martin Spiessl LMU Munich, Dirk Beyer LMU Munich
Pre-print Media Attached File Attached
11:06
12m
Talk
CEGAR-PT: A Tool for Abstraction by Program Transformation
Tool Demonstrations
Dirk Beyer LMU Munich, Marian Lingsch-Rosenfeld LMU Munich, Martin Spiessl LMU Munich
Pre-print Media Attached File Attached
11:18
12m
Talk
Symbolic Verification of Fuzzy Logic ModelsRecorded talk
NIER Track
Siang Zhao School of Computer, National University of Defense Technology, China, Zhongyang Li School of Computer, National University of Defense Technology, China, Zhenbang Chen National University of Defense Technology, Ji Wang School of Computer, National University of Defense Technology, China
Pre-print Media Attached
11:30
12m
Talk
HOBAT: Batch Verification for Homogeneous Structural Neural NetworksRecorded talk
Research Papers
Jingyang Li Shanghai Jiao Tong University, Guoqiang Li Shanghai Jiao Tong University
Media Attached File Attached