<figure><img src="image_1.png" /></figure>

HAL
open science

Predictive models & reasoning with explanations

Ryma Boumazouza

► To cite this version:

Ryma Boumazouza. Predictive models & reasoning with explanations. Artificial Intelligence [cs.AI]. Université d'Artois, 2022. English. NNT: tel-04507525

HAL Id: tel-04507525

https://hal.science/tel-04507525

Submitted on 16 Mar 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

Public Domain
ÉCOLE DOCTORALE SCIENCES TECHNOLOGIES ET SANTÉ N°585

Predictive models & reasoning with
explanations

DOCTORAL THESIS

presented and publicly defended on 08 December 2022

in partial fulfillment of requirements for the degree of

Doctor of Philosophy of Artois University
in Computer Science

by

Ryma BOUMAZOUZA

Doctoral Committee

Advisors: Bertrand MAZURE Professor, Artois University
Karim TABIA Assoc. Professor, Artois University

Supervisor: Fahima CHEIKH-ALILI Assoc. Professor, Artois University

Chair: Sylvain LAGRUE Professor, Compiègne University

Reviewer: Marie-Jeanne LESOT Assoc. Professor, Sorbonne University

Examiner: Christine SOLNON Professor, INSA Lyon

CENTRE DE RECHERCHE EN INFORMATIQUE DE LENS - CNRS UMR 8188

Université d'Artois, rue Jean Souvraz, S.P. 18 F-62307, Lens Cedex France

Secrétariat : +33 (0)3 21 79 17 23

http://www.cril.univ-artois.fr
Mise en page avec memcril (B. Mazure, CRIL) et thloria (D. Roegel, LORIA).
Acknowledgements

This doctoral journey has been quite incredible despite the several ups and downs including the enormous
pressure during the pandemic. Although it is often said that to pursue a thesis is a lonesome journey,
that was not the case with this one. I am grateful to all of those with whom I have had the pleasure to
spend this journey.

This work would not have been possible without the financiel support of the Région Hauts-de-France
and the Artois University. I would like to thank them along with the CRIL laboratory for supporting this
thesis.

I take this moment to express my gratitude to my supervisors: starting with my co-thesis director
Mr. Karim TABIA, who have been supportive and pushed me to learn by doing. My supervisor Mme.
Fahima CHEIKH-ALILI has been quite encouraging and supportive throughout this journey, and I must
thank her for the pleasing conversations on both scientific research and life in general. My thesis director
Mr. Bertrand MAZURE has provided me with his thoughtful advice and pitched in at important times.

I am grateful to each of the members of my Dissertation Committee for evaluating my thesis work.
I would like to begin by thanking Mme. Marie-Jeanne LESOT and Sylvain LAGRUE for reviewing my
thesis. I would also like to thank Mme. Christine SOLNON for examining my thesis. I am very thankful
to all of you for your insightful comments and thought-provoking questions during the defense session.

During this thesis, as I moved to a foreign country, the experience has been enlightening. I am
thankful to each one of my friends and colleagues at CRIL laboratory for the in-depth discussion on
various topics and the light moments during the coffee and tea breaks. I cherish to have known Sara,
Marie, Alexis, Thanh, Hugues, Anasse, Ikram, Yazid, Chouaib, Thibault, Karen, Antony and Romain.

Lastly, I would be remiss in not mentioning or not thanking the members of my family and loved
ones : Hiba, Sidahmed, Wafa, Ines, Azwaw and Maïa. I could not have undertaken the pursuit of this
project without them. I am especially thankful to my parents, whose love and guidance are with me
whatever I pursue and whose support and proud were always a motivation for me.

I would like to dedicate this thesis in memory of my loved grandmother who always prayed for me
and to my loved grandfather who always encouraged me to work hard and live with dignity and pride.
I dedicate this thesis
to my family.
# Contents

List of Figures ix

General introduction 1

Background and notations

<table><tbody><tr><td>1</td><td>Classification problems</td><td>4</td></tr><tr><td>1.1</td><td>Single-label classification</td><td>5</td></tr><tr><td>1.2</td><td>Multi-label classification</td><td>6</td></tr><tr><td>2</td><td>Propositional logic and Boolean satisfiability</td><td>7</td></tr><tr><td>2.1</td><td>Syntax of propositional logic</td><td>7</td></tr><tr><td>2.2</td><td>Semantics of propositional logic</td><td>8</td></tr><tr><td>2.3</td><td>Normal forms</td><td>9</td></tr><tr><td>3</td><td>Boolean satisfiability problem</td><td>9</td></tr><tr><td>3.1</td><td>Boolean satisfiability problem</td><td>9</td></tr><tr><td>3.2</td><td>Partial Maximum Satisfiability problem</td><td>11</td></tr></tbody></table>
# Part I State-of-the-art

<table><tr><td><strong>Chapter 1 Explainable AI</strong></td><td><strong>14</strong></td></tr><tr><td>1.1 Explainable Artificial Intelligence</td><td>15</td></tr><tr><td>1.1.1 The need to explanation</td><td>16</td></tr><tr><td>1.1.2 Purpose of interpretability</td><td>17</td></tr><tr><td>1.1.3 Audiences interested in explainable AI</td><td>18</td></tr><tr><td>1.2 Related works</td><td>18</td></tr><tr><td>1.2.1 Interpretable models (intrinsic methods)</td><td>19</td></tr><tr><td>1.2.2 Post-hoc interpretability</td><td>21</td></tr><tr><td>1.2.3 Local interpretability versus global interpretability</td><td>31</td></tr><tr><td><strong>Chapter 2 XAI methodologies</strong></td><td><strong>34</strong></td></tr><tr><td>2.1 Ad-hoc methods</td><td>34</td></tr><tr><td>2.2 Formal methods</td><td>34</td></tr><tr><td>2.2.1 Knowledge compilation</td><td>35</td></tr><tr><td>2.2.2 Abductive reasoning</td><td>36</td></tr><tr><td>2.3 Conclusion</td><td>37</td></tr></table>

# Part II Symbolic explanations

<table><tr><td><strong>Chapter 3 Symbolic explanations for single-label classification</strong></td><td><strong>41</strong></td></tr><tr><td>3.1 General framework</td><td>42</td></tr><tr><td>3.2 Encoding of the model</td><td>44</td></tr><tr><td>3.2.1 Direct encoding into CNF</td><td>44</td></tr><tr><td>3.2.2 Surrogate model encoding into CNF</td><td>49</td></tr><tr><td>3.3 Enumeration of symbolic explanations</td><td>52</td></tr><tr><td>3.3.1 Satisfiability solving for explanation generation</td><td>52</td></tr></table>
<table><tbody><tr><td>3.3.2</td><td>Enumerating sufficient reason explanations (SR<sub>x</sub>)</td><td>53</td></tr><tr><td>3.3.3</td><td>Enumerating counterfactual explanations (CF<sub>x</sub>)</td><td>54</td></tr><tr><td>3.3.4</td><td>On enumerating sufficient reasons and counterfactuals</td><td>56</td></tr><tr><td>3.3.5</td><td>Beyond SR<sub>x</sub> and CF<sub>x</sub> explanations</td><td>59</td></tr><tr><td>3.4</td><td>Experimental study</td><td>60</td></tr><tr><td>3.4.1</td><td>Results</td><td>61</td></tr><tr><td>3.5</td><td>Conclusion</td><td>68</td></tr><tr><td colspan="2"><strong>Chapter 4 Symbolic explanations for multi-label classification</strong></td><td><strong>70</strong></td></tr><tr><td>4.1</td><td>Brief review of related works</td><td>70</td></tr><tr><td>4.2</td><td>Feature-based explanations</td><td>71</td></tr><tr><td>4.2.1</td><td>Entire-outcome explanations</td><td>73</td></tr><tr><td>4.2.2</td><td>Fine-grained explanations</td><td>74</td></tr><tr><td>4.3</td><td>Label-based explanations</td><td>76</td></tr><tr><td>4.3.1</td><td>Impact of presence of relationships on explanations</td><td>81</td></tr><tr><td>4.4</td><td>A model-agnostic SAT-based approach for enumerating symbolic explanations</td><td>82</td></tr><tr><td>4.4.1</td><td>Step 1: Multi-label classifier symbolic modeling</td><td>83</td></tr><tr><td>4.4.2</td><td>Step 2: Symbolic explanation enumeration</td><td>84</td></tr><tr><td>4.5</td><td>Experimental analysis</td><td>87</td></tr><tr><td>4.5.1</td><td>Results</td><td>89</td></tr><tr><td>4.6</td><td>Conclusion</td><td>92</td></tr></tbody></table>

## Part III Feature-attribution explanations

<table><tbody><tr><td colspan="2"><strong>Chapter 5 Feature attribution explanations for single-label classification</strong></td><td><strong>94</strong></td></tr><tr><td>5.1</td><td>Feature attribution explanations</td><td>94</td></tr><tr><td>5.1.1</td><td>Review of related works</td><td>94</td></tr><tr><td>5.2</td><td>Feature attribution explanations for single-label classification</td><td>95</td></tr><tr><td>5.2.1</td><td>Properties of symbolic explanations and scoring functions</td><td>99</td></tr><tr><td>5.2.2</td><td>Properties of features-based explanations and scoring functions</td><td>100</td></tr><tr><td>5.3</td><td>Experimental results</td><td>102</td></tr><tr><td>5.4</td><td>Conclusion</td><td>105</td></tr></tbody></table>
<table><tr><td>Chapter 6 Feature-attribution explanations for multi-label classification</td><td>107</td></tr><tr><td>6.1 Introduction</td><td>107</td></tr><tr><td>6.2 Aggregation-based feature attribution</td><td>108</td></tr><tr><td>6.2.1 Three basic properties for feature attribution in multi-label classification</td><td>109</td></tr><tr><td>6.2.2 Aggregation operators</td><td>111</td></tr><tr><td>6.3 Multi-label feature attribution through problem transformation</td><td>112</td></tr><tr><td>6.4 Multi-label feature attribution through symbolic explanations</td><td>113</td></tr><tr><td>6.4.1 Generating symbolic explanations</td><td>113</td></tr><tr><td>6.4.2 From symbolic explanations to feature attributions</td><td>113</td></tr><tr><td>6.5 Experimental study</td><td>114</td></tr><tr><td>6.5.1 Evaluating aggregation-based feature attribution scheme</td><td>115</td></tr><tr><td>6.5.2 Evaluating problem transformation-based feature attribution scheme</td><td>117</td></tr><tr><td>6.5.3 Evaluating symbolic explanation-based feature attribution scheme</td><td>117</td></tr><tr><td>6.5.4 Comparative study</td><td>122</td></tr><tr><td>6.5.5 Evaluating feature attribution inference</td><td>123</td></tr><tr><td>6.6 Conclusion</td><td>126</td></tr><tr><td>Conclusion and future work avenues</td><td>127</td></tr></table>

Bibliography
List of Figures

<table>
  <tbody>
    <tr>
      <td>1.1</td>
      <td>The need for explainable AI (Illustration from DARPA XAI Program [GA19])</td>
      <td>15</td>
    </tr>
    <tr>
      <td>1.2</td>
      <td>Trade-off between the accuracy of models and their interpretability. (Illustration from DARPA XAI Program [GA19])</td>
      <td>16</td>
    </tr>
    <tr>
      <td>1.3</td>
      <td>Audience interested in explainable AI (Illustration from [Hin19])</td>
      <td>18</td>
    </tr>
    <tr>
      <td>1.4</td>
      <td>Example of a feature importance for a global and local explanation for a malware detection system based on a linear model and boolean features (Illustration from [Mel21])</td>
      <td>20</td>
    </tr>
    <tr>
      <td>1.5</td>
      <td>Example of a decision tree classifier with 3-classes (Illustration from [Fis36])</td>
      <td>20</td>
    </tr>
    <tr>
      <td>1.6</td>
      <td>Example of interpretable decision set.</td>
      <td>21</td>
    </tr>
    <tr>
      <td>1.7</td>
      <td>Visualization of the pixel-wise decomposition process of the LRP method. (Illustration from [BBM<sup>+</sup>15])</td>
      <td>23</td>
    </tr>
    <tr>
      <td>1.8</td>
      <td>Example of visualization techniques highlighting the pixels' relevance for the "cat" and "dog" classes. Sub-figures (a,d) correspond to original image with a cat and a dog. (b,e) correspond to guided Backpropagation [SDBR14] highlighting all contributing features. (c, f) correspond to Grad-CAM output localizing class-discriminative regions. (Illustration from [SCD<sup>+</sup>17])</td>
      <td>24</td>
    </tr>
    <tr>
      <td>1.9</td>
      <td>Example presenting the intuition behind LIME. The blue/pink background represents the model's decision function f. The bold red cross in the sample to explain x. The samples around x gets predictions from f and are weighted by their proximity to x (represented here by size). The dashed line is the function g learned (locally faithful to f). (Illustration from [RSG16])</td>
      <td>26</td>
    </tr>
    <tr>
      <td>1.10</td>
      <td>Explanation for a prediction with LIME. The top three predicted classes are "tree frog", "pool table" and "balloon". (Illustration from [MTR16])</td>
      <td>27</td>
    </tr>
    <tr>
      <td>1.11</td>
      <td>Example of visualization plots explanations from [CE13].</td>
      <td>28</td>
    </tr>
    <tr>
      <td>1.12</td>
      <td>Example of the ICE and the PDP of a prediction with respect to feature X<sub>1</sub> (Illustration from [GKBP15])</td>
      <td>29</td>
    </tr>
    <tr>
      <td>1.13</td>
      <td>Example of a counterfactual explanation scenario (Illustration from [SGZS21])</td>
      <td>30</td>
    </tr>
    <tr>
      <td>1.14</td>
      <td>Example from [KK19b] representing the prediction of an input sample and its neighbors.</td>
      <td>31</td>
    </tr>
    <tr>
      <td>1.15</td>
      <td>Taxonomy of machine learning interpretability techniques</td>
      <td>32</td>
    </tr>
    <tr>
      <td>3.1</td>
      <td>Methodologies proposed within the explainability techniques</td>
      <td>42</td>
    </tr>
    <tr>
      <td>3.2</td>
      <td>A global overview of the proposed approach</td>
      <td>43</td>
    </tr>
    <tr>
      <td>3.3</td>
      <td>A naive Bayes network classifier and its corresponding OBDD.</td>
      <td>45</td>
    </tr>
    <tr>
      <td>3.4</td>
      <td>Off-set of a Boolean function represented by an Ordered Binary Decision Diagram.</td>
      <td>46</td>
    </tr>
    <tr>
      <td>3.5</td>
      <td>A random forest classifier trained on the neighborhood of x</td>
      <td>51</td>
    </tr>
    <tr>
      <td>3.6</td>
      <td>The random forest paths set by x</td>
      <td>56</td>
    </tr>
    <tr>
      <td>3.7</td>
      <td>Set of MUSes and MCSes of the CNF Σ from Example 19.</td>
      <td>57</td>
    </tr>
    <tr>
      <td>3.8</td>
      <td>The classification accuracy of RF models with respect to the max_depth parameter.</td>
      <td>62</td>
    </tr>
  </tbody>
</table>
<table>
  <tbody>
    <tr>
      <td>3.9</td>
      <td>Example to compare the average total number of CF<sub>x</sub> explanations with respect to the neighborhood size when it is limited to a maximum number (|V<sub>x</sub>| ≤ T) or not limited.</td>
      <td>63</td>
    </tr>
    <tr>
      <td>3.10</td>
      <td>The classification accuracy of RF models with the respect to the neighborhood size.</td>
      <td>64</td>
    </tr>
    <tr>
      <td>3.11</td>
      <td>The classification accuracy of RF models with respect to the ntree parameter.</td>
      <td>65</td>
    </tr>
    <tr>
      <td>3.12</td>
      <td>The percentage of relevant features w.r.t the initial feature space composed of 784 variables for the MNIST dataset.</td>
      <td>66</td>
    </tr>
    <tr>
      <td>3.13</td>
      <td>The range of explanations size enumerated for the different datasets.</td>
      <td>68</td>
    </tr>
    <tr>
      <td>3.14</td>
      <td>Example inputs from MNIST dataset and their respective symbolic explanations.</td>
      <td>69</td>
    </tr>
    <tr>
      <td>4.1</td>
      <td>Binary Relevance classifier trained on the Yelp dataset using decision trees as base classifiers</td>
      <td>72</td>
    </tr>
    <tr>
      <td>4.2</td>
      <td>Illustration of a fine-grained counterfactual</td>
      <td>76</td>
    </tr>
    <tr>
      <td>4.3</td>
      <td>Feature-based explanation for a sample from augmented MNIST dataset.</td>
      <td>77</td>
    </tr>
    <tr>
      <td>4.4</td>
      <td>Combining feature and label-based explanation for a sample from augmented MNIST.</td>
      <td>78</td>
    </tr>
    <tr>
      <td>4.5</td>
      <td>Decision tree classifiers trained on different labels.</td>
      <td>80</td>
    </tr>
    <tr>
      <td>4.6</td>
      <td>Overview of the proposed approach for the multi-label setting</td>
      <td>82</td>
    </tr>
    <tr>
      <td>5.1</td>
      <td>Focus on the Step 3 of the proposed approach</td>
      <td>96</td>
    </tr>
    <tr>
      <td>5.3</td>
      <td>Extent of E(x, f) in the neighborhood V(x, 3) = {x', x''}.</td>
      <td>97</td>
    </tr>
    <tr>
      <td>5.4</td>
      <td>Cover of the variables in the explanation set E(x, f).</td>
      <td>98</td>
    </tr>
    <tr>
      <td>5.5</td>
      <td>Cover of variables in E(x, f) in the neighborhood V(x, 3).</td>
      <td>98</td>
    </tr>
    <tr>
      <td>5.6</td>
      <td>Examples of explanations on a test input negatively predicted from the SPECT dataset.</td>
      <td>103</td>
    </tr>
    <tr>
      <td>5.7</td>
      <td>SHAP values for test input explained in Figure 5.6.</td>
      <td>104</td>
    </tr>
    <tr>
      <td>5.8</td>
      <td>Heatmaps in columns (b-c) representing the (FI) score, and (d-e) the (FR) computed over the SR<sub>x</sub> and CF<sub>x</sub> of the samples data from MNIST (column a) in comparison to heatmaps of the SHAP values (column f).</td>
      <td>104</td>
    </tr>
    <tr>
      <td>5.9</td>
      <td>Average (and maximum) proportion of common important variables between SHAP explanations and those of our ASTERYX approach.</td>
      <td>105</td>
    </tr>
    <tr>
      <td>6.1</td>
      <td>Illustrative figure of the problem studied</td>
      <td>108</td>
    </tr>
    <tr>
      <td>6.2</td>
      <td>Example illustrating the sensitivity property evaluated on the explanations of a multi-label prediction.</td>
      <td>109</td>
    </tr>
    <tr>
      <td>6.3</td>
      <td>Example illustrating the data-explanation stability evaluated on the explanations of a multi-label prediction.</td>
      <td>110</td>
    </tr>
    <tr>
      <td>6.4</td>
      <td>Evaluating label-explanation correlation using the mutual information (MI) coefficient.</td>
      <td>117</td>
    </tr>
    <tr>
      <td>6.5</td>
      <td>Evaluating label-explanation correlation using the Pearson's R coefficient.</td>
      <td>117</td>
    </tr>
    <tr>
      <td>6.6</td>
      <td>Evaluating label-explanation stability using the mutual information (MI) coefficient.</td>
      <td>122</td>
    </tr>
    <tr>
      <td>6.7</td>
      <td>Evaluating label-explanation stability using the Pearson's R coefficient.</td>
      <td>123</td>
    </tr>
    <tr>
      <td>6.8</td>
      <td>Average difference between real vs deduced feature attribution scores (SHAP/LIME) given the MI between labels.</td>
      <td>124</td>
    </tr>
    <tr>
      <td>6.9</td>
      <td>Average difference between real vs deduced feature attribution scores(FR/FIxFG) given the MI between labels.</td>
      <td>125</td>
    </tr>
  </tbody>
</table>
# General introduction

## Context and motivations

As our daily environment increasingly incorporates artificial intelligence (AI), it has become important to understand how models make decisions, particularly in a context where user confidence in the AI technology has become a societal issue. The explainability field became a hot topic and has grown along with the rapid rise of « black-box » machine learning techniques such as deep learning and the start of DARPA's eXplainable Artificial Intelligence (XAI) program [GA19] in 2016. Especially with the recent regulations of the European General Data Protection Regulation (GDPR) that came into effect in 2018, which requires providing explanations to users both for legal and ethical reasons. For instance, the Article 22 imposing a right to "information about the logic involved" forces the explanations to represent the inner logic of a system and need to be faithful to it. This is particularly important in high stakes decision making settings such as medical decision support system, military and security applications. To comply with all those regulations and needs, several approaches were proposed to explain the decision function of a classifier or explain predictions individually. The aim of such XAI methods is to provide in addition to a prediction, interpretable and useful information that justifies and explains a prediction.

Despite the rapid growth in attention on eXplainable AI, most of the current explainability methods for black-box models are ad-hoc. Namely, the feature relevance techniques that are among the most popular approaches and that have received much attention in the machine learning literature face critical issues that prevent their deployment. Indeed, much of these techniques have focused on estimating importance score, for how much a given input feature contributes to a model's output by the means of non-deterministic components. For instance, LIME [RSG16] (Local Interpretable Model-agnostic Explanations) uses random perturbation during the sampling process which results in shifts in data and instability in the generated explanations. Yet, in a context where XAI methods are expected to generate robust and stable explanations (i.e same explanations given the same instance and model with the same configuration), there is no guarantee that the explanations generated using ad-hoc methods are not accurate nor sufficient and they may even suffer from instability (i.e different explanations can be generated for the same prediction) due to random perturbations often used in this type of methods. These are critical issues that can prevent deployment of such methods in sensitive domains and limit their use. On the other hand, there exist formal methods to generate rigorous explanations for different machine learning models. However, the main bottleneck of such methods is their efficiency in computing explanations when it comes to large input feature sets. In addition, most of the current formal methods use information about the model and deal with its inner working to interpret the results, reducing the type of predictor to use to a set of interpretable models, that relatively enjoy a less good predictive performance compared to some black-box models.

The challenge that this thesis attempts to address is to understand what is happening beneath the surface and explain how black-boxes make decisions, and thus by integrating concepts and formalism of symbolic AI. We try to leverage formal methods and logical reasoning to develop a novel local model-agnostic interpretability approach for explaining the prediction of black-box classifiers, for both multi-
class and multi-label settings. Our contributions include the proposal of an explainability method that combines both the "agnostic" nature of numerical methods and offers more "rigorous" explanations that characterize symbolic explanations. We use propositional logic as a formalization framework to associate some logical representation (encoding) to our machine learning model. Thus, we reduce the given problem of explaining individual predictions to a variant of the propositional Boolean satisfiability problem (SAT). We use SAT solvers as the problem solving engine without implementing dedicated programs. This makes our approach efficient since SAT solvers are extremely well studied. Note that SAT framework is just one possibility and that other constraint solvers (e.g Satisfiability Modulo theories (SMT), Mixed-integer linear programming (MILP), etc) can be used for a similar process. Therefore, our approach is centered around Minimal Unsatisfiable Subsets (MUS) and Minimal Correction Subsets (MCS) and provides a comprehensive solution for feature importance on both explanations and variables level.

We present an approach based on modeling the problem in the form of variants of the propositional satisfiability problem (SAT) in order to take advantage of the strengths of already existing and proven SAT technologies, and of the powerful practical tools for the generation of MCSes and MUSes. Then, we propose to overcome the complexity of encoding a machine learning classifier into an equivalent logical representation by the means of a surrogate model. This latter will be used to symbolically approximate the original model in the vicinity of the sample of interest, allowing it to be locally faithful [RSG16]. We propose two complementary types of symbolic explanations which are *sufficient reasons* and *counterfactuals*. Given an input data item and its prediction, a *sufficient reason* would answer the question : "What *are the feature values in the input which are sufficient in order to trigger the prediction whatever the values of the other variables?"" while a *counterfactual* explanation would answer the question : "Which *values are sufficient to change in the input to have a different prediction?*". This type of questions is fundamental for the end-user's understanding and for the explanations to be usable. The adequate type of explanation is directly linked with the end user. For instance, what may be important for the doctors in a XAI method is to know if they can act (need an actionable explanation) and not only understand how the algorithm works. From another perspective, domain experts may require to observe the effects and the results which will provide an intuition about the data that can directly help them to understand the decision process and how the model works.

As for the multi-label setting, we propose semantics and reasoning approaches to infer from first
level explanations provided by the base classifier explanations the multi-label explanations. We adapt
our agnostic and declarative approach to provide different types of symbolic explanations for multi-label
classifiers. The explanations proposed are distinguished according to the associated semantics (sufficient
reasons or counterfactuals), the elements composing an explanation (features, labels or a combination
of the two) and the level of granularity of the explanations (the whole prediction or parts of the predic-
tion). We will also be particularly interested in so-called feature-attribution explanations. We propose
three schemes to achieve feature attribution for multi-label tasks using existing attribution methods as
oracles, namely i) an aggregation-based scheme, ii) a problem transformation-based scheme and iii) a
symbolic explanation-based one. A property we call label-explanation correlation, specific to multi-label
classification is used in addition to the extension of the basic properties of sensitivity and stability to the
multi-label setting.

**Organization of the manuscript**

This manuscript is composed of three parts. The first one is devoted to the state-of-the-art and the second and third parts bring together the contributions of this thesis.
The **Background and notations** section is a reminder of the basic notions of classification, propositional logic and Boolean satisfiability problem that constitute the technical preliminaries necessary to the understanding of the rest of the manuscript. In the first part, **Chapter 1** is devoted to explainability in AI. We present the eXplainable Artificial Intelligence field, the need to explanation and the different purposes and audiences of an XAI method. We present a review of the different explainability methods proposed by the community. We rely on a taxonomy that depends on what the methods explain (intrinsic/post-hoc) and how they are applied (local/global) in order to distinguish the methods of explainability. We present within the **Chapter 2** of the first part two main methodologies of the XAI methods : Ad-hoc methods and formal based ones.

The contributions are presented within the second and third part of this thesis. **Chapter 3** is dedicated to the symbolic explanations for single-label classification. We define the different types of symbolic explanations we propose to enumerate and we present a general framework of our **declarative** and **model-agnostic** approach. This latter allows to provide sufficient reason and counterfactual explanations based on SAT technologies.

**Chapter 4** describes our contributions to provide different types of symbolic explanations for multi-label classifiers, where a prediction is a subset of labels. More precisely, in addition to global sufficient reason and counterfactual explanations, our approach makes it possible to generate explanations at different levels of granularity in addition to structural relationships between labels (provides both feature and label-based explanations).

**Chapter 5** and **6** are dedicated to the feature-attribution explanations. We describe in **Chapter 5** how we associate scores reflecting the relevance of the explanations and the features w.r.t some properties, in order to explain individual predictions of single-label classifiers. We present a set of fine-grained properties allowing to analyze, rank and select explanations and a set of scores allowing to assess the relevance of explanations and features w.r.t the suggested properties. In **Chapter 6**, we propose three schemes to achieve feature attribution for multi-label tasks using existing attribution methods as oracles. The first scheme is based on aggregating feature attribution scores obtained for each label while the second one is based on problem transformation. The third scheme combines problem transformation with symbolic explanations. In order to evaluate the quality of feature attributions, we extend the basic properties of sensitivity and stability to the multi-label setting and propose a third property, called label-explanation correlation, specific to multi-label classification. Moreover, we propose to exploit the correlations between labels in order to infer feature attributions from already computed explanations.

## Publications

→ R. Boumazouza, F. Cheikh-Alili, B. Mazure, K. Tabia, A Symbolic Approach for counterfactual explanations in the 14th International Conference on Scalable Uncertainty Management (SUM20), September 2020.

→ R. Boumazouza, F. Cheikh-Alili, B. Mazure, K. Tabia, A Model-Agnostic SAT-based approach for Symbolic Explanation Enumeration in the 23rd International Conference on Artificial Intelligence (ICAI'21), July 2021.

→ R. Boumazouza, F. Cheikh-Alili, B. Mazure, K. Tabia, ASTERYX: a model-Agnostic SaT-basEd appRoach for sYmbolic and score-based eXplanations in the 30th ACM International Conference on Information and Knowledge Management (CIKM), November 2021. (Core rank A)
# Background and notations

Machine Learning (ML) is a sub field of AI that is specifically focused on learning a model from data without being explicitly programmed. Machine learning can be supervised (relies on labelled data) or unsupervised (processes unlabelled data). The first one fits the data while the second one separates and explores the data. Supervised learning deals with two main tasks that are regression and classification. In this thesis, we deal with classification where we propose an approach to explain individual predictions of classifiers.

## 1 Classification problems

In this thesis, we want to explain supervised Machine Learning (ML) models trained for classification problems. We define in the following what is a classifier and present the different types of classification. We provide some details about single-label classification problems in section 1.1 and multi-label classification problems in section 1.2.

In supervised learning, a structured dataset for classification is defined as set of instances of the form $(x, y)$ where $x = (x_1, ..., x_n)$, $n \in N$, is an input vector called features (or variables, attributes) and $y$ is an outcome variable often called the label (or class variable or target). We denote by $X$ the feature space and $Y$ the outcome space. We use the notation $\{,}$ to denote the domain of a discrete variable and $| \cdot |$ to denote its size. Classification is a supervised machine learning task whose aim is to predict the class (output) variable based on the values of the input variables. In [dCF09], it is defined as the process of approximating the mapping function that associates input samples to corresponding target classes (labels).

**Definition 1.** (*Decision function*) A decision function of a classifier is a function $f : X \to Y$ mapping each instantiation $x$ of $X$ to $y=f(x)$.

A decision function describes the classifier's behavior to perform classification. We distinguish three main types of classification problems :

* Binary classification: This task involves predicting one of two classes ($|Y|=2$). A binary classifier is defined as $f: X \to \{0, 1\}$.

* Multi-class classification: This task deals with predicting one class among a set of classes with $|Y|> 2$. A multi-class classifier is defined as $f: X \to Y$ where $|Y|> 2$.

* Multi-label classification: This task involves predicting a subset of labels for each instance. Contrary to binary and multi-class classification, classes are not mutually exclusive in multi-label tasks. A multi-label classifier is defined as follows : $f: X \to Y = (Y_1, ..., Y_k)$ where $Y$ is a vector of binary variables ($Y_i=1$ denotes the fact that the label $l_i$ is predicted positively).
## 1.1 Single-label classification

Single-label classification is concerned with learning from a set of examples that are associated with a single class *y* from a set of disjoint labels (classes are mutually exclusive). It covers binary and multi-class classification (|Y|> 2). Among the main applications where binary classification is used, there is disease diagnosis [GLB+10, PGA08], spam and malware detection [SKG09]. Multi-class classification is also used in different applications such as character recognition [AJM12, CVKRBA12], biometric identification [TYRW14], computer security [RSE16], etc.

Several multi-class classification techniques exist such as multi-layer perceptron (MLP)[Hay94], decision trees (DT)[WKQ+08], k-nearest neighbors (k-NN)[Alt92], support vector machines (SVMs)[CV95], naïve bayes classifier (BNC)[HY01]. The choice of the learning algorithm to use should take into account the specific application requirements and many other factors such as the type and number of features, interpretability, accuracy, etc.

**Evaluation measures** There are several ways to measure a classifier accuracy and generalization quality. The most known for multi-class classification are accuracy, precision, and recall. The accuracy is a metric used to assess the performance of a model and it is used to measure how well the classifier predicts.

**Confusion matrix** A confusion matrix is a summary of the prediction results in a classification problem. Table 1 illustrates an example of a confusion matrix for the case of binary classification.

* True Positive (TP) : For correctly predicted positive values.

* True Negative (TN) : For correctly predicted negative values.

* False positive (FP) : For values incorrectly predicted as positive.

* False Negative (FN) : For values incorrectly predicted as negative.

<table><caption>Table 1: Confusion matrix</caption><thead><tr><th rowspan="2" scope="col">Predicted class</th><th colspan="2" scope="colgroup">Actual class</th></tr><tr><th scope="col">Positive (P)</th><th scope="col">Negative (N)</th></tr></thead><tbody><tr><th scope="row">Positive (P)</th><td>TP</td><td>FP</td></tr><tr><th scope="row">Negative (N)</th><td>FN</td><td>TN</td></tr></tbody></table>

**Accuracy** It is defined as the number of predictions a model correctly makes divided by the total number of predictions made.

$$ Accuracy(acc) = \frac{TP + TN}{TP + TN + FP + FN} \qquad (1) $$

**Precision** As the name suggests, precision determines how precise and correct the model is with respect to positive predictions (how many of them are actually positive).

$$ Precision = \frac{TP}{TP + FN} \qquad (2) $$
**Recall** Is defined as the proportion of positive predictions made among the total number of positive samples. It measures the model's ability to detect positive samples.

$$ \text{Recall} = \frac{TP}{TP + FP} \qquad (3) $$

## 1.2 Multi-label classification

In contrast to single-label classification in which instances can only belong to a single class, in multi-label classification instances are associated with a vector of (binary) variables $Y = (Y_1, ..., Y_k)$. Multi-label classification is very common in many real-world applications [TKV09]. It is a well-known predictive task in many domains such as text categorization (where each document can belong at the same time to several predefined topics. For example, a conference paper may at the same time be labeled as *Artificial intelligence* and *Philosophy*), object recognition in images, sentiment analysis, audio, text categorization, video categorization [BLSB04], bioinformatics, information retrieval, multimedia content annotation, web mining, protein function classification [EW01], music categorization [LO03] and so on.

A dataset in multi-label classification is a collection of couples $(x,y)$ where $x$ is an instance of $X$ and $y$ a vector of binary variables in $Y$ encoding the true labels associated with $x$.

**Definition 2 (Multi-label classifier).** A multi-label classifier is a function mapping each input data instance $x$ to a multi-label prediction $y$. Each input $x$ is a vector of $n$ values assigned to $X$. Each corresponding output is a vector $y$ of $k$ binary values assigned to $Y$. Given the prediction $y=f(x)$, the instance $x$ is classified by $f$ in the label $Y_j$ if $Y_j=1$ in the prediction $y$.

**Example 1.** Table 2 represents an example of a multi-label dataset. Assume a multi-label text classification problem of studying toxic comments online. For the sake of simplicity, assume that each comment is described by a set of keywords. Using a binary bag-of-words representation, each comment will have a set of binary features where feature $X_i = 1$ (resp. $X_i = 0$) denotes that keyword $X_i$ is present (resp. absent) in the comment. In this example, the feature space $X$ is composed of five binary variables associated to five keywords. The set of labels $Y$ is composed of seven classes : toxic, severe_toxic, obscene, threat, insult, identity_hate and none. A toxic comment might at the same time be about any of or none of them. The variable $Y_j = 1$ (resp. $Y_j = 0$) denotes the fact that the current comment is positively labelled i.e. $Y_j = 1$ (resp. not labelled, $Y_j = 0$) in label $Y_j$.

<table><caption>Table 2: Example of a multi-label dataset.</caption><thead><tr><th>X = (X<sub>1</sub>, X<sub>2</sub>, X<sub>3</sub>, X<sub>4</sub>, X<sub>5</sub>)</th><th>Y = (Y<sub>1</sub>, Y<sub>2</sub>, Y<sub>3</sub>, Y<sub>4</sub>, Y<sub>5</sub>, Y<sub>6</sub>, Y<sub>7</sub>)</th></tr></thead><tbody><tr><td>0 1 0 1 1</td><td>1 1 0 1 0 0 0</td></tr><tr><td>1 0 1 1 0</td><td>0 1 0 0 0 1 1</td></tr><tr><td>1 0 0 1 1</td><td>0 0 0 1 1 0 1</td></tr><tr><td>0 0 0 1 1</td><td>1 0 0 0 1 0 1</td></tr><tr><td>...</td><td>...</td></tr><tr><td>1 0 0 0 1</td><td>1 0 0 1 1 0 1</td></tr></tbody></table>

**Remark 1.** The label space $Y = (Y_1, .., Y_k)$ (interchangeably denoted as $L = \{l_1, .., l_k\}$) is consisting of $k$ binary variables encoding the presence/absence of the $k$ labels.

As for categories of multi-label classifiers, there exist mainly three :
1. **Problem transformation approaches** where the multi-label classification problem is transformed into a set of multi-class classification or mono-label regression problems. Examples of methods in this category are Binary Relevance (BR) [LDB+12], Classifier Chains (CC) [RPHF09] and Label Powerset (LP) [TV07, RPH08, TK07].

2. **Method adaptation approaches** based on extending multi-class techniques to predict instead of one single class a set of relevant labels. Examples of this category are ML-kNN [ZZ05] and ML-C4.5 [CK01].

3. **Ensemble approaches** that combine ideas from the two first categories. RAndom k labEL sets (RAkEL) [TV07], Hierarchy Of multi-label classifiERs (HOMER) [TKV08], Ensemble of Classi-fier Chains (ECC) [RPHF09] and Ensemble of Binary Relevance (EBR) [RPHF11].

One of the characteristics of multi-label data that must be taken into consideration compared to the multi-class datasets is the density of labels. This characteristic defined as the average number of labels per dataset entry divided by the number of labels is very low in most multi-label datasets [BdSRM14] and can impact the multi-label learning. Another difference worth mentioning compared with the multi-class case is related to evaluation metrics used to assess the accuracy of multi-label techniques. Indeed, standard multi-class classification metrics (e.g. precision, recall) are no more enough and appropriate measures are specifically designed for this purpose (e.g. Hamming-Loss).

# 2 Propositional logic and Boolean satisfiability

Propositional logic (PL) is a framework for representing knowledge in a logical form. It is the simplest kind of logic and is also called Boolean logic. The term "proposition" refers to a statement which can be either true or false. The propositions are linked together with logical connectives such as **and**, **or** and **not**.

## 2.1 Syntax of propositional logic

The syntax of propositional logic defines the allowable propositions to be used to represent the knowl-edge. In what follows, we define the basic elements of the language (propositions and connectives) and the structuring rules.

A propositional language $\mathcal{L}$ is composed of:

• a set of propositional variables (atoms) noted $V$;

• logical connectives (also called logical operators) $\neg$, $\vee$, $\wedge$, $\Rightarrow$, $\Leftrightarrow$ respectively corresponding to the Negation, Disjunction, Conjunction, Implication and Logical equivalence;

• Boolean constants $\top$ for True (equivalent to 1) and $\bot$ for False (equivalent to 0);

• parenthesis;

**Definition 3.** (*Propositional variable*) *a propositional variable (also called atom) is a Boolean variable that takes the value true or false.*

An atomic proposition consists of a single proposition symbol (it contains no logical connectives) and it is the fundamental block from which more complex statements can be built.

**Definition 4.** (*Literal*) A literal is either a propositional variable $\ell$ or its logical negation $\neg\ell$ (also called complement or negation of $\ell$).
**Example 2.** Let $\alpha$ be a Boolean variable, $\alpha$ and $\neg\alpha$ are respectively positive and negative literals.

**Definition 5.** (Formula) A formula is said to be a Well-Formed Formula (WFF) if it belongs to one of this set of formulae :

* $\top$ and $\bot$ are formulae;

* an atom $\alpha$ is a formula;

* if $\alpha$ is a formula then $\neg\alpha$ is a formula;

* $\alpha \lor \beta$ is a formula if $\alpha$ and $\beta$ are formulae;

* $\alpha \land \beta$ is a formula if $\alpha$ and $\beta$ are formulae;

* $\alpha \Rightarrow \beta$ is a formula if $\alpha$ and $\beta$ are formulae;

* $\alpha \Leftrightarrow \beta$ is a formula if $\alpha$ and $\beta$ are formulae;

**Example 3.** Let $\mathcal{V} = \{a, b, c, d\}$ be a set of propositional variables. An example of a well-formed formula can be $((a \lor b \lor \neg d) \land (a \lor c))$.

We define in the next section how semantics are associated to formulae.

## 2.2 Semantics of propositional logic

**Definition 6.** An interpretation $\mu$ of a propositional formula $\alpha$ is an application that assigns values from $\{0, 1\}$ to every propositional variable. It is therefore a function :

$$ \mu : \mathcal{V}_{\alpha} \rightarrow \{0, 1\} $$

An interpretation $\mu$ satisfies a formula $\alpha$ iff $\mu$ satisfies all sub-formulae of $\alpha$. We can determine the truth value of any formula using the usual semantics of logical operators.

**Remark 2.** An interpretation can be complete (assigns a value to every propositional variable appearing in a formula $\alpha$) or partial (assigns values to a subset of propositional variables appearing in a formula $\alpha$).

**Remark 3.** An interpretation $\mu$ can be written in the form $\{v_1 \rightarrow b_1, \dots, v_n \rightarrow b_n\}$ where $v_i \in \mathcal{V}$ is a propositional variable and, $b_i \in \{0, 1\}$ the Boolean value associated to it. It can also be represented in a more compact way using only the literals.

**Example 4.** Let $\mathcal{V} = \{a, b\}$ be a set of propositional variables. An example of an interpretation is $\mu = (a \rightarrow 1, b \rightarrow 0)$. It can also be written as $\mu = (a, \neg b)$.

**Definition 7.** (Model) An interpretation $\mu$ making a formula $\alpha$ true is called a model of $\alpha$ ($\mu(\alpha) = 1$).

Similarly, an interpretation $\mu$ making a formula $\alpha$ false is called a counter-model of $\alpha$ ($\mu(\alpha) = 0$).

**Example 5.** Let $P = \neg(a \land b) \Rightarrow \neg b$ be a formula. The interpretation $\mu = \{a, \neg b\}$ is a model of $P$ while $\mu' = \{\neg a, b\}$ is a counter-model.

**Definition 8.** (Equivalent formulae) Two propositional formulas $\alpha$ and $\beta$ are equivalent and we note $\alpha \equiv \beta$, when they take the same truth value for all the interpretations.

**Definition 9.** (Satisfiable formula) A formula $\alpha$ is satisfiable (consistent) if there is an interpretation that makes it true. In other terms, $\alpha$ has at least one model.

Similarly, a formula $\alpha$ is unsatisfiable (inconsistent) if there is no model for it. A "Tautology" refers to a propositional formula that is always true. A "Contradiction" is a proposition formula that is always false.
## 2.3 Normal forms

We present within this section two normal forms used in propositional logic: Disjunctive Normal Form (DNF) and Conjunctive Normal Form (CNF).

Using the introduced definitions, we can define the following.

**Definition 10.** (Disjunctive Normal Form (DNF)) A propositional formula is in disjunctive normal form (DNF) if it is a disjunction of conjunctive clauses. A conjunctive clause is a conjunction of literals.

**Definition 11.** (Conjunctive Normal Form (CNF)) A propositional formula is in conjunctive normal form (CNF) if it is a conjunction of disjunctive clauses. A disjunctive clause is a disjunction of literals.

**Example 6.** Here is an example of a CNF formula referred to as $\Sigma$. $T_i$ refers to clauses at position i in $\Sigma$.

$$ \Sigma = \begin{array}{llllll} T_1 & & T_2 & & T_3 & & T_4 \\ (l_1) & \wedge & (\neg l_2) & \wedge & (l_1 \vee l_3) & \wedge & (\neg l_1 \vee l_2) \\ & & & & & & \end{array} $$

**Remark 4.** A clause composed of one literal is called a unit clause. A clause composed of n literals is called n-ary clause.

It is possible to convert statements into a conjunctive normal form (CNF) that are written in another form, such as disjunctive normal form (DNF).

In our work, we used the Conjunctive Normal Form as the target representation. Namely, we take a binary machine learning model $f$, together with a data instance, and produce a propositional CNF formula $\Sigma$ which has the same number of models as $f$ and with respect to the number of the input variables. Such encoding is required in order to use the Boolean satisfiability solvers as the problem solving engine.

# 3 Boolean satisfiability problem

We present within this section different definitions and concepts of the Boolean satisfiability problem.

## 3.1 Boolean satisfiability problem

The Boolean satisfiability problem (also called SAT for short) is a decision problem consisting in determining whether the variables in a given Boolean formula can be assigned so that the formula evaluates to TRUE. SAT was the first problem to be shown to be NP-complete by Cook's theorem [Coo71] which is the basis of NP-completeness theory and the P = NP problem. Despite this worst-case complexity, recent SAT-solving algorithms are capable of solving problem instances involving tens of thousands of variables and formulas consisting of millions of symbols [OSC07] which is sufficient for many practical SAT problems.

**Definition 12.** (SAT: The Boolean satisfiability problem) the Boolean satisfiability problem is the decision problem, which, given a CNF formula, determines whether there is an assignment of propositional variables that makes the formula true.

**Example 7.** The formula $(x_1 \wedge x_2) \vee \neg x_1$ where $x_1$ and $x_2$ are Boolean variables is satisfiable since if $x_1$ takes the value False, the formula evaluates to True.
Using a SAT-solver, one can decide if a CNF formula is satisfiable and can enumerate its models. In case a formula is unsatisfiable, one may need to identify subsets of clauses that cause the inconsistency or identify parts of the clauses to relax in order to restore the consistency.

**Definition 13. (MUS)** A Minimal Unsatisfiable Subset (MUS in short) is a minimal subset $\Gamma$ of clauses of a CNF $\Sigma$ such that $\forall \alpha \in \Gamma$, $\Gamma \setminus \{\alpha\}$ is satisfiable.

Intuitively, it is enough to have the subset $\Gamma$ so that the formula $\Sigma$ becomes inconsistent. A MUS is a sufficient reason for inconsistency. An unsatisfiable CNF $\Sigma$ can have many MUSes.

**Example 8.** Let $\Sigma$ be a CNF formula composed of six clauses ($\alpha_i$) where $\Sigma = \{\alpha_1 = (a \lor b), \alpha_2 = (\neg a \lor b), \alpha_3 = (a \lor \neg b), \alpha_4 = (\neg a \lor \neg b), \alpha_5 = (\neg b), \alpha_6 = (b)\}$. The set of MUSes for $\Sigma$ is the following:

$$ \text{MUSes}(\Sigma) = \{\{\alpha_1, \alpha_2, \alpha_3, \alpha_4\}, \{\alpha_1, \alpha_2, \alpha_5\}, \{\alpha_3, \alpha_4, \alpha_6\}, \{\alpha_5, \alpha_6\}\} $$

**Definition 14. (MSS)** A maximal satisfiable subset (in short, MSS) $\Phi$ of a CNF $\Sigma$ is a subset of clauses $\Phi \subseteq \Sigma$ that is satisfiable and such that $\forall \alpha \in \Sigma \setminus \Phi, \Phi \cup \{\alpha\}$ is unsatisfiable.

**Definition 15. (MCS (Co-MSS))** A minimal correction subset (in short MCS, also called Co-MSS) $\Psi$ of a CNF $\Sigma$ is a set of formulas $\Psi \subseteq \Sigma$ whose complement in $\Sigma$, i.e., $\Sigma \setminus \Psi$, is an MSS of $\Sigma$.

**Example 9.** Given the CNF formula from Example 8, the set of MCSes is the following:

$$ \text{MCSes}(\Sigma) = \{\{\alpha_1, \alpha_6\}, \{\alpha_2, \alpha_6\}, \{\alpha_3, \alpha_5\}, \{\alpha_4, \alpha_5\}\} $$

Intuitively, an MCS is subset of $\Sigma$ that restores its satisfiability once removed and it is minimal (i.e. removing any smaller subset cannot restore the consistency). The enumeration of MUSes/MCSes is a well-known problem dealt with in many areas such as knowledge-base reparation. Recent years have witnessed the proposal of a large number of tools and novel algorithms for the extraction and enumeration MUSes/MCSes [GMP07, LS08, MPMS15, BK15, LPMMS16, BK16, MIPMS16, PMJMS18, NBMS18, BČB18].

A well-known minimal hitting set (MHS) relationship between MUSes and MCSes exists and is expressed as follows:

**Proposition 1.** MCSes are MHSes of MUSes and vice-versa.

This duality was originally presented in [Rei87] in the context of model-based diagnosis and was later investigated in [BL03] for propositional formulas in clausal form. Many of the proposed MUS enumeration algorithms are based on this duality between MUSes and MCSes. Given the set of MCSes, each MUS is an irreducible subset of the clauses that covers<fnref n="1" /> all of these MCSes and vice versa.

The computational complexity of finding a MUS or an MCS are already established in the literature as they are well-studied problems. The extraction of a MUS is a problem of complexity $FP^{NP}$ and checking whether there exists a MUS of size $\le k$ is of complexity $\Sigma_2^P$-complete [Gup06, Lib05]. Computing the smallest MUS (SMUS) is in $FP^{\Sigma_2^P}$. Checking whether a subset of a CNF formula is an MCS is DP-complete<fnref n="2" /> [CT95] and the computation of an MCS is a problem of complexity $FP^{NP}$ [Chr94].

<footnote n="1">¹A clause is said to cover an MCS (resp MUS) if it is included in the MCS (resp MUS).</footnote>

<footnote n="2">²A problem $\mathcal{P}$ belongs to the class DP if it can be written as $\mathcal{P} = \mathcal{P}_1 \cup \mathcal{P}_2$ with $\mathcal{P}_1 \in \text{NP}$ and $\mathcal{P}_2 \in \text{coNP}$.</footnote>
## 3.2 Partial Maximum Satisfiability problem

The maximum satisfiability problem (Max-SAT) is the problem of determining the maximum number of clauses, of a given Boolean formula in conjunctive normal form, that can be made true by an assignment of truth values to the variables of the formula. Formally, we have the following definitions:

**Definition 16. (Max-SAT)** Given a Boolean CNF formula $\Sigma$, Max-SAT is the problem of finding a truth assignment that satisfies the maximum number of clauses in $\Sigma$.

**Example 10.** Let a set of propositional variables $\mathcal{V} = \{x_1, x_2, x_3, x_4\}$ and let a CNF formula $\Sigma = \{(\neg x_1 \lor \neg x_2), (\neg x_1 \lor x_3), (\neg x_1 \lor \neg x_3), (\neg x_2, x_4), (\neg x_2 \lor \neg x_4), (x_1), (x_2)\}$. An example of Max-SAT assignment that maximize satisfied clauses is $(x_1 = 0, x_2 = 0, x_3 = 0, x_4 = 1)$, where only 2 clauses are violated.

The Partial Maximum Boolean Satisfiability (Partial Max-SAT or PMSAT) is an optimization variant of SAT problem defined as follows.

**Definition 17. (Partial Max-SAT)** Given a Boolean CNF formula $\Sigma$ in which some clauses are hard and some are soft, Partial Max-SAT is the problem of finding a truth assignment that satisfies all the hard constraints and the maximum number of soft ones.

In order to solve Partial Max-SAT, we will consider the general setting where a formula is composed of two disjoint sets of clauses $\Sigma = \Sigma_H \cup \Sigma_S$ [BHvM09], where $\Sigma_H$ denotes the hard clauses (which must be satisfied) and $\Sigma_S$ denotes the soft ones (which may be relaxed).

**Definition 18. (Hard and Soft clauses)** Let $\Sigma_1$ and $\Sigma_2$ be two sets of clauses where $\Sigma_2$ is satisfiable. Partial Max-SAT($\Sigma_1, \Sigma_2$) computes one maximal subset of $\Sigma_1$ that is satisfiable with $\Sigma_2$. $\Sigma_1$ and $\Sigma_2$ are called the sets of soft and hard constraints (clauses), respectively.

**Example 11.** Using the same set of propositional variables $\mathcal{V}$ from Example 10, an example of a CNF formula ($\Sigma$) in Partial Max-SAT problem is: $\Sigma = \Sigma_H \cup \Sigma_S$ where $\Sigma_H = \{(x_1 \lor \neg x_2 \lor x_4), (\neg x_1 \lor \neg x_2 \lor x_3)\}$ and $\Sigma_S = \{(\neg x_2 \lor \neg x_4), (\neg x_3 \lor x_2), (x_1 \lor x_3)\}$. An example of Partial Max-SAT solution that satisfies all hard clauses and a maximum number of soft clauses is: $(x_1 = 1, x_2 = 0, x_3 = 0, x_4 = 0)$.
# Part I

## State-of-the-art
Chapter 1

# Explainable AI

Symbolic artificial intelligence, also known as "Good Old Fashioned Artificial Intelligence" (GOFAI) [Hau85] started as philosophers' attempts to describe human thinking as a symbolic system and was often the dominant paradigm in the AI community until the late 1980s. The author in [Wal12] claims that the "classical" or "symbolic" approach comes from the idea that mind and cognition can be understood in broadly mechanical specifically computational terms, giving it an explanatory power. For a long time, symbolic AI, which involves humans in the learning process, took precedence over machine learning AI considered as opaque and incomprehensible to humans. Indeed, symbolic AI systems built of nested if-then statements that allow conclusions to be drawn are considered human-readable. Unlike machine learning from data without being assisted by human beings (abstract and higher-order concepts).

From the 2010s', machine learning suddenly started exploding because of the availability of huge amounts of digital data and of powerful hardware resources (e.g. GPUs) which caused shifts from a knowledge-driven approach to a data-driven approach (IBM's Deep Blue beats the world champion at chess in 1997, ImageNet [KSH12], Deep learning [LBH15], Deepface [TYRW14] involving more than 120 million parameters, etc). The emergence of modern AI systems have raised dramatically and so has their ability to process, analyze and learn from the quantities of data that continue to grow exponentially. The fact remains that most of the performing approaches suffer from lack of robustness and reliability and may be vulnerable to attacks [SZS<sup>+</sup>13, NYC15, MDFF16], in addition to their inability to explain their decisions and actions to human users. It is in this context that the quest for more transparent and interpretable AI has intensified in recent years. Indeed, in symbolic AI, the models used are often simple and are considered as interpretable in comparison to the recent ML models such as Deep neural networks (DNNs) that are lacking transparency.

There is no consensus from the literature on the definition of interpretability or explainability. The author in [Mil19] defines interpretability as "the degree to which a human can understand the cause of a decision". Thus, a model is said to be interpretable if a human is able to understand alone the model decision-making process or predictions by looking at its parameters [Lip18, ADRDS<sup>+</sup>20].

In practice, interpretable AI approaches aim to build machine learning models with low complexity (inherently human-interpretable) while keeping a high level of performances [Mol22]. On the other hand, explainable AI approaches aim at providing accurate and user comprehensible explanations of the underlying complex models to users [WYAL19, Lip18, ADRDS<sup>+</sup>20].
<figure><img src="image_2.png" /><figcaption>Figure 1.1: The need for explainable AI (Illustration from DARPA XAI Program [GA19])</figcaption></figure>

## 1.1 Explainable Artificial Intelligence

The term *eXplainable Artificial Intelligence* (XAI) has been introduced by DARPA [GA19] and has been since used to refer this field that aims at helping users understand the workings of an AI system [Mil19], [GA19], [DVK17], detect data bias and discovering flows in the models. Explainability for AI systems has grown along with the success and adoption of deep learning systems that are applied in many fields where trustworthiness is critically needed such as in legal systems [Lip18, MB18, Rud19], autonomous driving [TPJR18, BTD<sup>+</sup>16], cybersecurity [Vre19, SNPS18, NZ17], phishing detection [SMA<sup>+</sup>18], transportation [ARAB<sup>+</sup>17], law enforcement [DF18], recruiting [Das18], health care and criminal justice [RU18], energy reliability [RPR<sup>+</sup>10], financial risk assessment [CLR<sup>+</sup>18], detecting heart attacks [WRK<sup>+</sup>17], diagnosing Alzheimer's disease [PHL<sup>+</sup>17], assessing recidivism risk [BB13, TvdH13], medical sciences and diagnostics [ADWF15, CNC<sup>+</sup>16, LKB<sup>+</sup>17], surveillance systems [DFL<sup>+</sup>18], biometric and handwritten character recognition [BLS<sup>+</sup>18, SPG<sup>+</sup>19, TVRFOG18] and so on.

Miller [Mil19] suggests the idea that explainability of AI systems can be refined if a close collaboration comes into place between the social science and the XAI researchers. He argues that interactions between human and AI systems can be improved by replicating and understanding from social science how people define, generate, select, present and evaluate explanations and that these mechanisms could be extended to the XAI field. The author in [Mil19] also reviews some of the relevant findings from social science research on human explanation, and has provided some insights into how this work can be used in explainable AI. Other papers also reviewed social science aspects of XAI systems such as [DVKB<sup>+</sup>17] that studies the role of algorithmic transparency and explanation in lawful AI (Trustworthy AI) and [LOL<sup>+</sup>18] that analyzes the fairness and accountability of algorithmic decision-making processes. Several XAI approaches have been proposed to achieve the general goals of accomplishing explainability of AI systems used for high-stakes prediction problems. There are different users or target audience of machine learning methods (e.g. users impacted by model decisions, developers, data scientists, regulatory entities, managers, etc) that require different explanations depending on their goals [ADRDS<sup>+</sup>20, VdWSNI<sup>+</sup>14]. Thereby, the form of the explanations are application and user-dependent.
1.1.1 The need to explanation

Despite the widespread use of XAI methods recently, no proper formal definition of what is an explana-
tion is provided in the literature. We try to present it in the following through the different roles it can
have from an AI perspective. Based on the research in [Mil19] and [AB18], an explanation can be used
to justify the result of a system to a user in order to gain his trust, identify errors in a system to enable
control, get an oversight in case of adverse or unwanted effects such as biased decision-making or social
discrimination, understand a system well in order to improve it and learn knowledge by allowing humans
to discover new facts that are not directly explicit from an AI system.

Explainability is not a new topic and has been dealt with in the 1970’s where expert systems were
already able to provide pieces of explanation [SB75]. It emerged again and became a hot topic since
the adoption of deep learning models, a new generation of AI system called "black-box" models. These
models would return a prediction to a given input but could not provide an explanation for its decision.
"The current generation of AI systems offer tremendous benefits, but their effectiveness will be limited
by the machine’s inability to explain its decisions to users" [GA19]. This trade-off between the accuracy
of these ML models and their ability to be understood by humans is illustrated in Figure 1.2. It is
particularly the case of AI systems which are developed to be used in areas where the decision of an AI
system can have serious consequences and critical situations. The domain experts and users are reluctant
to adopt decisions they cannot understand, which limits the use of machine learning methods in such
sensitive contexts. Recent work have highlighted the vulnerability of deep learning models in different
tasks such as speech recognition [CW18], text classification [ERLD17], malware detection [GPM+17]
and particularly image classification [GSS15, PMJ+16, CW17]. Thus, this kind of system decisions must
be explained in order to prevent errors and gain trust of the user [AB18]. In addition to recent regulations
that has grown a need to explain for both legal and ethical reasons such as the "right to explanation"
introduced by the European General Data Protection Regulation (GDPR) [Vos16] in 2018. Therefor,
we need explanations to decide whether an AI system is robust enough or trustworthy to be used in
safety-critical environments.

<figure><img src="image_3.png" /><figcaption>Figure 1.2: Trade-off between the accuracy of models and their interpretability. (Illustration from DARPA XAI Program [GA19])</figcaption></figure>
1.1.2 Purpose of interpretability

The need for interpretable AI models is motivated by different purposes that can be technical, social or
ethical [BVKV<sup>+</sup>18, DSZ16, Kas21, KK19a, LOL<sup>+</sup>18]. For instance, methods for creating white-box
models aim to increase societal acceptance of machine learning models by establishing trust in decision
results. On the other hand, methods for explaining complex black-box models aim to provide users with
the reasons for models' decision and actionable insights to the results of algorithms. Other methods
were created to promote fairness or to mitigate unwanted algorithmic bias and discrimination and lastly,
methods for analysing the sensitivity of a model predictions to identify errors or biases in training data
that result in adverse and unexpected behaviors (reliability).

XAI methods of the first category design systems based on learning algorithms that are easily un-
derstandable for a human being. This type of models are also referred to as intrinsic, transparent, or
white-box models. Most of the methods of this category include self-explaining models such as linear
models, decision trees and rule-based learners. They are discussed in Section 1.2.1 and a summary of
existing white-box approaches can be found in Table 1.1.

Methods that attempt to explain black-boxes are the most common in the literature. These methods are also called post-hoc methods because they are designed to provide a posteriori explanations for predictive models (e.g random forests, deep neural networks, etc). Several desiderata can be considered to categorize these methods : the type of model to explain (specific/agnostic), the level of interpretability (local/global) or the representation of the explanation. Each of these sub-categories are presented in Section 1.2.2 and a summary of the discussed interpretability methods can be found in Table 1.2 and 1.3.

Another category for interpretability methods are the ones created to promote fairness by check-
ing that the learned model generates decisions that are free from discrimination of specific inputs (e.g.,
admission to a university, and the goal is to prevent discrimination against individuals based on their
membership to some group). These kinds of methods are necessary especially when working with sen-
sitive data that can potentially affect human lives. The existing fairness methods usually evaluate the
fairness of a ML system by checking the models' predictions and errors across certain demographic seg-
ments (e.g. groups of a specific ethnicity or gender). The authors in [KAAS12] presented prejudice,
underestimation, and negative legacy as three major causes of unfairness in ML models and analyzed
them. In [HPS16], the authors proposed a framework for quantifying and reducing discrimination in ML
models. In [ZVRG17], a new metric for evaluating decision boundary fairness with respect to one or
more sensitive features was introduced. Other approaches were proposed to train models to make fair
predictions by removing bias from both training data and model predictions. The authors in [ZVR<sup>+</sup>17]
propose to use collective preference of different demographic groups as a base to define notions of fair-
ness. The authors in [ABD<sup>+</sup>18] considered certain definitions of fairness previously outlined as special
cases and proposed to incorporate them into a systematic framework.

The last category is the sensitivity-based interpretability methods proposed to analyze the trustwor-
thiness and reliability of the model’s predictions. Those methods rely on the property of stability of the
decision function and the sensitivity of its output. The idea is to check if a small perturbation of an input
may lead to a significant perturbation of the outcome. A large set of adversarial examples approaches
based on sensitivity analysis have been proposed within the literature [GSS15, MDFF16, MDFFF17,
DLP<sup>+</sup>18, CW17, NK17, LCLS17, BRB18, DLT<sup>+</sup>18, ZAG18, LLS<sup>+</sup>17]. They aim at finding impercep-
tible changes in the input to fool models into producing incorrect predictions. Sensitivity analysis can
be broadly partitioned into black-box and white-box methods and can also be both a global and local
interpretation technique.
1.1.3 Audiences interested in explainable AI

The purpose of the explanation and its form are linked to the audience for which it is intended. The type
of explanations will vary according to different groups of people and their role in the system [BXS<sup>+</sup>20,
Hin19]. Thus, to provide meaningful explanations we need to determine who is receiving the explanation
(see Figure 1.3). For domain experts such as medical doctors or insurance agents, the purpose of an
explanation is to gain knowledge about its reasoning in order to gain trust in the model itself. For users
such as regulatory entities, the explanation should certify model compliance with the legislation in place
and stated regulatory requirements [Hin19]. The purpose of the explanation for the users affected by
model decisions is to understand their situation and verify the outcome's fairness. As for data scientists
and developers, explanations are meant to improve the model efficiency, evaluate the training data and
facilitate the debugging process.

<figure><img src="image_4.png" /><figcaption>Figure 1.3: Audience interested in explainable AI (Illustration from [Hin19])</figcaption></figure>

In this thesis, we consider all the cases where an explanation is provided to a user without making
any assumptions about his background (can be a domain expert, a decision maker or any user who is not
familiar with AI technology).

1.2 Related works

There is more than a single way to classify XAI methods in the literature, which makes it not easy
to list them giving the different perspectives. Especially for supervised ML classification techniques
that has been extensively studied in the field of explainable AI, where most of the works in the cur-
rent literature propose methods to explain the predictions of this type of models such as feature at-
tributions approaches[RSG16, LL17], decision rules [RSG18, JCS<sup>+</sup>20], logic-based [SCD18b, DH22,
INMS19a] and counterfactual examples that has been attracting attention in recent years [WMR17,
VDH20, KTKA20, AALC21, DPB<sup>+</sup>19, DCL<sup>+</sup>18, GWE<sup>+</sup>19, HHDA18, KTKA20, KBBV20, LK21,
MST20, MTS19, Rus19, vdWRvD<sup>+</sup>18]. We will mention different interpretability methods according
to the taxonomy presented in [Mol22] where the interpretability methods were summarized as : intrinsic
or post-hoc methods, designed as model-specific or model-agnostic methods and provide local or global
<table><caption>Table 1.1: Summary of intrinsic interpretability methods.</caption><thead><tr><th>Acronym</th><th>Ref</th><th>Target Model</th><th>Data Type</th><th>Year</th></tr></thead><tbody><tr><td>InterpretML</td><td>[CLG<sup>+</sup>15]</td><td>Generalized Additive Model (GAM)</td><td>tab<sup>3</sup></td><td>2015</td></tr><tr><td>iBCM</td><td>[KGJS15]</td><td>Bayesian Models</td><td>tab</td><td>2015</td></tr><tr><td>—</td><td>[LRMM15]</td><td>Decision Lists<sup>4</sup></td><td>tab</td><td>2015</td></tr><tr><td>Slim</td><td>[UR16]</td><td>Linear Integer Model</td><td>tab</td><td>2016</td></tr><tr><td>AIX360</td><td>[DGW18]</td><td>Boolean Decision Rules</td><td>tab</td><td>2018</td></tr><tr><td>—</td><td>[IPNMS18]</td><td>Decision sets<sup>5</sup></td><td>tab</td><td>2018</td></tr><tr><td>—</td><td>[WDGG19]</td><td>Generalized Linear Models (GLM)</td><td>tab</td><td>2019</td></tr><tr><td>—</td><td>[HRS19]</td><td>Decision Trees</td><td>tab</td><td>2019</td></tr></tbody></table>

explanations. Accordingly, we review and categorize in this section the state-of-the-art approaches for XAI.

### 1.2.1 Interpretable models (intrinsic methods)

Interpretable models are readily interpretable by design which makes their predictions and behaviors directly (human) understandable. Intrinsic interpretability consists in using interpretable models that have a low complexity given their simple structure and then derive straightforward explanations from it (self-explaining). The common learning algorithms that are considered interpretable by humans are linear and logistic regression, rule-based models and short decision trees [Fre14, HDM<sup>+</sup>11, RSG16]. Although these models offer better interpretability, they have limited performance on high-dimensional data and are considered directly interpretable only if the number of features and classes is limited and the size of the model is reasonable.

#### Linear models

Linear models are among the simplest classification models in supervised learning and demonstrate a good generalization abilities. A linear model associates an output class to an input instance $x$ by computing a weighted sum of the features, where each weight represents the relevance of a feature. Such models make the assumption of linear dependence between the input variables and the output class which makes them highly interpretable. The influence of a feature on a prediction is actually the value of each parameter $w^i$, associated to the variable $X_i$ [RSG16]. The feature $X^i$ contributes to increase the model's output by $w^i$ if the weight is positive, and in contrast, decreases it if the weight is negative.

**Example 12.** An example of the features importance explanation is given in Figure 1.4 where we can visualize both the sign and the magnitude of the contribution of the attributes toward the model's behavior (global explanation) and the prediction of the input sample (local explanation).

However, real-world applications do not necessarily assume a linear relationship. In order to cope with this restrictions, other extensions of linear models exist. For instance, the Generalized Linear Models (GLMs) which allow to model all types of outcomes and Generalized Additive Models (GAMs) to model nonlinear relationships. GAM is able to interpret linear and logistic regression, single trees and tree ensembles (bagged trees, boosted trees, boosted bagged trees and random forests).

<footnote n="3">³tab is a short of tabular data.</footnote>

<footnote n="4">⁴Decision lists models are a series of IF-THEN statements (for example, if high blood pressure, then stroke).</footnote>

<footnote n="5">⁵Decision sets can be viewed as unordered sets of rules, under some sort of rule non-overlap constraint.</footnote>
<figure><img src="image_5.png" /><figcaption>Figure 1.4: Example of a feature importance for a global and local explanation for a malware detection system based on a linear model and boolean features (Illustration from [Mel21]).</figcaption></figure>

## Decision trees

A Decision tree (DT) is a hierarchical structures used for both classification and regression problems [BFOS84, LR76, Qui87b]. It is a powerful technique used to fit data and it is widely adopted when the relation between the features and the outcome is non-linear or when the features are not independent from each other. A decision tree is designed with an explainable structure where a tree is grown on training set. The internal nodes corresponding to the features are split nodes where each one represents a test (for numerical features, does the feature have a value lower or greater than a threshold). In a classification setting, the leaf nodes of a tree represent the output classes. Given an input instance, the solution path in the decision tree presents the path from the root to the leaf. This path called a *decision rule* is associated to every decision made by the tree and can be understood even by non-expert users as long as the number of features remains reasonable. Thus, the interpretability of DTs relies on the *decision rule* set.

**Example 13.** An example of a decision tree trained on IRIS-flower dataset.

<figure><img src="image_6.png" /><figcaption>Figure 1.5: Example of a decision tree classifier with 3-classes (Illustration from [Fis36]).</figcaption></figure>

Decision trees have long been considered as embodying interpretable classifiers in ML [Bre01b,
Fre14, Mol22] and have been adopted to globally explain neural networks [CS95, KSB99] and tree ensembles [HH18, TSHW20]. Nevertheless, recent works argued that interpretability of DTs can be compromised due to the large size of its explanations [BMPS20, ABB$^{+}$21, HIIM21].

Rule-based learners

Together with decision trees, rule-based learners (RBML) are considered closer to human reasoning
[BJL09, PGG$^{+}$19]. Rule-based learners are systems that create their own models by learning rules that
characterize the data to fit. Given the data and their corresponding output classes, a rule-based model
learns a set of rules in different forms (IF-THEN structure, a combination of rules, etc).

Several rule-based methods have been proposed in the last few years where the learned rules are used
to explain the model's prediction [NAC02, LBL16, MVED17]. Authors in [WRDV$^{+}$17] proposed an
algorithm ((Bayesian Rule Sets) to build Bayesian classifiers by learning short rule sets. These models
are interpretable by humans since they produce a set of rules that concisely describe a specific class.
The proposed method in [LBL16] learns rules by optimizing a loss function that directly depends on the
length of the explanations (rules) generated.

**Example 14.** This example presents a rule set learned using the method proposed in [LBL16].

<figure><img src="image_7.png" /><figcaption>Figure 1.6: Example of interpretable decision set.</figcaption></figure>

The rule generation approaches have the advantage of being transparent and explainable if the gen-
erated rules set coverage (number of rules) and specificity (number of predicates in a rule) are kept
constrained since the number of conditions can significantly grow given the number of features or the
output classes [HDM$^{+}$11].

1.2.2 Post-hoc interpretability

Post-hoc interpretability (also referred to as post-modeling explainability) is another approach mainly
used for the models with higher complexity [RPF$^{+}$21, Lip18]. These methods analyze the models that
are not transparent by design. A black-box predictor is an opaque system where the mapping from input
to output is invisible to the user or they are known but uninterpretable by humans. Depending on the
level of interpretation, post-hoc methods may explain a model locally or globally.

Model-specific methods

Model-specific methods can only be used to interpret a specific family of models and provide model-
based types of explanation. They are usually used to weight the importance of the features for the
model's decision [Bre01a, OMS17, YCN$^{+}$15, JMD$^{+}$05] and they rely on the internal states of the learn-
ing mechanism to derive an explanation. Most of them approximate the behavior of the black-box by

<footnote>$^{6}$tab/img/txt are a short for tabular/image/text.</footnote>
<table><caption>Table 1.2: Summary of post-hoc XAI methods.</caption><thead><tr><th>Name</th><th>Ref</th><th>Model-Specific vs Model-Agnostic</th><th>Data Type</th><th>Year</th></tr></thead><tbody><tr><td>G-REX</td><td>[JKN04]</td><td>Agnostic</td><td>tab/img/txt<sup>6</sup></td><td>2004</td></tr><tr><td>ICE</td><td>[KKS07]</td><td>Agnostic</td><td>tab</td><td>2007</td></tr><tr><td>PDP</td><td>[Fri01]</td><td>Agnostic</td><td>tab</td><td>2007</td></tr><tr><td>SAlib</td><td>[SRA<sup>+08</sup>]</td><td>Agnostic</td><td>tab</td><td>2008</td></tr><tr><td>DeLP3E</td><td>[SSF14]</td><td>Specific (Bayesian)</td><td>tab</td><td>2014</td></tr><tr><td>DeepExplain</td><td>[ZF14]</td><td>Specific (CNN)</td><td>img</td><td>2014</td></tr><tr><td>iNNvestigate</td><td>[SDBR14]</td><td>Specific (CNN)</td><td>img</td><td>2014</td></tr><tr><td>LIME</td><td>[RSG16]</td><td>Agnostic</td><td>tab/img/txt</td><td>2016</td></tr><tr><td>CAM</td><td>[ZKL<sup>+16</sup>]</td><td>Specific (CNN)</td><td>img</td><td>2016</td></tr><tr><td>MMD-critic rationale</td><td>[KKK16]</td><td>Specific (Bayesian)</td><td>tab</td><td>2016</td></tr><tr><td></td><td>[LBJ16]</td><td>Specific (DNN)</td><td>txt</td><td>2016</td></tr><tr><td>SHAP</td><td>[LL17]</td><td>Agnostic</td><td>tab/img/txt</td><td>2017</td></tr><tr><td>fair-classification</td><td>[ZVR<sup>+17</sup>]</td><td>Agnostic</td><td>tab</td><td>2017</td></tr><tr><td>fairness</td><td>[DHP<sup>+12</sup>]</td><td>Agnostic</td><td>tab</td><td>2018</td></tr><tr><td>L2X</td><td>[CLP<sup>+18</sup>]</td><td>Agnostic</td><td>tab</td><td>2018</td></tr><tr><td>CAV</td><td>[KWG<sup>+18</sup>]</td><td>Specific (DNN)</td><td>tab/img</td><td>2018</td></tr><tr><td>ANCHOR</td><td>[RSG18]</td><td>Agnostic</td><td>tab</td><td>2018</td></tr><tr><td>Grad-CAM++</td><td>[CSHB18]</td><td>Specific (CNN)</td><td>img</td><td>2018</td></tr><tr><td>LEMNA</td><td>[GMX<sup>+18</sup>]</td><td>Agnostic</td><td>tab/img/txt</td><td>2018</td></tr><tr><td>—</td><td>[MWM18]</td><td>Specific (Gradient based)</td><td>tab</td><td>2018</td></tr><tr><td>—</td><td>[SCD18b]</td><td>Specific (Bayesian)</td><td>tab</td><td>2018</td></tr><tr><td>BEEF</td><td>[GPSS19]</td><td>Agnostic</td><td>tab/img/txt</td><td>2019</td></tr><tr><td>—</td><td>[INMS19a]</td><td>Agnostic</td><td>tab</td><td>2019</td></tr><tr><td>DeNNeS</td><td>[MG20]</td><td>Specific (DNN)</td><td>tab</td><td>2020</td></tr><tr><td>Tree explainer</td><td>[LEC<sup>+20a</sup>]</td><td>Specific (Tree-based)</td><td>tab</td><td>2020</td></tr><tr><td>—</td><td>[DH22]</td><td>Specific (DT/BNN)</td><td>tab</td><td>2020</td></tr><tr><td>Glocalx</td><td>[SGM<sup>+21</sup>]</td><td>Agnostic</td><td>tab</td><td>2021</td></tr><tr><td>—</td><td>[DLM<sup>+22</sup>]</td><td>Specific (Tree-based)</td><td>tab</td><td>2022</td></tr><tr><td>DeepGlobal</td><td>[SLZS22]</td><td>Specific (NNs)</td><td>tab/img</td><td>2022</td></tr><tr><td>—</td><td>[FdSRGL22]</td><td>Specific (NNs)</td><td>tab/img</td><td>2022</td></tr></tbody></table>

means of interpretable models (decision rules, decision trees and linear models) as presented in section 1.2.1.

Various methods were proposed to explain the different types of deep learning models. An example of model-specific method for explaining deep learning models is DeepLIFT [SGK17] in which the contributions of all neurons in the network are back-propagated to the input features. Several approaches used to explain different architectures of neural networks propose saliency maps (also referred to as heatmaps) as an explanation. Authors in [ZF14] present a visualization technique to produce saliency maps. The approach relies on assessing the property of sensitivity by iteratively forwarding the same image through the network occluding a different region at a time.

The TreeView method proposed in [TKSR16] extract a visual interpretation via a surrogate decision tree to explain DNNs. The approach takes as input a DNN and a number K given by the user to define the number of hierarchical partitions (clusters) of the feature space. Subsequently, the approach will create a meta-feature associated with each of the K clusters and train a random forest to predict the K
labels. Thus, the decision trees of the random forest are used to build a TreeView representation of the complex model. Other methods were proposed to interpret deep neural networks via decision trees in [WHP$^{+}$18, ZYMW19].

Methods in [SVZ13a, BCC$^{+}$16, ZCAW17, NDY$^{+}$16] aim to explain the inner working of Convolutional Neural Network (CNN) based on activation maximization. The idea is to highlight the areas (pixels) used by the image classification black-box to make a decision. For example, the authors in [ZF14] propose a method based on sensitivity analysis of the network input/output relationship to understand the CNN using visualisation. By backtracking the network computations, the method identifies the regions in input images that are responsible of the activation of certain neurons.

The Layer-wise Relevance Propagation (LRP) [BBM$^{+}$15] is another post-hoc method specific to multi-layered neural networks and Bag of Words (BoW) models built on non-linear kernels. The idea exploited by LRP is to back-propagate the effects of a decision on a given instance to the input level (layer-wise relevance propagation). For instance, building such saliency maps is based on a layer-wise conservation principle. Those heatmaps are comprehensible (to a human) and are used to visually identify which input had how much influence on the predicted output (i.e. which input contributed most to the obtained result). As shown in Figure 1.7, given an input sample x, the LRP method decomposes the classification output into sums of feature and pixel relevance scores. It is a way for obtaining the features importance then visualize it through saliency masks. The pixel-attribution representing the pixel-wise explanation is built using final relevances that correspond to the contributions of single pixels to the prediction.

<figure><img src="image_8.png" /><figcaption>Figure 1.7: Visualization of the pixel-wise decomposition process of the LRP method. (Illustration from [BBM$^{+}$15])</figcaption></figure>

Another type of post-hoc methods specific to deep neural networks that are used to generate saliency maps are the gradient-based and attribution-based methods. The methods of the first category analyze the impact that small changes to the inputs have on the model's outcome (e.g. [SVZ13a]). The methods of the second one compute the contribution of input features to the model's output such that the sum of all contributions should be approximately equal to the output (e.g. [MLB$^{+}$17, STY17]). One interpretation is given as a saliency map. Note that saliency maps need the input to be interpretable. The interpretation of a pixel attribution explanation generated with a gradient-based method is as follows : increasing the color values of the pixel would increase the probability of the predicted class (for positive gradient) or decrease it (for negative gradient). Besides, the effect of a change of a pixel is proportional to the absolute value of the gradient (the larger the value the more the effect) [Mol22].

Another known method for visual explanations for CNN decisions is the Gradient-weighted Class Activation Map (Grad-CAM) [SCD$^{+}$17]. It is actually a generalization of the Class Activation Mapping (CAM) firstly proposed in [ZKL$^{+}$16] and can be used for a wider range of CNN architectures (e.g. fully-
connected layers, structured output such as captioning in multi-task outputs and also for reinforcement
learning). Grad-CAM propagates the gradient into the last convolutional layer. Thus, the relevance score
assigned to each neuron for the decision of interest is the combination of the before last layer’s feature
maps and the output-specific weights. Figure 1.8 shows an example of visualization such as Guided
Back-propagation [SDBR14] and Grad-CAM highlighting the pixels’ relevance for the "cat" and "dog"
classes. An extension of Grad-CAM called Grad-CAM++ was proposed in [CSHB18] to make better
visual explanations of CNN models.

<figure><img src="image_9.png" /><figcaption>Figure 1.8: Example of visualization techniques highlighting the pixels’ relevance for the "cat" and "dog" classes. Sub-figures (a,d) correspond to original image with a cat and a dog. (b,e) correspond to guided Backpropagation [SDBR14] highlighting all contributing features. (c, f) correspond to Grad-CAM output localizing class-discriminative regions. (Illustration from [SCD+17]).</figcaption></figure>

Another trend for post-hoc model specific methods are the symbolic and logic-based XAI approaches
that can be used for different purposes [Dar20]. For instance, sufficient reasons were introduced in
[SCD18b] under the name of *PI-explanations*. Authors in [INMS19b, INMS19a] deal with some forms
of symbolic explanations referred to as abductive explanations (AXp) and contrastive explanations (CXp)
using SMT oracles. In [IMS21, IM21], the authors explain the predictions of decision list classifiers and
decision tree classifiers using a SAT-based approach. Explaining random forests and decision trees is
dealt with for instance in [AKM20b] and [INAM20, IIM20] respectively.

Model-agnostic methods

Model-agnostic methods are not tied to a particular type of function to explain. It means that post-hoc
model-agnostic approaches can be used to provide an explanation for the decisions of any ML model
disregarding its inner processing or internal representations (only need a query-level access). The expla-
nations provided are "model free" and generally based on approximations of the behavior of the learning
mechanisms. Different perspectives to classify post-hoc model-agnostic methods can be considered. In our classification we take into account the explanation technique (explanation by simplification, explanation using formal representation) and the type of explanations presented to the user (feature-based, counterfactual, example-based). We will mention different XAI methods by looking at these perspectives.

**Explanation by simplification**

Explanation by simplification refers to those techniques that rely on building an interpretable model to approximate the original decision function which can be used for explanations purposes. It can be a global surrogate model in order to approximate the behaviour of the original model to explain or a local surrogate model built in the neighborhood of the sample to explain, producing a local approximation of the original target system. The desiderata of a surrogate model is mainly accuracy (how accurate is the model performance on data) and fidelity (how much is good an interpretable model to mimic the behavior of the black-box). For instance, authors in [LRL<sup>+</sup>18] propose to generate surrogate-based explanations for individual predictions based on a sampling centered on particular place of the decision boundary and show the importance of defining the right locality in order to locally approximate accurately the black-box predictions.

The purpose of these approaches by simplification is to reduce the complexity of the model by means of a simplified approximation to gain in interpretability (for example reducing the number of architectural elements or number of parameters of a DNN). Model simplification is usually done by adopting a transparent model (cf section 1.2.1) which is easier to be implemented and explained than black-box systems.

Several methods using a simplified approximation of black-box models have been proposed withing the literature. For instance, the authors in [CS95] proposed a training algorithm TREPAN to approximate the concepts learned by black-box model using decision trees. Authors in [BCNM06, HVD<sup>+</sup>15] proposed knowledge distillation to get a smaller model that is less computationally expensive while approximating the performance of the original model, it has been used in [FH17] to get a decision tree that could explain the predictions of a black-box models. This other known and widely used model-agnostic methods proposed to explain black-box classifiers are LIME [RSG16], SHAP [LL17] and ANCHORS [RSG18]. LIME [RSG16] stands for Local Interpretable Model-agnostic Explanations (LIME), an approach to explain the predictions of any classifier by learning an interpretable model locally around the prediction. LIME uses a linear classifier to approximate local properties of the black-box models and produces coefficients of this surrogate model that is subsequently used as interpretations. Concretely, given an input instance $x$ and its prediction by a black-box model, a surrogate model is trained on a set of randomly generated perturbations of the sample $x$ weighted by their distance to $x$ (see Figure 1.9). An interpretable model $g$ is then trained using a Lasso regression on these synthetic samples in order to optimize the objective function formally defined in [RSG16] as :

$$ \xi(x) = \underset{g \in G}{\operatorname{argmin}}(\mathcal{L}(f, g, \pi_x) + \Omega(g)) \qquad (1.1) $$

The objective function $\xi(x)$ illustrates interpretability vs fidelity trade-off and represents the explanation. It is the sum of: (1) the term representing the local fidelity of $g$ corresponding to the inverse of $\mathcal{L}(f, g, \pi_x)$, and (2) the term representing the complexity of $g$ corresponding to $\Omega(g)$. Note that the number of features for which the explanation should be attributed is given by the user as input and it corresponds to the number of coefficients of the Lasso regression trained on the synthetic samples.

A rule-based improvement of LIME was proposed in ANCHORS [RSG18] for high-precision model-agnostic explanations. Similarly to LIME, ANCHORS generates local explanations for individual predictions of black-box ML models by sampling instances in the vicinity of the sample being explained.
<figure><img src="image_10.png" /><figcaption>Figure 1.9: Example presenting the intuition behind LIME. The blue/pink background represents the model’s decision function $f$. The bold red cross in the sample to explain $x$. The samples around $x$ gets predictions from $f$ and are weighted by their proximity to $x$ (represented here by size). The dashed line is the function $g$ learned (locally faithful to $f$). (Illustration from [RSG16]).</figcaption></figure>

Unlike LIME, ANCHORS explanations are expressed as IF-THEN rules and are faithful by design because the coverage is adapted to the original model’s behavior. A similar approach was proposed in [LKCL19] to capture the behavior of a black-box model using two-level decision sets and allowing users to input the features of interest.

SHAP [LL17] stands for Shapley additive explanations. It is a unifying approach that provides global and local attribution features by computing the Shapley values [Sha53] based on concepts from the coalitional game theory. The Shapley value of a variable is the average of its marginal contributions across all permutations w.r.t to three desirable properties: local accuracy, missingness, and consistency. Hence, SHAP explanations aim at identifying which features contribute the most to the difference in model prediction at a specific input versus a background distribution. Given a instance $x$, the explanation model $g$ used to compute the importance values for each feature proposed by SHAP is defined as :

$$g(x) = \sum_{j=0}^{n} \phi_j, \phi_i \in \mathbb{R} \qquad (1.2)$$

where $\phi_j$ is the contribution of feature $X_j$ to $g(x)$ for all $j \in [1, n]$; and $\phi_0$ is the output of the model when none of the features in $x$ is present.

Unlike LIME that builds sparse linear models around an individual prediction in its local vicinity, SHAP computes all permutations in order to give the exact Shapley values. However, the computational cost of this evaluation is intractable. This variant of SHAP called KernelSHAP is impractical and other model-specific versions have been proposed to overcome this limitation like TreeExplainer [LEC+20b] which computes the exact Shapley values in polynomial time for tree-based models, LinearSHAP (for linear models) and DeepSHAP (for deep neural networks) to compute approximations of the Shapley values [LL17].

Several other post-hoc methods exist (see for instance [ŠK14, DSZ16, LC01, BBM+15]). They are often model-agnostic as they only need to compute the output of a model regardless of its internal working and are listed in Table 1.2.
**Explanation via formal representations** refers to those post-hoc explainability techniques that relies on formal methods and are mainly based on compilation knowledge or abductive reasoning (see section 2.2). Authors in [INMS19a] present a method based on encoding the machine learning model into constraints and provide cardinality and/or minimal explanations by applying abductive reasoning on the model to answer XAI queries. Then Boolean representation of the ML model will be generated and further simplified into symbolic explanations. These later are generally prime implicants, sufficient reasons referred to as abductive explanations (AXp) representing an answer to a "why?" question, or also contrastive explanations (CXp) representing an answer to "why not?" question. More details about this type of approaches are presented in the Section 2.2.

**Feature-based explanations** aim to explain a trained model outcome by computing a relevance score for its input features. These methods are popular in Explainable AI as they give intuitive readings on relations between features and predictions. They generally rely on model simplification explanations (cf section 1.2.2).

For instance, SHAP is a feature attribution method that computes local and global explanations. It estimates the contribution of each feature to a decision value and returns a list of feature attributions to a specific prediction (local explanation) or to the model (global explanation). LIME provides an explanation as a list of feature contributions to the prediction of the instance *x* and highlights the features changes that have the most influence on the prediction. The image illustrated in Figure 1.10 was assigned "tree frog" by Google's Inception neural network. The explanation generated using LIME highlights the most important features, where the classifier primarily focuses on the frog's face as an explanation for the predicted class.

<figure><img src="image_11.png" /><figcaption>Figure 1.10: Explanation for a prediction with LIME. The top three predicted classes are "tree frog", "pool table" and "balloon". (Illustration from [MTR16]).</figcaption></figure>

The advantage of feature-based attribution methods is that they are generally more scalable than their alternatives. It can associate attributions to different types of data (tabular data, text and image). However, in spite of their popularity, feature attribution methods are often accused of being inconsistent, meaning they can lower a feature's assigned importance when the true impact of that feature actually increases [LEL18, Ign20] and can be fooled by adversarial attacks [SHJ+20].

**Feature visualization explanations** in this category, approaches are proposed for visualizing the relationship between the outcome class and the input variables. The aim is to increase the model's inter-
pretability by the mean of visualizations (parallel coordinate plots, scatter plots or projection methods).

Visualization techniques are generally used in data mining and statistics and lately, as visualization tools for model inspection. There are few works about the visualization techniques to explain the black-box output [KKS07] compared to the model-specific techniques. It is mainly due to the high dimension of feature space of black-box model's that makes it hard to analyze.

Authors in [GDL03] presented a survey about visualization methods based on the sensitivity analysis (SA) computation. Although most of these methods were mainly developed for neural networks (NNs), some of them can be used directly for any black-box model analysis. The authors in [CE13] presented a visualization method based on sensitivity analysis [RRK90] where they query the black-box model with sensitivity samples and analyze it to create different visualization plots for the results such as input importance bars, color matrix, variable effect characteristic curve, surface and contour (see example of Figure 1.11).

Authors in [KKS07] also propose a visualization technique using the sensitivity analysis to deal with the visualization of the black-box model's output. They propose to study the relationships between variables for regression models and classification boundaries for classifiers in order to answer to "How is the output of the artificial model related to the measured input?". They also provide visualization to estimate the credibility of any black-box model.

A popular method for feature visualization is the Partial Dependence Plot (PDP) [Fri01]. Partial dependence plots represent the expected output of a model when the value of a specific variable (or group of variables) is fixed. In [Mol22], the authors describe it as the marginal effect of one or two features having on the predicted outcome of a machine learning model. These plots help in visualizing and understanding the relationship between the outcome of a black-box and the input in a reduced feature space. Authors in [KKS07] provide an extension of PDP named Individual Conditional Expectation (ICE). The idea is to generate for each sample, a plot to show the evolution of the prediction with respect to a grid of values of one given feature (while the others remain constant). ICE plot shows the average partial relationship between the outcome and some features. Figure 1.12 shows an example from [GKBP15] representing the ICE of a prediction with respect to a feature $X_1$ (dots correspond to the actual value of $X_1$ for each instance). We can see that there is a parabolic relationship between the model studied $f$ and $X_1$. The PDP is also represented as a yellow line, which is the average of the ICE over all instances.

**Counterfactual explanations:** Another popular type of explanations are counterfactual explanations (CF). A counterfactual explanation tells the user how an input should be modified to make the system's decision change based on the provided explanation. This type of explanation have been widely explored

<figure><img src="image_12.png" /><figcaption>Figure 1.11: Example of visualization plots explanations from [CE13].</figcaption></figure>
<figure><img src="image_13.png" /><figcaption>Figure 1.12: Example of the ICE and the PDP of a prediction with respect to feature $X_1$ (Illustration from [GKBP15]).</figcaption></figure>

recently and are proved to help the user understand the decision of a models [GKC$^{+}$18, LPNC$^{+}$17, Byr19, AALC21, HHDA18, KTKA20, KBBV20, WMR17, DCL$^{+}$18, DPB$^{+}$19, GWE$^{+}$19, LK21, Rus19, MTS19, MST20]. Consider the case of a bank's decisions regarding whether or not to accept a loan application as illustrated in Figure 1.13. The model decision is based on binary features like "does the requester has a stable job" and "does he have a criminal record" ? An intuitive question that a user who has obtained a refusal for his loan application would be: "what are the elements of his application that led to such a decision?" and "what he can possibly do to change his loan decision ?" The counterfactual explanation identifies the features to change in his application to get an acceptation from the model.

Most of the methods proposed within the XAI field for the generation of the nearest counterfactual explanation are optimization-based (rely on separate optimizations for each input) and there is a risk of generating unjustified counterfactual examples as shown in [LLM$^{+}$19]. The methods in [Rus19, MST20] generate counterfactual explanations for the mixed datasets commonly used in the real world using an optimization based on the original features. In [JKV$^{+}$19], the authors provide an optimization framework to traverse the data manifold via its latent representation and in [LKLH19] they used generative adversarial network. Authors in [SHG19] proposed CERTIFAI : "Counterfactual Explanations for Robustness, Transparency, Interpretability, and Fairness of Artificial Intelligence models". The approach uses a customized genetic algorithm to generate perturbations of an input that lead to a different outcome. The counterfactuals can be used to check the robustness and examine fairness of a ML model at individual and global level. Authors in [WMR17] propose to find a counterfactual explanation for a sample $x$ by solving a relaxed version of the original optimization problem using gradient-based approaches. A solution to this optimization problem represents an instance $x'$ that presents the perturbations in the original input features that can lead to a change in the prediction of the ML model. In [MTS19], the authors proposed a causal view of the feasibility of CF examples using structural causal models. They also proposed to generate counterfactual explanations using a proximity loss based on causal relationships between features instead of the standard proximity measure usually used.
<figure><img src="image_14.png" /><figcaption>Figure 1.13: Example of a counterfactual explanation scenario (Illustration from [SGZS21]).</figcaption></figure>

Other methods were used to generate counterfactual explanations without relying on an optimization problem. For instance, authors in [INMS19a] proposed a method based on abductive reasoning to generate two types of symbolic explanations. Among them, the contrastive explanations (CXp) as an answer to "why not?" question, which corresponds to CF explanation. [KBBV20] proposed MACE for "model-agnostic approach to generate nearest counterfactual explanations". MACE relies on encoding the predictive model, the distance function, the plausibility and diversity constraints into a logical formulae. Thus, the problem of finding the nearest CF becomes a sequence of satisfiability (SAT) problems where the goal is to verify if there exists a counterfactual explanation at a distance smaller than a given threshold, and can be solved using standard SMT (satisfiability modulo theories) solvers. Authors in [BL22] proposed a fuzzy framework to deal with imprecise knowledge or data and imprecise formulations of explanations. Such an approach is based on the integration of fuzzy semantics to a logical framework exploiting knowledge represented as structural causal graphs from [Mil21].

Note that adversarial examples are like counterfactual examples; however, they do not focus on explaining the model by providing an actionable explanation in the form of data instances that would have received a different outcome, but on misleading it (e.g. an adversarial example in computer vision would correspond to an imperceptible change in the image to fool models into producing incorrect predictions).

**Example-based explanations:** Explanations by example are mainly aiming at extracting representative examples from the dataset to explain the model being analyzed. They are actually not considered as model-agnostic methods in the taxonomy of [Mol22] since they do not generate explanations but actually select them by extracting data samples that relate to the prediction being explained. The example-based explanations are similar to how humans behave when attempting to explain a given process by thinking in examples or analogies [Mol22].

An example of such explainability method is the one of k-Nearest Neighbors (kNN). In order to explain an input instance, the idea is to return the closest instances, like the work presented in [KK19b]. The *k*-Nearest Neighbor is a machine learning technique based on assigning the most represented class to a sample based on the outcome of its *k* closest neighbors. By definition, the interpretability of this approach is local since it gives an interpretation for a particular instance by presenting the instances
from the neighborhood that were used to decide of the output class. An example suitable for that kind
of interpretability is presented in [KK19b] where they applied their approach on the MNIST dataset in
order to explain the prediction of an image predicted as a "0" while it represents a "6" digit. The visual
explanation shows that the input image was predicted as a "0" based on its similarity with instances from
its neighborhood representing a "0".

**Example 15.** *The example in Figure 1.14 shows how kNN can be used to interpret a prediction by looking at the outcome of the closest nearest neighbors of the query sample.*

<figure><img src="image_15.png" /><figcaption>Figure 1.14: Example from [KK19b] representing the prediction of an input sample and its neighbors.</figcaption></figure>

Thus, we can understand that the model was actually mislead by the outcome of the nearest neighbors
of the input image.

Another example-based method is proposed to extract *prototypes* and *criticism*. Namely, the representative samples used to explain the global behaviour of a model are called *prototypes* and *criticism* are the data samples that do not fit the model well. Methods which extract those samples (such as [Zad96, LRBM08] for fuzzy prototypes, [KRS14, KK19b, AP94,LLCR18] for case-based reasoning) can be used to analyze the behaviour of a trained model by analyzing its predictions on *prototypes* and the *criticisms* samples, and, quickly extract a few instances that should be harder to predict (criticism) or easier to predict (prototypes). In [KKK16], the authors propose a Bayesian model criticism framework, called MMD-critic which efficiently learns prototypes and criticism, designed to help human explainability.

1.2.3 Local interpretability versus global interpretability

Explainable AI methods can be further distinguished into local and global methods. Local explainability methods give an interpretation for a specific decision (individual prediction) of a particular data instance. It generates the explanations with respect to a specific instance. In contrast, the global (model) explainability methods are used to understand the model's behavior through its working mechanisms and follow the entire reasoning that produces all the different possible outcomes. It generally takes a group of instances to generate one or more explanations.

Most of the post-hoc existing methods are local approximation methods. They explain a specific
decision of a sample *x* by segmenting the data space and focusing on the samples around *x* to generate
explanations such as the feature attribution methods (e.g. LIME [RSG16], Local Explanation Method-
using Nonlinear Approximation (LEMNA) [GMX<sup>+</sup>18], SHAP [LL17]) and saliency maps ([SCD<sup>+</sup>17,
ZKL<sup>+</sup>16, SDBR14, CSHB18, MLB<sup>+</sup>17, STY17, BBM<sup>+</sup>15]). Authors in [BAL<sup>+</sup>21] propose to help
non-expert users understand the ML predictions by providing contextualisation elements. They propose
an experimental study to assess the impact of adding contextual information on the understanding of
local explanations. Explaining the global behaviour of a model is more difficult compared to interpreting
<figure><img src="image_16.png" /><figcaption>Figure 1.15: Taxonomy of machine learning interpretability techniques</figcaption></figure>

the outcome of a specific instance, especially if the predictor is a complex model. Global XAI methods assess the role of features and their contribution to the model output. A summary of the included methods is shown in Table 1.3.

To contextualize and situate our work that we will be presenting in the second part of this thesis, we use Figure 1.15 of AI interpretability techniques from [LPK20] to highlight the elements describing our work. Our contributions to explain individual predictions of single and multi-label classification models consist of a post-hoc local model-agnostic approach. Indeed, our main approach for providing symbolic explanations is model-agnostic, which means it can explain the outcome of any ML model. It is declarative, which means it does not require the implementation of specific algorithms since its based on well-known concepts (more details in the upcoming sections) in SAT solving and it is local, meaning that it is used to explain individual predictions of black-box ML models.
<table><caption>Table 1.3: Summary of local vs global XAI methods.</caption><thead><tr><th>Name</th><th>Ref</th><th>Local vs Global</th><th>Model-Specific vs Model-Agnostic</th><th>Category</th><th>Year</th></tr></thead><tbody><tr><td>G-REX</td><td>[JKN04]</td><td>Global</td><td>Agnostic</td><td>Post-hoc</td><td>2004</td></tr><tr><td>ICE</td><td>[KKS07]</td><td>Global</td><td>Agnostic</td><td>Post-hoc</td><td>2007</td></tr><tr><td>PDP</td><td>[Fri01]</td><td>Global</td><td>Agnostic</td><td>Post-hoc</td><td>2007</td></tr><tr><td>SAlib</td><td>[SRA<sup>+08</sup>]</td><td>Global</td><td>Agnostic</td><td>Post-hoc</td><td>2008</td></tr><tr><td>DeLP3E</td><td>[SSF14]</td><td>Local</td><td>Specific</td><td>Post-hoc</td><td>2014</td></tr><tr><td>DeepExplain</td><td>[ZF14]</td><td>Local</td><td>Specific</td><td>Post-hoc</td><td>2014</td></tr><tr><td>iNNvestigate</td><td>[SDBR14]</td><td>Local</td><td>Specific</td><td>Post-hoc</td><td>2014</td></tr><tr><td>InterpretML</td><td>[CLG<sup>+15</sup>]</td><td>Global</td><td>/</td><td>Intrinsic</td><td>2015</td></tr><tr><td>iBCM</td><td>[KGJS15]</td><td>Global</td><td>/</td><td>Intrinsic</td><td>2015</td></tr><tr><td>—</td><td>[LRMM15]</td><td>Global</td><td>/</td><td>Intrinsic</td><td>2015</td></tr><tr><td>SLIM</td><td>[UR16]</td><td>Global</td><td>/</td><td>Intrinsic</td><td>2016</td></tr><tr><td>LIME</td><td>[RSG16]</td><td>Global/Local</td><td>Agnostic</td><td>Post-hoc</td><td>2016</td></tr><tr><td>CAM</td><td>[ZKL<sup>+16</sup>]</td><td>Local</td><td>Specific</td><td>Post-hoc</td><td>2016</td></tr><tr><td>MMD-critic</td><td>[KKK16]</td><td>Global</td><td>Specific</td><td>Post-hoc</td><td>2016</td></tr><tr><td>rationale</td><td>[LBJ16]</td><td>Local</td><td>Specific</td><td>Post-hoc</td><td>2016</td></tr><tr><td>SHAP</td><td>[LL17]</td><td>Global</td><td>Agnostic</td><td>Post-hoc</td><td>2017</td></tr><tr><td>fair-classification</td><td>[ZVR<sup>+17</sup>]</td><td>Global</td><td>Agnostic</td><td>Post-hoc</td><td>2017</td></tr><tr><td>fairness</td><td>[DHP<sup>+12</sup>]</td><td>Local</td><td>Agnostic</td><td>Post-hoc</td><td>2018</td></tr><tr><td>L2X</td><td>[CLP<sup>+18</sup>]</td><td>Local</td><td>Agnostic</td><td>Post-hoc</td><td>2018</td></tr><tr><td>CAV</td><td>[KWG<sup>+18</sup>]</td><td>Local</td><td>Specific</td><td>Post-hoc</td><td>2018</td></tr><tr><td>ANCHOR</td><td>[RSG18]</td><td>Local</td><td>Agnostic</td><td>Post-hoc</td><td>2018</td></tr><tr><td>Grad-CAM++</td><td>[CSHB18]</td><td>Local</td><td>Specific</td><td>Post-hoc</td><td>2018</td></tr><tr><td>LEMNA</td><td>[GMX<sup>+18</sup>]</td><td>Local</td><td>Agnostic</td><td>Post-hoc</td><td>2018</td></tr><tr><td>—</td><td>[MWM18]</td><td>Local</td><td>Specific</td><td>Post-hoc</td><td>2018</td></tr><tr><td>—</td><td>[SCD18b]</td><td>Local</td><td>Specific</td><td>Post-hoc</td><td>2018</td></tr><tr><td>AIX360</td><td>[DGW18]</td><td>Global</td><td>/</td><td>Intrinsic</td><td>2018</td></tr><tr><td>SENN</td><td>[AMJ18]</td><td>Global</td><td>/</td><td>Intrinsic</td><td>2018</td></tr><tr><td>—</td><td>[WDGG19]</td><td>Global</td><td>/</td><td>Intrinsic</td><td>2019</td></tr><tr><td>BEEF</td><td>[GPSS19]</td><td>Local</td><td>Agnostic</td><td>Post-hoc</td><td>2019</td></tr><tr><td>—</td><td>[INMS19a]</td><td>Local</td><td>Agnostic</td><td>Post-hoc</td><td>2019</td></tr><tr><td>DeNNeS</td><td>[MG20]</td><td>Global</td><td>Specific</td><td>Post-hoc</td><td>2020</td></tr><tr><td>Tree explainer</td><td>[LEC<sup>+20a</sup>]</td><td>Global/Local</td><td>Specific</td><td>Post-hoc</td><td>2020</td></tr><tr><td>—</td><td>[DH22]</td><td>Local</td><td>Specific</td><td>Post-hoc</td><td>2020</td></tr><tr><td>Glocalx</td><td>[SGM<sup>+21</sup>]</td><td>Global</td><td>Agnostic</td><td>Post-hoc</td><td>2021</td></tr><tr><td>—</td><td>[DLM<sup>+22</sup>]</td><td>Local</td><td>Specific</td><td>Post-hoc</td><td>2022</td></tr><tr><td>DeepGlobal</td><td>[SLZS22]</td><td>Global</td><td>Specific</td><td>Post-hoc</td><td>2022</td></tr><tr><td>—</td><td>[FdSRGL22]</td><td>Global</td><td>Specific</td><td>Post-hoc</td><td>2022</td></tr></tbody></table>
# Chapter 2

## XAI methodologies

The scientific communities may have different requirements and priorities when it comes to the characteristics of the XAI approach to be developed (e.g. tractability, scalability, formal aspects, level of explanation, need for access to data and model, parcimony, etc). This difference in design goals and desired properties is reflected by adopting diverse methodologies in the development of XAI approaches.

The proposed methodologies in the literature can roughly be classified in two types: formal methods and ad-hoc or numerical methods presented in the following sections.

### 2.1 Ad-hoc methods

The ad-hoc methods are defined as methods designed to answer a specific question or to accomplish a goal. Although they may work well in practice, they may be considered untrustworthy and capable of producing errors. Their major issue is that they offer no guarantee of correctness w.r.t the ML model explained since they are model-agnostic, thus, the explanations may be incorrect, inaccurate or unstable and are not necessary minimal [Ign20].

Most of the current XAI approaches are based on ad-hoc methodologies and compute approximations of real explanations. For instance, SHAP [LL17] is based on the cooperative game theory Shapley value [Sha53] and determines the features that contribute the most to the difference in model prediction at a specific input versus a background distribution. LIME [RSG16] generates an explanation by approximating the underlying black-box by an interpretable model. ANCHOR [RSG18] based on LIME provide rule-based explanations on local behaviors of the models, Partial Dependence Plot (PDP) [ZH21] and Accumulated Local Effect Plot (ALEP) [AZ20] describe how features affect the decision of ML models and the nature of the relationship between them (e.g linear or monotonic).

Recent works have highlighted undesirable behavior of ad-hoc methods [INM19, Ign20, SHJ$^{+}$20, FdHvE22, ADLPR22]. Among these, the work in [Ign20] where the authors showed that explanations provided by SHAP and LIME are mostly incorrect from a global perspective. The same idea is expressed in [INM19, SHJ$^{+}$20], where it is shown that some ad-hoc based approaches return the same explanation for two different data point that were predicted differently (incompatible classes). This shows that ad-hoc based explanations can be misleading and incorrect.

### 2.2 Formal methods

Formal methods are defined as mathematically or formally verifiable. They have been widely investigated for explainability [SCD18b, SSDC20, DH22, SCD19, INMS19a, INMS19b, Ign20, IMS21, ABB$^{+}$22a, AKM20a, ABB$^{+}$21, APR21, WGH19, MSGC$^{+}$20, IIN$^{+}$21, HIIM21, IMS21, GR22]. They are mainly
based on knowledge compilation or abductive reasoning [Ign20] and provide explanations that guarantee to have the same behavior with the model (accurate), and so, trustable. The approaches based on knowledge compilation compile predictive models into Boolean circuits and propose to interpret the model by enumerating the prime implicants of the circuit [DH22, SCD18b]. The abductive based approaches represent a model into a set of constraints and provide minimal explanations by applying abductive reasoning on the model's encoding to answer XAI queries [INMS19a, Rei87, INMS19b, ABB<sup>+</sup>22a, ABB<sup>+</sup>22b, IIN<sup>+</sup>22, HM22, IIM22, GR22]. Formal methods are often too expensive to compute (worst-case exponential complexity in time and space for compilation, number of explanations is worst-case exponential), and are strongly dependent on the type of classifier to treat since we need to develop dedicated algorithms for each ML model (model-specific) when using the compilation approach.

We present in the following sections the main line works used by these methods, namely knowledge compilation and abductive reasoning.

### 2.2.1 Knowledge compilation

Knowledge compilation is a technique used to overcome the difficulty (intractability) of some AI problems by pre-processing the available information. It is expressed as a translation problem which is done in two phases. A first phase called off-line which allows to compile a part of the information and a second phase called on-line where the compiled form with the rest of the information is used to efficiently answer queries. Authors in [DM02] presented a map for deciding the target compilation language that is most suitable for a particular application. Note that different target compilation languages exist such as the : Conjunctive Normal Form (CNF), Disjunctive Normal Form (DNF), Negation Normal Form language (NNF) formally defined in [Dar99, Dar01], Ordered Binary Decision Diagrams (OBDD) first presented in [Bry86], Decomposable Negation Normal Form (DNNF), Deterministic Decomposable Negation Normal Form (d-DNNF), Sentential Decision Diagrams (SDD) [Dar11] and so on. Knowledge compilation has been applied in different areas : diagnosis [TT04, HD05, SH<sup>+</sup>08], configuration [AFM02, HSJ<sup>+</sup>04], planning [GT99, EMW97, JV00, CRT98] and lately, knowledge compilation had been used to address fundamental problems for explainable and robust AI.

Formal XAI methods compile ML models into Boolean circuits that can make the same predictions with the models and provide valid and complete explanations. The advantages of such approaches is the possibility of efficiently checking, verifying the symbolic representations of classifiers (e.g. [CD07, SCD18a, CSSD17, OD15, Dar11]). Authors in [SCD18b] proposed an algorithm to compile latent-tree Bayesian network classifiers into decision functions in the form of Ordered Decision Diagram (ODD). This equivalent and tractable<sup>7</sup> symbolic representation is used to explain Bayesian network classifiers by providing two types of explanations. The first type called the *minimum-cardinality explanations* (MC-Explanations) corresponds to the minimal subsets of inputs that is sufficient for the current decision, while the second type called *prime-implicant explanations* (PI-Explanations) corresponds to the smallest subset of features that makes the rest of the features irrelevant to the current prediction. For instance, the authors in [NKR<sup>+</sup>18] proposed a CNF encoding for Binarized Neural Networks (BNNs) for verification purposes. In [SSDC20], the authors propose a compilation algorithm of BNNs into tractable representations such as OBDDs and SDDs. In [CD03, SCD19], the authors proposed algorithms for compiling Naive and Latent-Tree Bayesian network classifiers into decision graphs (symbolic representations). Authors in [SCD18b] and [AKM20a] use knowledge compilation techniques to design tractable cases for a set of XAI queries (e.g. enumerating minimum-cardinality explanations, deriving one prime implicant explanation, enumerating counterfactual explanations). These queries were also used in [ABB<sup>+</sup>21] to evaluate the intelligibility of several families of Boolean classifiers (decision trees, DNF formulae,

<footnote n="7"><sup>7</sup>can be answered using a polynomial-time algorithm</footnote>
decision lists, random forests, boosted trees, Boolean multilayer perceptrons, and binarized neural nets).

The major issue for knowledge compilation based methods is the tractability of the compilation phase for large feature spaces and complex models. In addition to finding a suitable representation for the compiled model, there is need to provide dedicated compilation algorithms for each new ML models since its a model-specific technique.

### 2.2.2 Abductive reasoning

Abduction is defined as a form of logical reasoning that allows to explain a phenomenon or an observation from certain facts. It is considered as a type of inference that is frequently employed both in everyday and in scientific reasoning, where we make a probable conclusion from what we know (e.g. a detective's identification of a criminal by piecing together evidence at a crime scene). Abductive reasoning is well-known concept [Sha89, Mar91] for computing explanations. Many works used abductive reasoning to answer queries such as verification of properties of systems [KBD+17, LNPT18, NKR+18, SDC19] and diagnosis purposes [Rei87, Rym94] were proposed. However, in the last few years it has been used specifically for XAI tasks.

Authors in [CSGD20a] tackle the problem of explaining the decisions of machine learning models with discrete/continuous input and output variables. They analyze three symbolic encodings using Boolean expressions to reason about the behavior of the system. Based on the PI-explanation<fnref n="8" /> introduced in [SCD18b] and notions on multi-valued variables, they formally define the notion of PI-explanations in a multi-valued setting. In [INMS19a], authors propose an approach based on abductive reasoning to generate explanations using some constraint reasoning system (e.g. Satisfiability Modulo Theories (SMT), Constraint Programming (CP), or Mixed Integer Linear Programming (MILP)) to encode the ML model to be explained and answer some entailment queries. For instance, they consider neural network models and use a MILP encoding in order to compute prime implicants, which are used to find the minimal subset or cardinality minimal explanations. The paper deals with some forms of symbolic explanations referred to as abductive explanations (AXp) as an answer to a "why?" question and contrastive explanations (CXp) as an answer to "why not?" question. The authors in [INMS19b] analyze the duality relationship between explanations (defined as a prime implicants) and counterexamples (defined as negated prime implicate) and investigated how to compute adversarial examples from counterexamples. They use First Order Logic (FOL) for the representation of ML model and overview algorithms for the enumeration of explanations and adversarial examples. The authors in [Ign20] overview recent logic-based XAI approaches to explain ML model predictions. The paper proposes an empirical study to assess the correctness of the explanations of ad-hoc methods like LIME, SHAP and ANCHOR in order to validate them and argue that rigorous explanations based on abductive reasoning are trustworthy and can be independently validated. Authors in [IMS21] discuss the computational complexity of computing explanations for Decision Lists (DLs) and show the contrast compared to Decision Trees (DTs). They propose AXp and CXp explanations for Decision Lists using the SAT solvers. Authors in [ABB+22a] focus on abductive explanations of random forests. They propose (1) "direct reasons" which are an extension of the abductive explanations of decision trees, and (2) "majority reasons" which are implicants of a majority of trees in the forest and which can be computed in polynomial time. They tackle the problem of generating and minimizing (in terms of size) these two types of explanations and propose algorithms to compute and compare them empirically.

The major issue for formal explanation methods is finding a logical language suitable for describing the ML model as faithful as possible. Another limitation is their tractability in practice, although some improvement are made possible, like in recent work [IIM22] that proposes algorithms for computing

<footnote n="8">⁸defined as minimal set of instance characteristics that are sufficient to trigger the decision [SCD18b]</footnote>
path explanations for DTs which run in worst-case polynomial time. The experimental results reported
in [SCD18b, INMS19a] show that the approaches based on logical representations are limited and may
be difficult to obtain for large datasets. Another drawback of symbolic methods is linked to the nature of
data as real-world data is often numerical and not binary.

## 2.3 Conclusion

The evaluation of XAI methods is on early stages (e.g. [JBB+21, BWM20]). The XAI community does not have a standardized terminology yet and there is no effective evaluation methodologies to assess which methods will do well for a given use-case [DVK17]. The evaluation of an explanation often depends of the target audience (different roles, background, objectives), and thus, have a different explainability requirements [TBH+18, MZR21, ARLG20].

Evaluating explanation methods is considered as an open problem [DVK17, JG20]. Although there is no standards established for their evaluation, some desired requirements for XAI methods were summarized in [HYHI21] such as faithfulness [AGM+18, LKCL19, JG20], plausibility (explanations must be sufficiently convincing to users) [LBJ16, LCH+19, SZM19], robustness [AJ18], and readability [AET18, YRS17, ALSA+17]. For instance, the authors in [BP19] proposed a human-grounded evaluation, done by assessing 17 criteria splitted into three categories for evaluating explanations : natural language (aims at assessing the correctness of the language used in explanations), human-computer interaction (enables to evaluate what the explanation conveys when it is transmitted from the system to the user) and also the content and form (dedicated to assessing the content and the form of the explanation).
# Part II

## Symbolic explanations
This second part of the thesis is devoted to the contributions made to explain predictive models and reason about explanations.

Firstly, we will present in Chapter 3 the general framework of our declarative and model-agnostic approach as well as the different modules that compose it. We formally define what is a sufficient reason and what is a counterfactual and how this kind of complementary symbolic explanations are generated for single-label classification problems with the help of Boolean satisfiability concepts. The results of an experimental study is conducted on several datasets from the literature in order to evaluate the feasibility of the approach in practice. The different characteristics of the enumerated symbolic explanations are also presented.

Chapter 4 concerns the explanation of multi-label tasks. We define several symbolic explanation types and show how we can enumerate them by adapting our approach to the multi-label case. We also introduce a concept specific to multi-label problems called the label-based explanations, allowing to take advantage of the structural relationships between labels. An experimental study is also provided in order to evaluate in practice the different concepts discussed in the chapter.

In Chapter 5 of this manuscript, we go beyond symbolic explanations and address score-based explanations for classification in a single-label setting. We define some desired properties of an explanation score to assess the relevance of both explanations and features individually, in order to evaluate them in ways that are closer to how users perceive them.

The last Chapter 6 is dedicated to feature attribution for multi-label classification. We first point out some deficiencies in attribution methods based on aggregation by defining three desirable properties. As a second contribution, we present a framework based on problem transformation allowing to provide global feature attributions capturing the above properties while using existing attribution methods as an oracle. The third contribution consists in a new attribution method based on symbolic explanations such as sufficient and counterfactual reasons, from which attribution scores are generated. Finally, we propose to go further concerning the property of label-explanation correlation by exploiting it to infer features attribution on a label using the explanations already computed on another label with which it is correlated.
Chapter 3

Symbolic explanations for single-label
classification

After having presented the current state of the field of XAI in the previous chapters, we introduce now a
novel framework for explainable classification. In this chapter, we will provide insights of the approach
to handle single-label classification problems. Chapter 4 addresses the case of multi-label classification.

Explanations generated using symbolic reasoning approaches are called symbolic explanations and have been investigated in a number of applications such as generation of rigorous explanations, detection of decision bias and evaluation of counterfactual queries. Symbolic explanations are important as they provide the user with more detailed information beyond a simple numeric score (e.g., model inputs that contributed to the outcome). The existing symbolic explainability methods are mainly model-specific (can only be applied to specific models for which they are intended) and cannot be applied agnostically to any model, which is their main limitation. In the other hand, feature-attribution methods such as LIME [RSG16] and SHAP [LL17] provide the features’ importance values for a particular prediction. These values provide an overall information on the contribution of features individually but do not really allow answering certain questions such as: "What are the feature values which are sufficient in order to trigger the prediction whatever are the values of the other variables? " or "Which values are sufficient to change in the instance x to have a different prediction?". This type of questions is fundamental for the understanding, and, above all, for the explanations to be usable. For example, if a user’s application is refused, the user will naturally ask the question: "What must be changed in my application to be accepted?". We cannot answer this question in a straightforward manner with the features attribution explanations. Thus, the major objective of our contribution is to provide both symbolic explanations and score-based ones for a better understanding and usability of explanations.

We leverage formal methods to develop a novel model-agnostic method for explaining the prediction of single-label and multi-label classification models. We propose a model-agnostic SAT-based approach for symbolic and score-based explanations named ASTERYX. In particular, we focus in this chapter on the symbolic explanations and we present the general framework of ASTERYX. We are going to motivate the choices we made for designing a declarative and model-agnostic approach to globally or locally explain the prediction of single-label classifiers. We are interested in two complementary types of symbolic ex- planations: the sufficient reasons ($SR_x$) which lead to a given prediction (also known as PI-explanation [SCD18b, SCD19, Dar20] or abductive explanation (AXp) [INMS19a]) and the counterfactuals ($CF_x$) allowing to know minimal changes to apply on the data instance $x$ to obtain a different outcome (corre- sponding to contrastive explanation (CXp) [INAMS20]).

In the following, we present and provide details about **Step 1** and **Step 2** from Figure 3.2 of the
approach we propose. In Chapter 3, we provide insights of the approach to handle single-label classifi-
cation problems. Chapter 4 addresses the case of multi-label classification. The description of **Step 3** is given in Chapter 5 for feature-attribution explanations for the single and multi-label settings.

As depicted in Figure 3.1a, and to recall what have been presented in Chapter 2, the methodologies used in XAI are either formal methods or ad-hoc methods. The formal methods generate symbolic explanations such as prime implicants, if-then-rules, sufficient reasons, etc. On the other hand we have ad-hoc methods, developed to explain complex models by providing numerical explanations such as importance scores and saliency maps. Figure 3.1b allows to situate our work w.r.t the methodology used. Our approach relies on a formal method based on the symbolic representation of a model, and use a substitution approach to make it model agnostic. In Section 3.1, we present the general framework of the proposed approach. Section 3.2 is devoted to describe how to associate a symbolic representation to the model used. In Section 3.3, we specify how to generate the type of explanations we would like our model to return and how to reason directly from it. Finally, we complete this chapter by giving some experimental results that show the feasibility of the approach in Section 3.4.

<figure><img src="image_17.png" /><figcaption>Figure 3.1: Methodologies proposed within the explainability techniques</figcaption></figure>

**3.1 General framework**

The main idea is based on associating a symbolic representation that is equivalent or almost equivalent to the decision function of the model to explain. After that, we use this symbolic encoding to generate explanations based on formal methods. We are also interested in post-processing the explanations and select the relevant ones w.r.t to some intuitive desiderata in order to select and rank the explanations according to the user expectations. We investigate a set of fine-grained properties allowing to analyze and select explanations. We also proposed some scores allowing to assess the relevance of explanations and features w.r.t the suggested properties. An illustration of the main components of our approach is given in Figure 3.2. Note that a binarization step may be performed since our approach applies on binary classification problems.

Given a decision function $f$ representing a binary classifier $f: X \rightarrow Y$ from the input domain $X$ to the output domain $Y$, we would like to explain the output $f(x)$ for some input $x \in X$ by providing ex-
<figure><img src="image_18.png" /><figcaption>Figure 3.2: A global overview of the proposed approach</figcaption></figure>

planations to justify why the output class was triggered and what modifications of the input can possibly be made to change it. Concretely, our approach proceeds in three major steps as follows:

*   **Step 1 (Encoding the classifier into CNF):** This comes down to associating an equivalent symbolic representation $Σ_f$ to $f$ as well as $Σ_x$ encoding the input instance $x$ whose prediction by $f$ is to be explained. $Σ_f$ will serve to generate symbolic explanations in the next step. The encoding is done either using model encoding algorithms if available and if the encoding is tractable as described in Section 3.2.1, or using a surrogate approach as described in Section 3.2.2.

*   **Step 2 (SAT-based modeling of the explanation enumeration problem):** Once we have the CNF representation $Σ_f$ and $Σ_x$, we model the explanation generation task as a partial maximum satisfiability problem, also known as Partial Max-SAT [BHVMO9]. The main idea is to view classifiers as a set of constraints describing a Boolean function that is inconsistent on instances that do not satisfy the constraints. This step, presented in Section 3.3, aims to provide two types of symbolic explanations: $SR_x$ and $CF_x$. They respectively correspond to Minimal Unsatisfiable Subsets (MUS) and Minimal Correction Subsets (MCS) in the SAT terminology.

*   **Step 3 (Explanation and feature relevance scoring):** This step aims to assess the relevance of explanations by associating scores evaluating those explanations with regard to a set of properties presented in Section 5.2 of Chapter 5. Moreover, this step allows to assess the relevance of features using scoring functions and to evaluate their individual contributions to the outcome. We propose a set of fine-grained properties allowing to analyze and select explanations and a set of scores allowing to assess the relevance of explanations and features w.r.t the suggested properties.

**Remark 5.** It is important to notice that the SAT choice is one possibility among other possible oracles such as the ones of Satisfiability Modulo Theories (SMT), Constraint satisfaction problem (CSP), Mixed Integer Linear Programming (MILP)) and so on.

In the following we present and provide details about **Step 1** and **Step 2** of our approach.
## 3.2 Encoding of the model

In this section, we present the addressed ways of encoding a model into a symbolic representation. This encoding phase corresponds to **Step 1** in Figure 3.2 where the goal is to encode the decision function associated with the ML model under study into our target representation, which is the Conjunctive Normal Form (CNF) (cf Section 2.3 in **Background and notations** section) in our SAT-base modeling. Two cases are considered in our approach : Either an encoding of classifier *f* into an equivalent symbolic representation exists (non agnostic case) and is tractable, in which case we can use it, or we consider the classifier *f* as a black-box and we use a surrogate model to approximate it in the vicinity of the instance to explain *x* (agnostic case). Such propositional encoding allows to exploit existing algorithms for reasoning about propositional formulae and propose a declarative approach lying on well-known concepts and efficient existing algorithms for the enumeration of Minimal Unsatisfiable Subsets (MUSes) and Minimal Correction Subsets (MCSes).

### 3.2.1 Direct encoding into CNF

A direct encoding of the classifier *f* into CNF is possible for some machine learning models such as Binarized Neural Networks (BNNs) [NKR+18], Naive and Latent-Tree Bayesian networks [SCD19]. We give more insights in the following using two examples on how we would use such approaches to encode a specific ML model, for instance, Naive Bayes and Random forests classifiers into a symbolic representation.

**CNF encoding of Naive Bays classifiers** Authors in [SCD18b] proposed a symbolic approach to explain Naive Bayes classifiers and thus, by proposing two types of explanations called "MC-explanations" for minimal cardinality explanations and "PI-explanations" for prime implicant explanations. The MC-explanations minimize the number of positive features in an instance, while maintaining its prediction. The PI-explanations identify a smallest set of features in an instance that renders the remaining features irrelevant to a prediction. Such approach is based on compiling Naive Bayes Classifiers (NBCs) into a specific symbolic and tractable representation known as Ordered Decision Diagram (ODD). The objective here is to equip such methods with other types of symbolic explanations, namely, counterfactuals. Given a NBC *f* whose predictions are to be explained, and once compiled into a decision function in the form of ODD, we show in the following how we encode it into a CNF to use our approach.

**Definition 19. (Ordered Decision Diagram ODD)** An Ordered Decision Diagram is a rooted, directed acyclic graph, defined over an ordered set of discrete variables, and encoding a decision function. Each node is labeled with a variable $X_i$, $i = 1, ..., n$ and has an outgoing edge corresponding to each value $x_i$ of the variable $X_i$, except for the sink nodes, which represent the terminal nodes.

An Ordered Binary Decision Diagram (OBDD) is an ODD where all the variables are binary. As shown in Example 16, in case of an OBDD representing the decision function of a binary classifier, a node labeled with variable $X_i$ has two outgoing edges labeled 1 and 0 respectively, and two sinks (class variable), 1-sink and 0-sink. If there is an edge from a node labeled $X_i$ to a node labeled $X_j$, then $i < j$ (more on tractable representations such as ODDs can be found in [SCD19]). The proposed algorithm for NBC (and some of its variants) has many nice features in terms of tractability, explanation enumeration and formal analysis of classifiers. Authors in [SCD18b] showed how it facilitates the efficient explanation of classifiers and used it to compile such classifier into an ODD then enumerate two types of explanations : the first class is *minimum-cardinality* explanations and the second class is *prime-implicant* explanations.
**Example 16.** Figure 3.3a shows a NBC for deciding whether a student will be admitted to a university (class variable: Admit (A)). The features of an applicant are: work-experience (WE), first-time-applicant (FA), entrance-exam (E) and gpa (GPA). In Figure 3.3b, we provide the OBDD representing the classifier decision function *f* with the variable ordering (WE, FA, E, GPA). Here, the sinks correspond to the values of the class variable (A).

<figure><img src="image_19.png" /><figcaption>Figure 3.3: A naive Bayes network classifier and its corresponding OBDD.</figcaption></figure>

To explain such Bayesian classifiers following our framework (cf Figure 3.2), we need in the first step to encode the decision diagram into our target representation, which is the Conjunctive Normal Form (CNF) (see Section 2.3).

There are several methods to encode a decision diagram as a CNF formula. For instance in [CNQ03], the authors proposed a method called "Single-Cut-Node" to store a BDD (Binary Decision Diagram) as a CNF. The BDD nodes are modeled as multiplexers. The data inputs of the multiplexer are the children nodes, the selection input is the node variable and the output is the function value which is assigned to an additional CNF variable. A second method called "The No-Cut method" creates clauses starting from *f* corresponding to the "off-set" and a last method called "The Auxiliary-Variable-Cut" which combines the two previous methods. For the sake of simplicity and clarity, we choose the simplest method which does not involve adding new variables during the encoding process since we want to restrict our explanations to the input variables of the classifier. We implement a simple way to encode the symbolic representation of a classifier as a CNF formula based on the "The No-Cut" method [CNQ03]. In our case, since we are dealing with binary Boolean functions (binary features and class variable), our tractable representation of the decision function *f* is an OBDD. Recall that we use along with this manuscript positive/true/1 and negative/false/0 interchangeably. Let us first define an "off-set" of a Boolean function and a CNF formula.

**Definition 20. (Off-set of a Boolean function)** The Off-set of a Boolean function *f*, denoted as $f^0$, is
$f^0 = \{v \in \bigcup_{i=1}^{n} \{0, 1\}^i | f(v) = 0\} \text{ If } f^0 = \{0, 1\}^n, \text{ then } f \text{ is unsatisfiable. Otherwise, } f \text{ is satisfiable.}$

Intuitively, $f^0$ is the set of counter-models of $f$. This concept of "off-set" contains the counter-models we need to enumerate in order to construct our CNF's clauses. The OBDD is used to enumerate all the paths from the root to the 0-sink node (the off-set), where each element of $f^0$ corresponds to a path within it.

**Definition 21. (CNF encoding of an OBDD)** Let *f* be the decision function encoded by an ordered binary decision diagram *OBDD*<sub>*f*</sub>. Let *f*<sup>0</sup> be the off-set of *OBDD*<sub>*f*</sub>. We define the obtained CNF formula from *OBDD*<sub>*f*</sub> as :
$$ \Sigma_f = \wedge \neg e_i \qquad (3.1) $$

where $e_i \in f^0$ and $i \in [1, M]$ with $M = |f^0|$.

**Example 17 (Example 16 continued).** Given the variable ordering (WE, FA, E, GPA) associated with the OBDD of the example 16, the variable $X_1, X_2, X_3$ and $X_4$ correspond respectively to the variable WE, FA, E and GPA. To simplify, let us consider the following notation: $\neg X_2$ means that the variable numbered $X_2$ in a sample $x$ is instantiated negatively (has the value 0). A decision path ($X_1=1, X_2=0, X_3=1, X_4=0$) corresponds to a clause $\mathcal{T} = (\neg X_1 \lor X_2 \lor \neg X_3 \lor X_4)$ and is written ($X_1, \neg X_2, X_3, \neg X_4$). Note that the elements of $f^0$ are a complete assignation but can be written in a reduced form for the sake of simplicity. The corresponding "off-set" of the OBDD of Example 16 representing the counter models of the OBDD$_f$ is presented in Figure 3.4.

<figure><img src="image_20.png" /><figcaption>Figure 3.4: Off-set of a Boolean function represented by an Ordered Binary Decision Diagram.</figcaption></figure>

**Proposition 2.** Let $f$ be a binary decision function and OBDD$_f$ its representation. Let also $\Sigma_f$ be the CNF representation of the decision function $f$ obtained following Definition 21. Then, an interpretation $\mu$ is model (resp. counter-model) of $\Sigma_f$ iff it is mapped to 1 (resp. to 0) by $f$.

*Proof.* The proof is straightforward. Indeed, it is easy to see that the Boolean function $f$ encoded by an OBDD can be equivalently represented as the disjunction of its models (called disjunctive normal form, DNF for short). Let $\alpha$ be the associated formula of $f$. Similarly, $\neg \alpha$ is equivalently represented as the disjunction of the counter-models of $f$. Then $\neg(\neg \alpha)$ comes down to $\alpha$ which corresponds to $f$ in conjunctive normal form CNF. $\square$

Let $\alpha$ be the associated formula of $f$. The intuition is that $\neg \alpha \equiv \lor e_i$ where $e_i \in f^0$. Then $f$ comes down to negating paths in $f^0$ ($\lor e_i$) allowing to obtain directly $f$ in the form of a CNF. Following Definition 21, we have:

- Every variable of the feature space $X = \{X_1, \dots, X_n\}$ of the classifier will correspond to a Boolean variable in the CNF $\Sigma_f$.
- The class variable *Y* of the classifier is captured by the truth value of the CNF ($\Sigma_f$).

- Modeling a prediction made by the classifier for a given data instance *x* comes down to the truth value of: CNF ($\Sigma_f \wedge \Sigma_x$) where $\Sigma_x$ stands for the data instance *x* encoded as a CNF by a set of unit<fnref n="9" /> clauses.

The encoding of Definition 21 guarantees the logical equivalence between the $OBDD_f$ and the obtained CNF $\Sigma_f$ and Proposition 2 formally states that $\Sigma_f$ is logically equivalent to the function $f$, i.e, they have the same truth value for each data instance $x$. Thus, we can assert the following result.

**Lemma 1.** Given a binary classifier, a data instance $x$ and the predicted class $f(x)=y$, the formula $(\Sigma_f \cup \Sigma_x)$ is SAT iff $f(x)=1$.

**Example 18.** Let $f$ be the decision function of the classifier represented by an $OBDD$ in Figure 3.4a. The running example shows the CNF formula $\Sigma_f$ corresponding to the "off-set" of $f$ within the $OBDD_f$, and $\Sigma_x$ corresponding to the data instance $x=(X_1=1, X_2=0, X_3=1, X_4=0)$.

<table><tr><td rowspan="4">Σ<sub>f</sub></td><td>(¬X<sub>1</sub> ∨ ¬X<sub>2</sub> ∨ X<sub>3</sub> ∨ X<sub>4</sub>)</td><td>∧</td></tr><tr><td>(¬X<sub>1</sub> ∨ X<sub>2</sub> ∨ ¬X<sub>3</sub> ∨ X<sub>4</sub>)</td><td>∧</td></tr><tr><td>(¬X<sub>1</sub> ∨ X<sub>2</sub> ∨ X<sub>3</sub>)</td><td>∧</td></tr><tr><td>(X<sub>1</sub> ∨ ¬X<sub>2</sub> ∨ X<sub>3</sub>)</td><td>∧</td></tr><tr><td>(X<sub>1</sub> ∨ X<sub>2</sub>)</td><td>∧</td></tr></table>

<table><tr><td rowspan="4">Σ<sub>x</sub></td><td>(X<sub>1</sub>)</td><td>∧</td></tr><tr><td>(¬X<sub>2</sub>)</td><td>∧</td></tr><tr><td>(X<sub>3</sub>)</td><td>∧</td></tr><tr><td>(¬X<sub>4</sub>)</td><td></td></tr></table>

**Proposition 3. (CNF size)** Let $\Sigma_f$ be the CNF obtained from $OBDD_f$ following Definition 21. The CNF size (number of clauses) is linear in the size of the $OBDD_f$ (number of nodes).

*Proof.* Let $N$ be the size of $OBDD_f$ (number of nodes). From Definition 21, we have: $\Sigma_f=\wedge \neg e_i$ where $e_i \in f^0$ and $i \in [1, M]$ where $M = |f^0|$. Note that for each $e_i \in f^0$ there exists a path within the $OBDD_f$ from the root to the 0-sink node. The number of clauses involved in $\Sigma_f$ is equal to the number of those paths. In the worst case, the number of paths is at most equal to $2*N$. □

Model enumeration is a polytime operation on $OBDDs$ since they are a subset of $DNNFs$ [DM02]. Besides, the authors in [SCD18b] show experimentally that compiling Bayes network classifiers into $ODDs$ can be handled efficiently and the number of PI explanations remains reasonable for small size feature spaces. Thus, such approaches may face scalability issues when applying them to real-world applications. The authors in [SCD18b] also showed that given a $NBC$, compiling an $ODD$ representing its decision function is NP-hard.

<footnote n="9">⁹A unit clause involves only one Boolean variable represented by a literal</footnote>
**CNF encoding of Random Forest classifiers** Random Forest classifiers (RF) [Ho95] are tree-based models built using a stochastic approach. The decision trees composing it are grown on randomly selected subspaces of the feature space, in order to further improve predictive performance. The output value of a RF classifier is given from a combination of the trees' predictions, often using the majority vote. RF classifiers are attractive due to their high execution speed and good predictive performance with relatively little hyper-parameter tuning.

The encoding of a random forest into a CNF amounts to encode the decision trees individually and then encode the combination rule (majority voting rule). We only consider binary variables which can either be True or False (1 or 0 respectively).

**Encode in CNF every decision tree:** The decision trees are seen as directed acyclic graphs whose internal nodes represent propositional variables and whose edges represent assignments to source nodes. A decision tree (DT) in our case represents a Boolean decision function. Recall that the internal nodes of a DT represent a binary test on one of the features. Each leaf of a decision tree is annotated with the predicted class (namely, 0 or 1 for binary classification). A *decision rule* is the solution path going from the root to the leaf leading to the final decision assigned to an input *x*. We can represent a decision tree as a CNF formula as the conjunction of *k* clauses *T*, where a clause is a disjunction of literals of variables in the tree defined on the input features.

Let $x = (x_1, \dots, x_n)$ be the sample of interest. The CNF encoding of a decision tree is :

$$ \Sigma_{DT} = \bigwedge_{j \in [1,k]} \mathcal{T}_j \qquad (3.2) $$

$$ \mathcal{T}_j = \bigvee_{i \in [1,n]} l_j^i $$

where $l_j^i$ is the value of the literal associated to the variable's value $x_i \in x$ in clause *j*. Example 19 shows how the Boolean function encoded by a decision tree can be captured into a CNF as the conjunction of the negation of paths leading from the root node to leaves labelled 0.

**Encode in CNF the combination rule:** Let $y_i$ be a Boolean variable capturing the truth value of the CNF $\Sigma_{DT_i}$ associated to a decision tree. Hence, the majority rule used in random forests to combine the predictions of *m* decision trees can be seen as a cardinality constraint<fnref n="10" /> [Sin05] that can be stated as follows:

$$ y \Leftrightarrow \sum_{i \in [1,m]} y_i \geq t, \qquad (3.3) $$

where *t* is a threshold (usually $t=\frac{m}{2}$). Cardinality constraints have many CNF encodings (e.g. [Sin05, BB03, ANORC13]). To form the CNF corresponding to the entire random forest, it suffices to conjecture the *m* CNFs associated to the equivalences between $y_i$ and the CNF of the decisions trees, and the CNF of the combination rule.

**Definition 22. (Equivalence of a classifier and its CNF encoding)** A binary classifier *f* is said to be equivalently encoded as a CNF $\Sigma_f$ if the following condition is fulfilled: $f(x)=1$ iff *x* is a model of $\Sigma_f$.

Thus, representing the model as a CNF formula allows the capturing of all the models (resp counter-models) likely to make the formula satisfiable (resp unsatisfiable), and thus, matched with the predictions of the classifier *f* as reported in Definition 23.

<footnote n="10">¹⁰In the case of binary classification, this constraint means that at least *t* decision trees predicted the positive label.</footnote>
**Tseitin transformation** Unfortunately, putting a formula in conjunctive normal form can make this formula exponentially larger than the original one. Hence, we use the Tseitin transformation [Tse83] which converts any propositional formula into a CNF formula of size linear in the size of the starting formula.

**3.2.2 Surrogate model encoding into CNF**

**Motivation**

Despite the guarantees of fidelity and completeness offered by direct encoding algorithms which are based on formal methods, a very restricted class of classifiers can be represented directly into a symbolic representation, which makes it hard to use them in practice to explain the different ML classifiers. In addition, their computational complexity makes it hard to use in real-world applications involving a large number of features and parameters.

To overcome those limitations, we propose to integrate a surrogate approach in the encoding phase. The goal is to explain any classifier regardless of the used technique and implementation (model-agnostic). In our setting, no assumptions about the model are made other than that it maps from some known input feature space to a known output domain. The overall goal is to build a surrogate model to faithfully approximate the output around a sample of interest (locally faithful to the classifier). In the same manner as for other approaches such as LIME [RSG16] and Anchor [RSG18], the intuition behind using this simplification approach is that the decision boundary for the black-box can be arbitrarily complex over the whole data space but in the neighborhood of a data point there is a high probability that the decision boundary is clear and simple, and thus, can be captured by a surrogate model.

**Local fidelity for a surrogate model**

Generally, local surrogate models that are used to explain individual predictions of black-boxs are interpretable models (see Explanation by simplification in Section 1.2.2). For our case, the interpretability of the model is not a criterion. We require from the surrogate model $f_S$ to be i) as faithful as possible to the initial model $f$ (ensures same predictions) and ii) to allow obtaining a tractable symbolic encoding. Thus, the surrogate model must meet a **fidelity-tractability** trade-off. Given a classifier $f$ and a sample data $x$ whose prediction $f(x)$ is to be explained, we want to maximize the local fidelity of a surrogate model $f_S$, used to approximate $f$ in the neighborhood of $x$ noted $V(x, r)$ (also written $V_x$ for clarity's sake). In the same time, the encoding of $f_S$ must remain tractable in terms of the size of the logical representation and the time to generate it. Since our target encoding is a CNF formula, its size is expressed in terms of the number of clauses composing it and the total number of variables used.

We use the surrogate model $f_S$ to approximate the classifier $f$ in the neighborhood of the instance to be explained. The neighborhood of $x$ within the radius $r$ noted $V(x, r)$ is constructed by sampling data instances within a radius $r$ from $x$. It is formally defined as $V(x, r): \{v \in X \mid \text{dist}^{11}(x, v) \le r\}$. Note that the value of the radius $r$ is an input information given by the user. We consider mainly the case where a dataset is available in the following but both options can be used.

The intuition behind the explanations generated in the locality of an instance $x$ is to detect what are the reasons used by the model to differentiate two classes that are assigned to similar samples. In case the dataset is not available, we can draw new perturbed samples around $x$. A similar approach for sampling is presented in [RSG16] where they propose to sample instances around $x$ by drawing elements of $x$ uniformly at random.

Concretely, $f_S$ is built according to the following steps :

<footnote n="11">¹¹dist(x,v) denotes a distance measure between x and v.</footnote>
1. Select/sample a balanced set of neighbor instances of the given instance $x$;

2. Once the initial training samples determined, use the original model $f$ as a predictor to determine their predictions;

3. Approximate the ML model chosen by a surrogate model on the pairs of the selected training samples and their corresponding predicted classes;

Given an input sample $x$ whose prediction by a model $f$ is to be explained, the original model $f$ and the surrogate model $f_S$ are supposed to have almost the same input-output behaviour in the vicinity of $x$. A surrogate model $f_S$ is a logical consequence of $f$ if any model (positive prediction) of $f$ is a model (positive prediction) of $f_S$ and vice-versa. In other words, for any pair $(x, y)$ of the sampled training dataset, we have $f(x) = f_S(x)$.

**Definition 23.** For a binary setting, a classifier $f_S$ is locally equivalent to the initial classifier $f$ in the neighborhood $V_x$ if $f(X) = f_S(X)$.

Two models are said to be locally equivalent if they both predict the same output value for the same samples. Thus, the explanation generated using the surrogate model $f_S$ will be consistent (faithful) to the model $f$ since $f_S$ is locally faithful to the model $f$.

The evaluation of the faithfulness of the surrogate model $f_S$ to $f$ is based on the difference between the predictions of $f$ and $f_S$. A low consistency between these predictions means that the outputs of $f_S$ are not consistent with those from the original model $f$ for $x \in V_x$.

We mainly focus in the remaining of this manuscript on the agnostic option used when no direct CNF encoding exists for $f$ or if the encoding is intractable. We make the realistic assumption that the surrogate model is faithful to $f$ in the neighborhood of the sample $x$ to explain.

## Random Forest as surrogate model

A machine learning model that can guarantee a good trade-off between faithfulness and tractability (tractable CNF encoding) is the one of random forests (RF).

Given a sample $x$ and its prediction $f(x)$ we follow the steps described previously in order to build a surrogate model $f_S$ that can be converted into logical formulae (interchangeably noted $\Sigma_f$ or $\Sigma_{f_S}$). We determine the neighborhood of $x$ by sampling instances within a radius $r$ of $x$. We train a random forest on the new dataset composed of pairs $(x', y')$ where $x' \in V(x, r)$ and $y' = f(x')$. Once we have trained a RF $f_S$ to agnostically approximate a classifier $f$ in the locality of $x$, we need to encode it into a CNF formula following the same steps explained in 3.2.1. Namely, data instances $x$ predicted positively ($f(x)=1$) by the classifier are models of the CNF encoding the classifier. Similarly, data instances $x$ predicted negatively ($f(x)=0$) are counter-models of the CNF encoding the classifier. Such equivalence is tightly related to the fidelity of the surrogate model. Indeed, a high accuracy that tends towards 100% ensures that the original model and the surrogate one have the same input-output behavior. An illustration of this encoding phase is shown in Example 19

**Example 19.** As a running example to illustrate the different steps, we trained a Neural Network model $f$ on the United Stated Congressional Voting Records Dataset<fnref n="12" />. In this example, the label Republican corresponds to a positive prediction, noted 1 while the label Democrat corresponds to a negative prediction, noted 0. An input instance $x$ is defined over the following set of binary features :

<footnote n="12">¹²Available at https://archive.ics.uci.edu/ml/datasets/congressional+voting+records.</footnote>
<table><tr><td>X<sub>1</sub></td><td>handicapped-infants</td><td>X<sub>9</sub></td><td>mx-missile</td></tr><tr><td>X<sub>2</sub></td><td>water-project-cost-sharing</td><td>X<sub>10</sub></td><td>immigration</td></tr><tr><td>X<sub>3</sub></td><td>adoption-of-the-budget-resolution</td><td>X<sub>11</sub></td><td>synfuels-corporation-cutback</td></tr><tr><td>X<sub>4</sub></td><td>physician-fee-freeze</td><td>X<sub>12</sub></td><td>education-spending</td></tr><tr><td>X<sub>5</sub></td><td>el-salvador-aid</td><td>X<sub>13</sub></td><td>superfund-right-to-sue</td></tr><tr><td>X<sub>6</sub></td><td>religious-groups-in-schools</td><td>X<sub>14</sub></td><td>crime</td></tr><tr><td>X<sub>7</sub></td><td>anti-satellite-test-ban</td><td>X<sub>15</sub></td><td>duty-free-exports</td></tr><tr><td>X<sub>8</sub></td><td>aid-to-nicaraguan-contras</td><td>X<sub>16</sub></td><td>export-administration-act-south-africa</td></tr></table>

Assume an input instance $x=(1,1,1,0,0,0,1,1,1,0,0,0,0,1,0,1)$ whose prediction is to be explained. As a surrogate model, we trained a random forest classifier $RF_f$ composed of 3 decision trees (decision tree 1 to 3 from left to right in Figure 3.5) on the vicinity of the input sample $x$.

<figure><img src="image_21.png" /><figcaption>Figure 3.5: A random forest classifier trained on the neighborhood of $x$</figcaption></figure>

In this example, $RF_f$ achieved an accuracy of 91.66%. This $RF_f$ classifier will later be encoded into CNF to serve for the enumeration of symbolic explanations. Each decision tree ($DT_i$) represents a Boolean function whose truth value is captured by Boolean variable $y_i$. The Boolean function of $RF_f$ is captured by the variable $y$. Note that the encoding of $RF_f$ is provided in this example in propositional logic in order to avoid heavy notations. The following formulae illustrate the encoding steps applied to $RF_f$:

<table><tr><td>DT<sub>1</sub></td><td>y<sub>1</sub> ⇔ (X<sub>5</sub>) ∧<br/>(¬X<sub>5</sub> ∨ ¬X<sub>15</sub> ∨ X<sub>4</sub>)</td></tr><tr><td>DT<sub>2</sub></td><td>y<sub>2</sub> ⇔ (X<sub>4</sub>) ∧<br/>(¬X<sub>4</sub> ∨ ¬X<sub>11</sub> ∨ X<sub>16</sub>)</td></tr><tr><td>DT<sub>3</sub></td><td>y<sub>3</sub> ⇔ (X<sub>9</sub> ∨ X<sub>14</sub>) ∧<br/>(X<sub>9</sub> ∨ ¬X<sub>14</sub> ∨ X<sub>5</sub>) ∧<br/>(¬X<sub>9</sub> ∨ X<sub>12</sub>) ∧<br/>(¬X<sub>9</sub> ∨ ¬X<sub>12</sub> ∨ ¬X<sub>11</sub>)</td></tr><tr><td>Majority vote</td><td>y ⇔ (y<sub>1</sub> ∧ y<sub>2</sub>) ∨ (y<sub>1</sub> ∧ y<sub>3</sub>) ∨ (y<sub>2</sub> ∧ y<sub>3</sub>) ∨ (y<sub>1</sub> ∧ y<sub>2</sub> ∧ y<sub>3</sub>)</td></tr></table>
## 3.3 Enumeration of symbolic explanations

In this section we give more insights on how we model the explanation-generation problem and present the setting used to enumerate the desired types of explanations. We provide the formal definitions of the symbolic explanations which are described as a set of selected features but with guarantees of sufficiency and minimality. This enumeration phase corresponds to **Step 2** in Figure 3.2. To generate symbolic explanations, we rely on analyzing inconsistent formulae and focus on finding and enumerating explanations of inconsistency and corrections.

### 3.3.1 Satisfiability solving for explanation generation

In order to enumerate the symbolic explanations, we propose to model the problem using different concepts from the propositional satisfiability problem (SAT). This choice is justified by our desire to propose a declarative approach, i.e. does not require the implementation of specific algorithms nor dedicated programs with the aim of using SAT solvers as the problem solving engine. Given a test instance, a SAT solver can be viewed as an oracle which answers either positively (for satisfiable instances) or negatively (for unsatisfiable instances). Recall that we are interested in two complementary types of symbolic explanations: sufficient reasons ($SR_x$) which lead to a given prediction and counterfactuals ($CF_x$) allowing to know the minimal changes to apply on the data instance $x$ to obtain a different outcome.

Our approach is based on the reduction of the problem of explaining a prediction to a variant of the SAT problem called Partial-Max SAT [BHvM09] and relies on two very common concepts in SAT which are Minimal Unsatisfiable Subsets (MUSes) and Minimal Correction Subsets (MCSes) to enumerate these explanations. Such a declarative approach allows to exploit the strengths of modern SAT solvers and already existing and proven solutions and algorithms for the extraction of MUSes and MCSes such as [GMP07, LS08, MPMS15, BK15, LPMMS16, BK16, MIPMS16, PMJMS18, NBMS18, BČB18]. In addition, it makes it possible to restrict the explanations only to that which concern the input data $x$ and do not include clauses that concern the encoding of the classifier.

Given an unsatisfiable formula, a maximum satisfiability problem (Max-SAT) returns the maximum number of OR clauses that can be satisfied. Namely, for a CNF with $m$ clauses and $n$ variables, a Max-SAT solution would be an assignment of the $n$ variables to satisfy the maximum number of clauses. A Partial Max-SAT problem is composed of two disjoint sets of clauses where $\Sigma_H$ denotes the hard clauses (those that could not be relaxed) and $\Sigma_S$ denotes the soft ones (those that could be relaxed). The aim is finding an assignment to the variables such that no hard clause $\Sigma_H$ is falsified and the minimum number of soft clauses $\Sigma_S$ are falsified. In our modeling, the set of hard clauses $\Sigma_H$ corresponds to $\Sigma_f$, the CNF formula encoding the classifier $f$ while the set of soft clauses $\Sigma_S$ corresponds to $\Sigma_x$, the CNF encoding of the data instance $x$ whose prediction $f(x)$ is to be explained. Let $\Sigma_x$ be the set of soft clauses, defined as follows :

* Each clause $\alpha \in \Sigma_x$ is composed of exactly one literal ($\forall \alpha \in \Sigma_x, |\alpha| = 1$).

* Each literal corresponds to a Boolean variable $\{X_i \in X\}$ from the input feature space of $f$.
**Example 20.** Let us consider the input instance $x=(1,1,1,0,0,0,1,1,1,0,0,0,0,1,0,1)$ from Example 19. The CNF $\Sigma_x$ associated to it is :

$$ \Sigma_x (X_1) \wedge (X_2) \wedge (X_3) \wedge \neg(X_4) \wedge \neg(X_5) \wedge \neg(X_6) \wedge (X_7) \wedge (X_8) \wedge (X_9) \wedge \neg(X_{10}) \wedge \neg(X_{11}) \wedge \neg(X_{12}) \wedge \neg(X_{13}) \wedge (X_{14}) \wedge \neg(X_{15}) \wedge (X_{16}) $$

Recall that since the classifier $f$ is "equivalently" encoded by $\Sigma_f$, then a negative prediction $f(x)=0$ corresponds to an unsatisfiable CNF $\Sigma_f \cup \Sigma_x$. Now, given an unsatisfiable CNF $\Sigma_f \cup \Sigma_x$, it is possible to identify the subsets of $\Sigma_x$ responsible for the unsatisfiability (corresponding to reasons of the prediction $f(x)=0$), or the ones allowing to restore the consistency of $\Sigma_f \cup \Sigma_x$ (corresponding to counterfactuals allowing to flip the prediction and get $f(x)=1$). For positively predicted instances, we can simply work on the negation of the decision function of the classifier.

### 3.3.2 Enumerating sufficient reason explanations ($SR_x$)

We are interested here in identifying minimal reasons of why the prediction is $f(x)=0$. This is done by identifying subsets of clauses causing the inconsistency of the CNF $\Sigma_f \cup \Sigma_x$ (recall that the prediction $f(x)$ is captured by the truth value of $\Sigma_f \cup \Sigma_x$). A sufficient reason explanation of a given instance $x$ ($SR_x$) is the minimal subset of feature values that explains why the decision was made for this specific instance. This means that it is enough to fix this group of features so that the model will make the same prediction whatever the values of the remaining features in $x$ are. We formally define the $SR_x$ explanations as follow:

**Definition 24.** ($SR_x$ explanations) Let $x$ be a data instance and $f(x)$ its prediction by the classifier $f$. A sufficient reason explanation $\tilde{x}$ of $x$ is such that:

1. $\tilde{x} \subseteq x$ ($\tilde{x}$ is a part of $x$)

2. $\forall \acute{x} \in X, \tilde{x} \subset \acute{x} : f(\acute{x})=f(x)$ ($\tilde{x}$ suffices to trigger the prediction)

3. There is no partial instance $\hat{x} \subset \tilde{x}$ satisfying 1 and 2 (minimality)

Intuitively, a sufficient reason $\tilde{x}$ is defined as the part of the data instance $x$ such that $\tilde{x}$ is minimal and triggers the prediction $f(x)$.

**Example 21.** For example, let us consider a binary classification task for predicting if credit applications should be granted or denied. A model $f$ is trained on attributes such as age, education, working hours, income, debt and accounts. Given an input instance $x = (\text{age}=20, \text{education}=\text{high school}, \text{working hours}=30, \text{income}=800, \text{debt}=200, \text{accounts}=5)$ and the prediction $f(x) = \text{"loan denied"}$. Assume a sufficient reason to trigger the reject decision is as follows $SR_x = \{\text{Income}=800, \text{Debt}=200, \text{accounts}=5\}$. This means that the reject decision sticks for any instance $\acute{x}$ having the features income, debt and accounts respectively set to 800, 200 and 5, and thus whatever the values of the other features are.

Given Definition 13 of minimal unsatisfiable subsets, it is clear that a MUS for $\Sigma_f \cup \Sigma_x$ comes down to a subset of soft clauses, namely a part of $x$ that is causing the inconsistency (the prediction $f(x)=0$).

**Proposition 4.** Let $f$ be a classifier, let $\Sigma_f$ be its CNF representation. Let $x$ be a data instance predicted negatively ($f(x)=0$) and let $\Sigma_f \cup \Sigma_x$ be the corresponding Partial Max-SAT encoding. Let $SR(x, f)$ be the set of sufficient reasons of $x$ w.r.t $f$. Let MUS($\Sigma_{f,x}$) be the set of MUSes of $\Sigma_f \cup \Sigma_x$. Then:

$$ \forall \tilde{x} \subseteq x, \tilde{x} \in SR(x, f) \iff \tilde{x} \in MUS(\Sigma_{f,x}) \qquad (3.4) $$
**Proposition 4** states that each MUS of the CNF $\Sigma_f \cup \Sigma_x$ is a $SR_x$ for the prediction $f(x)=0$ and vice versa.

*Proof.* The proof is straightforward. It suffices to remember that the decision function of $f$ is equivalently encoded by $\Sigma_f$ and that the definition of a MUS on $\Sigma_f \cup \Sigma_x$ corresponds exactly to the definition of an $SR_x$ for $f(x)$. Recall that MUSes can only include soft clauses in our modeling. For the first implication (each MUS $\tilde{x}$ is a sufficient reason explanation), it is easy to verify that if $\tilde{x}$ is a MUS then it satisfies the 3 properties of Definition 24 (sufficient reason explanation). Namely, (1) $\tilde{x}$ is part of the data instance $x$ (since the MUS are limited to soft clauses in our modeling), (2) Since $f(x)=0$ iff $(\Sigma_f \cup \Sigma_x)$ is unsatisfiable and $\tilde{x} \in MUS$ then $\forall \acute{x} \in X, \tilde{x} \subset \acute{x} : f(\acute{x})=f(x)$, (3) $\tilde{x}$ is minimal.

For the implication in the opposite direction, it holds since for each sufficient reason $\tilde{x}$, there exists a MUS containing only the elements of $\tilde{x}$ as unit clauses. From Definition 24 we have $\tilde{x} \subseteq x$, $f(x) = 0$ and $\forall \acute{x} \in X, \tilde{x} \subset \acute{x} : f(\acute{x})=f(x)$. We know that $f(x)=0$ iff $(\Sigma_f \cup \Sigma_x)$ is unsatisfiable. Hence, since $f(x[\tilde{x}])=f(x)$ then $(\Sigma_f \cup \Sigma_{x[\tilde{x}]})$ is unsatisfiable. Consequently, $\tilde{x}$ is a MUS ($\tilde{x}$ is minimal and causes the inconsistency). □

**Example 22** (Example 19 continued). Given the CNF $\Sigma_f \cup \Sigma_x$ associated to $RF_f$ from Example 19 and the input $x=(1, 1, 1, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 1, 0, 1)$, we enumerate the $SR_x$ for $f(x)=0$ ($x$ is predicted as Democrat). There are three $SR_x$:

* $SR_x^1=$"$X_4=0$ AND $X_5=0$" (meaning that if the features physician-fee-freeze ($X_4$) and el-salvador-aid ($X_5$) are set to 0, then the prediction is Democrat);

* $SR_x^2=$"$X_{12}=0$ AND $X_5=0$" (meaning that if the features education-spending ($X_{12}$) and el-salvador-aid ($X_5$) are set to 0, then the prediction is Democrat);

* $SR_x^3=$"$X_4=0$ AND $X_{12}=0$ AND $X_9=1$" (meaning that if the features physician-fee-freeze ($X_4$) and education-spending ($X_{12}$) are set to 0, then the prediction is Democrat);

It is easy to check for instance that if $X_4=0$ and $X_5=0$ then decision trees $DT_1$ and $DT_2$ of Figure 3.5 predict 0 leading the random forest to predict 0 thanks to the majority vote.

### 3.3.3 Enumerating counterfactual explanations ($CF_x$)

A counterfactual explanation of a given instance $x$ ($CF_x$) is the minimal subset of features to modify to alter the outcome of the black-box model. It is an actionable explanation provided to the user in the form of data instances that would have received a different outcome. A $CF_x$ distinguishes between variables that need to be modified (activated for binary classifiers) and the ones that need to remain unchanged (deactivated for binary classifiers).

Let us formally define the concept of counterfactual explanation.

**Definition 25.** (*$CF_x$ Explanations*) Let $x$ be a complete data instance and let $f(x)$ be its prediction by the decision function of $f$. A counterfactual explanation $\tilde{x}$ of $x$ is such that:

1. $\tilde{x} \subseteq x$ ($\tilde{x}$ is a part of $x$)

2. $f(x[\tilde{x}])=1-f(x)$ (prediction inversion)

3. There is no partial instance $\hat{x} \subset \tilde{x}$ satisfying 1 and 2 (minimality).

In Definition 25, the term $x[\tilde{x}]$ denotes the data instance $x$ where variables included in $\tilde{x}$ are inverted.
**Example 23** (Example 21 continued). Keeping up with the task of classifying loan applications as accepted/rejected and giving the same input $x$ and the same prediction from the previous example, a counterfactual explanation to change the reject decision "loan denied" into "loan granted" is $CF_x = (Income=1000, accounts=3)$. This means that the loan will be approved if the user increases his income by 200€ and closes two accounts.

Most approaches proposed within the literature (e.g. [DCL$^+$18, MCV$^+$18, MST20, WMR17]) to find counterfactual explanations are based on solving optimization problems. Thus, the generated explanations may be considered heuristic and not fully trustable. Recently, there has been work on a applying formal reasoning to generate counterfactuals. Authors in [INAMS20] address the "Why Not?" question and proposed an approach based on abductive reasoning to find contrastive explanations (CXp), i.e. find a change of feature values that guarantees a change of prediction.

Following our modeling, an MCS for $\Sigma_f \cup \Sigma_x$ comes down to a subset of soft clauses denoted $\tilde{x}$, namely a part of $x$ that is enough to remove (or reverse in our case) in order to restore the consistency (flip the prediction $f(x)=0$ to $f(x[\tilde{x}])=1$). Recall that the term $x[\tilde{x}]$ denotes the data instance $x$ where variables included in the counterfactual $\tilde{x}$ are inverted.

**Proposition 5.** Let $f$ be the decision function of a ML classifier, $\Sigma_f$ be its CNF representation, $x$ be a data instance predicted negatively and $\Sigma_f \cup \Sigma_x$ the corresponding Partial Max-SAT encoding of $f(x)=0$. Let $CF(x, f)$ be the set of counterfactuals of $x$ w.r.t $f(x) = 0$. Let $MCS(\Sigma_{f,x})$ the set of MCSes of $\Sigma_f \cup \Sigma_x$. Then,

$$ \forall \tilde{x} \subseteq x, \tilde{x} \in CF(x, f) \iff \tilde{x} \in MCS(\Sigma_{f,x}) \qquad (3.5) $$

Proposition 5 states that each MCS of the CNF $\Sigma_f \cup \Sigma_x$ represents a $CF \tilde{x} \subseteq x$ for the prediction $f(x)=0$ and vice versa.

*Proof.* Recall that MCSes can only include soft clauses in our modeling. For the first implication (each MCS $\acute{x}$ is a counterfactual explanation), it is easy to check that if $\acute{x}$ is an MCS then it satisfies the 3 properties of Definition 25 (counterfactual explanation). Namely, (1) $\acute{x}$ is part of the data instance $x$ (since the MCS are limited to soft clauses in our modeling), (2) Since $f(x)=0$ iff $(\Sigma_f \cup \Sigma_x)$ is unsatisfiable and $\acute{x} \in MCS$ then $f(x[\acute{x}])=1-f(x)$, (3) $\acute{x}$ is minimal.

For the implication in the opposite direction, it is enough to see that for each counterfactual $\acute{x}$, there exists an MCS containing only the elements of $\acute{x}$ as unit clauses. From Definition 25 we have $\acute{x} \subseteq x$, $f(x)=0$ and $f(x[\acute{x}])=1$. We know that $f(x)=0$ iff $(\Sigma_f \cup \Sigma_x)$ is unsatisfiable. Hence, since $f(x[\acute{x}])=1$ then $(\Sigma_f \cup \Sigma_{x[\acute{x}]})$ is satisfiable. Consequently, $\acute{x}$ is an MCS ($\acute{x}$ is minimal and restores the consistency). $\square$

**Example 24** (Example 19 continued). Given the CNF $\Sigma_f \cup \Sigma_x$ associated to $RF_f$ from Example 19 and the input $x=(1, 1, 1, 0, 0, 0, 1, 1, 1, 0, 0, 0, 0, 1, 0, 1)$, we enumerate the counterfactual explanations to identify the minimal changes to alter the outcome vote Democrat to Republican. The reading of such explanations is as follows : in order to force the prediction to be Republican (1), it is enough to alter $x$ by activating/deactivating the variables included in $CF_x$. There are four $CF_x$ such that :

* $CF_x^1 = \text{"X}_4=0 \text{ AND } \text{"X}_{12}=0\text{"}$ : activate (set to 1) physician-fee-freeze ($X_4$) and education-spending ($X_{12}$) while keeping the remaining values unchanged);

* $CF_x^2 = \text{"X}_5=0 \text{ AND } \text{"X}_{12}=0\text{"}$ : activate el-salvador-aid ($X_5$) and education-spending ($X_{12}$) while keeping the remaining values unchanged);

* $CF_x^3 = \text{"X}_5=0 \text{ AND } \text{"X}_9=1\text{"}$ : activate (set to 1) el-salvador-aid ($X_5$) and deactivate (set to 0) mx-missile ($X_9$) while keeping the remaining values unchanged);
* $CF_x^4 = \text{"X}_4\text{=0 AND X}_5\text{=0"} : \text{activate physician-fee-freeze (X}_4\text{) and el-salvador-aid (X}_5\text{) while keeping the remaining values unchanged)}$;

<figure><img src="image_22.png" /><figcaption>Figure 3.6: The random forest paths set by $x$</figcaption></figure>

It is easy to see that the four $CF_x$ allow to flip the negative prediction associated with $x$. Indeed, in Figure 3.6, the pink lines show the branches of the trees that are fixed by the current input instance $x$. Clearly, according to $CF_x^1 = \text{"X}_4\text{=0 AND X}_1\text{=0"}$, if we set $X_4=1$ and $X_1=1$ then this will force $DT_2$ and $DT_3$ to predict 1 making the prediction of the random forest flips to 1.

### 3.3.4 On enumerating sufficient reasons and counterfactuals

The results presented in Section 3.3.2 and 3.3.3 establishing that counterfactual and sufficient reason notions correspond to MCS and MUS respectively within Partial MaxSAT-based setting allow us to exploit the state-of-the-art algorithms for the extraction and enumeration of MUSes and MCSes. The decision problem of checking if a propositional formula is satisfiable (SAT) is known to be NP-complete [Coo71]. An unsatisfiable CNF formula can have an exponential number of MCSes and MUSes of the instance. The time needed to this complete computation is exponential as well. However, this number in practice is often relatively small, allowing for complete enumeration of the MCSes of a given instance. From a computational point of view, the enumeration of MCSes presents a real challenge. Yet, the task of finding MCSes is often easier than the one of finding MUSes directly because in practice, it is easier to find satisfiable subsets of constraints than unsatisfiable subsets [LS08].

However, advances in constraint solver technologies have allowed the development of more efficient algorithms [BL03, DRGM10, MSHJ$^+13$, GLM14, BDTK14, MPMS15, MIPMS16] which can handle problems with several million clauses and variables, allowing them to be efficiently used in many applications and made the resolution of some previously impossible instances feasible. Approaches such as [LS09, MSHJ$^+13$, BDTK14, PMJMS17, PMJMS18] calculate all MCSes. The main principle of these methods is to iteratively block the MCS found in order to avoid recalculating it. To do so, these methods match to each MCS found, a new clause formed by the disjunction of the literals of the clauses forming it. The aim is to ensure that at least one of the MCS clauses will be activated in the solutions of the following enumerations.

A second category of methods proposed to enumerate MCSes is the one based on the duality hitting set. For instance, the CAMUS system [LS08] uses this relation to compute all MUSes in two steps. The first step is to compute all the MCSes of the unsatisfiable formula $\Sigma$. The second one is to find MUSes by computing the minimal hitting sets of the MCSes.
Duality of sufficient reasons and counterfactuals

Given a collection Ω of sets from some finite domain *D*, a hitting set (denoted HS) of Ω is a set of
elements from *D* that "hits" every set in Ω by having at least one element in common with it. A formal
definition is given in Definition 26.

**Definition 26.** *Given* Ω ⊆ 2<sup>*D*</sup>, *a hitting set* H *of* Ω *is* H ⊆ D *such that* ∀S ∈ Ω, H ∩ S ≠ ∅.

A hitting set *H* is said to be *minimal*, denoted MHS, if no subset of *H* is a hitting set of Ω. In other
words, no element can be removed from *H* without losing the property of being a hitting set. A hitting
set *H* is *minimum* if it has the smallest size over all hitting sets.

Given a CNF formula Σ, the set of its MUSes(Σ) and the set of its MCSes(Σ) are "hitting set duals"
of one another <sup>13</sup>. The minimal hitting set duality between MUSes and MCSes is a well known rela-
tionship [Rei87, BL03] used in many works (e.g. [LS08],[BS05]). Concretely, every MUS hits every
MCS. Dually, every correction subset hits every unsatisfiable subset. The duality of explanations and
their enumeration has been also investigated in [INAMS20] where they exploit it to establish a duality
relationship between abductive and contrastive explanations. The same relation stands between SR<sub>x</sub> and
CF<sub>x</sub> explanations which allows us to exploit any algorithm for computing MUSes/MCSes to enumerate
both kinds of explanations. The enumeration of sufficient reasons explanations of Σ<sub>f</sub> ∪ Σ<sub>x</sub> can be done
using the hitting set duality over the counterfactuals explanations.

**Example 25.** Given a set of MCSes enumerated for the CNF Σ of Example 24 and composed of four reparation sets : MCSes(Σ) = {{X₄, X₁₂}, {X₅, X₁₂}, {X₄, X₅}, {X₅, X₉}}, we select the variable X₉ to be contained in a growing MUS. It appears only in the last MCS of the set. To ensure that X₉ is not redundant, we remove X₅ from the remaining MCSes. This leaves {{X₄}, {X₁₂}} as the remaining sub-problem. The set of MUSes(Σ) computed as the hitting set of MCSes(Σ) as described above and illustrated in Figures 3.7a and 3.7b is presented as follows :

<figure><img src="image_23.png" /><figcaption>Figure 3.7: Set of MUSes and MCSes of the CNF Σ from Example 19.</figcaption></figure>

An example of minimal hitting set (yet not minimum) in the set of MUSes(Σ) is {X₄, X₉, X₁₂}. In the same set MUSes(Σ), {X₄, X₅} and {X₅, X₁₂} are the only minimum hitting sets.

<footnote n="13"><sup>13</sup> A subset α of Σ is MUS iff α is a minimal hitting set of MCSes(Σ), a subset p of Σ is an MCS iff p is a minimal hitting set of MUSes(Σ)</footnote>
$$MCSes(\Sigma) = \{\{X_4, X_{12}\}, \{X_5, X_{12}\}, \{X_4, X_5\}, \{X_5, X_9\}\}$$

$$MUSes(\Sigma) = \{\{X_4, X_5\}, \{X_5, X_{12}\}, \{X_4, X_9, X_{12}\}\}$$

In our case, we can use any state-of-the-art algorithm to enumerate MCSes for Partial Max-SAT formulae. We use the EnumELSRMRCache tool that implements the boosting algorithm for MCSes enumeration proposed in [GIL18], which introduces a technique that improves the performance of the best approaches for enumerating the MCSes of an inconsistent CNF formula. This method implements the model rotation paradigm [BMS11, NRS14, BK15, NBMS18] allowing it to recursively compute sets of MCSes in a heuristic and efficient way. The EnumELSRMRCache tool is implemented in C++ and uses Minisat<fnref n="14" /> as backend SAT solver. We also use the LBX-like MCS enumerator module from the PySAT toolkit [IMMS18]<fnref n="15" /> framework implements a prototype of the LBX algorithm for the computation of a minimal correction subset (MCS) and/or MCS enumeration for partial MaxSAT formulae. The LBX abbreviation stands for literal-based MCS extraction algorithm, which was proposed in [MPMS15]. The module can use any SAT solver available in PySAT toolkit [IMMS18]. As for the enumeration of sufficient reasons, it is associated to the one of MUSes. In our case, the enumeration of MUSes is achieved by computing all the minimal hitting sets of all the MCSes enumerated.

## Complexity of $SR_x$ and $CF_x$ enumeration

The complexity associated with the enumeration of a sufficient reason or a counterfactual explanations amounts to the complexity associated respectively to the enumeration of a MUS or an MCS (Propositions 4 and 5). These results already exist in the literature. The extraction of a MUS has a complexity of $FP^{NP}$ and checking whether there exists a MUS of size $\le k$ is of complexity $\Sigma_2^P$-complete [Gup06, Lib05]. The task of finding the smallest MUS has been studied in several papers such as [IPLMS15, MLA+05] and its complexity is $FP^{\Sigma_2^P}$.

**Lemma 2.** Let $\Sigma_f \cup \Sigma_x$ the CNF encoding of the classifier $f$ and the data $x$. Finding a sufficient reason explanation is a problem of complexity $FP^{NP}$ and finding the smallest SR explanation is in $FP^{\Sigma_2^P}$.

*Proof.* According to proposition 4 that states that a MUS is a sufficient reason explanation, finding a sufficient reason is equivalent to finding a MUS, hence, it has the same complexity. The same reasoning applies for finding the smallest SR explanation. $\square$

Checking whether a subset of a CNF formula is an MCS is DP-complete<fnref n="16" /> [CT95] and the computation of an MCS is a problem of complexity $FP^{NP}$.

**Lemma 3.** Let $\Sigma_f \cup \Sigma_x$ the CNF encoding of the classifier $f$ and the data $x$. Let $f(x) = 0$, then finding a counterfactual explanation is a problem of complexity $FP^{NP}$.

*Proof.* Due to Proposition 5 which states that counterfactual explanations corresponds to MCSes, finding a counterfactual explanation is equivalent to finding an MCS, hence, it has the same complexity. $\square$

To sum up, we model the enumeration of symbolic explanations as a Partial Max-SAT problem which allows us to exploit any existing algorithms for the enumeration of MUSes and MCSes such as [LS08, BMS12, NRS13, MSHJ+13, BK15, WH13]. Since we are using MUSes and MCSes as a basis

<footnote n="14">¹⁴MiniSat is a open-source SAT solver http://minisat.se/</footnote>

<footnote n="15">¹⁵PySAT toolkit is designed for simple, fast, and effective Python-based prototyping using SAT oracles. It is composed of four modules which are wrappers for the code originally implemented in the C/C++ and Python languages.</footnote>

<footnote n="16">¹⁶A problem $\mathcal{P}$ belongs to the class DP if it can be written as $\mathcal{P} = \mathcal{P}_1 \cup \mathcal{P}_2$ with $\mathcal{P}_1 \in \text{NP}$ and $\mathcal{P}_2 \in \text{coNP}$.</footnote>
for providing interpretable explanations and thanks to the hitting set duality between them, it is possible to first enumerate MCSes and then use the minimal hitting set duality for computing the MUSes of a formula such as in [BS05, LS08]. Such enumeration involves calling SAT solvers for each explanation. This constraint might cause scalability problems since a call to a SAT-solver amounts to the resolution of an NP-complete decision problem. Recent works [SSDC20, AKM20a, MSGC$^+$20, IIM20, ABB$^+$21, Ign20, CSGD20b, IM21] study same families of classifiers whose explanations can be enumerated either in a polynomial time or at least, efficiently in practice.

#### 3.3.5 Beyond $SR_x$ and $CF_x$ explanations

The symbolic explanations ($SR_x$ and $CF_x$) directly enumerated are complementary to the feature attribution explanations in the sense that they answer questions beyond the contribution of input features into a decision. In addition, once enumerated, such explanations can be exploited to answer requests such as *what are the irrelevant features for a given decision?* and *what are the features to have complete explanations?* For instance, such requests are useful for system builders (data scientists, developers, etc) to check whether an algorithm is correctly relying on the right variables. In addition, this kind of information is necessary to have confidence and gain trust in the model before it is deployed. It is also useful to regulatory bodies (e.g public organization or government agencies) to know if a change in a legally sensitive feature (e.g. race, gender, country of origin) produces a change in the model's outcome.

Based on $SR_x$ and $CF_x$ explanations, one can answer other XAI queries such as what are the relevant/irrelevant features for a given $f(x)$ prediction.

**Irrelevant features** Irrelevant features are meant to answer the question *what are the irrelevant features for a given decision?* An irrelevant feature is a feature that do not appear in any explanation of a prediction $f(x)$.

**Definition 27.** (Irrelevant features) Let $f(x)$ be the prediction of a sample $x$ by a model $f$, $X$ the input feature space of $f$ and $E(x, f)$ the set of explanations associated to $f(x)$ (either $SR_x$ or $CF_x$ explanations). The set of irrelevant features $X^{IRL}$ is formally defined as : $\{X_i \in X \mid X_i \notin e_i, \forall e_i \in E(x, f)\}$.

**Example 26** (Example 19 continued). Let us continue with the United Stated Congressional Voting records dataset. The input space $X$ is composed of 16 features $X=\{X_1, \dots, X_{16}\}$. Given the set of $SR_x$ and $CF_x$ explanations in Examples 22 and 24, and the sample $x$ from Example 19, the set of irrelevant features is : $X^{IRL} = \{X_1, X_2, X_3, X_6, X_7, X_8, X_{10}, X_{11}\}$.

**Relevant features** A relevant feature is defined as a feature involved in at least one explanation $e_i \in E(x, f)$.

**Definition 28.** (Relevant features) Let $f(x)$ be the prediction of a sample $x$ by a model $f$, $X$ the input feature space of $f$ and $E(x, f)$ the set of explanations associated to $f(x)$ (either $SR_x$ or $CF_x$ explanations). The set of relevant features $X^{RLV}$ is formally defined as : $\{X_i \in X \mid \exists e_i \in E(x, f) \text{ s.t. } X_i \in e_i\}$.

**Example 27** (Example 26 continued). Let us continue with the United Stated Congressional Voting records dataset, given the set of irrelevant features from the previous Example 26, the set of relevant features would be : $X^{RLV} = \{X_4, X_5, X_9, X_{12}\}$.

**Remark 6.** It is clear that the set of relevant features $X^{RLV}$ is the complement of $X^{IRL}$ in $X$.
**Necessary features** A necessary feature is a feature appearing in every explanation.

**Definition 29.** (Necessary features) Let $f(x)$ be the prediction of a sample $x$ by a model $f$, $X$ the input feature space of $f$ and $E(x, f)$ the set of explanations associated to $f(x)$ (either $SR_x$ or $CF_x$ explanations). The set of necessary features $X^{NCS}$ is formally defined as : $\{X_i \in X \mid X_i \in e_i, \forall e_i \in E(x, f)\}$.

A necessary feature denotes a highly relevant feature since it is involved in every explanation.

## 3.4 Experimental study

This section presents an experimental evaluation to verify the tractability of the proposed approach in this chapter. The evaluation will follow the processing flow proposed in this chapter (surrogate modeling, encoding into CNF and explanation enumeration). The experimental protocol followed is described in the following: We considered a selection of datasets known from the literature and publicly available and can be found on Kaggle (https://www.kaggle.com/) or UCI (http://archive.ics.uci.edu/ml/). The studied datasets deal with binary classification and are listed in Table 3.1. No pre-processing was performed on the data except the binarization of variables. We transform the data using a binary threshold<fnref n="17" />. The binarization threshold ($T$) used was defined empirically as follows: given a starting set of values (such as the mean, the median, etc.) associated to each variable, we choose the threshold $T$ which optimizes the accuracy of the model trained on binarized data using $T$. For instance, the widely used standard "MNIST" dataset <fnref n="18" /> composed of handwritten digit images of size 28 × 28 pixels was binarized using a threshold set to $T = 127$.

<table><caption>Table 3.1: Properties of the datasets used.</caption><thead><tr><td>Dataset</td><td>#instances</td><td>#features</td><td>data type</td></tr></thead><tbody><tr><td>MNIST</td><td>70000</td><td>784</td><td>Images</td></tr><tr><td>MONK's Problems</td><td>181</td><td>16</td><td>Numerical</td></tr><tr><td>Spect Heart</td><td>160</td><td>22</td><td>Numerical</td></tr><tr><td>Congressional US Voting</td><td>435</td><td>16</td><td>Numerical</td></tr><tr><td>Breast Cancer</td><td>287</td><td>48</td><td>Numerical</td></tr></tbody></table>

All experiments were performed on machines equipped with an Intel Core i7-7700 (3.60GHz ×8) processors, with 32 Gb of RAM and under the Linux Cen-tOS operating system. The time-out has been set to 600 seconds for each execution of an enumeration algorithm.

To enumerate the explanations, our approach principally needs the black-box ($f$), the instance to explain ($x$) and the radius $r$ to define the neighborhood of $x$. We trained our own black-box models ($f$) for the different dataset and used Multi-layer Perceptron (MLP), Decision Tree (DT) and Logistic Regression (LR) classifiers from the Python library Scikit-Learn in its version v0.22.1. The hyper-parameters of different classifiers were set to their default values. We also used "one-vs-all" Binary Neural Network (BNN)<fnref n="19" /> classifiers on the MNIST dataset to recognize digits (0 to 9) using the pytorch implementation<fnref n="20" /> of the Binary-Backpropagation algorithm BinaryNets [HCS+16]. As for the surrogate models, we used random forest (RF) from the Scikit-Learn in its version v0.22.1. A wide range of hyper-parameters for RFs were explored in attempts to reach relatively the best fidelity of the surrogate models

<footnote n="17">¹⁷All values above the threshold are marked as 1 and all values equal to or below the threshold are marked as 0.</footnote>

<footnote n="18">¹⁸MNISTdatasetavailableathttp://yann.lecun.com/exdb/mnist/</footnote>

<footnote n="19">¹⁹defined as a neural networks with binary weights and activations at run-time</footnote>

<footnote n="20">²⁰available at: https://github.com/itayhubara/BinaryNet.pytorch</footnote>