In contrast with ad-hoc methods for eXplainable Artificial Intelligence (XAI), formal explainability offers important guarantees of rigor. However, formal explainability is hindered by poor scalability for some families of classifiers, the most significant being neural networks. As a result, there are concerns as to whether formal explainability might serve to complement other approaches in delivering trustworthy AI. This paper addresses the limitation of scalability of formal explainability, and proposes novel algorithms for computing formal explanations. The novel algorithm computes explanations by answering instead a number of robustness queries, and such that the number of such queries is at most linear on the number of features. Consequently, the proposed algorithm establishes a direct relationship between the practical complexity of formal explainability and that of robustness. More importantly, the paper generalizes the definition of formal explanation, thereby allowing the use of robustness tools that are based on different distance norms, and also by reasoning in terms of some target degree of robustness. The experiments validate the practical efficiency of the proposed approach.

翻译：与针对可解释人工智能（XAI）的临时方法相比，形式化可解释性提供了重要的严谨性保证。然而，形式化可解释性在某些分类器家族（尤其是神经网络）中受到可扩展性差的阻碍。因此，人们担忧形式化可解释性是否能够作为其他方法的补充，助力实现可信赖的人工智能。本文针对形式化可解释性的可扩展性限制问题，提出了计算形式化解释的新型算法。该算法通过回答若干鲁棒性查询来计算解释，且此类查询的数量至多与特征数量呈线性关系。因此，所提出的算法建立了形式化可解释性实际复杂度与鲁棒性复杂度之间的直接关联。更重要的是，本文推广了形式化解释的定义，从而允许使用基于不同距离范数的鲁棒性工具，并基于某种目标鲁棒性程度进行推理。实验验证了所提出方法的实际效率。