Existing algorithms for explaining the output of image classifiers use different definitions of explanations and a variety of techniques to find them. However, none of the existing tools use a principled approach based on formal definitions of cause and explanation. In this paper we present a novel black-box approach to computing explanations grounded in the theory of actual causality. We prove relevant theoretical results and present an algorithm for computing approximate explanations based on these definitions. We prove termination of our algorithm and discuss its complexity and the amount of approximation compared to the precise definition. We implemented the framework in a tool, ReX, and we present experimental results and a comparison with state-of-the-art tools. We demonstrate that ReX is the most efficient black-box tool and produces the smallest explanations, in addition to outperforming other black-box tools on standard quality measures.

Existing explanation tools for image classifiers usually give only a single explanation for an image’s classification. For many images, however, image classifiers accept more than one explanation for the image label. These explanations are useful for analyzing the decision process of the classifier and for detecting errors. Thus, restricting the number of explanations to just one severely limits insight into the behavior of the classifier. In this paper, we describe an algorithm and a tool, MultiReX, for computing multiple explanations as the output of a black-box image classifier for a given image. Our algorithm uses a principled approach based on actual causality. We analyze its theoretical complexity and evaluate MultiReX against the state-of-the-art across three different models and three different datasets. We find that MultiReX finds more explanations and that these explanations are of higher quality.

Using AI models in healthcare is gaining popularity. To improve clinician confidence in the results of automated triage and to provide further information about the suggested diagnosis, an explanation produced by a separate post-hoc explainability tool often accompanies the classification of an AI model. If no abnormalities are detected, however, it is not clear what an explanation should be. A human clinician might be able to describe certain salient features of tumors that are not in scan, but existing Explainable AI tools cannot do that, as they cannot point to features that are absent from the input. In this paper, we present a definition of and algorithm for providing explanations of absence; that is, explanations of negative classifications in the context of healthcare AI. Our approach is rooted in the concept of explanations in actual causality. It uses the model as a black-box and is hence portable and works with proprietary models. Moreover, the computation is done in the preprocessing stage, based on the model and the dataset. During the execution, the algorithm only projects the precomputed explanation template on the current image. We implemented this approach in a tool, nito, and trialed it on a number of medical datasets to demonstrate its utility on the classification of solid tumors. We discuss the differences between the theoretical approach and the implementation in the domain of classifying solid tumors and address the additional complications posed by this domain. Finally, we discuss the assumptions we make in our algorithm and its possible extensions to explanations of absence for general image classifiers.

We focus on explaining image classifiers, taking the work of Mothilal et al. 2021 (MMTS) as our point of departure. We observe that, although MMTS claim to be using the definition of explanation proposed by Halpern 2016, they do not quite do so. Roughly speaking, Halpern’s definition has a necessity clause and a sufficiency clause. MMTS replace the necessity clause by a requirement that, as we show, implies it. Halpern’s definition also allows agents to restrict the set of options considered. While these difference may seem minor, as we show, they can have a nontrivial impact on explanations. We also show that, essentially without change, Halpern’s definition can handle two issues that have proved difficult for other approaches: explanations of absence (when, for example, an image classifier for tumors outputs “no tumor”) and explanations of rare events (such as tumors).

In many Deep Reinforcement Learning (RL) problems, decisions in a trained policy vary in significance for the expected safety and performance of the policy. Since RL policies are very complex, testing efforts should concentrate on states in which the agent's decisions have the highest impact on the expected outcome. In this paper, we propose a novel model-based method to rigorously compute a ranking of state importance across the entire state space. We then focus our testing efforts on the highest-ranked states. In this paper, we focus on testing for safety. However, the proposed methods can be easily adapted to test for performance. In each iteration, our testing framework computes optimistic and pessimistic safety estimates. These estimates provide lower and upper bounds on the expected outcomes of the policy execution across all modeled states in the state space. Our approach divides the state space into safe and unsafe regions upon convergence, providing clear insights into the policy's weaknesses. Two important properties characterize our approach. (1) Optimal Test-Case Selection: At any time in the testing process, our approach evaluates the policy in the states that are most critical for safety. (2) Guaranteed Safety: Our approach can provide formal verification guarantees over the entire state space by sampling only a fraction of the policy. Any safety properties assured by the pessimistic estimate are formally proven to hold for the policy. We provide a detailed evaluation of our framework on several examples, showing that our method discovers unsafe policy behavior with low testing effort.

In earlier work we defined a qualitative notion of harm: either harm is caused, or it is not. For practical applications, we often need to quantify harm; for example, we may want to choose the least harmful of a set of possible interventions. We first present a quantitative definition of harm in a deterministic context involving a single individual, then we consider the issues involved in dealing with uncertainty regarding the context and going from a notion of harm for a single individual to a notion of "societal harm", which involves aggregating the harm to individuals. We show that the "obvious" way of doing this (just taking the expected harm for an individual and then summing the expected harm over all individuals) can lead to counterintuitive or inappropriate answers, and discuss alternatives, drawing on work from the decision-theory literature.

Consider a bank that uses an AI system to decide which loan applications to approve. We want to ensure that the system is fair, that is, it does not discriminate against applicants based on a predefined list of sensitive attributes, such as gender and ethnicity. We expect there to be a regulator whose job it is to certify the bank’s system as fair or unfair. We consider issues that the regulator will have to confront when making such a decision, including the precise definition of fairness, dealing with proxy variables, and dealing with what we call allowed variables, that is, variables such as salary on which the decision is allowed to depend, despite being correlated with sensitive variables. We show (among other things) that the problem of deciding fairness as we have defined it is co-NP-complete, but then argue that, despite that, in practice the problem should be manageable.

As autonomous systems rapidly become ubiquitous, there is a growing need for a legal and regulatory framework toaddress when and how such a system harms someone. There have been several attempts within the philosophy literature to define harm, but none of them has proven capable of dealing with with the many examples that have been presented, leading some to suggest that the notion of harm should be abandoned and ``replaced by more well-behaved notions''. As harm is generally something that is caused, most of these definitions have involved causality at some level. Yet surprisingly, none of them makes use of causal models and the definitions of actual causality that they can express. In this paper we formally define a qualitative notion of harm that uses causal models and is based on a well-known definition of actual causality (Halpern, 2016). The key novelty of our definition is that it is based on contrastive causation and uses a default utility to which the utility of actual outcomes is compared. We show that our definition is able to handle the examples from the literature, and illustrate its importance for reasoning about situations involving autonomous systems.

Abstract When synthesizing a system from a given specification, there is room for automatically adding various requirements, hence improving the resulting system. One such requirement covered extensively in past literature is that of robustness. In particular, the system can fail to read the inputs correctly from the environment, and the environment can fail to satisfy our assumptions about its behavior. Nevertheless, we want the system to still satisfy the specification even under these failures, in some limited way. It has to be limited because it is typically too strong of a requirement to realize the property regardless of the inputs and the environment’s assumptions. In this work, we propose a simple and flexible framework for synthesizing robust systems, where the user defines the required robustness via a temporal robustness specification. For example, the user may specify that the environment is eventually reliable, or input misreadings cannot occur more than $$k$$ k consecutive steps and synthesize a system under this assumption. Furthermore, our framework enables us to specify a temporal recovery specification, which describes how the designer expects the system to recover after a failure of the environment assumptions. We show examples of robust systems that we synthesized with this method using our synthesis tool Party.

Existing algorithms for explaining the output of image classifiers perform poorly on inputs where the object of interest is partially occluded. We present a novel, black-box algorithm for computing explanations that uses a principled approach based on causal theory. We have implemented the method in the DEEPCOVER tool. We obtain explanations that are much more accurate than those generated by the existing explanation tools on images with occlusions and observe a level of performance comparable to the state of the art when explaining images without occlusions.

Policies trained via Reinforcement Learning (RL) without human intervention are often needlessly complex, making them difficult to analyse and interpret. In a run with $n$ time steps, a policy will make $n$ decisions on actions to take; we conjecture that only a small subset of these decisions delivers value over selecting a simple default action. Given a trained policy, we propose a novel black-box method based on statistical fault localisation that ranks the states of the environment according to the importance of decisions made in those states. We argue that among other things, the ranked list of states can help explain and understand the policy. As the ranking method is statistical, a direct evaluation of its quality is hard. As a proxy for quality, we use the ranking to create new, simpler policies from the original ones by pruning decisions identified as unimportant (that is, replacing them by default actions) and measuring the impact on performance. Our experimental results on a diverse set of standard benchmarks demonstrate that pruned policies can perform on a level comparable to the original policies. We show that naive approaches for ranking policies, e.g. ranking based on the frequency of visiting a state, do not result in high-performing pruned policies. To the best of our knowledge, there are no similar techniques for ranking RL policies' decisions.

Abstract In reactive synthesis, one begins with a temporal specification $$\varphi $$ φ , and automatically synthesizes a system $$M$$ M such that $$M\models \varphi $$ M ⊧ φ . As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system M satisfies $$\varphi $$ φ non-vacuously, then M is likely to be closer to the user’s intent, because it satisfies $$\varphi $$ φ in a more “meaningful” way. Narrowing the gap between the formal specification and the designer’s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.

We propose to use algorithms for learning deterministic finite automata (DFA), such as Angluin’s L* algorithm, for learning a DFA that describes the possible scenarios under which a given program error occurs. The alphabet of this automaton is given by the user (for instance, a subset of the function call sites or branches), and hence the automaton describes a user-defined abstraction of those scenarios. More generally, the same technique can be used for visualising the behavior of a program or parts thereof. It can also be used for visually comparing different versions of a program (by presenting an automaton for the behavior in the symmetric difference between them), and for assisting in merging several development branches. We present experiments that demonstrate the power of an abstract visual representation of errors and of program segments, accessible via the project’s web page. In addition, our experiments in this paper demonstrate that such automata can be learned efficiently over real-world programs. We also present lazy learning, which is a method for reducing the number of membership queries while using L*, and demonstrate its effectiveness on standard benchmarks.

Past literature on synthesis identified the need to synthesize systems that are robust to failures of the system in reading the inputs from the environment, and also to failures of the environment itself to satisfy our assumptions about its behavior. In this work, we propose a simple and flexible framework for synthesizing robust systems, where the user defines the required robustness via a temporal robustness specification. For example, the user may specify that the environment is eventually reliable, or input misreadings cannot occur more than k consecutive steps, and synthesize a system under this assumption. Furthermore, our framework enables us to specify, also, a temporal recovery specification, i.e., describing the way the system is expected to recover after a failure of the environment assumptions. We show examples of robust systems that we have synthesized with this method by our synthesis tool PARTY.

We present a lattice-based satisfiability modulo theory for verification of programs with library functions, for which the mathematical libraries supporting these functions contain a high number of equations and inequalities. Common strategies for dealing with library functions include treating them as uninterpreted functions or using the theories under which the functions are fully defined. The full definition could in most cases lead to instances that are too large to solve efficiently.

Consider a policymaker who wants to decide which intervention to perform in order to change a currently undesirable situation. The policymaker has at her disposal a team of experts, each with their own understanding of the causal dependencies between different factors contributing to the outcome. The policymaker has varying degrees of confidence in the experts’ opinions. She wants to combine their opinions in order to decide on the most effective intervention. We formally define the notion of an effective intervention, and then consider how experts’ causal judgments can be combined in order to determine the most effective intervention. We define a notion of two causal models being compatible, and show how compatible causal models can be combined. We then use it as the basis for combining experts causal judgments. We illustrate our approach on a number of real-life examples.

SMT-based program verification can achieve high precision using bit-precise models or combinations of different theories. Often such approaches suffer from problems related to scalability due to the complexity of the underlying decision procedures. Precision is traded for performance by increasing the abstraction level of the model. As the level of abstraction increases, missing important details of the program model becomes problematic. In this paper we address this problem with an incremental verification approach that alternates precision of the program modules on demand. The idea is to model a program using the lightest possible (i.e., less expensive) theories that suffice to verify the desired property. To this end, we employ safe over-approximations for the program based on both function summaries and light-weight SMT theories. If during verification it turns out that the precision is too low, our approach lazily strengthens all affected summaries or the theory through an iterative refinement procedure. The resulting summarization framework provides a natural and light-weight approach for carrying information between different theories. An experimental evaluation with a bounded model checker for C on a wide range of benchmarks demonstrates that our approach scales well, often effortlessly solving instances where the state-of-the-art model checker CBMC runs out of time or memory.

The lookahead approach for binary-tree-based search in constraint solving favors branching that provide the lowest upper bound for the remaining search space. The approach has recently been applied in instance partitioning in divide-and-conquer-based parallelization, but in general its connection to modern, clause-learning solvers is poorly understood. We show two ways of combining lookahead approach with a modern DPLL(T)-based SMT solver fully profiting from theory propagation, clause learning, and restarts. Our thoroughly tested prototype implementation is surprisingly efficient as an independent SMT solver on certain instances, in particular when applied to a non-convex theory, where the lookahead-based implementation solves 40% more unsatisfiable instances compared to the standard implementation.

Halpern and Pearl introduced a definition of actual causality; Eiter and Lukasiewicz showed that computing whether X = x is a cause of Y = y is NP-complete in binary models (where all variables can take on only two values) and Σ^P_2 -complete in general models. In the final version of their paper, Halpern and Pearl slightly modified the definition of actual cause, in order to deal with problems pointed out by Hopkins and Pearl. As we show, this modification has a nontrivial impact on the complexity of computing whether {X} = {x} is a cause of Y = y. To characterize the complexity, a new family D_k^P , k = 1, 2, 3, . . ., of complexity classes is introduced, which generalises the class DP introduced by Papadimitriou and Yannakakis (DP is just D_1^P). We show that the complexity of computing causality under the updated definition is D_2^P -complete. Chockler and Halpern extended the definition of causality by introducing notions of responsibility and blame, and characterized the complexity of determining the degree of responsibility and blame using the original definition of causality. Here, we completely characterize the complexity using the updated definition of causality. In contrast to the results on causality, we show that moving to the updated definition does not result in a difference in the complexity of computing responsibility and blame.

An important challenge in the field of law is the attribution of responsibility and blame to individuals and organisations for a given harm. Attributing legal responsibility often involves (but is not limited to) assessing to what extent certain parties have caused harm, or could have prevented harm from occurring. This paper presents a causal framework for performing such assessments that is particularly suitable for the analysis of complex legal cases, where the actions of many parties have had a direct or indirect effect on the harm that did occur. This framework is evaluated by means of a case study that applies it to the Baby P. case, a high-profile case of child abuse leading to the death of a child that has been the subject of a number of public inquiries in the UK. The paper concludes with a discussion of the framework, including a roadmap of future work and barriers to adoption.

Halpern and Pearl introduced a definition of actual causality; Eiter and Lukasiewicz showed that computing whether X = x is a cause of Y = y is NP-complete in binary models (where all variables can take on only two values) and \Sigma^P_2-complete in general models. In the final version of their paper, Halpern and Pearl slightly modified the definition of actual cause, in order to deal with problems pointed by Hopkins and Pearl. As we show, this modification has a nontrivial impact on the complexity of computing actual cause. To characterize the complexity, a new family D_k^P , k = 1,2,3,..., of complexity classes is introduced, which generalizes the class D^P introduced by Papadimitriou and Yannakakis (DP is just D^P_1). We show that the complexity of computing causality under the updated definition is D^P_2 -complete. Chockler and Halpern extended the definition of causality by introducing notions of responsibility and blame. The complexity of determining the degree of responsibility and blame using the original definition of causality was completely characterized. Again, we show that changing the definition of causality affects the complexity, and completely characterize it using the updated definition.

A numerical algorithm is called stable if an error, in all possible executions of the algorithm, does not exceed a predefined bound. Introduction of concurrency to numerical algorithms results in a significant increase in the number of possible computations of the same result, due to different possible interleavings of concurrent threads. This can lead to instability of previously stable algorithms, since rounding can result in a larger error than expected for some interleavings. Such errors can be very rare, since the particular combination of rounding can occur in only a small fraction of interleavings. In this paper, we apply the cross-entropy method -- a generic approach to rare event simulation and combinatorial optimization -- to detect rare numerical instability in concurrent programs. The cross-entropy method iteratively samples a small number of executions and adjusts the probability distribution of possible scheduling decisions to increase the probability of encountering an error in a subsequent iteration. We demonstrate the effectiveness of our approach on implementations of several numerical algorithms with concurrency and rounding by truncation of intermediate computations. We describe several abstraction algorithms on top of the implementation of the cross-entropy method and show that with abstraction, our algorithms successfully find rare errors in programs with hundreds of threads. In fact, some of our abstractions lead to a state space whose size does not depend on the number of threads at all. We compare our approach to several existing testing algorithms and argue that its performance is superior to other techniques.

Coverage is a means to quantify the quality of a system specification, and is frequently applied to assess progress in system validation. Coverage is a standard measure in testing, but is very difficult to compute in the context of formal verification. We present efficient algorithms for identifying those parts of the system that are covered by a given property. Our algorithm is integrated into state-of-the-art Boolean satisfiability problem-based model checking using Craig interpolation. The key insight into our algorithm is the re-use of previously computed inductive invariants and counterexamples. This re-use permits a a rapid completion of the vast majority of tests, and enables the computation of a coverage measure with 96% accuracy with only 5× the runtime of the model checker.

Coverage is a means to quantify the quality of a system specification, and is frequently applied to assess progress in system validation. Coverage is a standard measure in testing, but is very difficult to compute in the context of formal verification. We present efficient algorithms for identifying those parts of the system that are covered by a given property. Our algorithm is integrated into state-of-the-art SAT-based Model Checking using Craig interpolation. The key insight of our algorithm is to re-use previously computed inductive invariants and counterexamples. This re-use permits a quick conclusion of the vast majority of tests, and enables the computation of a coverage measure with 96% accuracy with only 5x the runtime of the Model Checker.

No abstract available.

Given an LTL formula phi in negation normal form, it can be strengthened by replacing some of its literals with FALSE. Given such a formula and a model M that satisfies it, vacuity and mutual vacuity attempt to find one or a maximal set of literals, respectively, with which phi can be strengthened while still being satisfied by M. We study the problem of finding the strongest LTL formula that satisfies M and is in the Boolean closure of strengthened versions of phi as defined above. This formula is stronger or equally strong to any formula that can be obtained by vacuity and mutual vacuity. We present our algorithms in the framework of lattice automata.

Even when a system is proven to be correct with respect to a specification, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the system.Coverage metricsattempt to check which parts of a system are actually relevant for the verification process to succeed. Recent work on coverage in model checking suggests several coverage metrics and algorithms for finding parts of the system that are not covered by the specification. The work has already proven to be effective in practice, detecting design errors that escape early verification efforts in industrial settings. In this article, we relate a formal definition of causality given by Halpern and Pearl to coverage. We show that it gives significant insight into unresolved issues regarding the definition of coverage and leads to potentially useful extensions of coverage. In particular, we introduce the notion ofresponsibility, which assigns to components of a system a quantitative measure of their relevance to the satisfaction of the specification.

In simulation-based verification, we check the correctness of a given program by executing it on some input vectors. Even for medium-size programs, exhaustive testing is impossible. Thus, many errors are left undetected. The problem of increasing the exhaustiveness of testing and decreasing the number of undetected errors is the main problem of software testing. In this paper, we present a novel approach to software testing, which allows us to dramatically raise the probability of catching rare errors in large programs. Our approach is based on the cross-entropy method. We define a performance function, which is higher in the neighborhood of an error or a pattern we are looking for. Then, the program is executed many times, choosing input vectors from some random distribution. The starting distribution is usually uniform, and it is changed at each iteration based on the vectors with highest value of the performance function in the previous iteration. The crossentropy method was shown to be very efficient in estimating the probabilities of rare events and in searching for solutions for hard optimization problems. Our experiments show that the cross-entropy method is also very efficient in locating rare bugs and patterns in large programs.We show the experimental results of our cross-entropy based testing tool and compare them to the performance of ConTest and of Java scheduler.

In formal verification, we verify that a system is correct with respect to a specification. Cases like antecedent failure can make a successful pass of the verification procedure meaningless. Vacuity detection can signal such "meaningless" passes of the specification, and indeed vacuity checks are now a standard component in many commercial model checkers. We address two dimensions of vacuity: the computational effort and the information that is given to the user. As for the first dimension, we present several preliminary vacuity checks that can be done without the design itself, which implies that some information can be found with a significantly smaller effort. As for the second dimension, we present algorithms for deriving three types of information that are not provided by standard vacuity checks, assuming M \= phi for a model M and property phi: a) behaviors that are possibly missing from M (or wrongly restricted by the environment) b) the largest subset of occurrences of literals in phi that can be replaced with false simultaneously without falsifying phi in M, and finally c) the degree of responsibility of each occurrence of a literal in phi to its satisfaction in the model M, which can be seen as a fine-grain form of vacuity. The complexity of each of these problems is proven. Overall this extra information can lead to tighter specifications and more guidance for finding errors.

Causality is typically treated an all-or-nothing concept; either A is a cause of B or it is not. We extend the definition of causality introduced by Halpern and Pearl [2004a] to take into account the degree of responsibility of A for B. For example, if someone wins an election 11-0, then each person who votes for him is less responsible for the victory than if he had won 6-5. We then define a notion of degree of blame, which takes into account an agent's epistemic state. Roughly speaking, the degree of blame of A for B is the expected degree of responsibility of A for B, taken over the epistemic state of an agent.