在反应式系统中对神经网络进行形式化解释
人工智能
2023-10-06 v3 机器学习
计算机科学中的逻辑
摘要
深度神经网络（DNN）正日益被用作反应式系统中的控制器。然而，DNN 高度不透明，这导致其行动难以解释与论证。为缓解此问题，可解释人工智能（XAI）技术引起了广泛关注，此类技术能够精确定位导致 DNN 采取相应行动的输入特征。现有 XAI 技术通常面临两点局限：（i）它们是启发式的，无法提供解释正确的形式化保证；以及（ii）它们常应用于“一次性”系统，即 DNN 的调用独立于过往调用，而非反应式系统。在此，我们开始弥合这一差距，并提出一种基于形式化 DNN 验证的 XAI 技术，用于推理多步反应式系统。我们提出了高效计算简洁解释的方法，通过利用系统的转移约束来缩减底层验证器所探索的搜索空间。我们在自动化导航领域的两个流行基准上评估了我们的方法，并观察到我们的方法能够高效计算极小与最小解释，显著优于当前最优（SOTA）方法。我们还证明，我们的方法所生成的形式化解释比竞争性的、非验证类的 XAI 技术更为可靠。
引用
@article{arxiv.2308.00143,
title = {Formally Explaining Neural Networks within Reactive Systems},
author = {Shahaf Bassan and Guy Amir and Davide Corsi and Idan Refaeli and Guy Katz},
journal= {arXiv preprint arXiv:2308.00143},
year = {2023}
}
备注
To appear in Proc. 23rd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD)