Hierarchical Expertise Level Modeling for User Specific Contrastive Explanations

1 Introduction

AI systems have the potential to transform society by assisting humans in diverse situations ranging from extraplanetary exploration to assisted living. In order to achieve this potential, however, humans working with such systems need to be able to understand them just as they would understand human team members. This presents a number of challenges because most humans do not understand AI algorithms and their behavior at the same intuitive level that they understand other humans. Recently, there have been attempts to bridge this gap by developing systems capable of explaining their behavior. Most recently [Chakraborti et al., 2017] formulated the problem of explaining plans as that of model reconciliation. Their approach relied on identifying ways of bringing the human model (i.e the explainee model) closer to the robot model so that the plan in question appears optimal in the new model. Their work looked at scenarios in which the human used a model of the domain that was at the same level of fidelity as the one used by the agent to generate the plan. This approach, unfortunately, did not capture scenarios where the human possessed a lower level of expertise and thus used a more "abstract" or coarser representation of the model as compared to the AI agent.

In this paper, we propose a new approach to this problem where the agent explains its ongoing or planned behavior to humans with differing levels of expertise. We consider explanations in the framework of counterfactual reasoning, where a user who is confused by the agent's activity (or proposed activity) presents alternative behavior that they would have expected the agent to execute. This aligns with the widely held belief that humans expect explanations to be contrastive [Miller, 2017]. In keeping with the terminology used in social sciences literature we will call the set of alternative behaviors as foils to the proposed robot behavior.

For instance, consider a mission-control operator who needs to supervise the activity of an autonomous robot on Mars in the midst of a sandstorm that could present valuable data for analysis. If the robot proposes to go back to the base before going to a vantage point for observing the storm, the operator would naturally be perplexed, and may be motivated to ask, why doesn't the robot go directly to the vantage point?! Similarly, a human team member at a manufacturing plant may be perplexed by a robot's unnecessary detours while assembling an automobile engine. Not only do such situations involve personnel with varying skill levels, they also place a premium on the size of explanations.

A natural interaction would have the robot present an explanation about why the human's counterfactual suggestion would not apply in the current situation. This explanation could involve facts about the environment as well as about the robot's constraints. E.g., "I need to get a new battery pack to observe the sandstorm for at least 30 minutes without interruption". Such explanations need to be attuned to the level of understanding of the human involved. If the operator happens to be the lead designer of the robot's sequential decisionmaking engine, the robot could provide more specific information, e.g. "I am carrying battery-pack #00920", because this operator knows that some battery packs wouldn't allow it to carry out the full observation.

In this paper we present the Hierarchical Expertise-Level Modeling or the HELM approach for facilitating such context and user-specific explanations. We assume that the human user's understanding of the task is an abstraction of the model used by the robot. HELM generates the appropriate explanation by searching through a model lattice of possible abstractions of the agent's model. Each model within this lattice represents a different level of understanding of the task, with the highest fidelity representation (corresponding to the most detailed understanding of the domain used by the robot) forming the base of the lattice and the model representing the most naive understanding of the task (for example one held by a lay user) forming the highest node. Since the user's level of expertise is unknown to the agent, our algorithm estimates the human model before searching for an explanation. While we assume a closed form model in this paper, we plan to extend our approach to arbitrary generative models or simulations in future work.

Our explanations consist of information that may be absent in the user's abstract model, and show why the foil doesn't apply in the true situation. These explanations will cause the user's model to shift to a more accurate model in the lattice (and ultimately achieve model reconciliation). We will refer to model updates constituting these explanations as model concretizations. Our framework can also be extended to situations where a user's understanding is abstract and erroneous. In this paper, we focus on the fundamental aspects of the problem and restrict our attention to settings where the user's understanding is an abstraction of the actual situation.

Readers familiar with counter-example guided model checking (CEGAR) literature [Clarke et al., 2000] or its applications in planning [Seipp and Helmert, 2013] will notice that our method of refining models is quite reminiscent of model refinement methods discussed in that literature. The foils we consider in our approach are equivalent to the counter-examples used by CEGAR methods and similar to these methods we too are looking for concretizations that refute these counter-examples. We provide a more detailed comparison between the methods in Section 5.

The rest of this paper is structured as follows. In Section 2, we present our formal framework. Section 3 covers different approaches for generating explanation and Section 4 presents empirical evaluation of these methods on standard IPC domains. In sections 5 and 6, we will discuss the related work and possible future directions.

2 Hierarchical Expertise-Level Models

In this work, we focus on abstractions that form models by projecting out state fluents. While the presentation in the following sections is equally valid for both predicate and propositional abstractions, we will focus on propositional abstractions to keep our formulation clear and concise. We will look at planning models of the formM = 〈P, S,A, I,G〉 where P gives the set of state fluents, S the set of possible states, A the set of actions, I the initial state and G the goal. Each state s ∈ S is uniquely represented by the set of propositions that are true in that state, i.e, s ⊆ P.

Each action a ∈ A is associated with a set of preconditions preca that need to hold for the effects (ea) of that action to be applied to a particular state. Each effect set ea can be further separated into a set of add effects e+a and a set of delete effects e-a . The result of executing an action a on a state s in this setting is defined as follows

A plan π is defined as a sequence of actions (〈a1, .., an〉, n being the size of the plan), and a plan is said to solve M (i.e, π(I) |=M G) if π(I) ⊇ G.

Automated planning has a long tradition of employing abstraction both for plan generation (c.f [Sacerdoti, 1974]) and for generating heuristics (c.f [Seipp and Helmert, 2013; Keyder et al., 2012]) and a number of different abstraction schemes have been proposed in these works. In fact, state abstractions as presented in this work have been widely used in pattern databases and are referred to as projections in that literature (c.f [Culberson and Schaeffer, 1998; Edelkamp, 2000]). Following works like [Seipp and Helmert, 2013; Backstrom and Jonsson, 2013], we will also use the concept of a transition system induced by the planning model to define state abstractions. Intuitively, a transition system constitutes a graph where the nodes represent possible states, and the edges capture the transitions between the states that are valid in the corresponding planning model. We refer the readers to the previously mentioned works for further analyses of state transition systems and their connection to abstractions.

Definition 1. A set X is said to be a propositional abstraction of a set of states S with respect to some set of propositions Λ, if there exists a surjective mapping fΛ : S → X, such that for every state s ∈ S, there exists a state fΛ(s) ∈ X where fΛ(s) = s \ Λ.

For notational convenience we will refer to the set of states obtained by abstracting out the proposition set Λ from some set of states S as [S]fΛ .

Definition 2. For a planning model M = 〈P, S,A, I,G〉 with a corresponding transition system T , a model M′ = 〈P ′ , S′ ,A, I ′ ,G′ 〉 with a transition system T ′ is considered an abstraction of M, if there exists a set of propositions Λ, such that P ′ = P - Λ, S′ = [S]fΛ , I ′ = fΛ(I), G′ = fΛ(G) and for every transition s1 a-→ s2 in T corresponding to an action a, there exists an equivalent transition (s1 \ Λ) [a]fΛ ---→ (s2 \ Λ) in T ′ , where [a]fΛ is part of the new action set A′ .

As per Definition 2, the abstract model is complete in the sense that all plans that were valid in the original model will have an equivalent plan in this new model. We will use the operator ⊏ to capture the fact that a model M is less abstract than the model M′ , i.e if M ⊏ M′ then there exist a set of propositions Λ such that M = [M′ ]fΛ . With the definition of abstraction and related notations in place, we are now ready to define a model lattice. We will use this lattice to both estimate the human model and to identify explanations.

Definition 3. For a model M#, the model lattice L is a tuple of the form L = 〈M, E, P, ℓ〉, where M is the set of lattice nodes such that M# ∈ M and ∀ M′ ∈ M,M# ⊑ M′ , E is the lattice edges, P is the superset of propositions considered for abstraction within this lattice and ℓ is a function mapping edges to labels. Additionally, for each edge ei = (Mi,Mj) there exists a proposition p ∈ P such that [Mi]fp =Mj and ℓ(Mi, Mj ) = p.

Thus each edge in this lattice corresponds to an abstraction formed by projecting out a single proposition (represented by the label of the edge). We can also define a concretization function γp that retrieves the model that was used to generate the given abstract model by projecting out the proposition p, i.e, γp(M) =M′ if (M′ ,M) ∈ E and ℓ(M′ ,M) = p else γp(M) = M.

Throughout the rest of this work, we will make some assumptions on the structure of the lattice L and the abstraction methods used by L to simplify our discussions. In this paper, we will focus on lattices where each node in M has an incoming edge for every proposition missing from its corresponding model. We will refer to lattices that satisfy this property as Proposition Conserving lattices. Additionally, we will call a proposition conserving lattice that contains an abstract node corresponding to each possible subset of P as the Complete Lattice for M given P.

Formally, a lattice L is proposition conserving, iff for any model M ∈ M and ∀p ∈ P, if p is not in PM then there exists a model M′ ∈ M, such that (M′ ,M) ∈ E and ℓ(M′ ,M) = p). Notice that enforcing conservation of propositions doesn't require any further assumptions about the human model and can be easily ensured by the agent generating the lattice.

We also assume that all abstraction functions used in generating the models in the lattice are commutative and idempotent, i.e., [[M]fp1 ]fp2 = [[M]fp2 ]fp1 and [[M]fp1 ]fp1 = [M]fp1 . Readers can refer to [Srivastava et al., 2016] for a comprehensive list of ways to generate abstract models that satisfy these properties.

As mentioned earlier, we consider an explanation generation setting where the human observer uses a task model (denoted as MH = 〈PH, SH,AH, IH,GH〉), that is a more abstract version of the robot's model (MR = 〈PH, SR, AR, IR, GR〉). While the robot may not knowMH, it knows that MH is a member of the set M for the lattice L. The human comes up with a foil set F = {π1, π2, ..., πm} that the robot needs to refute by providing an explanation E regarding the task. The explanation should contain information about specific domain properties (i.e., state fluents) that are missing from the human's model and how these properties affect different actions (For example, which actions use these propositions as preconditions and which ones generate/delete them). To illustrate the utility of such explanations consider an example involving a simplified version of the rover domain mentioned earlier.

Example 1. Let us suppose that the rover uses a modified version of the IPC rover domain [International Planning Competition, 2011] that also takes into account the battery level of the rover. Each rover operation has a different energy requirement, and the battery level needs to be above a predefined threshold for it to execute them, e.g., it can perform rock sampling only if the battery level is above 75%. Furthermore, the rover needs to visit the base station (i.e., the lander) and perform a reset action to recharge its batteries.

The rover knows that the human observer is at most ignorant of its energy requirements and/or storage capabilities. So the model lattice L needs to consider abstractions corresponding to the following propositions P={battery level above 25 perc, battery level above 50 perc, battery level above 75 perc, full store}. Figure 2 shows the lattice that the robot would use in this setting. Here we will create each abstract model by dropping a proposition from the more concrete model and by making the effects of action non-deterministic if the dropped predicate appears in the precondition. For example, if the action drop store1 has effects of the form

{full store1, store of store1} → {¬full store1, empty store1}

Now in an abstract version of this model, if the proposition full store1 is dropped the effect becomes

{ store of store1} → ND{ empty store1}

Which now says that the action's effects are nondeterministic and executing drop store1 may or may not turn the fluent empty store1 true.

Here the robot presents the plan

πR = 〈 navigate w0 lander, reset at lander, navigate lander w1, sample rock store0 w1〉 and the observer responds by proposing the foil set F = {〈 navigate w0 w1, navigate lander w1, sample rock store0 w1 〉}

If the robot knew that the human was ignorant about all the battery level predicates and nothing else, the robot could help resolve the human confusion by informing them about the fact that action sample rock requires the battery to be above 75% (i.e describing the proposition battery level above 75 perc) and in this updated model the human foil can no longer achieve the goal. We can represent such an explanation using the set of propositions whose concretization is required to refute the given foils.

Definition 4. An explanation E of size n for the human model MH and a foil set F can be represented as a set of proposi-

tions of the form E = {p1, ..., pn} such that ∀π ∈ F, π(IγE(MH)) ̸|=γE(MH) GγE(MH)

Where γE(MH) is the model obtained by applying the concretizations corresponding to E on the model MH .

In Example 1, the rover would have difficulty coming up with a single explanation as it does not knowMH. One possibility would be to restrict its attention to just the models that are consistent with the foils . In this scenario, this would correspond to {c6, c7, c9, c10, c11, c12}.

Now we need to find a way of generating explanations given this reduced set of models.

Proposition 1. LetMi be some model in L such thatMH ⊑ Mi. If E is a valid explanation for Mi and some foil set F, then E must also explain F for MH.

This proposition directly follows from the fact that for a proposition conserving lattice γE(Mi) will be a logical weaker model than γE(MH). Next, we will define the concept of a minimal abstraction set for a given lattice L and foils

FDefinition 5. Given an the abstraction lattice L = 〈M, E, P, ℓ〉 the minimal abstraction set Mmin is the supremum of all the models that are consistent with the foil set F. Mmin = sup{Mi|Mi ∈ M, ∀π ∈ F (π(IMi ) |=Mi GMi )}

In Example 1, the minimal abstract model set will be Mmin = {c11, c12}.

If we can find an explanation that is valid for all the models in Mmin then by Proposition 1 it must work for MH as well.

Proposition 2. For a given model lattice L, the minimal abstraction set Mmin and a set of foils F , there exists an explanation E such that ∀M′ ∈ Mmin and ∀π ∈ F ,

It is easy to see why this property holds, as any explanation that involves concretizing all possible propositions in P satisfies this property.

In most cases, we would prefer to compute the least costly or the shortest explanation (if all concretizations are equally expensive) to the explainee. In the rover example, even if the human is unaware of multiple task details, the robot can easily resolve the explainee's doubts by just explaining the concretizations related to the proposition battery level above 75 perc without getting into other details. Describing the details of remaining propositions is unnecessary and in the worst case might leave the human feeling overwhelmed and confused. In this case, the explanation would just include information regarding battery levels and how to identify when the battery level is or above 75% and model updates like sample rock-has-precondition-battery level above 75 perc sample soil-has-precondition-battery level above 75 perc

...

Before delving into the optimization version of the problem, let us look at the complexity of the corresponding decision problem

Theorem 1. Given a minimal abstraction set Mmin, a plan πR, the set of propositions being abstracted P and the set of foils F for a model M, the problem of identifying whether an explanation of size k exists for the complete lattice is NPcomplete.

Proof (Sketch). The fact that we can test the validity of the given explanation in polynomial time (size of the explanation is guaranteed to be smaller than |P|) shows that the problem is in NP. We can show NP-completeness by reducing the set covering problem [Bernhard and Vygen, 2008] to an instance of the explanation generation problem. Let's consider a set covering problem with U as the universe set and S as the set of sub-collections. Now let us create an explanation generation problem where the set of foils F is equal to U and the propositions in the set P contain a proposition for each member of S. Additionally concretizing with respect to a proposition will resolve only the foils covered by its corresponding subset in S. For this setting, we can construct a fully connected proposition conserving lattice L of height |S|. Within the lattice, there exists a unique most abstract model where all the foils hold and a single most concrete model (where none of the foils hold). Now if we can come up with an explanation of size k in this setting, then this explanation corresponds to a set cover of size k.

3 GeneratingMinimal Explanations

As mentioned earlier, we are interested in producing the minimal explanation. Additionally, in most domains, the cost of communicating the concretization details could vary among propositions. An explanation that involves a proposition that appears in every action definition might be harder to communicate than one that only uses a proposition that is part of the definition of a single action.

In addition to the actual size, the comprehensibility of the explanations may also depend on factors like human's mental load, the familiarity with the concepts captured by the propositions, etc.. To keep our discussions simple, we will restrict the cost of communicating an explanation to just the number of unique model updates this explanation would bring about in the human model.We will use the symbol Cp to represent the cost of communicating the changes related to the proposition p and also overload it to work on sets of propositions.

Now our problem is to find the cheapest explanation (represented as Emin) for a given set of foils F , and the minimal abstract model set Mmin. One possibility is to perform an A* search [Hart et al., 1968] over the space of possible propositional concretizations to identify Emin. Each search state consists of the minimal set of abstract models for the human model given the current explanation prefix. We will stop the search as soon as we find a state where the foils no longer hold for the current minimal set.

Proposition 3. Let Mmin be the minimal abstraction set for a given lattice L = 〈M, E, P, ℓ〉 and foil set F. Then for a proposition p, the set ̂Mmin formed by applying the concretization corresponding to p on every element of Mmin will be the minimal abstract set for ̂M formed by applying the concretization γp on every element of M given F .

The above property implies that we don't need to look at the lattice L to recalculate minimal abstraction set after the application of every concretization function. We can also further simplify our problem by exploiting the fact that a particular propositional concretization resolves a foil (i.e., make the foil no longer valid) when it either adds a precondition (or a new condition for a conditional effect) or a goal fact that can not be satisfied by the foil. To concisely capture this idea we will introduce the concept of a foil resolution set to represent the subset of foils resolved by the concretization of a particular proposition.

Definition 6. For a set of models M′ , a foil set F and a proposition p, the resolution set RF (M′ , p) gives the subset of foils that no longer holds in the concretized models, i.e RF (M′ , p) = {π|π ∈ F ∧ (∀M′ ∈ M′ (π(Iγp(M′ )) ̸|=γp(M′ ) Gγp(M′ ) ∧π(IM′) |=M′ GM′))}.

We will also use RF to represent the set of foils resolved by a sequence of propositions

Proposition 4. For a set of model M′ and a foil set F

The above property implies that concretizing any n propositions cannot resolve foils that weren't resolved by the individual propositions. The idea of generating resolution sets are again closely related to the idea of resolving counterexamples and can be understood

Proposition 5. For two modelsM1, M2 and a set of foils F , if M1 ⊑ M2 then for any proposition p, RF ({M1}, p) ⊆ RF ({M2}, p)

The above proposition ensures that if an explanation is the minimal one for Mmin, then it must be the minimal explanation for MH as well.

These propositions will be instrumental in proving the effectiveness of our greedy algorithm described by Algorithm 1. In each iteration of this search, the algorithm greedily chooses the proposition that minimizes Cp |F ′∩RF (M′ ,p)| , where F ′ is the set of unresolved foils at that iteration and the search ends when all foils are resolved.

Theorem2. The explanation ̂ E generated by Algorithm 1 for a set of foils F and a lattice L = 〈M, E, P, ℓ〉 is less than or equal to (ln k)∗CEmin , where CEmin is the cost of an optimal explanation and k represents the maximum number of foils that can be resolved by concretizing a single proposition, i.e, k = maxp |RF (Mmin, p)|.

Proof (Sketch). We will prove the above theorem by showing that Algorithm 1 corresponds to the greedy search algorithm Algorithm 1 Greedy Algorithm for Generating ̂ E

• 1: procedure GREEDY-EXP-SEARCH 2: Input: 〈F,L = 〈M, E, P, ℓ〉〉 3: Output: Explanation ̂ E 4: Procedure: 5: curr model = 〈Mmin, F〉 6: ̂ E = {} 7: Mmin ←MinimalAbstractModels(L, F) 8: Precompute the resolution sets RF (Mmin, p) for each p ∈ P 9: while True do 10: M′ , F ′ = curr model 11: if |F ′ | = 0 then return ̂ E ▷ Return ̂ E if all the foils are resolved 12: else 13: pnext = argminp( Cp |F ′∩RF (M′ ,p)| ) 14: Mnew = {γpnext (M)|M ∈ M′ } 15: curr model = 〈Mnew, F \ RF (M′ , p)〉 16: ̂ E = ̂ E ∪ p

for a weighted set cover problem. Consider a weighted set cover problem 〈U, S,W〉 such that the universe set U = F, the subcollections set S is defined as S = {sp|p ∈ P} where sp = RF (Mmin, p) and the cost of each subset sp is gives as W(sp) = Cp. Proposition 4 ensures that the size of resolution set is a submodular and monotonic function. In this setting, the act of identifying a set of propositions that resolve the foil set is identical to coming up with a set cover for U in the new weighted set cover problem. Furthermore, we can show that the optimal set cover Copt must correspond to the cheapest explanation Emin (We can prove this equivalence using Propositions 1,2 and 4, we are skipping the details of this proof due to space constraints). Algorithm 1 describes a greedy way of identifying the cheapest set cover for this weighted set cover problem and thus the minimal explanation for the original problem. For weighted set cover the above greedy algorithm is guaranteed to generate solutions that are at most ln k∗W(Copt) [Young, 2008], where k = maxs∈S |s| and this approximation guarantee will hold for Emin as well.

We can use this algorithm to either generate solutions and or to calculate an inadmissible heuristic for the previously mentioned A* search. For the heuristic generation, we will further simplify the calculations (specifically step 8 in Algorithm 1) by considering an over-approximation of RF . Instead of considering the set of all foils resolved by concretizing each proposition p, we will consider the set of foils where p appears in the precondition of one of the actions in it. This set should be a superset for RF for any proposition.

4 Empirical Evaluations

In our evaluation, we wanted to understand how effective our approaches were in terms of the conciseness of the explanations produced, the solution computation time and the usefulness of approximation. For the approximation, we were interested in identifying the trade-off between decrease in runtime vs. reduction in solution quality.

All three explanation methods discussed in this paper (blind, heuristic and greedy) were evaluated on five IPC benchmark domains[International Planning Competition, 2011]. All the experiments detailed in this section were run on an Ubuntu workstation with 64G RAM.

For each domain, we selected 30 problems from either available test sets or by using standard problem generators (the problems sizes were selected to reflect the size of previous IPC test problems). The lattice for each problem-domain pair was generated by randomly selecting 50% of domain predicates and then generating a fully connected proposition conserving lattice using that set of predicates. Since none of the models contained any conditional effects or negative preconditions, we created the abstract models by dropping the propositions to be abstracted from the domain models (which are complete for these domains). The foils were generated by selecting random models from the lattice and creating plans from these models that do not hold in the concrete model. Each search evaluated here, generates the set of proposition whose concretizations can resolve the foils set F. In actual applications, this set of propositions needs to be converted into an explanan (the actual message) by considering how this proposition is used in the robot model. Figure 3 shows the explanation generated by our approach for a problem in Rover domain.

The table in Figure 4 presents the results from our empirical evaluation on the IPC domains. The table shows the average cost/size of each explanation along with the time taken to generate them. Note that by size, we refer to the number of predicates that are part of the explanation while the cost reflects the total number of unique model updates induced by that explanation. We attempted explanation generation for foil set sizes of one, two and four per problem.

Our main conclusion is that heuristic search seems to outperform blind search in almost every problem and generates near-optimal solutions (Blind search always generates the minimal explanation). Further, we saw that greedy search outperformed heuristic search in most cases barring a few exceptions. The greedy search was able to make significant gains especially for higher foil set sizes. This is entirely expected due to the fact that step 8 in Algorithm 1 can be expensive for problems with long plans (but still polynomial). This expensive pre-computation pays off as we move to cases where Emin consists of multiple propositions. Additionally, we found out that greedy solutions were quite comparable to the optimal solutions with respect to their costs. For example in |F | = 4 for satellite domain, while the greedy solution cost took a penalty of ∼ 1.4% the search time was reduced by ∼ 68%. Figure 5 plots the comparison between the time saved by the greedy search versus any loss in optimality incurred by the greedy search.

5 RelatedWork

There is increasing interest within the automated planning community to solve the problem of generating explanations for plans ([Fox et al., 2017; Langley et al., 2017]). Earlier works like [Seegebarth et al., 2012; Bercher et al., 2014; Kambhampati, 1990] looked at explanations as a way of describing the effects of plans, while works like [Sohrabi et al., 2011; Meadows et al., 2013] looked at plans itself as explanations for a set of observations. Another approach that has received a lot of interest recently is to view explanations as a way of achieving model reconciliation [Chakraborti et al., 2017]. Such explanations are seen as a solution to a model reconciliation problem (referred to as MRP) and this approach postulates that the goal of an explanation is to update the model of the observer so they can correctly evaluate the plans in question.

Similar to MRP, we can also see our explanations as model updates, but we focus on a specific type of update, namely model concretization. Unlike MRP we do not make any assumptions about the availability of human model or the human's computational capabilities. The assumption that we have access to foils help us scale to much larger problems as compared to the original MRP approach to generate contrastive explanations. Following the conventions of the original MRP paper, we can see that the explanations studied here are both complete and monotonic.

As noted, our work is closely related to the well studied method of counter-example guided refinement or CEGAR that was originally developed for Model checking. Many planning works have successfully used CEGAR based methods to generate heuristics for plan generation ([Seipp and Helmert, 2013; 2014]). The idea of foil resolution set for a given concretization is also closely related to the process of identifying spurious counter examples employed by CEGAR based methods (c.f [Haslum et al., 2012; Keyder et al., 2012; Steinmetz and Hoffmann, 2016]). One major difference between our work and standard CEGAR based methods is the fact that in our setting the abstract model producing the foil (or counter-example) is unknown. Since we are exclusively dealing with spurious counter-examples we are also not bound to testing our foils (in other words identifying faults or pivot states) in the most concrete model (which could be quite expensive). Further, traditional CEGAR methods are generally not as focused on identifying the cheapest refinements.

Many abstraction schemes have been proposed for planning tasks (starting with [Sacerdoti, 1974]), but in this paper, we mainly focused on state abstractions and based our formulation on previous works like [Srivastava et al., 2016] and [Backstrom and Jonsson, 2013]. It would be interesting to see how we can extend the approaches discussed in this paper to handle temporal and procedural abstractions (e.g., HLAs [Marthi et al., 2007]).

6 Conclusion and Discussion

In this paper, we investigated the problem of generating explanations when the explainee understands the task model at a lower levels of abstraction. We looked at how we can use explanations as concretization for such scenarios and proposed algorithms for generating minimal explanations. One unique aspect of our approach is the use of foils as a way of capturing human confusion about the problem. This not only helps us formulate more efficient explanation generation methods but also aligns with the widely held belief that human expect contrastive explanations (c.f. [Lombrozo, 2012; 2006]). Moreover, in most real-world scenarios humans usually include the foil in the request for explanations unless the foil is quite apparent from the context. Future directions include extending the methods to handle models that are incorrect in addition to being imprecise and looking at other possible methods for abstraction. We also plan to perform human factors studies on this explanation paradigm to evaluate its effectiveness.

Acknowledgments

We thank Dan Weld for helpful comments on a previous draft. This research is supported in part by the AFOSR grant FA9550-18-1-0067, ONR grants N00014161-2892, N0001413-1-0176, N00014- 13-1-0519, N00014-15-1-2027, and the NASA grant NNX17AD06G.