POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom

The intrinsic complexity of deep neural networks (DNNs) makes it challenging to verify not only the networks themselves but also the hosting DNN-controlled systems. Reachability analysis of these systems faces the same challenge. Existing approaches rely on overapproximating DNNs using simpler polynomial models. However, they suffer from low efficiency and large overestimation, and are restricted to specific types of DNNs. This paper presents a novel abstraction-based approach to bypass the crux of over-approximating DNNs in reachability analysis. Specifically, we extend conventional DNNs by inserting an additional abstraction layer, which abstracts a real number to an interval for training. The inserted abstraction layer ensures that the values represented by an interval are indistinguishable to the network for both training and decision-making. Leveraging this, we devise the first blackbox reachability analysis approach for DNN-controlled systems, where trained DNNs are only queried as black-box oracles for the actions on abstract states. Our approach is sound, tight, efficient, and agnostic to any DNN type and size. The experimental results on a wide range of benchmarks show that the DNNs trained by using our approach exhibit comparable performance, while the reachability analysis of the corresponding systems becomes more amenable with significant tightness and efficiency improvement over the state-of-the-art white-box approaches.

Tue 16 Jan

Displayed time zone: London change

14:00 - 15:30
Session 7: Probabilistic and Quantum Programs, Neural NetworksVMCAI at Marconi Room
Chair(s): Andreas Podelski University of Freiburg
14:00
20m
Talk
Guaranteed inference for probabilistic programs: a parallelisable, small-step operational approach
VMCAI
Michele Boreale UniversitĂ  di Firenze, Luisa Collodi University of Florence
14:20
20m
Talk
Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
VMCAI
Yuxin Deng East China Normal University, Huiling Wu East China Normal University, Ming Xu East China Normal University
14:40
20m
Talk
Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
VMCAI
Jiaxu Tian East China Normal University, Dapeng Zhi East China Normal University, Si Liu ETH Zurich, Peixin Wang University of Oxford, Guy Katz Hebrew University, Min Zhang East China Normal University
15:00
20m
Talk
Verification of Neural Networks’ Local Differential Classification Privacy
VMCAI
Roie Reshef Technion, Anan Kabaha Technion, Israel Institute of Technology, Olga Seleznova Technion, Dana Drachsler Cohen Technion
15:20
10m
Talk
AGNES: Abstraction-guided Framework for Deep Neural Networks Security
VMCAI