Towards Dynamic Oracle-guided Synthesis of Abstractions for Deep Neural Networks
23/09/2020
Speaker
Teodora Baluta
Abstract
Despite the success of deep neural networks to increasingly more application domains, their trustworthiness remains a crucial open challenge. To address this challenge, both testing and verification techniques have been proposed. But these existing techniques provide either scalability to large networks or formalguarantees, not both.
We propose a new approach to analyzing DNNs based on abstraction synthesis. In abstraction synthesis, we learn abstractions from concrete values observed for each neuron under dynamically generated inputs. We then query an oracle (e.g. a complete solver) to check if guessed candidate abstractions for each fragment are sound, i.e. they over-approximate all possible concrete values. If not, we repair our candidate abstractions to either relax or tighten them and then iterate until we exhaust the available computational budget. We call this approach DOSA or Dynamic Oracle-guided Synthesis of Abstractions. We show preliminary results where this approach is useful for verifying properties ofrobustness.