通过布尔变换实现神经网络的全局可解释性

《Neural Networks》：Toward Global Interpretability of Neural Networks via Boolean Transformation

　　摘要：在深度神经网络的部署过程中，可解释性始终是一个核心挑战，尤其是在那些对安全性及决策准确性要求极高的领域。本研究提出了一种统一的框架，用于实现事后全局可解释性，该方法可将包括残差网络和变换器在内的各类神经网络架构转化为基于实值输入与多类输出的等价决策图。这些决策图能够以直观、结构化的形式展现神经网络的整体行为，其中每条路径都对应一条易于理解且可操作的决策规则。我们在构建决策图时的节点合并过程中发现了一种看似反直觉但效果显著的改进方法，该方法能够加快熵值降低的速度，并缩小等价区间大小，从而在保持与原始网络功能等价的前提下显著减小决策图规模。所得到的表示形式不仅有助于分析逻辑特性，如决策边界追踪、等价性检验、鲁棒性分析以及模型计数，还能作为原始神经网络的全局可解释替代模型。实验结果验证了所提方法的有效性与可扩展性，展现了其在实现可靠神经网络分析与验证方面的潜力。

引言：深度神经网络在计算机视觉、自然语言处理以及语音识别等诸多领域取得了显著成就。尽管其实际表现优异，但由于高度非线性的架构以及高维参数空间，这些网络往往被视为“黑箱”，其背后的决策过程难以被理解——Bassan等人（2024年）与Zhang等人（2021年）均有相关研究指出这一点。在那些对安全性及决策准确性要求极高的应用场景中，这种缺乏透明度的特性带来了诸多挑战，因为在此类场景中，理解并验证模型行为与预测精度同样重要。为解决这一问题，人们越来越重视对神经网络决策过程的解析与解释，这也推动了可解释人工智能技术的快速发展。通过为神经网络的决策过程提供可解释的表示形式，可解释人工智能旨在提升现代神经网络的透明度、可靠性与可信度。

在可解释人工智能领域，事后全局可解释性方法因能够通过结构化且易于分析的表示形式来描述神经网络的整体决策行为而备受关注——Du等人（2020年）与Molnar（2018年）均有相关论述。这类方法通过将神经网络计算转化为布尔表达式、决策图以及逻辑电路等符号形式，使得形式化推理任务成为可能，包括鲁棒性验证、可满足性分析、等价性检验以及规则提取等。近期的一些研究已经证明了通过逐神经元布尔转换及决策图构建技术，可以将神经网络转化为符号形式的决策图——Bassan等人（2024年）、Lu与Lee（2025年）、Seidel与Borghoff（2025年）以及Tang等人（2023年）均有过相关探索。这些研究为神经网络的符号推理与验证奠定了重要基础。

然而，将逐神经元符号转换方法应用于现代复杂的神经网络架构仍面临诸多挑战。为确保符号转换的可行性以及形式化推理的合理性，现有方法通常采用一些简化假设，比如使用二进制或离散化的输入输出、结构较为浅层的神经网络，或是维度较低的表示形式——Goel与Klivans（2019年）、Narodytska等人（2018年）、Shi等人（2020年）以及Shih等人（2019年）均有相关研究。虽然这些假设有助于实现逐神经元的符号转换，但要将其应用于残差网络和变换器这类广泛使用的架构则十分困难。残差结构通过跳连接引入了复杂的跨层依赖关系，而注意力机制则能动态地关联输入序列中的上下文信息。这些架构特性大大增加了构建简洁且等价的符号表示的难度。此外，实际的神经网络通常处理的是实值输入与多类输出，这进一步加剧了符号转换与精确推理的难度。

为应对这些挑战，本研究提出了一种统一的框架，用于实现事后全局可解释性，该框架可将各类通用神经网络转化为等价的符号决策图表示形式。在Tang等人（2023年）提出的逐神经元对齐二进制决策图构建方法基础上，本框架进一步拓展了符号转换的应用范围，使其能够处理包含残差结构与注意力机制的架构、实值输入以及多类输出，同时仍保持与原始网络的功能等价性。与传统基于替代模型的可解释性方法不同，本框架注重实现精确的符号等价，而非仅追求行为上的近似模拟。由此生成的决策图能够以清晰、结构化的形式呈现神经网络的决策逻辑，每条路径都对应一条符号化的决策规则。此外，这些表示形式可直接用于后续的形式化分析任务，如鲁棒性评估以及逻辑特性验证。

如图1所示，本框架的一个核心组成部分是通过改进的等价区间生成策略来优化ABDD构建过程。虽然从节点合并的角度来看，这种改进方法似乎有些反直觉，但实验结果表明，它能够在保持函数完全等价的前提下大幅缩小生成的决策图规模。此外，我们还研究了针对实值神经网络的参数化S形函数二进制转换方法，该方法能够在有限近似误差的情况下实现更稳定的符号转换。

本研究的主要贡献可归纳如下：
- 针对现代神经网络架构，开发了一种通用的符号转换框架，该框架能够为包含残差结构与注意力机制、且具有实值输入与多类输出的神经网络生成符号决策图表示。
- 通过优化的等价区间生成策略对ABDD构建过程进行了改进，该策略能够在保持函数完全等价的前提下大幅缩小生成的决策图规模。
- 所得到的符号表示形式还可进一步转换为布尔电路与句子决策图，从而便于开展鲁棒性分析以及特性验证等后续形式化推理任务。

总体而言，本研究将符号转换技术从传统的二进制神经网络扩展到了更为广泛的深度学习架构，为构建具备全局可解释性且可进行形式化分析的神经网络表示形式提供了统一且具备可扩展性的框架。