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 blackbox 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\"uchi automaton of exponential size. We show how these can be used to address common verification and interpretation tasks like adversarial robustness, minimum sufficient reasons etc. We report on a proof-of-concept implementation translating DNN to automata on finite words for better efficiency at the cost of losing precision in analysis.
翻译:校验和解释深神经网络(DNN)的特性和行为是一项重要任务,因为它们在应用中普遍使用,包括安全临界系统,以及黑匣子的性质。我们建议采用自动模型理论方法来解决DNN分析中出现的问题。我们表明,一个(特别)弱的B\\"uchi"指数大小的自动图能准确地捕捉到DNN的输入-输出行为。我们表明,如何利用这些方法来处理共同的核查和解释任务,例如对抗性强力、最低限度的充分理由等。我们报告,我们用一个概念证明,将DNND转换为用有限词的自动模型,以便提高效率,而牺牲分析的精确度。