跳转至

从信息流视角看可解释性需求：规范与验证

文章背景与核心概要

本文从信息流的全新视角探讨了可解释人工智能（XAI）系统的需求规范与验证问题。作者指出，可解释系统向交互智能体传达“特定效果为何发生”的信息，这本质上是一种“正向信息流”，必须与可能导致隐私泄露等风险的“负向信息流”进行精确的权衡与规范。

由于可解释性和隐私保护都根植于对智能体认知状态的推理，该研究引入了扩展了“反事实因果量词”的认知时序逻辑（Epistemic Temporal Logic）。该方法不仅能够将可解释性明确定义为系统级需求，还提供了针对有限状态模型的验证算法、原型实现及基准测试，成功实现了对可解释系统与不可解释系统的精准区分。

Summary

Summary

Explainable AI systems provide interacting agents with information explaining why specific effects occur. This paper frames explainability as a positive information flow that must be precisely specified, verified, and carefully balanced against negative information flow (such as privacy violations). Because both explainability and privacy fundamentally rely on reasoning about agent knowledge, the authors utilize epistemic temporal logic extended with quantification over counterfactual causes. This methodology enables the specification of explainability as a system-level requirement and introduces verification algorithms, prototype implementations, and benchmarks to distinguish between explainable and unexplainable systems.

Metadata

Metadata

  • arXiv ID: arXiv:2509.01479 [cs.LO]
  • Subjects: Logic in Computer Science (cs.LO), Artificial Intelligence (cs.AI)
  • Authors: Bernd Finkbeiner, Hadar Frenkel, Julian Siber
  • Submitted: September 1, 2025
  • Last Revised: August 25, 2026 (Version v4)
  • DOI: 10.48550/arXiv.2509.01479
  • Comments: Extended and corrected version of the paper presented at the 22nd International Conference on Principles of Knowledge Representation and Reasoning (KR 2025).

Abstract

Abstract

Explainable systems expose information about why certain observed effects are happening to the agents interacting with them. We argue that this constitutes a positive flow of information that needs to be specified, verified, and balanced against negative information flow that may, e.g., violate privacy guarantees. Since both explainability and privacy require reasoning about knowledge, we tackle these tasks with epistemic temporal logic extended with quantification over counterfactual causes. This allows us to specify that a multi-agent system exposes enough information such that agents acquire knowledge on why some effect occurred. We show how this principle can be used to specify explainability as a system-level requirement and provide an algorithm for checking finite-state models against such specifications. We present a prototype implementation of the algorithm and evaluate it on several benchmarks, illustrating how our approach distinguishes between explainable and unexplainable systems, and how it allows to pose additional privacy requirements.

Access & Resources

Access & Resources