Hana Chockler

CLeaR Conference 2026 Conference Paper

Differentiable Causal Search

• Kaveh Aryan
• Hana Chockler
• Mohammad Reza Mousavi

Actual causality–identifying the causes of particular events–is formalised by the Halpern–Pearl (HP) definitions via counterfactual reasoning over structural causal models. Computing HP causes requires solving a combinatorial optimisation problem that is, depending on the variant, \(D^P_1\)-complete or worse. We propose a differentiable approximation of HP causality that leverages the robustness semantics of logical specifications and additive intervention relaxations. Specifically, we replace discrete satisfiability constraints with continuous robustness scores, and model interventions as soft variable shifts rather than hard graph surgeries. This, along with a sparsity relaxation, allows for using continuous optimisation techniques such as gradient descent. Experiments on synthetic graphs show that our method, on average, approximates the true causes with a $\pm$5 % error margin, while achieving at least a 60$\times$ speedup. The framework also supports fine-grained control over additional causal properties such as the desired counterfactual robustness.

UAI Conference 2025 Conference Paper

Explaining Negative Classifications of AI Models in Tumor Diagnosis

• David A. Kelly
• Hana Chockler
• Nathan Blake

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.

ECAI Conference 2025 Conference Paper

Multiple Different Black Box Explanations for Image Classifiers

• Hana Chockler
• David A. Kelly
• Daniel Kroening

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.

KR Conference 2024 Conference Paper

Explaining Image Classifiers

• Hana Chockler
• Joseph Y. Halpern

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).

NeurIPS Conference 2024 Conference Paper

Test Where Decisions Matter: Importance-driven Testing for Deep Reinforcement Learning

• Stefan Pranger
• Hana Chockler
• Martin Tappler
• Bettina Könighofer

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.

IJCAI Conference 2023 Conference Paper

Quantifying Harm

• Sander Beckers
• Hana Chockler
• Joseph Y. Halpern

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.

NeurIPS Conference 2022 Conference Paper

A Causal Analysis of Harm

• Sander Beckers
• Hana Chockler
• Joseph Halpern

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.

AAAI Conference 2022 Conference Paper

On Testing for Discrimination Using Causal Models

• Hana Chockler
• Joseph Y. Halpern

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.

NeurIPS Conference 2021 Conference Paper

Ranking Policy Decisions

• Hadrien Pouget
• Hana Chockler
• Youcheng Sun
• Daniel Kroening

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.

AIJ Journal 2020 Journal Article

Combining experts' causal judgments

• Dalal Alrajeh
• Hana Chockler
• Joseph Y. Halpern

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 merged. We then use it as the basis for combining experts' causal judgments. We also provide a definition of decomposition for causal models to cater for cases when models are incompatible. We illustrate our approach on a number of real-life examples.

JAIR Journal 2020 Journal Article

Learning the Language of Software Errors

• Hana Chockler
• Pascal Kesseli
• Daniel Kroening
• Ofer Strichman

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.

AAAI Conference 2018 Conference Paper

Combining Experts’ Causal Judgments

• Dalal Alrajeh
• Hana Chockler
• Joseph Halpern

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 de- fine 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.

LPAR Conference 2018 Conference Paper

Function Summarization Modulo Theories

• Sepideh Asadi
• Martin Blicha
• Grigory Fedyukovich
• Antti E. J. Hyvärinen
• Karine Even-Mendoza
• Natasha Sharygina
• Hana Chockler

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.

LPAR Conference 2018 Conference Paper

Lookahead-Based SMT Solving

• Antti E. J. Hyvärinen
• Matteo Marescotti
• Parvin Sadigova
• Hana Chockler
• Natasha Sharygina

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.

JAIR Journal 2017 Journal Article

The Computational Complexity of Structure-Based Causality

• Gadi Aleksandrowicz
• Hana Chockler
• Joseph Y. Halpern
• Alexander Ivrii

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.

SAT Conference 2017 Conference Paper

Theory Refinement for Program Verification

• Antti E. J. Hyvärinen
• Sepideh Asadi
• Karine Even-Mendoza
• Grigory Fedyukovich
• Hana Chockler
• Natasha Sharygina

Abstract Recent progress in automated formal verification is to a large degree due to the development of constraint languages that are sufficiently light-weight for reasoning but still expressive enough to prove properties of programs. Satisfiability modulo theories (SMT) solvers implement efficient decision procedures, but offer little direct support for adapting the constraint language to the task at hand. Theory refinement is a new approach that modularly adjusts the modeling precision based on the properties being verified through the use of combination of theories. We implement the approach using an augmented version of the theory of bit-vectors and uninterpreted functions capable of directly injecting non-clausal refinements to the inherent Boolean structure of SMT. In our comparison to a state-of-the-art model checker, our prototype implementation is in general competitive, being several orders of magnitudes faster on some instances that are challenging for flattening, while computing models that are significantly more succinct.

AAAI Conference 2014 Conference Paper

The Computational Complexity of Structure-Based Causality

• Gadi Aleksandrowicz
• Hana Chockler
• Joseph Halpern
• Alexander Ivrii

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 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 DP k, k = 1, 2, 3, .. ., of complexity classes is introduced, which generalizes the class DP introduced by Papadimitriou and Yannakakis (DP is just DP 1 ). We show that the complexity of computing causality under the updated definition is DP 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.

TCS Journal 2004 Journal Article

ω -Regular languages are testable with a constant number of queries

• Hana Chockler
• Orna Kupferman

We continue the study of combinatorial property testing. For a property ψ, an ɛ -test for ψ, for 0 < ɛ ⩽ 1, is a randomized algorithm that given an input x, returns “yes’’ if x satisfies ψ, and returns “no’’ with high probability if x is ɛ -far from satisfying ψ, where ɛ -far essentially means that an ɛ -fraction of x needs to be changed in order for it to satisfy ψ. In (Proceedings of the 40th IEEE Symposium on Foundations of Computer Science, 1999, pp. 645–655), Alon et al. show that regular languages are ɛ -testable with a constant (depends on ψ and ɛ and independent of x) number of queries. We extend the result in (Proceedings of the 40th IEEE Symposium on Foundations of Computer Science, 1999, pp. 645–655) to ω -regular languages: given a nondeterministic Büchi automaton A on infinite words and a small ɛ > 0, we describe an algorithm that gets as input an infinite lasso-shape word of the form x · y ω, for finite words x and y, samples only a constant number of letters in x and y, returns “yes’’ if w ∈ L ( A ), and returns “no’’ with probability 2 3 if w is ɛ -far from L ( A ). We also discuss the applicability of property testing to formal verification, where ω -regular languages are used for the specification of the behavior of nonterminating reactive systems, and computations correspond to lasso-shape words.

IJCAI Conference 2003 Conference Paper

Responsibility and Blame: A Structural-Model Approach

• Hana Chockler
• Joseph Y Halpern

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 2001a 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 cpistemic state. Roughly speaking, the degree of blame of A for D is the expected degree of responsibility of A for B, taken over the epistemic state of an agent.

SODA Conference 2001 Conference Paper

Which formulae shrink under random restrictions?

• Hana Chockler
• Uri Zwick