With the rapid growth of machine learning, deep neural networks (DNNs) are now being used in numerous domains. Unfortunately, DNNs are "black-boxes", and cannot be interpreted by humans, which is a substantial concern in safety-critical systems. To mitigate this issue, researchers have begun working on explainable AI (XAI) methods, which can identify a subset of input features that are the cause of a DNN's decision for a given input. Most existing techniques are heuristic, and cannot guarantee the correctness of the explanation provided. In contrast, recent and exciting attempts have shown that formal methods can be used to generate provably correct explanations. Although these methods are sound, the computational complexity of the underlying verification problem limits their scalability; and the explanations they produce might sometimes be overly complex. Here, we propose a novel approach to tackle these limitations. We (1) suggest an efficient, verification-based method for finding minimal explanations, which constitute a provable approximation of the global, minimum explanation; (2) show how DNN verification can assist in calculating lower and upper bounds on the optimal explanation; (3) propose heuristics that significantly improve the scalability of the verification process; and (4) suggest the use of bundles, which allows us to arrive at more succinct and interpretable explanations. Our evaluation shows that our approach significantly outperforms state-of-the-art techniques, and produces explanations that are more useful to humans. We thus regard this work as a step toward leveraging verification technology in producing DNNs that are more reliable and comprehensible.

翻译：随着机器学习的快速发展，深度神经网络（DNN）已被广泛应用于众多领域。然而，DNN作为"黑箱"模型无法被人类解释，这在安全关键系统中引发了重大关切。为解决这一问题，研究人员开始致力于可解释人工智能（XAI）方法的研究，这类方法能够识别导致DNN对特定输入做出决策的输入特征子集。现有技术多为启发式方法，无法保证所提供解释的正确性。相比之下，近期令人振奋的尝试表明，形式化方法可用于生成可证明正确的解释。尽管这些方法具有可靠性，但底层验证问题的计算复杂性限制了其可扩展性，且生成的解释有时可能过于复杂。本文提出了一种应对这些局限性的创新方法。我们：(1) 提出了一种高效的基于验证的极小解释求解方法，该方法构成了全局最小解释的可证明近似；(2) 展示了DNN验证如何协助计算最优解释的下界与上界；(3) 提出了能显著提升验证过程可扩展性的启发式策略；(4) 引入"解释束"概念，以生成更简洁且可解释性更强的解释。评估结果表明，我们的方法显著优于现有最优技术，能够生成对人类更具实用价值的解释。因此，我们将本研究视为利用验证技术构建更可靠、更可理解的DNN的重要一步。