An Information-Flow Perspective on Explainability Requirements: Specification and Verification
This work addresses the challenge of balancing explainability and privacy in AI systems, offering a formal method for system-level verification, though it is incremental as it builds on existing epistemic logic frameworks.
The paper tackles the problem of specifying and verifying explainability requirements in multi-agent systems by treating explainability as positive information flow, using epistemic temporal logic with counterfactual causes to ensure agents gain knowledge about why effects occur, and presents an algorithm with a prototype implementation that distinguishes explainable from unexplainable systems and integrates privacy requirements.
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.