Verifying And Interpreting Neural Networks using Finite Automata
This work addresses the black-box nature of DNNs for applications in safety-critical domains, representing an incremental advancement in formal methods for neural network analysis.
The paper tackles the problem of verifying and interpreting deep neural networks by proposing an automata-theoretic approach, showing that DNN behavior can be precisely captured by a weak Büchi automaton to address tasks like adversarial robustness and minimum sufficient reasons.
Verifying properties and interpreting the behaviour of deep neural networks (DNN) is an important task given their ubiquitous use in applications, including safety-critical ones, and their black-box nature. We propose an automata-theoric approach to tackling problems arising in DNN analysis. We show that the input-output behaviour of a DNN can be captured precisely by a (special) weak Büchi automaton and we show how these can be used to address common verification and interpretation tasks of DNN like adversarial robustness or minimum sufficient reasons.