Understanding the QuickXPlain Algorithm: Simple Explanation and Formal Proof
University of Klagenfurt（克拉根福大学）
Patrick Rodler
备注：
This is a preprint of the formally published work "Patrick Rodler. A formal proof and simple explanation of the QuickXplain algorithm. Artificial Intelligence Review, 2022." (https://doi.org/10.1007/s10462-022-10149-w)
In his seminal paper of 2004, Ulrich Junker proposed the QuickXPlain algorithm, which provides a divide-and-conquer computation strategy to find within a given set an irreducible subset with a particular (monotone) property. Beside its original application in the domain of constraint satisfaction problems, the algorithm has since then found widespread adoption in areas as different as model-based diagnosis, recommender systems, verification, or the Semantic Web. This popularity is due to the frequent occurrence of the problem of finding irreducible subsets on the one hand, and to QuickXPlain's general applicability and favorable computational complexity on the other hand.
However, although (we regularly experience) people are having a hard time understanding QuickXPlain and seeing why it works correctly, a proof of correctness of the algorithm has never been published. This is what we account for in this work, by explaining QuickXPlain in a novel tried and tested way and by presenting an intelligible formal proof of it. Apart from showing the correctness of the algorithm and excluding the later detection of errors (proof and trust effect), the added value of the availability of a formal proof is, e.g., (i) that the workings of the algorithm often become completely clear only after studying, verifying and comprehending the proof (didactic effect), (ii) the shown proof methodology can be used as a guidance for proving other recursive algorithms (transfer effect), and (iii) the possibility of providing "gapless" correctness proofs of systems that rely on (results computed by) QuickXPlain, such as numerous model-based debuggers (completeness effect).
Machine learning is becoming increasingly important to control the behavior of safety and financially critical components in sophisticated environments, where the inability to understand learned components in general, and neural nets in particular, poses serious obstacles to their adoption. Explainability and interpretability methods for learned systems have gained considerable academic attention, but the focus of current approaches on only one aspect of explanation, at a fixed level of abstraction, and limited if any formal guarantees, prevents those explanations from being digestible by the …
National University of Singapore（新加坡国立大学）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）
This paper presents LEXR, a framework for explaining the decision making of recurrent neural networks (RNNs) using a formal description language called Linear Temporal Logic (LTL). LTL is the de facto standard for the specification of temporal properties in the context of formal verification and features many desirable properties that make the generated explanations easy for humans to interpret: it is a descriptive language, it has a variable-free syntax, and it can easily be translated into plain English. To generate explanations, LEXR follows the principle of counterexample-guided inductive …
The CREST 2018 workshop is the third in a series of workshops addressing formal approaches to reasoning about causation in systems engineering. The topic of formally identifying the cause(s) of specific events - usually some form of failures -, and explaining why they occurred, are increasingly in the focus of several, disjoint communities. The main objective of CREST is to bring together researchers and practitioners from industry and academia in order to enable discussions how explicit and implicit reasoning about causation is performed. A further objective is to link to the foundations of c…
In this paper, we discuss necessary and sufficient explanations for formal argumentation - the question whether and why a certain argument can be accepted (or not) under various extension-based semantics. Given a framework with which explanations for argumentation-based conclusions can be derived, we study necessity and sufficiency: what (sets of) arguments are necessary or sufficient for the (non-)acceptance of an argument?
Most General Explanations of Tree Ensembles (Extended Version)
CREATE, NUS, Singapore（新加坡国立大学CREATE研究所）；Monash University, Australia（澳大利亚墨尔本大学）；The University of Sydney, Australia（澳大利亚悉尼大学）；ICREA, University of Lleida, Spain（西班牙莱里达大学ICREA研究所）；OPTIMA ARC Industrial Training and Transformation Centre, Australia（澳大利亚OPTIMA ARC工业培训与转型中心）
Inspired by a novel action-theoretic formalization of actual cause, Khan and Lespérance (2021) recently proposed a first account of causal knowledge that supports epistemic effects, models causal knowledge dynamics, and allows sensing actions to be causes of observed effects. To date, no other study has looked specifically at these issues. But their formalization is not sufficiently expressive enough to model explanations via causal analysis of mental states as it ignores a crucial aspect of theory of mind, namely motivations. In this paper, we build on their work to support causal reasoning a…
University of North Carolina at Chapel Hill（北卡罗来纳大学教堂山分校）
Many methods now exist for conditioning model outputs on task instructions, retrieved documents, and user-provided explanations and feedback. Rather than relying solely on examples of task inputs and outputs, these approaches use valuable additional data for improving model correctness and aligning learned models with human priors. Meanwhile, a growing body of evidence suggests that some language models can (1) store a large amount of knowledge in their parameters, and (2) perform inference over tasks in textual inputs at test time. These results raise the possibility that, for some tasks, hum…
University of Konstanz（康斯坦茨大学）；CNRS（法国国家科学研究中心）；Université de Paris（巴黎大学）；King’s College London（伦敦国王学院）；Alexandru Ioan Cuza University of Iasi（雅西亚历山德鲁·伊万·库扎大学）；Western Norway University of Applied Sciences（西挪威应用科学大学）；INRIA（法国国家信息与自动化研究所）；Stevens Institute of Technology（史蒂文斯理工学院）；University of Bologna（博洛尼亚大学）；University College London（伦敦大学学院）；University of Pennsylvania（宾夕法尼亚大学）；Reykjavik University（雷克雅未克大学）；Icelandic Institute for Intelligent Machines（冰岛智能机器研究所）；Université Paris Est - Créteil（巴黎东-克雷泰伊大学）
The fourth edition of the international workshop on Causation, Responsibility and Explanation took place in Prague (Czech Republic) as part of ETAPS 2019. The program consisted in 5 invited speakers and 4 regular papers, whose selection was based on a careful reviewing process and that are included in these proceedings.
The last decade witnessed an ever-increasing stream of successes in Machine Learning (ML). These successes offer clear evidence that ML is bound to become pervasive in a wide range of practical uses, including many that directly affect humans. Unfortunately, the operation of the most successful ML models is incomprehensible for human decision makers. As a result, the use of ML models, especially in high-risk and safety-critical settings is not without concern. In recent years, there have been efforts on devising approaches for explaining ML models. Most of these efforts have focused on so-call…
Department of Linguistics, Stanford University（斯坦福大学语言学系）；Google Research（谷歌研究院）；Department of Computer Science, The University of Texas at Austin（德克萨斯大学奥斯汀分校计算机科学系）
A question answering system that in addition to providing an answer provides an explanation of the reasoning that leads to that answer has potential advantages in terms of debuggability, extensibility and trust. To this end, we propose QED, a linguistically informed, extensible framework for explanations in question answering. A QED explanation specifies the relationship between a question and answer according to formal semantic notions such as referential equality, sentencehood, and entailment. We describe and publicly release an expert-annotated dataset of QED explanations built upon a subse…
Donders Institute for Brain, Cognition, and Behaviour（唐德斯大脑、认知与行为研究所）；Radboud University（拉德堡德大学）
In decision support systems the motivation and justification of the system's diagnosis or classification is crucial for the acceptance of the system by the human user. In Bayesian networks a diagnosis or classification is typically formalized as the computation of the most probable joint value assignment to the hypothesis variables, given the observed values of the evidence variables (generally known as the MAP problem). While solving the MAP problem gives the most probable explanation of the evidence, the computation is a black box as far as the human user is concerned and it does not give ad…
University of Strathclyde（斯特拉斯克莱德大学）；PS Research（PS研究公司）
In automated planning, the need for explanations arises when there is a mismatch between a proposed plan and the user's expectation. We frame Explainable AI Planning in the context of the plan negotiation problem, in which a succession of hypothetical planning problems are generated and solved. The object of the negotiation is for the user to understand and ultimately arrive at a satisfactory plan. We present the results of a user study that demonstrates that when users ask questions about plans, those questions are contrastive, i.e. "why A rather than B?". We use the data from this study to c…
Explainable AI has attracted much research attention in recent years with feature attribution algorithms, which compute "feature importance" in predictions, becoming increasingly popular. However, there is little analysis of the validity of these algorithms as there is no "ground truth" in the existing datasets to validate their correctness. In this work, we develop a method to quantitatively evaluate the correctness of XAI algorithms by creating datasets with known explanation ground truth. To this end, we focus on the binary classification problems. String datasets are constructed using form…
King's College London（伦敦国王学院）；Amazon.com, Inc.（亚马逊公司）；Mohamed bin Zayed University of Artificial Intelligence（穆罕默德·本·扎耶德人工智能大学）；University of Manchester（曼彻斯特大学）
University of Illinois at Chicago（伊利诺伊大学芝加哥分校）；MTA-SZTE RGAI（MTA-SZTE人工智能研究组）
Explainable components in XAI algorithms often come from a familiar set of models, such as linear models or decision trees. We formulate an approach where the type of explanation produced is guided by a specification. Specifications are elicited from the user, possibly using interaction with the user and contributions from other areas. Areas where a specification could be obtained include forensic, medical, and scientific applications. Providing a menu of possible types of specifications in an area is an exploratory knowledge representation and reasoning task for the algorithm designer, aiming…
