发表机构
University of Lugano (USI); SUPSI; IDSIA; Florida State University（卢加诺大学; 瑞士南部应用科学与艺术大学; 达尔莫尔人工智能研究所; 佛罗里达州立大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一种以神经元激活为参数、基于SMT求解器的灵活符号框架，用于高效计算深度神经网络的形式化逻辑解释，克服了现有方法在特征关系保证和可扩展性上的局限，并在图像识别和医学基准上验证了其计算效率优势。
AI 中文摘要
分类神经网络（NN）的形式化可解释性是一个活跃的研究领域，它提供了在输入特征空间的连续区域内具有可证明的分类保证的解释。然而，现有技术要么局限于单个输入特征且不保证其关系，要么所提供的解决方案无法扩展到深层架构。本文通过引入一个灵活的形式化框架来解决这些问题，该框架以内部神经元的激活为参数，并使用诸如SMT求解器之类的逻辑引擎，对神经网络行为进行高效、引导式的解释计算。与先前依赖专门神经网络验证器的方法不同，我们的方法产生的解释在形状上不受限制。我们的算法可以在通用逻辑求解器之上实现，将神经网络特定的编码与算法框架分离开来。我们使用来自图像识别和医学领域的大量基准进行了实验，展示了新方法的优势，特别是在计算效率方面。值得注意的是，我们的方法能够对先前基于逻辑的方法无法处理的深层网络进行逻辑解释。
英文摘要
Formal explainability of classifying neural networks (NNs) is an active area of research, providing explanations with provable guarantees of the classification within continuous regions of the input feature space. However, the existing techniques are either limited to individual input features without guarantees on their relations or the provided solutions fail to scale to deep architectures. This paper addresses these issues by introducing a flexible symbolic framework for an efficient, guided computation of explanations of the NN behavior, parametrized by the activations of internal neurons, and using logical engines such as SMT solvers. Unlike prior methods that rely on specialized NN verifiers, our method yields explanations that are not restricted in shape. Our algorithm is implementable on top of a general-purpose logical solver, isolating the NN-specific encoding from the algorithmic framework. We experimented with a wide range of benchmarks from the domains of image recognition and medicine, illustrating the advantages of the new method, particularly in computational efficiency. Notably, our approach enables logical explanation of deep networks not amenable to prior logic-based methods.
