Abstract Interpretation-based Feature Importance
for Support Vector Machines

Abhinandan Pal¹[0000-0002-4122-5092], Francesco Ranzato²[0000-0003-0159-0068], Caterina Urban³[0000-0002-8127-9642], and Marco Zanella²[0000-0002-6164-6169]

¹ School of Computer Science, University of Birmingham, United Kingdom
a.pal@bham.ac.uk

² Dipartimento di Matematica, University of Padova, Italy
{francesco.ranzato,marco.zanella}@unipd.it

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

³ INRIA and Ecole Normale Supérieure | Université PSL, France
caterina.urban@inria.fr

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

**Abstract.** We study how a symbolic representation for support vector machines (SVMs) specified by means of abstract interpretation can be exploited for: (1) *en-hancing the interpretability* of SVMs through a novel feature importance measure, called abstract feature importance (AFI), that does not depend in any way on a given dataset or the accuracy of the SVM and is very fast to compute; and (2) *cer-tifying individual fairness* of SVMs and producing concrete counterexamples when this verification fails. We implemented our methodology and we empirically showed its effectiveness on SVMs based on linear and nonlinear (polynomial and radial basis function) kernels. Our experimental results prove that, independently of the accuracy of the SVM, our AFI measure correlates much strongly with sta-bility of the SVM to feature perturbations than major feature importance measures available in machine learning software such as permutation feature importance, therefore providing better insight into the trustworthiness of SVMs.

# 1 Introduction

Machine learning (ML) software is increasingly being employed in high-stakes or sensitive applications. [10, 16, etc.]. As a consequence, research in ML verification rapidly gained popularity [28,45], and the quest for interpretable ML models is becoming more and more pressing [43].

A fundamental and popular interpretability methodology is *feature importance*, that is, techniques for measuring the contribution of each input feature to a model prediction [5]. Nowadays, the most influential and used feature importance measures are Permutation Feature Importance (PFI) [6,18], Local Interpretable Model-agnostic Explanations (LIME) [38], and SHapley Additive exPlanations (SHAP) [29]. PFI observes the decrease in predictive performance when a feature value is randomly shuffled: an increased loss is indicative of how much that feature is important for the predictive model. LIME approximates the prediction model locally by training an interpretable surrogate model on points in a meaningful neighborhood around a given input. SHAP is a framework based on locally estimating so-called Shapley values [42]. The downsides of PFI and SHAP are that their outcome may greatly vary depending on the dataset and
may be misleading when features are correlated [25]. Furthermore, they also have a
high computational cost when the number of features is large, even for small models.
Moreover, the quality of the output of PFI strongly depends on the accuracy of the model.
Notably, model variance to feature perturbations [23] and PFI are strongly correlated
only when the model generalizes well. Similarly, it is unclear how to define a meaningful
optimal neighborhood for LIME and this may lead to explanations that are unstable
and manipulable. More importantly, LIME assumes that the decision boundary of the
underlying model is locally linear, but there is no guarantee that this actually happens.

**Contributions.** In this work, we focus on the interpretability of Support Vector Machines (SVMs), which nowadays are used in extensive repertoire of critical and high-stakes applications such as credit card fraud detection, facial recognition, and melanoma classification [9]. In particular, we propose a novel feature importance measure for SVMs, called *Abstract Feature Importance* (AFI), that: (a) leverages an approximation of the underlying predictive model which is *formally correct-by-construction*; (b) does *not* depend on a given dataset or on model accuracy; and (c) is extremely *fast to compute*, independently of the number of features. We support both linear and nonlinear kernels, in particular the polynomial and radial basis function (RBF) kernels.

We derive our importance measure from a symbolic representation of a SVM based
on *abstract interpretation* [12]. Specifically, the concrete vectors being manipulated by
model computations are symbolically represented through an abstract domain, which
defines their abstract counterparts and their data structure representations, as well as
algorithms to process them by approximating the behaviour of operations, such as
additions and dot products, used in model computations.

We leverage existing numerical abstract domains such as intervals (i.e., geometric hyperrectangles) [13] and affine forms (i.e., geometric zonotopes) [31] that we combine with a novel abstract domain tailored for precisely representing computations with one-hot encoded categorical input features. We show the effectiveness of this new combined abstract domain for certifying model stability against feature perturbations. In particular, we focus on verifying *individual fairness* [16] of SVMs, which, to the best of our knowledge, has not been investigated before. We evaluate our approach by certifying SVMs trained on the reference datasets in the literature on ML fairness [30] and by considering different similarity relations. Our approach is *sound by design*, meaning that an individually fair abstract representation of a SVM implies that this SVM is actually fair. Thus, the fraction of successful fairness verifications over a test dataset turns out to be a *lower bound* on the real individual fairness of a SVM. On the other hand, our approach is *incomplete*, as there are cases in which the SVM is fair whereas the verification of its abstract representation fails, due to imprecisions introduced by the abstraction process. Our third contribution is a method to leverage this abstract representation of SVMs to generate concrete counterexamples when the abstraction is unable to prove individual fairness, i.e., we deliver concrete similar inputs to a SVM that result in different classifications. The fraction of successful counterexample searches over a test dataset yields a lower bound on how biased an SVM is, and therefore, by complement, an *upper bound* on the real individual fairness of a SVM.

Finally, we conduct an extensive experimental comparison between our new feature
importance measure AFI and popular interpretability methods like PFI and LIME. The
experimental results show that AFI is better correlated with stability of a SVM model to feature perturbations, independently of the accuracy of the model.

**Related Work.** Feature importance measures can be *local*, i.e., measuring feature importance for a specific prediction, or *global*, i.e., measuring importance over the entire input space of the predictive model. We also distinguish *model-agnostic* measures, which can be applied to any model, and *model-specific* measures. Finally, we classify importance measures in *performance-based*, i.e., measuring importance w.r.t. the predictive performance of the model (thus requiring knowledge of the ground truth values), and *effect-based*, measuring importance based on the magnitude of change in the predicted outcome due to changes in the feature value (requiring no knowledge of the ground truth values).

PFI [6,18] is a global, model-agnostic, performance-based measure. LIME [38] and SHAP [29] are both local, model-agnostic, effect-based measures. Our novel feature importance measure AFI is specific for SVMs but can be used both as *global and local* measure, is *effect-based* and is *dataset independent*, thus removing bias to the dataset. LIME can also be extended to a global measure by considering several local instances [38, Section 4]. However, the choice of how many and which instances to select remains not obvious, thus not providing correctness guarantees. By contrast, our AFI measure is based on a formally correct-by-construction approximation of the underlying predictive model.

Several other model-agnostic importance measures have been proposed in the literature. Prominent effect-based measures are visual tools such as partial dependence (PD) [19], individual conditional expectation (ICE) [22], and accumulated local effects (ALE) [4] plots. Visual tools, such as individual conditional importance (ICI) and partial importance (PI) curves [8], are also proposed for local performance-based measures. [8] proposes a Shapley feature importance measure, called SFIMP, that allows comparing feature importance across different models. Input gradient [24] is a local measure that can be both effect-based and performance-based. Feature importance measures specific for SVMs are typically limited to linear SVMs or face scalability issues w.r.t. the number of features, e.g. [10,32]. By contrast, our AFI measure supports nonlinear kernels and has no scalability issues.

Our work generally contributes to the research ecosystem around the verification of ML models using formal methods [2,28,45]. Most approaches consider (deep) neural networks [40,41,44,48, etc.], while here we focus on SVMs. Our work leverages a SVM verifier called SAVer [36]. In addition, we introduce here a more precise abstraction for one-hot encoded features that we integrated within SAVer. Our fairness analysis is in line with the approach investigated in [35], that evaluated the individual fairness of decision tree ensembles trained by a new fairness-aware learning technique. Similar works either consider an orthogonal notion of fairness or a different “threat model”, in most cases both. [47] evaluates security against flipping a few labels to maximize classification error. [21] considers group and causal fairness metrics. [27] deals with robustness of SVMs against adversarial attacks. [17] proposes a new fairness metric where it adds a new feature with random values and bias individuals on this feature: the model is fair when it recovers the original labels. [34] puts forward a protocol to protect sensitive information
and trains a fair model using homomorphic encryption. [30,46] discuss several fairness metrics used to verify a variety of ML models.

## 2 Background

**Support Vector Machines.** SVMs [14] are supervised machine learning models based on separation curves that partition the input vector space into regions that best fit binary classification labels $L = \{-1, +1\}$. Separation curves are computed by maximizing their distance (margin) from the closest vectors in the training dataset. The simplest SVM is linear, which in its primal form boils down to a hyperplane $w \cdot z - b = 0$, where $w \in \mathbb{R}^n$ and $b \in \mathbb{R}$ are learned parameters, that determines whether an input $z \in \mathbb{R}^n$ falls above/below (i.e., sgn($w \cdot z - b$) = $\pm 1$) w.r.t. the hyperplane. This approach is extended to nonlinear SVMs through a projection to a high-dimensional space via a kernel function $k: \mathbb{R}^n \times \mathbb{R}^n \rightarrow \mathbb{R}$. More precisely, given an input space $X \subseteq \mathbb{R}^n$, a training dataset $T = \{(x_1, y_1), \dots, (x_N, y_N)\} \subseteq X \times \{-1, +1\}$, a kernel function $k$ and parameters $w_i, b \in \mathbb{R}$, with $i \in [1, N]$, a SVM classifier $C: \mathbb{R}^n \rightarrow \{-1, +1\}$ is represented in its dual form by the function $C(z) \triangleq \operatorname{sgn}(\sum_{i=1}^N (w_i y_i k(x_i, z)) - b)$. Most common kernels are: (i) linear, where $k(x, z) = x \cdot z$; (ii) polynomial, where $k(x, z) = (x \cdot z + c)^p$, for some hyperparameters $c \in \mathbb{R}$ and $p \in \mathbb{N}$; (iii) radial basis function (RBF), where $k(x, z) = e^{-\gamma \|x-z\|^2_2}$, for some hyperparameter $\gamma > 0$. In multi-classification for labels $L = \{y_1, \dots, y_m\}$, with $m > 2$, the standard approach is a reduction into multiple binary classification problems combined by leveraging a voting over different labels.

**Example 2.1.** Let us consider a space $X \subseteq \mathbb{R}^2$ of values normalized in the range $[-1, 1]$, thus $X = \{x \in \mathbb{R}^2 | -1 \le x_1, x_2 \le 1\}$. A toy linear SVM $C: X \to \{-1, +1\}$ with two support vectors $v_1 = (-0.5, 1)$, $v_2 = (0.5, -1) \in X$, respectively labeled as $-1, +1$, with weights $w_1 = w_2 = 0.5$ and bias $b = 0$, is represented in its dual form by the function $C(z) = \operatorname{sgn}(-1 * 0.5(v_1 \cdot z) + 1 * 0.5(v_2 \cdot z))$. $\square$

**Abstract Interpretation.** A tuple $(A, \subseteq^A, \gamma^A)$ is a numerical abstract domain (or abstraction) when $\langle A, \subseteq^A \rangle$ is a partially ordered set of abstract values and $\gamma^A: A \to \wp(\mathbb{R}^n)$ is a concretization function which maps an abstract value $a$ to the set $\gamma^A(a)$ of real vectors represented by $a$, and monotonically preserves the ordering relation, i.e., $a_1 \subseteq^A a_2$ implies $\gamma^A(a_1) \subseteq \gamma^A(a_2)$. Intuitively, an abstract domain defines a symbolic representation of some sets of vectors in $\wp(\mathbb{R}^n)$: given $X \in \wp(\mathbb{R}^n)$ and $a \in A$, if $X \subseteq \gamma^A(a)$ then $a$ is a sound representation, or approximation, of the set $X$, while if $X = \gamma^A(a)$ holds then $a$ is called a precise (or exact) representation of $X$. We sometimes use the notation $A_n$ for highlighting that $A_n$ is an abstraction of sets of $n$ dimensional vectors ranging in $\wp(\mathbb{R}^n)$.

Given a $k$-ary operation $f: (\mathbb{R}^n)^k \to \mathbb{R}^n$, for some $k > 0$, a corresponding abstract function $f^A: A^k \to A$ is a sound approximation of $f$ on $(a_1, \dots, a_k) \in A^k$ when $\{f(x_1, \dots, x_k) | x_i \in \gamma^A(a_i)\} \subseteq \gamma^A(f^A(a_1, \dots, a_k))$ holds. Moreover, $f^A$ is a complete approximation of $f$ on its input $(a_1, \dots, a_k)$ when equality holds. In words, soundness means that $f^A(a_1, \dots, a_k)$ never misses a concrete computation of $f$ on some input $(x_1, \dots, x_k)$ abstractly represented by $(a_1, \dots, a_k)$, while completeness entails that
$f^A(a_1, ..., a_k)$ is precisely a symbolic abstract representation of these concrete computations of $f$. When soundness/completeness of $f^A$ holds for any abstract input then $f^A$ is called a sound/complete approximation of $f$.

**Abstract Domains.** We consider the well-known abstract domain of hyperrectangles (or intervals) [12,13]. The hyperrectangle abstract domain $HR_n$ consists of n-dimensional vectors of real intervals $h = ([l_1, u_1], ..., [l_n, u_n]) \in HR_n$, with lower and upper bounds $l_i, u_i \in \mathbb{R} \cup \{-\infty, +\infty\}$ such that $l_i \le u_i$. Hence, the concretization function $\gamma^{HR}: HR_n \to \wp(\mathbb{R}^n)$ is defined by $\gamma^{HR}(h) \triangleq \{\mathbf{x} \in \mathbb{R}^n | \forall i. l_i \le \mathbf{x}_i \le u_i\}$. Conversely, hyperrectangles also have an abstraction map $\alpha^{HR}: \wp(\mathbb{R}^n) \to HR_n$ that provides the smallest hyperrectangle approximating a set of vectors: $\alpha^{HR}(X) \triangleq ([\inf\{\mathbf{x}_i \in \mathbb{R} | \mathbf{x} \in X\}, \sup\{\mathbf{x}_i \in \mathbb{R} | \mathbf{x} \in X\}])_{i=1}^n$. Abstract operations are defined by extending componentwise the following additions and multiplications of intervals:

$$[l_1, u_1] +^{HR} [l_2, u_2] \triangleq [l_1 + l_2, u_1 + u_2],$$

$$[l_1, u_1] *^{HR} [l_2, u_2] \triangleq [\min(l_1 l_2, l_1 u_2, l_2 u_1, l_2 u_2), \max(l_1 l_2, l_1 u_2, l_2 u_1, l_2 u_2)].$$

It is known that a compositional abstract evaluation on HR of an expression can be imprecise, e.g., the evaluations of the simple expressions $x - x$ and $x \cdot x$ on an input interval $[-c, c]$, with $c > 0$, yield, resp., $[-2c, 2c]$ and $[-c^2, c^2]$, rather than the exact intervals $[0, 0]$ and $[0, c^2]$. This dependency problem can trigger a significant source of imprecision for the hyperrectangle abstraction of a nonlinear (i.e., polynomial/RBF) SVM classifier. Thus, following [36], for our SVM abstract representations, we leverage the reduced affine form (RAF) abstraction, which is a domain of zonotopes representing dependencies between components of input vectors. A RAF for vectors in $\mathbb{R}^n$ is given by an expression $a_0 + \sum_{i=1}^n a_i \epsilon_i + a_r \epsilon_r$, where the $\epsilon_i$'s are symbolic variables ranging in the real interval $[-1, 1]$ representing a dependence from the i-th component of the vector, while $\epsilon_r$ is a further symbolic variable in $[-1, 1]$ that accumulates all the approximations introduced by nonlinear operations such as multiplications and exponentials. Thus, RAF$_n \triangleq \{a_0 + \sum_{i=1}^n a_i \epsilon_i + a_r \epsilon_r | a_0, a_1, ..., a_n \in \mathbb{R}, a_r \in \mathbb{R}_{\ge 0}\}$, where $a_r \in \mathbb{R}_{\ge 0}$ is the radius of the accumulative error of approximating all nonlinear operations during abstract computations. A RAF represents a real interval through the concretization map $\gamma^{RAF}: RAF_n \to \wp(\mathbb{R})$ defined by $\gamma^{RAF}(a_0 + \sum_{i=1}^n a_i \epsilon_i + a_r \epsilon_r) \triangleq \{x \in \mathbb{R} | a_0 - \sum_{i=1}^n |a_i| - |a_r| \le x \le a_0 + \sum_{i=1}^n |a_i| + |a_r|\}$. RAFs are a restriction to a given length—in our case to the dimension $n$ of $\mathbb{R}^n$—of the zonotope domain used in numerical program analysis [20]. Linear operations, namely additions and scalar multiplications, admit a complete approximation on the RAF abstraction, so that RAFs resolve the aforementioned dependency problem for linear expressions. Instead, nonlinear abstract operations, such as multiplications and exponentials, must still necessarily be approximated.

**Example 2.2.** Let us consider again the toy linear SVM C from Example 2.1. Its input space $X = [-1, 1]^2$ is abstracted as the RAF $a = (0 + \epsilon_1, 0 + \epsilon_2) \in (\text{RAF}_2)^2$. $\square$

**Robustness.** We consider an input space $X \subseteq \mathbb{R}^n$, a set of labels $L = \{y_1, ..., y_m\}$, and a dataset $T = \{(\mathbf{x}_1, y_1), ..., (\mathbf{x}_N, y_N)\} \subseteq X \times L$. A classifier trained on the dataset $T$ is modeled as a map $C_T: X \to L$.
An adversarial region for an input sample $\mathbf{x} \in X$ is designated by a perturbation $P(\mathbf{x}) \subseteq X$ such that $\mathbf{x} \in P(\mathbf{x})$. Usually, a perturbation function $P: X \to \wp(X)$ is defined through a metric $\mu$ to measure similarity between inputs as their distance w.r.t. $\mu$. The most common metric in ML [7] is induced by the $\ell_\infty$ maximum norm defined as $\|\mathbf{x}\|_\infty \triangleq \max\{|\mathbf{x}_1|, ..., |\mathbf{x}_n|\}$, so that the corresponding perturbation $P_\infty^\epsilon(\mathbf{x})$ includes all the vectors $\mathbf{z} \in X$ whose $\ell_\infty$ distance from $\mathbf{x}$ is bounded by a magnitude $\epsilon \in \mathbb{R}^+$, that is, $P_\infty^\epsilon(\mathbf{x}) \triangleq \{\mathbf{z} \in X \mid \|\mathbf{x} - \mathbf{z}\|_\infty \le \epsilon\}$. Given a perturbation function $P$, a classifier $C$ is robust (or stable) on $P(\mathbf{x})$, denoted by robust($C, P(\mathbf{x})$), when for all $\mathbf{z} \in P(\mathbf{x})$, $C(\mathbf{z}) = C(\mathbf{x})$ holds. Robustness to a perturbation $P$ is used as a major metric [23] to assess a classifier $C$ on a test set $T \subseteq X \times L$ as follows: $rob_T(C, P) \triangleq |\{(\mathbf{x}, y) \in T | \text{robust}(C, P(\mathbf{x}))\}|/|T|$.

**SAVer.** Our work leverages SAVer (SVM Abstract Verifier), an automatic tool for robustness certification of SVMs [36,37]. Given a SVM $C: X \to L$, SAVer leverages an $n$-dimensional abstraction $A_n$ of $\wp(\mathbb{R}^n)$ to first achieve a sound abstraction $P^\sharp(\mathbf{x}) \in A_n$ of a perturbation $P(\mathbf{x})$, i.e., $P(\mathbf{x}) \subseteq \gamma^A(P^\sharp(\mathbf{x}))$ must hold, and then applies sound abstract versions of the numerical functions used in $C$—notably, vector additions and dot products, scalar multiplications, exponentials—to design an abstract SVM classifier $C^\sharp: A \to \wp(L)$ that computes an over-approximation of the labels assigned to inputs in $P(\mathbf{x})$, i.e., $\{C(\mathbf{z}) \in L \mid \mathbf{z} \in P(\mathbf{x})\} \subseteq C^\sharp(P^\sharp(\mathbf{x}))$. If $C^\sharp(P^\sharp(\mathbf{x})) = \{y_i\}$, then every input in $P(\mathbf{x})$ is classified as $y_i$, so $C$ is proved robust on the perturbation $P(\mathbf{x})$. In the binary classification case $L = \{-1, +1\}$, the abstract SVM $C^\sharp$ consists of an abstract function $A_C^\sharp: A_n \to A_1$ that computes an over-approximation $A_C^\sharp(P^\sharp(\mathbf{x}))$ of the distances between samples in $P^\sharp(\mathbf{x})$ and the SVM separation curve, namely, it computes an abstract value $a = A_C^\sharp(P^\sharp(\mathbf{x})) \in A_1$ such that $\{\sum_{i=1}^N (w_i y_i k(\mathbf{x}_i, \mathbf{z})) - b \mid \mathbf{z} \in \gamma^{A_n}(P^\sharp(\mathbf{x}))\} \subseteq \gamma^{A_1}(a)$ holds. Afterwards, an over-approximation of the set of labels is inferred as follows:

$$C^\sharp(P^\sharp(\mathbf{x})) \triangleq \begin{cases} \textbf{if } \gamma^{A_1}(A_C^\sharp(P^\sharp(\mathbf{x}))) \subseteq \mathbb{R}_{<0} & \textbf{then } \{-1\} \\ \textbf{else if } \gamma^{A_1}(A_C^\sharp(P^\sharp(\mathbf{x}))) \subseteq \mathbb{R}_{>0} & \textbf{then } \{+1\} \\ \textbf{else } \{-1, +1\}. \end{cases}$$

**Example 2.3.** Let us consider again the toy linear SVM $C$ from Example 2.1. The abstraction $A_C^{\text{RAF}}: (\text{RAF}_n)^n \to \text{RAF}_n$ of $C$ in the RAF abstract domain is $A_C^{\text{RAF}}(a) = -1 * 0.5(\mathbf{v}_1)^{\text{RAF}} a + 1 * 0.5(\mathbf{v}_2)^{\text{RAF}} a$. By performing the abstract computations of $A_C^{\text{RAF}}$ on the abstraction $a \in (\text{RAF}_2)^2$ of its input space $X = [-1, 1]^2$ from Example 2.2, we obtain:

$$\begin{aligned} A_C^{\text{RAF}}(a) &= -0.5(-0.5(0 + \epsilon_1) + 1(0 + \epsilon_2)) + 0.5(0.5(0 + \epsilon_1) - 1(0 + \epsilon_2)) \\ &= -0.5(0 + (-0.5)\epsilon_1 + \epsilon_2) + 0.5(0 + 0.5\epsilon_1 + (-1)\epsilon_2) \\ &= 0 + 0.5\epsilon_1 + (-1)\epsilon_2 \end{aligned} \quad \square$$

# 3 Methodology

We delve into the four primary contributions, each elaborated within distinct subsections. Figure 1 delineates these contributions, categorizing them into improvements to SAVer
<figure><img src="image_3.png" /><figcaption>Fig. 1: Improvements to and new applications of SAVer</figcaption></figure>

and applications thereof. Section 3.1 introduces a method for assessing feature impor-
tance, drawing upon the RAF abstract transformers embedded in SAVer. Section 3.2
refines the aforementioned abstract transformers for both interval and RAF abstract
domains by introducing One-Hot constraints. Section 3.3 exemplifies how SAVer can be
used to verify individual fairness of SVM models leveraging the most common kernel
functions. Lastly, Section 3.4 shows how to extend SAVer to achieve a counterexample
search, thus providing additional insights on the analysis of fairness.

**3.1 Abstract Feature Importance**

Let us define our central notion of abstract feature importance (AFI).

**Definition 3.1 (Abstract Feature Importance).** Let $C: \mathbb{R}^n \to L$ be a SVM classifier and let $\mathcal{A}_C^{\text{RAF}}: (\text{RAF}_n)^n \to \text{RAF}_n$ be the abstraction of $C$ in the RAF abstract domain. Let $\mathcal{A}_C^{\text{RAF}}(f_1, \dots, f_n) \triangleq a_0 + \sum_{i=1}^n a_i \epsilon_i + a_r \epsilon_r$ be the abstract computation output for an abstract input $(f_1, \dots, f_n)$, with $f_i \in \text{RAF}_n$. The importance of every input feature $i \in [1, n]$ is defined as the absolute value $|a_i| \ge 0$. $\square$

This definition purposely ignores the accumulative error due to the approximations of all
nonlinear operations performed by *C*, i.e., the term $a_r \epsilon_r$, influenced by all input features.
When the input $(f_1, ..., f_n) \in (\text{RAF}_n)^n$ abstracts the whole input space $X \subseteq \mathbb{R}^n$, AFI
measures the *global* feature importance. Otherwise, AFI measures the *local* importance
on the output label.

<figure><img src="image_4.png" /><figcaption>Fig. 2: Toy example of AFI for a linear SVM</figcaption></figure>
**Example 3.2.** Let us consider again the toy linear SVM *C* from Example 2.1, and its abstract computation output *A*<sup>RAF</sup><sub>*C*</sub>(*a*) = 0 + 0.5*ε*<sub>1</sub> + (-1)*ε*<sub>2</sub> from Example 2.3, for its abstract input *a* ∈ (RAF<sub>2</sub>)<sup>2</sup> from Example 2.2.

Based on Definition 3.1, we infer the importance indices |a₁| = 0.5 and |a₂| = 1 for, resp., **x**₁ and **x**₂, and conclude that **x**₂ is twice as important as **x**₁, as also shown by the picture in Figure 2.

Note that, since *C* is a linear SVM, it can be rewritten in primal form as: *C'*(**x**) = -0.5(**v**<sub>1</sub> ⋅ **x**) + 0.5(**v**<sub>2</sub> ⋅ **x**) = -0.5(-0.5**x**<sub>1</sub> + **x**<sub>2</sub>) + 0.5(0.5**x**<sub>1</sub> - **x**<sub>2</sub>) = 0.5**x**<sub>1</sub> - **x**<sub>2</sub> = (0.5, -1) ⋅ **x**, thus obtaining an explicit weight **w** = (0.5, -1) for the input features, whose absolute values 0.5 and 1 coincide with our importance indices. □

For linear SVMs, as in the above example, the abstraction in the RAF abstract domain is *sound* and *complete* yielding an output RAF that matches the primal form of the SVM, ensuring the full accuracy of AFI. Instead, nonlinear SVMs cannot be represented in primal form and thus the output RAF acts as a pseudo-primal form, soundly over-approximating the true output region of the SVM. In this case, the accuracy of AFI hinges upon the precision of the SVM abstraction. Our work builds upon the RAF abstract transformers for linear and nonlinear (polynomial and RBF) kernels initially introduced within SAVer [36] and refines them by incorporating further constraints to better handle categorical input features, as elaborated in the next Section 3.2. Our experimental evaluation in Section 4 shows that our refined abstractions offer higher accuracy, meanwhile remaining computationally efficient. The potential introduction of more precise SVM abstractions in the future will directly benefit the accuracy of AFI.

**Example 3.3.** Let us consider a toy SVM *C* similar to that of Example 2.1, sharing the same support vectors, labels and weights but using the polynomial kernel *k*(**z**, **v**) ≜ (**z** ⋅ **v** + *c*)<sup>*d*</sup>, where *c* = 1, *d* = 2. Its abstract computation output turns out to be *A*<sup>RAF</sup><sub>*C*</sub>(*a*) = 0 + 1*ε*<sub>1</sub> − 2*ε*<sub>2</sub> + 1*ε*<sub>*r*</sub> for its abstract input *a* ∈ (RAF<sub>2</sub>)<sup>2</sup> from Example 2.2. We infer the importance indices |*a*<sub>1</sub>| = 1 and |*a*<sub>2</sub>| = 2 for, resp., **x**<sub>1</sub> and **x**<sub>2</sub>, and, once again, infer that **x**<sub>2</sub> is twice as important as **x**<sub>1</sub>. In this case, we also observe that the nonlinear noise accumulation term *ε*<sub>*r*</sub> is greater than zero, meaning that some approximations happened through the computation, as expected for nonlinear kernels. □

**Feature Grades.** The AFI indices $a_i \ge 0$ (we assume that $a_i$ implicitly denotes its absolute value) depend on the size of the abstract input, and this can make them harder to read and interpret, especially when the number of input features is high. To address this issue, we use a simple clustering strategy to assign an importance score to the input features. We consider the distribution of the AFI importance indices $(a_i)_{i=1}^n$ and compute its mean $\mu$ and standard deviation $\sigma$. Then, for each feature $i$, we consider its z-score $z_i \triangleq \frac{a_i - \mu}{\sigma}$, and the least integer greater than or equal to $z_i$ as a corresponding rating, i.e., $\text{score}_i \triangleq \lceil \frac{a_i - \mu}{\sigma} \rceil$: this has the effect of standardizing the distribution into a normal distribution, slicing the distribution at every unit, and then labeling every slice with a progressive number. By doing so, features moderately influencing the result will have a score close to zero, relevant features will have higher scores, and those not influencing the outcome will have a negative score. Lastly, we shift and clip such distribution to achieve
what we call feature grades ranging, e.g., in an interval $[a, b]$, as obtained by an easy transformation: $grade_i \triangleq \max(\min(b, score_i + shift), a)$. For instance, let us consider a distribution of AFI indices for 10 features given by $(1, 6, 2, 5, 6, 1, 6, 7, 8, 9)$, where $\mu = 5.1$ and $\sigma = 2.85$: the corresponding scores are $(-1, 1, -1, 0, 1, -1, 1, 1, 2, 2)$, we shift them by +6 and then we clip these shifted values in $[3, 10]$, thus achieving the grades $(5, 7, 5, 6, 7, 5, 7, 7, 8, 8)$. Hence, e.g., $x_1$ and $x_3$ have similar impact on the classification, although they have different AFI indices.

Finally, let us remark that AFI does not require any knowledge on the ground truth values, nor the actual output of the SVM classifier, as AFI focuses on the computation process performed by the classifier, rather than how the result of such computation is used to assign a label to an input, thus making this approach applicable to scenarios where the correct prediction is not known in advance.

## 3.2 Abstracting One-Hot Encoding

Most ML algorithms need a way to represent categorical data in numerical form. Let $F = \{c_1, c_2, ..., c_k\}$ be the set of values of some categorical feature $f$. A naïve approach assigning a different number to each value in $F$ introduces an unwanted ordering relation among features, that often induces bias or poor accuracy. A better and well-known method is one-hot encoding, that is, replacing $f$ with $k$ binary features $(x_1^f, x_2^f, ..., x_k^f) \in \{0, 1\}^k$ such that $\forall i \in [1, k]$, $x_i^f = 1 \Leftrightarrow f = c_i$. This sequence $(x_i^f)_{i=1}^k$ of $k$ bits is also referred to as a tier of $f$. Numerical abstractions, such as the hyperrectangle and RAF abstract domains, are likely to suffer from a significant loss of precision when dealing with these one-hot encoded features, as they are not able to keep track of the relation $\sum_{i=1}^k x_i^f = 1$ existing between the binary features resulting from one-hot encoding.

**Example 3.4.** Consider a categorical feature $f \in F = \{red, green, blue\}$, and let $(x_r, x_g, x_b) \in \{0, 1\}^3$ denote the corresponding one-hot encoded tiers. Consider the set of categories $\{red, green\}$, represented by the set of tiers $X = \{(1, 0, 0), (0, 1, 0)\}$. The most precise hyperrectangle abstraction of $X$ is $h = (x_r \in [0, 1], x_g \in [0, 1], x_b \in [0, 0]) \in \text{HR}_3$. Observe that $h$ also represents infinitely many vectors in $\mathbb{R}^3$ that do not belong to $X$ and are illegal one-hot encodings, such as $(0.4, 0.8, 0)$, $(1, 1, 0)$ or $(0, 0, 0)$. $\square$

To hinder this loss of precision, we define the *One-Hot abstraction*, a novel numerical abstraction tailored for one-hot encoded values.

Firstly, we recall the *constant propagation* abstract domain $\text{CP} \triangleq \mathbb{R} \cup \{\perp^{\text{CP}}, \top^{\text{CP}}\}$, ordinarily used for the constant folding optimization by modern compilers [1]. $\text{CP}$ is a flat domain whose partial order $\sqsubseteq^{\text{CP}}$ is defined by $\perp^{\text{CP}} \sqsubseteq^{\text{CP}} z \sqsubseteq^{\text{CP}} \top^{\text{CP}}$, for all $z \in \mathbb{R}$. The concretization map $\gamma^{\text{CP}}: \text{CP} \to \wp(\mathbb{R})$ is as follows: $\gamma^{\text{CP}}(z) \triangleq \{z\}$, for all $z \in \mathbb{R}$, meaning that a given numerical feature can only assume a constant value $z$; $\gamma^{\text{CP}}(\top^{\text{CP}}) \triangleq \mathbb{R}$ representing no constancy information; $\gamma^{\text{CP}}(\perp^{\text{CP}}) \triangleq \emptyset$ encodes unfeasibility. $\text{CP}$ also has an abstraction map $\alpha^{\text{CP}}: \wp(\mathbb{R}) \to \text{CP}$ that provides the best (i.e. least w.r.t. the order $\sqsubseteq^{\text{CP}}$) approximation in $\text{CP}$ of a set of values, which is as follows: $\alpha^{\text{CP}}(\emptyset) \triangleq \perp^{\text{CP}}$, $\alpha^{\text{CP}}(\{z\}) \triangleq z$, and $\alpha^{\text{CP}}(X) \triangleq \top^{\text{CP}}$ otherwise.
The One-Hot abstract domain for a k-dimensional, i.e. with k original categories, one-hot encoded feature space is $OH_k \triangleq (CP \times CP)^k$. Thus, abstract values are k-tuples of pairs of values in CP, that keep track of the numerical information originated from a single one-hot k-encoded feature, both when this was originally false, i.e. set to 0, or true, i.e. set to 1. Given $a \in OH_k$ and one generic component $a_i \in CP \times CP$, with $i \in [1, k]$, let $a_{i,f/t} \in CP$ denote, resp., the first/second element of $a_i$, i.e., $a_i = (a_{i,f}, a_{i,t})$. The partial order $\sqsubseteq$ of $OH_k$ is induced componentwise by $\sqsubseteq^{CP}$, namely, for all $a, b \in OH_k$, $a \sqsubseteq b \Leftrightarrow \forall i \in [1, k]. a_{i,f} \sqsubseteq^{CP} b_{i,f} \& a_{i,t} \sqsubseteq^{CP} b_{i,t}$. Then, for each component $i \in [1, k]$, the map $\hat{\gamma}_i : OH_k \to \wp(\mathbb{R}^k)$ is defined as:

$$ \hat{\gamma}_i(a) \triangleq \{ \mathbf{x} \in \mathbb{R}^k \mid \mathbf{x}_i \in \gamma^{CP}(a_{i,t}), \forall j \neq i. \mathbf{x}_j \in \gamma^{CP}(a_{j,f}) \}. $$

Therefore, $a \in OH_k$ symbolically represents through $\hat{\gamma}_i$ the set of tiers whose i-th component was originally set to true. Note that if, for some $i \in [1, k]$, either $a_{i,f} = \perp^{CP}$ or $a_{i,t} = \perp^{CP}$, then $\hat{\gamma}_i(a) = \emptyset$. To retrieve all the concrete vectors represented by $a$, we collect all the vectors obtained by assuming that any component of the tier was originally set to true, namely, the concretization map $\gamma^{OH_k} : OH_k \to \wp(\mathbb{R}^k)$ is defined by $\gamma^{OH_k}(a) \triangleq \cup_{i=1}^k \hat{\gamma}_i(a)$.

**Example 3.5.** Let us continue Example 3.4 by considering the abstract element $a = ((0,1), (0,1), (0, \perp^{CP})) \in OH_3$. It turns out that $a$ represents the set of tiers $X = \{(1,0,0), (0,1,0)\}$, which, in turn, is the one-hot encoding of $\{red, green\}$. In fact, its concretization is: $\gamma^{OH_3}(a) = \hat{\gamma}_1(a) \cup \hat{\gamma}_2(a) \cup \hat{\gamma}_3(a) = \{\mathbf{x} \in \mathbb{R}^3 \mid \mathbf{x}_1 \in \{1\}, \mathbf{x}_2 \in \{0\}, \mathbf{x}_3 \in \{0\}\} \cup \{\mathbf{x} \in \mathbb{R}^3 \mid \mathbf{x}_1 \in \{0\}, \mathbf{x}_2 \in \{1\}, \mathbf{x}_3 \in \{0\}\} \cup \{\mathbf{x} \in \mathbb{R}^3 \mid \mathbf{x}_1 \in \{0\}, \mathbf{x}_2 \in \{0\}, \mathbf{x}_3 \in \emptyset\} = \{(1,0,0), (0,1,0)\}$. Thus, $a$ precisely represents $X$. $\square$

Example 3.5 is not fortuitous. In fact, for any set $X$ of one-hot encoded tiers there always exists an abstract value $a$ in $OH$ which precisely represents this set, i.e., such that $\gamma^{OH}(a) = X$.

**Theorem 3.6.** If $X \in \wp(\mathbb{R}^k)$ is such that every vector of $X$ is a one-hot encoded tier $(0, ..., 0, 1, 0, ...0) \in \{0, 1\}^k$, then the abstract value $a^X \in OH_k$ defined as $a_i^X \triangleq (\alpha^{CP}(\{\mathbf{x}_i \mid \mathbf{x} \in X, \mathbf{x}_i = 0\}), \alpha^{CP}(\{\mathbf{x}_i \mid \mathbf{x} \in X, \mathbf{x}_i = 1\}))$, for all $i \in [1, k]$, precisely represents $X$.

It is worth remarking that this abstraction $OH$ allows us to represent one-hot encoded information in a compact way. For example, given three categorical features with five possible values each, an abstract value in $OH$ consists of $5 + 5 + 5 = 15$ pairs of type $(a_{i,f}, a_{i,t}) \in CP$, whereas the size of the concrete set of all the possible values for these three categorical features is $5^3 = 125$. In general, the size of an $OH$ representation is in $O(NV)$ where $N$ is the number of different categorical features and $V$ is the maximum number of different categorical values for a given feature, whereas the size of the actual concrete values is in $O(V^N)$.

A value $a \in OH_k$ such that, for all $i \in [1, k]$ and $u \in \{f, t\}$, $a_{i,u} \in CP \setminus \{\perp^{CP}\}$ holds, is called *top-less*. It is important to note that the abstract value $a^X \in OH_k$ defined in Theorem 3.6 is always top-less because the components of each pair $a_i^X$ range in $\{0, 1, \perp^{CP}\}$.
Given a numerical function $f: \mathbb{R} \to \mathbb{R}$, its sound abstract counterpart $f^{\text{CP}}: \text{CP} \to \text{CP}$ on the CP abstraction is defined as follows:

$$f^{\text{CP}}(a) \triangleq \begin{cases} \perp^{\text{CP}} & \text{if } a = \perp^{\text{CP}} \\ f(z) & \text{if } a = z \text{ for some } z \in \mathbb{R} \\ \top^{\text{CP}} & \text{if } a = \top^{\text{CP}} \end{cases}$$

In turn, $f^{\text{CP}}$ allows us to define a sound abstract counterpart of $f$ on our OH abstract domain.

**Theorem 3.7.** A sound approximation of $f$ on OH$_k$ is the function $f^{\text{OH}}: \text{OH}_k \to \text{OH}_k$ defined, for all $i \in [1, k]$, as follows:

$$(f^{\text{OH}}(a))_i \triangleq (f^{\text{CP}}(a_{i,f}), f^{\text{CP}}(a_{i,t})).$$

**Example 3.8.** Let us carry on Example 3.5. We assume a SVM with a polynomial kernel of degree two, whose abstract computation includes applying the nonlinear function $f(x) \triangleq x^2 - 3x + 1$ to each 0/1 component of the tiers in $\gamma^{\text{OH}}(a) = \{(1, 0, 0), (0, 1, 0)\}$, so that $f(\gamma^{\text{OH}}(a)) = \{(-1, 1, 1), (1, -1, 1)\}$. By Theorem 3.7, we have that $a' \triangleq f^{\text{OH}}(a) = ((f^{\text{CP}}(0), f^{\text{CP}}(1)), (f^{\text{CP}}(0), f^{\text{CP}}(1)), (f^{\text{CP}}(0), f^{\text{CP}}(\perp^{\text{CP}})) = ((1, -1), (1, -1), (1, \perp^{\text{CP}}))$, whose concretization is:

$$\begin{align*} \gamma^{\text{OH}}(a') &= \hat{\gamma}_1(a') \cup \hat{\gamma}_2(a') \cup \hat{\gamma}_3(a') \\ &= \{\mathbf{x} \in \mathbb{R}^3 \mid \mathbf{x}_1 \in \{-1\}, \mathbf{x}_2 \in \{1\}, \mathbf{x}_3 \in \{1\}\} \\ &\quad \cup \{\mathbf{x} \in \mathbb{R}^3 \mid \mathbf{x}_1 \in \{1\}, \mathbf{x}_2 \in \{-1\}, \mathbf{x}_3 \in \{1\}\} \\ &\quad \cup \{\mathbf{x} \in \mathbb{R}^3 \mid \mathbf{x}_1 \in \{1\}, \mathbf{x}_2 \in \{1\}, \mathbf{x}_3 \in \emptyset\} \\ &= \{(-1, 1, 1), (1, -1, 1)\}. \end{align*}$$

Notice that completeness holds because $f(\gamma^{\text{OH}}(a)) = \gamma^{\text{OH}}(f^{\text{OH}}(a))$.

On the other hand, using the hyperrectangle abstraction, we noticed in Example 3.4 that $h = ([0, 1], [0, 1], [0, 0]) \in \text{HR}_3$ is the initial hyperrectangle representation of the set of tiers $\{(1, 0, 0), (0, 1, 0)\}$. By applying the abstract transfer function $f^{\text{HR}}$ to $h$, we compute:

$$\begin{align*} h' = f^{\text{HR}}(h) &= ([0, 1]^{2\text{HR}} - 3 \cdot \text{HR} [0, 1] + \text{HR} [1, 1], \\ & \quad [0, 1]^{2\text{HR}} - 3 \cdot \text{HR} [0, 1] + \text{HR} [1, 1], \\ & \quad [0, 0]^{2\text{HR}} - 3 \cdot \text{HR} [0, 0] + \text{HR} [1, 1]) \\ &= (-2, 2, -2, 2, [1, 1]). \end{align*}$$

Thus, we have that $\gamma^{\text{HR}}(h') = \{\mathbf{x} \in \mathbb{R}^3 \mid -2 \le \mathbf{x}_1, \mathbf{x}_2 \le 2, \mathbf{x}_3 = 1\}$. This latter concrete set of vectors is much larger than $\gamma^{\text{OH}}(f^{\text{OH}}(a))$: while soundness is nevertheless guaranteed in HR, we have lost a good deal of information due to the imprecision of the interval abstraction. In particular, observe that for $\mathbf{x}_1$ and $\mathbf{x}_2$, OH was able to derive precisely their values ranging in $\{-1, +1\}$, while the HR analysis
computes much less precise lower/upper bounds for $x_1$ and $x_2$ such as -2 and 2, as a consequence of the abstract computation:

$$[0, 1]^{2^{HR}} - 3 \cdot^{HR} [0, 1] +^{HR} [1, 1] = [0, 1] + [-3, 0] + [1, 1] = [-2, 2].$$

For instance, the lower bound -2 for $x_1$ is obtained by adding the lower bounds 0 (for $x_1^2$), -3 (for -3$x_1$), 1 (for +1), namely, by requiring that $x_1$ simultaneously assumes both values 0 and 1, which is an unfeasible spurious case.

The relational RAF abstraction induces more precise approximations w.r.t. HR, although this increase of precision is limited to linear dependencies only, including the intermediate values of the abstract computations. Thus, the OH abstraction shows a clear precision gain over both domains HR and RAF for abstract computations on one-hot encoded vectors. □

In Example 3.8, we observed that $f^{OH}$ is a complete approximation of $f$ on $a$. This is a consequence of the following general result.

**Corollary 3.9.** Let $a \in \text{OH}_k$ be top-less. Then: (i) $f^{OH}$ is a complete abstraction of $f$ on $a$; (ii) Given $f_1, f_2, \dots, f_p : \mathbb{R} \to \mathbb{R}$, $f_1^{OH} \circ f_2^{OH} \circ \dots \circ f_p^{OH}$ is a complete abstraction of $f_1 \circ f_2 \circ \dots \circ f_p$ on $a$.

**Using OH in SAVer.** We implemented in SAVer our OH abstraction for categorical features on top of the interval and RAF abstract domains for numerical features: these instances of SAVer are denoted in Section 4, resp., by Interval+OH and RAF+OH. In what follows, we focus on the RAF abstraction, since the interval domain conceptually follows the same pattern. Assume a vector of numerical features $x \in \mathbb{R}^q$ and, for simplicity, a single categorical feature $f$ having $k$ categories$^4$. We first perform the one-hot encoding of $f$, that is, $f$ is transformed into a tier in $\{0, 1\}^k$. We consider the so-called CAT perturbations of a categorical feature $f$ (cf. Section 4), where $f$ may take the value of any of its $k$ categories: e.g., the CAT perturbation of color in Example 3.4 is $\{\text{red}, \text{green}, \text{blue}\}$. This means that in the CAT perturbation of the one-hot encoding of $f$, we allow every binary feature of the tier representing $f$ to be either 0 or 1, so that the corresponding perturbed abstract value is always of the shape $oh = (0^{\text{CP}}, 1^{\text{CP}})^k \in \text{OH}_k$. For the numerical features $x$, we consider a so-called NOISE perturbation (cf. Section 4), i.e., a maximum norm perturbation $P_\infty^\epsilon(x)$ for some magnitude $\epsilon > 0$. Hence, these NOISE and CAT perturbations define an initial RAF value $a \in \text{RAF}_q$ for $x$ and an initial OH value $oh \in \text{OH}_k$ for $f$. The abstract kernel of the SVM is then computed on the RAF$_q$ domain for $x$ and on the $\text{OH}_k$ domain for $f$, and we assume that the output of this abstract computation is $\langle a', oh' \rangle \in \text{RAF}_q \times \text{OH}_k$. For our purpose of certifying the robustness, the output OH value $oh'$ is converted back to a hyperrectangle representing the lower and upper bounds of the $k$ one-hot encoded components of $f$, namely, we compute $k$ intervals $\alpha^{\text{HR}_k}(\gamma^{\text{OH}_k}(oh')) = \langle [\alpha_j, \beta_j] \rangle_{j=1}^k \in \text{HR}_k$ that provide lower and upper bounds of the numerical contributions to the SVM output of the $k$ one-hot encoded components of $f$. On the other hand, the output $a' \in \text{RAF}_q$ is converted to

<footnote>$^4$ For multiple categorical features, we keep track of the relation between all the categorical features and their corresponding tiers through a global lookup table</footnote>
the interval $[l, u] = \gamma^{\text{RAF}}(a') \in \text{HR}_1$ that gives a lower and upper bound to the sum of the contributions to the SVM output of the $q$ numerical features $\mathbf{x}$. Hence, the sum of these $k+1$ intervals provides a single interval $[(l + (\sum_{j=1}^k \alpha_j), u + (\sum_{j=1}^k \beta_j))] \in \text{HR}_1$, which is a sound approximation of the sign of the SVM output.

**Example 3.10.** Consider a vector $\mathbf{x} \in \mathbb{R}^5$ where $\mathbf{x}_1, \mathbf{x}_2 \in \mathbb{R}$ are two numerical features and $\mathbf{x}_3, \mathbf{x}_4, \mathbf{x}_5 \in \{0, 1\}$ are three binary values deriving from the one-hot encoding of a categorical feature. Assume an input perturbation of these features such that the output of the abstract computation for the numerical features is given by $a' = 1 + \epsilon_1 + 1.5\epsilon_2 + 0.5\epsilon_r \in \text{RAF}_2$, which is converted into the interval $\gamma^{\text{RAF}}(a') = [-2, 4] \in \text{HR}$, while on for the three one-hot encoded features $\mathbf{x}_3, \mathbf{x}_4, \mathbf{x}_5$, the output on OH is $oh' = ((2, -1), (3, \perp^{\text{CP}}), (3, 2)) \in \text{OH}_3$. Thus, we have that $\gamma^{\text{OH}_3}(oh') = \{(-1, 3, 3), (2, 3, 2)\}$, which is then abstracted to the hyperrectangle $\alpha^{\text{HR}_3}(\gamma^{\text{OH}_3}(oh')) = ([1, 2], [3, 3], [2, 3]) \in \text{HR}_3$. Hence, we derive a range interval of the SVM output which is $[-2, 4] +^{\text{HR}} [-1, 2] +^{\text{HR}} [3, 3] +^{\text{HR}} [2, 3] = [2, 12]$. Since $\gamma^{\text{HR}_1}([2, 12]) \subseteq \mathbb{R}_{>0}$, we have that $\text{sgn}([2, 12]) = +1$, meaning that the SVM classification is certified to be robust for the input perturbation. $\square$

## 3.3 Individual Fairness

Several formal models of fairness have been investigated in the literature. Dwork et al. [16] point out several weaknesses of the notions of group fairness and therefore study individual fairness defined as “the principle that two individuals who are similar w.r.t. a particular task should be classified similarly”. This is formalized as a Lipschitz condition of the classifier, that is, by requiring that two individuals $\mathbf{x}, \mathbf{y} \in X$ whose distance is $\delta(\mathbf{x}, \mathbf{y}) \ge 0$, are mapped, resp., to distributions $D_\mathbf{x}$ and $D_\mathbf{y}$ whose distance is at most $\delta(\mathbf{x}, \mathbf{y})$. Intuitively, the output distributions for $\mathbf{x}$ and $\mathbf{y}$ are indistinguishable up to their distance. Several distance metrics $\delta: X \times X \to \mathbb{R}_{>0}$ can be used in this context, where Dwork et al. [16] study the total variation or relative $\ell_\infty$ distances.

Following [16], a classifier $C: X \to L$ is (individually) fair when $C$ outputs the same label for all pairs of individuals $\mathbf{x}, \mathbf{y} \in X$ satisfying a similarity relation $S \subseteq X \times X$ between input samples. This relation $S$ can be derived from a distance $\delta$ as follows: $(\mathbf{x}, \mathbf{y}) \in S \Leftrightarrow \delta(\mathbf{x}, \mathbf{y}) \le \epsilon$, where $\epsilon \in \mathbb{R}$ is a similarity threshold.

**Definition 3.11 (Individual Fairness).** A classifier $C: X \to L$ is fair on an individual $\mathbf{x} \in X$ w.r.t. a similarity relation $S \subseteq X \times X$, denoted by $\text{fair}(C, \mathbf{x}, S)$, when $\forall \mathbf{z} \in X$. $(\mathbf{x}, \mathbf{z}) \in S \Rightarrow C(\mathbf{z}) = C(\mathbf{x})$. $\square$

To define a fairness metric for a classifier $C$, we compute how often $C$ is fair on sets of similar individuals in a test set $T \subseteq X \times L$:

$$ \text{fair}_{T,S}(C) \triangleq |\{(\mathbf{x}, \mathbf{y}) \in T \mid \text{fair}(C, \mathbf{x}, S)\}|/|T|. $$

Hence, individual fairness for a similarity relation $S$ boils down to robustness on the perturbation $P_S(\mathbf{x}) \triangleq \{\mathbf{z} \in X \mid (\mathbf{x}, \mathbf{z}) \in S\}$ induced by $S$, i.e., for all $\mathbf{x} \in X$, $\text{fair}(C, \mathbf{x}, S) \Leftrightarrow \text{robust}(C, P_S(\mathbf{x}))$ holds.
## 3.4 Searching for Counterexamples

The abstract interpretation framework described in Section 2 is sound, thus a classifier $C$ certified to be robust over a region $P(\mathbf{x})$ guarantees that all the inputs $\mathbf{x}' \in P(\mathbf{x})$ actually receive the same label. The converse is generally not true for nonlinear kernels, due to lack of completeness: when the abstract verification is unable to certify robustness, it may be either due to a loss of precision or to a vector in $P(\mathbf{x})$ which truly receives a different label. We refer to the latter as a *counterexample* to the robustness of $\mathbf{x}$. In case of an inconclusive analysis, we can mitigate the effect of incompleteness by searching for counterexamples: if at least one is found, then the classifier can be marked as being *not robust*. Catching a counterexample within a possibly infinite set of vectors, however, is a daunting task. Let $a \in \text{RAF}_n$ be a sound abstraction for $P(\mathbf{x})$, $C$ a classifier, and $\mathcal{A}_C^{\text{RAF}}$ its abstraction on RAF. We define an informed heuristic search approach leveraging our AFI measure as follows.

**Definition 3.12 (Counterexample Search).**

(S$_1$) Let $a_{\text{out}} \triangleq a_0 + \sum_{i=1}^n a_i \epsilon_i + a_r \epsilon_r$ be the output of the abstract computation $\mathcal{A}_C^{\text{RAF}}(a)$ on RAF (cf. Section 3.1);

(S$_2$) If $C(\mathbf{x}) < 0$, we look for a potential counterexample $\mathbf{x}^*$ by maximizing $a_{\text{out}}$, i.e., by selecting the maximum possible value for every $\mathbf{x}_i$ when $a_i > 0$, and the minimum when $a_i < 0$ (the converse if $C(\mathbf{x}) > 0$);

(S$_3$) If $C(\mathbf{x}^*) \neq C(\mathbf{x})$, then $\mathbf{x}^*$ is a counterexample for $\mathbf{x}$, and the classifier $C$ is proved not robust on $\mathbf{x}$;

(S$_4$) Otherwise, we select the most influential feature $\mathbf{x}_M$, and its mean value in $P(\mathbf{x})$, which is defined by $m \triangleq (\min\{\mathbf{y}_M | \mathbf{y} \in P(\mathbf{x})\} + \max\{\mathbf{y}_M | \mathbf{x} \in P(\mathbf{x})\})/2$, and we partition $P(\mathbf{x})$ using the cutting hyperplane $\mathbf{x}_M \le m$, thus obtaining left and right subsets $P_l(\mathbf{x}), P_r(\mathbf{x}) \subseteq P(\mathbf{x})$;

(S$_5$) We consider $a_l, a_r \in \text{RAF}_n$ abstracting, resp., $P_l(\mathbf{x}), P_r(\mathbf{x})$, and we recursively repeat from step (S$_1$) until a counterexample is found, or a user-defined timeout is met. $\square$

Maximization in step (S$_2$) requires additional care for one-hot encoded features, as exactly one of them must be set to 1: we set to 1 the most influential feature only. We also observe that computing $a_l, a_r$ during step (S$_5$) does not introduce losses of precision, as RAFs represent hyperrectangles exactly, and partitioning a RAF by a cutting hyperplane of the form $\mathbf{x}_i \le k$ yields two smaller hyperrectangles. Steps (S$_1$) and (S$_2$) correspond to looking for a counterexample in the vertices of the hyperrectangle represented by $a$, which have the greatest distance from the center and are therefore intuitively more likely to exhibit different labels. Since a hyperrectangle in $\mathbb{R}^n$ has $2^n$ vertices, it is not feasible to check them all, and we thus use our feature importance analysis to infer a gradient pointing towards the most promising one. If no counterexample is found, it may be due to the separation curve of $C$ crossing $P(\mathbf{x})$ while leaving all the vertices on the same side. We therefore proceed to steps (S$_4$) and (S$_5$) that partition $P(\mathbf{x})$ into two smaller subsets $P_l(\mathbf{x})$ and $P_r(\mathbf{x})$ by cutting the former space in half along the axis of the most influential feature, and recursively repeating the process on the two components. Should a counterexample be found, $C$ can be definitely marked as not robust. Otherwise, we set a timeout mechanism, such as a limit on the recursion depth, to avoid divergence.
**Example 3.13.** Let $s = (0, -\sqrt{2})$, $t = (-1, 1)$, $v = (1, 1)$ be the support vectors of a SVM with polynomial kernel $k(x, y) = (x \cdot y + 1)^2$, $w_s = -1$, $w_t = w_v = 1$ their weights, and $b = 0$ the bias. The SVM classifier is therefore defined as $C(x) \triangleq -(s \cdot x + 1)^2 + (t \cdot x + 1)^2 + (v \cdot x + 1)^2$, and can be rewritten to its primal form $C(x) = 2x_1^2 + 2(2 + \sqrt{2})x_2 + 1$, thus highlighting the separation curve as the parabola $\Gamma \triangleq x_2 = -\frac{1}{2+\sqrt{2}}x_1^2 - \frac{1}{2(2+\sqrt{2})}$. We now consider $x' = (0.5, -0.5)$, and let $P(x')$ be the hyperrectangle of radius 0.5 centered in $x'$, that is, $P(x') \triangleq \{x \in \mathbb{R}^2 | 0 \le x_1 \le 1, -1 \le x_2 \le 0\}$. We observe that $C(x') \approx -1.91 < 0$, whereas every point $x \in P(x')$ having $x_2 = 0$ evaluates to $2x_1^2 + 1 > 0$, which is always positive, hence $C$ is not robust over $P(x')$. The parabola $\Gamma$ crosses $P(x')$ leaving some vertices on different sides of the space.

We consider $a = (0.5 + 0.5\epsilon_1, -0.5 + 0.5\epsilon_2) \in \text{RAF}_2^2$ that represents the perturbation $P(x')$ exactly, and compute $a_{\text{out}} = c + 0.5\epsilon_1 + (1 + \sqrt{2})\epsilon_2 + d\epsilon_r$, where the values of the center $c \in \mathbb{R}$ and the nonlinear accumulation term $d \in \mathbb{R}$ are omitted for simplicity, as they are not relevant for our purposes. Thus, the abstract feature importance vector is $(0.5, 1 + \sqrt{2})$ whose components are both positive. Since $C(x') < 0$, we are looking for positive counterexamples and, following step (S$_3$) above, we select the candidate counterexample $x^* \in P(x')$ by considering the maximum values for $x_1, x_2$ for vectors ranging in $P(x')$, that is, $x^* = (1, 0)$. Then, it turns out that $C(x^*) = 2(1)^2 + 2(2 + \sqrt{2})0 + 1 = 3 > 0$, so that $x^*$ is indeed a counterexample that makes $C$ not robust on $P(x')$. $\square$

<figure><img src="image_5.png" /><figcaption>Fig. 3: Example of counterexample search</figcaption></figure>

**Example 3.14.** Continuing with Example 3.13, we consider $x'' = (-1, 0)$ and the region $P(x'') = \{x \in \mathbb{R}^2 | -1 \le x_1 \le +1, -\frac{1}{2+\sqrt{2}} \le x_2 \le 0\}$, as depicted in Figure 3. Observe that every vertex of $P(x'')$ is on the same side of $\Gamma$ and thus receives the same class +1, while the subregion of $P(x'')$ below the parabola lays on the other side, making $C$ not robust. We iterate the search of counterexamples illustrated in Example 3.13, providing the AFI vector $i = (0, \frac{3+2\sqrt{2}}{(2+\sqrt{2})^2}) = (0, 0.5)$, which can be viewed as a gradient vector guiding the counterexample search. In this case, we look for a counterexample $x^* \in P(x'')$ such that $C(x^*) < 0$, hence moving in the opposite direction w.r.t. the gradient vector $i$. By doing so, we consider the bottom-left corner
<table><caption>Table 1: Reference datasets.</caption><thead><tr><th rowspan="2">Dataset</th><th rowspan="2">#Features</th><th colspan="2">Training Set</th><th colspan="2">Test Set</th></tr><tr><th>Size</th><th>Positive</th><th>Size</th><th>Positive</th></tr></thead><tbody><tr><td>Adult</td><td>103</td><td>30162</td><td>24.9%</td><td>15060</td><td>24.6%</td></tr><tr><td>Compas</td><td>371</td><td>4222</td><td>53.3%</td><td>1056</td><td>55.6%</td></tr><tr><td>German</td><td>56</td><td>800</td><td>69.8%</td><td>200</td><td>71.0%</td></tr></tbody></table>

$\mathbf{x}^* = (-1, -\frac{1}{2+\sqrt{2}})$ of $P(\mathbf{x}'')$ such that $C(\mathbf{x}^*) = 1$, thus meaning that we did not compute a counterexample. We therefore follow the steps ($S_4$) and ($S_5$) by partitioning $P(\mathbf{x}'')$ through the hyperplane $\mathbf{x}_2 \le -\frac{1}{2(2+\sqrt{2})}$, as shown by the dotted line in Fig. 3, and then starting the recursive search. After the first recursive step, none of the two new (hyper)rectangles have counterexamples in their vertices, so another recursive step is applied to the lower rectangle which is partitioned by the hyperplane $\mathbf{x}_1 \le 0$. This generates two new (hyper)rectangles, and both have now counterexamples in their vertices, which can be found through steps ($S_1$) and ($S_2$), therefore proving, through a counterexample witness, that $C$ is not robust. □

# 4 Experimental Evaluation

We consider the main reference datasets used in the fairness literature [30]:(i) **Adult** [15], which labels yearly incomes, above or below 50K US$, based on personal attributes; (ii) **Compas** [3], which labels recidivism risk based on personal attributes and criminal history; (iii) **German** [15], which labels good/bad credit scores. Table 1 displays size and distribution of positive samples for these datasets. The data is preprocessed according to [41]. Some of these datasets exhibit a highly unbalanced label distribution, leading to high accuracy and 100% individual fairness for a constant classifier like $C(\mathbf{x}) = 1$. Thus, following [41], we report in Table 2, for several SVM models, both accuracy and balanced accuracy, i.e., $\frac{1}{2} \left( \frac{\text{truePos}}{\text{truePos}+\text{falseNeg}} + \frac{\text{trueNeg}}{\text{trueNeg}+\text{falsePos}} \right)$.

**Similarity Relations.** Let $I \subseteq \mathbb{N}$ be a set of indices of features after one-hot encoding, and $\mathbf{x}, \mathbf{y} \in X$ be two individuals. Following [41], we consider three similarity relations.

**NOISE:** Given a subset of numerical features $I' \subseteq I$, let $S_{\text{noise}}(\mathbf{x}, \mathbf{y})$ iff $|\mathbf{x}_i - \mathbf{y}_i| \le \epsilon$ for all $i \in I'$, and $\mathbf{x}_i = \mathbf{y}_i$ for all $i \in I \setminus I'$. This means that all the features of $\mathbf{x}$ in $I'$ are subject to a maximum norm perturbation $P_{\infty}^{\epsilon}(\mathbf{x})$. For our experiments, we consider $\epsilon = 0.05$, namely, a $\pm 5\%$ perturbation for data normalised to [0, 1].

**CAT:** Given a subset of sensitive categorical attributes $I' \subseteq I$, let $S_{\text{cat}}(\mathbf{x}, \mathbf{y})$ iff $\mathbf{x}_i = \mathbf{y}_i$ for all $i \in I \setminus I'$. For Adult and German, we select the gender attribute, while for Compas, the race attribute.

**NOISE-CAT:** $S_{\text{noise-cat}}(\mathbf{x}, \mathbf{y}) \triangleq S_{\text{noise}}(\mathbf{x}, \mathbf{y}) \lor S_{\text{cat}}(\mathbf{x}, \mathbf{y})$.

**Setup.** We trained the SVMs used in our experiments with scikit-learn. Hyperparameters were chosen by hit-and-trial and observing trends. The final hyperparameters for each kernel and dataset were those that led to SVMs with high balanced accuracy.
<table><caption>Table 2: Accuracy, balanced accuracy, and verified individual fairness percentages leveraging different abstractions.</caption><thead><tr><th rowspan="2">Dataset</th><th rowspan="2">SVM Kernel</th><th rowspan="2">Acc.</th><th>Bal.</th><th colspan="3">Interval</th><th colspan="3">Interval+OH</th><th colspan="3">RAF</th><th colspan="3">RAF+OH</th></tr><tr><th>Acc.</th><th>N</th><th>C</th><th>NC</th><th>N</th><th>C</th><th>NC</th><th>N</th><th>C</th><th>NC</th><th>N</th><th>C</th><th>NC</th></tr></thead><tbody><tr><td rowspan="3">Adult</td><td>L(1)</td><td>84.6</td><td>75.6</td><td><strong>96.5</strong></td><td><strong>95.2</strong></td><td><strong>91.6</strong></td><td><strong>96.5</strong></td><td><strong>95.2</strong></td><td><strong>91.6</strong></td><td><strong>96.5</strong></td><td><strong>95.2</strong></td><td><strong>91.6</strong></td><td><strong>96.5</strong></td><td><strong>95.2</strong></td><td><strong>91.6</strong></td></tr><tr><td>R(0.05,0.01)</td><td>83.8</td><td>72.0</td><td>2.4</td><td>2.8</td><td>0.0</td><td>2.4</td><td>2.8</td><td>0.0</td><td>94.8</td><td>42.4</td><td>37.2</td><td><strong>97.5</strong></td><td><strong>97.9</strong></td><td><strong>95.4</strong></td></tr><tr><td>P(0.01,3,3)</td><td>83.9</td><td>76.7</td><td>0.0</td><td>0.0</td><td>0.0</td><td>0.0</td><td>0.0</td><td>0.0</td><td><strong>0.5</strong></td><td><strong>0.5</strong></td><td><strong>0.03</strong></td><td><strong>0.5</strong></td><td><strong>0.5</strong></td><td><strong>0.03</strong></td></tr><tr><td rowspan="3">Compas</td><td>L(1)</td><td>64.7</td><td>64.1</td><td><strong>95.5</strong></td><td><strong>99.5</strong></td><td><strong>94.9</strong></td><td><strong>95.5</strong></td><td><strong>99.5</strong></td><td><strong>94.9</strong></td><td><strong>95.5</strong></td><td><strong>99.5</strong></td><td><strong>94.9</strong></td><td><strong>95.5</strong></td><td><strong>99.5</strong></td><td><strong>94.9</strong></td></tr><tr><td>R(0.05,0.01)</td><td>64.5</td><td>63.1</td><td>54.3</td><td>42.5</td><td>1.0</td><td>54.3</td><td>42.5</td><td>1.0</td><td>91.8</td><td>71.6</td><td>66.9</td><td><strong>94.4</strong></td><td><strong>97.5</strong></td><td><strong>89.3</strong></td></tr><tr><td>P(0.01,3,3)</td><td>64.3</td><td>63.9</td><td>0.0</td><td>0.0</td><td>0.0</td><td>0.0</td><td>0.0</td><td>0.0</td><td><strong>0.5</strong></td><td><strong>0.6</strong></td><td><strong>0.1</strong></td><td><strong>0.5</strong></td><td><strong>0.6</strong></td><td><strong>0.1</strong></td></tr><tr><td rowspan="3">German</td><td>L(1)</td><td>79.0</td><td>70.8</td><td><strong>87.5</strong></td><td><strong>94.5</strong></td><td><strong>81.5</strong></td><td><strong>87.5</strong></td><td><strong>94.5</strong></td><td><strong>81.5</strong></td><td><strong>87.5</strong></td><td><strong>94.5</strong></td><td><strong>81.5</strong></td><td><strong>87.5</strong></td><td><strong>94.5</strong></td><td><strong>81.5</strong></td></tr><tr><td>R(10,0.05)</td><td>79.5</td><td>74.1</td><td>0.0</td><td>0.0</td><td>0.0</td><td>0.0</td><td>0.0</td><td>0.0</td><td><strong>2.0</strong></td><td>0.0</td><td>0.0</td><td><strong>2.0</strong></td><td><strong>82.0</strong></td><td>0.0</td></tr><tr><td>P(0.01,6,6)</td><td>75.5</td><td>71.8</td><td>0.0</td><td>0.0</td><td>0.0</td><td>0.0</td><td>0.0</td><td>0.0</td><td><strong>78.5</strong></td><td><strong>76.0</strong></td><td><strong>10.0</strong></td><td><strong>78.5</strong></td><td><strong>76.0</strong></td><td><strong>10.0</strong></td></tr></tbody></table>

**Data-Availability Statement.** Implementation, datasets, and scripts for reproducing the experimental results, are available on GitHub [33] and Zenodo with the identifier https://doi.org/10.5281/zenodo.10053395.

**Individual Fairness.** Table 2 shows accuracy, balanced accuracy, and verified individual fairness percentages fair$_{T,S}$ (SVM) on the test sets T and similarity relations S for linear SVMs (denoted in the table as L(regularization parameter C)), nonlinear SVMs with RBF kernels (denoted as R(regularization parameter C, γ)) and polynomial kernels (denoted as P(regularization parameter C, degree, basis)) trained on each dataset. Verified individual fairness percentages are computed w.r.t. the NOISE (columns ‘N’), CAT (columns ‘C’), and NOISE-CAT (columns ‘NC’) similarity relations. This table compares results obtained using intervals and RAFs, with and without the OH abstraction. In every row corresponding to a SVM instance, we present the highest verified individual fairness percentages for each similarity relation in bold font and the lowest percentages in a faded shade. It turns out that the RAF abstraction typically outperforms intervals, and adding our OH abstraction always yields equal or higher (even much higher) verified individual fairness. For the same SVMs, in the following table:

<table><thead><tr><th rowspan="2">Dataset</th><th colspan="2">Linear</th><th colspan="2">Polynomial</th><th colspan="2">RBF</th></tr><tr><th>LB</th><th>UB</th><th>LB</th><th>UB</th><th>LB</th><th>UB</th></tr></thead><tbody><tr><td>Adult</td><td>91.6</td><td>91.6</td><td>0.03</td><td>89.5</td><td>92.2</td><td>95.4</td></tr><tr><td>Compas</td><td>94.9</td><td>94.9</td><td>0.09</td><td>71.4</td><td>89.3</td><td>93.0</td></tr><tr><td>German</td><td>81.5</td><td>81.5</td><td>10.0</td><td>76.0</td><td>0.0</td><td>84.0</td></tr></tbody></table>

we provide lower and upper bounds on individual fairness w.r.t. the NOISE-CAT similarity relation using the RAF+OH abstraction. The lower bound (columns ‘LB’) is the verified individual fairness percentage as given in Table 2, while the upper bound (columns ‘UB’) is an estimate obtained through the counterexample search of Definition 3.12 without input partitioning, e.g., an upper bound of 76% for German/Polynomial means that we found concrete counterexamples to individual fairness for 48 over 200 test samples, thus entailing that at most 152 out of 200 test samples (i.e., 76%) are individually fair. The
<table><caption>Table 3: Comparison of AFI and PFI on German.</caption><thead><tr><th rowspan="2"></th><th rowspan="2"></th><th colspan="8">Grade for each feature</th><th rowspan="2">Distance</th></tr><tr><th>5</th><th>5</th><th>5</th><th>6</th><th>6</th><th>7</th><th>7</th><th>7</th><th>8</th></tr></thead><tbody><tr><td rowspan="3">Linear</td><td>Baseline (13.55s)</td><td>5</td><td>5</td><td>5</td><td>6</td><td>6</td><td>7</td><td>8</td><td>7</td><td>7</td><td>8</td><td>1.0</td></tr><tr><td>AFI (0.01s)</td><td>5</td><td>5</td><td>5</td><td>6</td><td>6</td><td>7</td><td>8</td><td>7</td><td>7</td><td>8</td><td>3.16</td></tr><tr><td>PFI (4.07s)</td><td>5</td><td>5</td><td>6</td><td>7</td><td>7</td><td>9</td><td>6</td><td>6</td><td>7</td><td>7</td><td></td></tr><tr><td rowspan="3">RBF</td><td>Baseline (17.98s)</td><td>5</td><td>5</td><td>5</td><td>6</td><td>6</td><td>7</td><td>7</td><td>7</td><td>8</td><td>8</td><td>Distance</td></tr><tr><td>AFI (0.02s)</td><td>5</td><td>6</td><td>5</td><td>6</td><td>6</td><td>8</td><td>7</td><td>7</td><td>8</td><td>7</td><td>1.73</td></tr><tr><td>PFI (6.23s)</td><td>6</td><td>7</td><td>5</td><td>6</td><td>7</td><td>8</td><td>7</td><td>6</td><td>7</td><td>5</td><td>4.24</td></tr><tr><td rowspan="3">Polynomial</td><td>Baseline (15.83s)</td><td>5</td><td>5</td><td>5</td><td>6</td><td>7</td><td>7</td><td>7</td><td>7</td><td>8</td><td>Distance</td></tr><tr><td>AFI (0.01s)</td><td>7</td><td>6</td><td>7</td><td>7</td><td>5</td><td>7</td><td>6</td><td>6</td><td>5</td><td>8</td><td>4.47</td></tr><tr><td>PFI (4.15s)</td><td>6</td><td>7</td><td>9</td><td>7</td><td>6</td><td>7</td><td>5</td><td>6</td><td>6</td><td>6</td><td>5.74</td></tr></tbody></table>

<table><caption>Table 4: Distances of AFI and PFI from several baselines for different SVMs.</caption><thead><tr><th></th><th>Baseline</th><th>N = 2k<br>ε = 0.2</th><th>N = 10k<br>ε = 0.2</th><th>N = 2k<br>ε = 0.4</th><th>N = 10k<br>ε = 0.4</th><th>N = 2k<br>ε = 0.6</th><th>N = 5k<br>ε = 0.6</th><th>N = 10k<br>ε = 0.6</th><th>N = 2k<br>ε = 0.8</th><th>N = 5k<br>ε = 0.8</th><th>N = 10k<br>ε = 0.8</th></tr></thead><tbody><tr><td>Adult</td><td>AFI (0.27s)</td><td><strong>0.0</strong></td><td><strong>0.0</strong></td><td><strong>1.0</strong></td><td><strong>0.0</strong></td><td><strong>1.0</strong></td><td><strong>1.41</strong></td><td><strong>1.0</strong></td><td><strong>1.0</strong></td><td><strong>1.41</strong></td><td><strong>1.0</strong></td></tr><tr><td>Linear</td><td>PFI (10009s)</td><td>2.45</td><td>2.45</td><td>2.24</td><td>2.45</td><td>2.24</td><td>2.45</td><td>2.24</td><td>2.24</td><td>2.45</td><td>2.24</td></tr><tr><td>Adult</td><td>AFI (0.48s)</td><td><strong>1.0</strong></td><td><strong>1.41</strong></td><td><strong>1.41</strong></td><td><strong>1.41</strong></td><td><strong>1.73</strong></td><td><strong>1.73</strong></td><td><strong>1.41</strong></td><td><strong>1.41</strong></td><td><strong>1.41</strong></td><td><strong>1.41</strong></td></tr><tr><td>RBF</td><td>PFI (25221s)</td><td>1.73</td><td>2.45</td><td>2.45</td><td>2.0</td><td>2.65</td><td>2.65</td><td>2.45</td><td>2.45</td><td>2.45</td><td>2.45</td></tr><tr><td>Adult</td><td>AFI (0.44s)</td><td><strong>1.0</strong></td><td><strong>1.0</strong></td><td><strong>0.0</strong></td><td><strong>1.41</strong></td><td><strong>0.0</strong></td><td><strong>0.0</strong></td><td><strong>0.0</strong></td><td><strong>0.0</strong></td><td><strong>0.0</strong></td><td><strong>0.0</strong></td></tr><tr><td>Polynomial</td><td>PFI (9985s)</td><td><strong>1.0</strong></td><td><strong>1.0</strong></td><td><strong>1.41</strong></td><td><strong>1.0</strong></td><td><strong>1.41</strong></td><td><strong>1.41</strong></td><td><strong>1.41</strong></td><td><strong>1.41</strong></td><td><strong>1.41</strong></td><td><strong>1.41</strong></td></tr><tr><td>Compas</td><td>AFI (0.22s)</td><td><strong>1.41</strong></td><td><strong>1.41</strong></td><td><strong>1.73</strong></td><td><strong>1.73</strong></td><td><strong>1.41</strong></td><td><strong>1.73</strong></td><td><strong>1.41</strong></td><td><strong>1.41</strong></td><td><strong>1.41</strong></td><td><strong>1.73</strong></td></tr><tr><td>Linear</td><td>PFI (1953s)</td><td>1.73</td><td>1.73</td><td>2.0</td><td>2.0</td><td>2.24</td><td>2.0</td><td>2.24</td><td>2.24</td><td>2.24</td><td>2.83</td></tr><tr><td>Compas</td><td>AFI (0.27s)</td><td><strong>2.0</strong></td><td><strong>2.0</strong></td><td><strong>2.65</strong></td><td><strong>2.65</strong></td><td><strong>2.83</strong></td><td><strong>2.83</strong></td><td><strong>2.83</strong></td><td><strong>2.83</strong></td><td><strong>2.83</strong></td><td><strong>2.83</strong></td></tr><tr><td>RBF</td><td>PFI (6827s)</td><td><strong>2.0</strong></td><td><strong>2.0</strong></td><td><strong>2.65</strong></td><td><strong>2.65</strong></td><td><strong>2.83</strong></td><td><strong>2.83</strong></td><td><strong>2.83</strong></td><td><strong>2.83</strong></td><td><strong>2.83</strong></td><td><strong>2.83</strong></td></tr><tr><td>Compas</td><td>AFI (0.22s)</td><td>4.24</td><td>4.24</td><td>4.12</td><td>4.12</td><td>4.24</td><td>4.24</td><td>4.24</td><td>4.24</td><td>4.24</td><td>4.24</td></tr><tr><td>Polynomial</td><td>PFI (2069s)</td><td><strong>2.45</strong></td><td><strong>2.45</strong></td><td><strong>3.0</strong></td><td><strong>3.0</strong></td><td><strong>3.74</strong></td><td><strong>3.74</strong></td><td><strong>3.74</strong></td><td><strong>3.74</strong></td><td><strong>3.74</strong></td><td><strong>3.74</strong></td></tr><tr><td>German</td><td>AFI (0.01s)</td><td><strong>1.0</strong></td><td><strong>1.0</strong></td><td><strong>1.0</strong></td><td><strong>1.0</strong></td><td><strong>1.0</strong></td><td><strong>1.0</strong></td><td><strong>1.0</strong></td><td><strong>1.41</strong></td><td><strong>1.73</strong></td><td><strong>1.41</strong></td></tr><tr><td>Linear</td><td>PFI (4.07s)</td><td>3.16</td><td>3.46</td><td>3.16</td><td>3.16</td><td>3.16</td><td>3.16</td><td>3.16</td><td>3.6</td><td>3.74</td><td>3.0</td></tr><tr><td>German</td><td>AFI (0.02s)</td><td><strong>1.73</strong></td><td><strong>1.0</strong></td><td><strong>1.73</strong></td><td><strong>1.73</strong></td><td><strong>2.0</strong></td><td><strong>1.41</strong></td><td><strong>1.73</strong></td><td><strong>1.73</strong></td><td><strong>2.0</strong></td><td><strong>2.24</strong></td></tr><tr><td>RBF</td><td>PFI (6.23s)</td><td>4.0</td><td>3.46</td><td>4.24</td><td>4.24</td><td>4.36</td><td>3.61</td><td>4.24</td><td>4.24</td><td>4.36</td><td>4.47</td></tr><tr><td>German</td><td>AFI (0.01s)</td><td><strong>4.90</strong></td><td><strong>4.12</strong></td><td><strong>4.47</strong></td><td><strong>3.87</strong></td><td><strong>3.87</strong></td><td><strong>4.24</strong></td><td><strong>3.46</strong></td><td><strong>3.46</strong></td><td><strong>3.46</strong></td><td><strong>3.46</strong></td></tr><tr><td>Polynomial</td><td>PFI (4.15s)</td><td>5.74</td><td>5.10</td><td>5.74</td><td>4.69</td><td>4.69</td><td>5.0</td><td>4.58</td><td>4.58</td><td>4.58</td><td>4.58</td></tr></tbody></table>

gap between these bounds is zero for linear SVMs and narrow for RBF kernels trained on the Adult and Compas datasets: in these cases, our RAF+OH abstraction turns out to be (very) precise and the counterexample search heuristics is strong. On the other hand, the gap is much wider in the remaining cases, notably for SVMs with polynomial kernels, mostly due to a lower precision of the abstraction. Using partitioning (i.e., step (S₄) of Definition 3.12) up to 3.125% of the original perturbation size, we get similar upper bounds, thus hinting the presence of a few additional counterexamples. Only partitioning up to 0.1% of the original input size, we could find substantially more counterexamples.

**Global Feature Importance.** We compare our abstract feature importance AFI, used as a global feature importance measure, with the popular global measure PFI, as implemented in the Python `sklearn.inspection` package with `nrepeat = 10`. For the sake of comparison with an outside baseline, we uniformly sampled *N* points in the input space of the SVMs and determined how often a NOISE perturbation for a single numerical input feature changed the SVM classification: the more often the classification changed, the more
<table><caption>Table 5: Local Comparison of AFI and LIME.</caption><thead><tr><th rowspan="2">Distance between<br>LIME and ...</th><th colspan="3">Adult</th><th colspan="3">Compas</th><th colspan="3">German</th></tr><tr><th>Lin.</th><th>RBF</th><th>Poly</th><th>Lin.</th><th>RBF</th><th>Poly</th><th>Lin.</th><th>RBF</th><th>Poly</th></tr></thead><tbody><tr><td>AFI (ε = 0.1)</td><td>2.42</td><td>2.04</td><td>2.98</td><td>1.67</td><td>1.06</td><td>3.05</td><td>2.62</td><td>2.03</td><td><strong>5.31</strong></td></tr><tr><td>AFI (ε = 0.2)</td><td>1.68</td><td>1.32</td><td>2.67</td><td>1.63</td><td>0.17</td><td>2.73</td><td>2.21</td><td>2.00</td><td>5.41</td></tr><tr><td>AFI (ε = 0.3)</td><td>1.39</td><td>0.51</td><td>2.58</td><td><strong>1.57</strong></td><td>0.14</td><td><strong>2.62</strong></td><td>1.92</td><td>2.05</td><td>5.45</td></tr><tr><td>AFI (Global)</td><td><strong>1.37</strong></td><td><strong>0.01</strong></td><td><strong>1.01</strong></td><td><strong>1.57</strong></td><td><strong>0.13</strong></td><td>3.16</td><td><strong>1.90</strong></td><td><strong>1.89</strong></td><td>5.53</td></tr></tbody></table>

<table><caption>Table 6: Time Comparison (in sec) of AFI, PFI, LIME.</caption><thead><tr><th rowspan="2">Dataset</th><th colspan="3">Linear</th><th colspan="3">Polynomial</th><th colspan="3">RBF</th></tr><tr><th>AFI</th><th>PFI</th><th>LIME</th><th>AFI</th><th>PFI</th><th>LIME</th><th>AFI</th><th>PFI</th><th>LIME</th></tr></thead><tbody><tr><td>Adult</td><td><strong>0.27</strong></td><td>1·10<sup>4</sup></td><td>3.78</td><td><strong>0.45</strong></td><td>1·10<sup>4</sup></td><td>6.21</td><td><strong>0.48</strong></td><td>2·10<sup>4</sup></td><td>9.82</td></tr><tr><td>Compas</td><td><strong>0.22</strong></td><td>2·10<sup>3</sup></td><td>2.72</td><td><strong>0.22</strong></td><td>2·10<sup>3</sup></td><td>2.89</td><td><strong>0.27</strong></td><td>6·10<sup>3</sup></td><td>8.97</td></tr><tr><td>German</td><td><strong>0.01</strong></td><td>4.07</td><td>0.198</td><td><strong>0.01</strong></td><td>4.15</td><td>0.355</td><td><strong>0.02</strong></td><td>6.23</td><td>0.223</td></tr></tbody></table>

important is the input feature. As a representative example, we show in Table 3, a comparison for the SVMs trained on the German dataset. In lines ‘Baseline’, ‘AFI’ and ‘PFI’, we show the feature grades, as defined in Section 3.1, of the 10 non-categorical (7 numerical plus 3 binary) input features of German based on the importance scores measured by, respectively, baseline, AFI and PFI. The baseline has been computed by considering $N = 10000$ samples and a NOISE perturbation with magnitude $ε = 0.4$. We also indicate in parenthesis the time needed (in seconds) to compute these scores, where for our AFI measure, we used the RAF+OH abstraction. In column ‘Distance’ we show the Euclidean distance between the feature grades computed by AFI and PFI w.r.t. the baseline. We can observe that AFI better correlates with model variance to feature perturbations than PFI. In fact, the correlation is almost perfect for the linear SVM. For nonlinear SVMs, the abstraction RAF+OH loses more precision, so that the correlation decreases, nevertheless the distance to the baseline is still smaller than for PFI. Note that AFI is computed in a negligible fraction of time w.r.t. PFI.

Table 4 compares the Euclidean distance between the feature grades computed by AFI and PFI w.r.t. different choices of the number of samples $N$ and magnitudes $ε$ used for computing the baseline of SVMs trained on the Adult, Compas, and German datasets. For each AFI-baseline and PFI-baseline pair, the smaller distance is made bold and the larger has a faded shade. The data indicates AFI is closer to the baseline than PFI in most cases, except for the polynomial SVM trained on Compas: for this case, the likely reason is the low precision of our polynomial SVM abstraction, as also hinted by the low verified individual fairness scores in the entries for Compas/Polynomial/RAF+OH in Table 2.

**Local Feature Importance.** In Table 5, we present a comparative analysis between our measure AFI, used as a *local* feature importance measure, and the extensively used local feature importance measure LIME as implemented in the Python `lime.lime_tabular` package [39], for SVMs trained on the three different datasets. The local neighborhood
used by LIME to determine the importance of features is obtained using a normal
distribution, and the influence of a point in the neighborhood is dependent on its dis-
tance from the original point [38, Section 3.3]. Instead, AFI considers a local uniform
distribution for the local neighborhood, i.e., a hyperrectangle abstraction where each
point is equiprobable. Thus, it is not possible to find a common local neighborhood in
which we can compare local AFI and LIME to a ground truth baseline. Instead, the
comparison in Table 5 is based on computing the average Euclidean distance between
the feature grades obtained with these two metrics for 200 inputs sampled from the test
sets. For our local AFI measure, we took as input to the SVMs a local neighborhood
determined by a NOISE perturbation with three different values of the magnitude $\epsilon$.
We also compared the distance of LIME with the global AFI computed over the entire
input space of the SVMs. The results show that these distances are consistently minimal
(except for the polynomial SVMs), implying a high degree of similarity between the two
feature importance measures. Interestingly, this table shows that the local LIME feature
grades are closer to the global AFI feature grades than to the local AFI feature grades.
Furthermore, as the value of the magnitude $\epsilon$ used to compute local AFI increases, the
distance between LIME and local AFI feature grades decreases.

***Computation Time.*** Finally, Table 6 presents a comparison of the computation times (in seconds) of AFI, PFI, and LIME for our SVMs. As time taken by global and local AFI is similar, we only report global AFI time. The results shows that AFI always outperforms both PFI and LIME.

5 Conclusion

We put forward a novel feature importance measure based on an abstract interpretation of SVMs, which is tailored for achieving a precise symbolic representation of one-hot encoded features. We showed that our abstraction is effective for certifying robustness properties—notably, individual fairness—of SVMs, and that our abstract feature importance measure outperforms the state-of-the-art. As future work, we plan to extend our approach to certify alternative or stronger fairness notions. We also aim to design quantitative verification methods to provide probabilistic guarantees on the behavior of SVM models.

**Acknowledgements.** Francesco Ranzato and Marco Zanella were partially funded by the *Italian MIUR*, under the PRIN 2017 project no. 201784YSZ5. Francesco Ranzato was partially funded by: the *Italian MUR*, under the PRIN 2022 PNRR project no. P2022HXNSC; *Meta* (formerly *Facebook*) *Research*, under a “Probability and Programming Research Award” and under a *WhatsApp Research Award* on “Privacy-aware Program Analysis”; by an *Amazon Research Award* for “AWS Automated Reasoning”. Caterina Urban was partially funded by the French PEPR Intelligence Artificielle SAIF project (ANR-23-PEIA-0006).
References

1. Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools (2nd Edition). Addison-Wesley Longman Publishing Co., Inc., USA (2006)

2. Albarghouthi, A.: Introduction to neural network verification. Found. Trends Program. Lang. 7(1-2), 1–157 (2021). https://doi.org/10.1561/2500000051

3. Angwin, J., Larson, J., Mattu, S., Kirchner, L.: Machine Bias. ProPublica 23 (2016), https://wwwpropublicaorg/article/machine-bias-risk-assessments-in-criminal-sentencing

4. Apley, D.W., Zhu, J.: Visualizing the Effects of Predictor Variables in Black Box Supervised Learning Models. Journal of the Royal Statistical Society Series B: Statistical Methodology 82(4), 1059–1086 (2020), https://doi.org/10.1111/rssb.12377

5. Bhatt, U., Xiang, A., Sharma, S., Weller, A., Taly, A., Jia, Y., Ghosh, J., Puri, R., Moura, J.M.F., Eckersley, P.: Explainable machine learning in deployment. In: Proc. 2020 Conference on Fairness, Accountability, and Transparency, FAT* ’20. pp. 648–657. ACM (2020). https://doi.org/10.1145/3351095.3375624

6. Breiman, L.: Random Forests. Machine Learning 45(1), 5–32 (2001). https://doi.org/10.1023/A:1010933404324

7. Carlini, N., Wagner, D.A.: Towards Evaluating the Robustness of Neural Networks. In: Proc. of 38th IEEE Symposium on Security and Privacy (S & P 2017). pp. 39–57 (2017). https://doi.org/10.1109/SP.2017.49

8. Casalicchio, G., Molnar, C., Bischl, B.: Visualizing the feature importance for black box models. In: Machine Learning and Knowledge Discovery in Databases - Proceedings of the European Conference, ECML PKDD 2018. Lecture Notes in Computer Science, vol. 11051, pp. 655–670. Springer (2018). https://doi.org/10.1007/978-3-030-10925-7_40

9. Cervantes, J., Garcia-Lamont, F., Rodríguez-Mazahua, L., Lopez, A.: A comprehensive survey on support vector machine classification: Applications, challenges and trends. Neurocomputing 408, 189–215 (2020), https://doi.org/10.1016/j.neucom.2019.10.118

10. Chang, Y.W., Lin, C.J.: Feature ranking using linear SVM. In: Proceedings of the Workshop on the Causation and Prediction Challenge at WCCI 2008. Proceedings of Machine Learning Research, vol. 3, pp. 53–64. PMLR (2008), http://proceedings.mlr.press/v3/chang08a.html

11. Chouldechova, A.: Fair Prediction with Disparate Impact: A Study of Bias in Recidivism Prediction Instruments. Big Data 5(2), 153–163 (2017). https://doi.org/10.1089/big.2016.0047

12. Cousot, P.: Principles of Abstract Interpretation. MIT Press (2021)

13. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th ACM Symposium on Principles of Programming Languages (POPL 1977). pp. 238–252 (1977). https://doi.org/10.1145/512950.512973

14. Cristianini, N., Shawe-Taylor, J.: An Introduction to Support Vector Machines and Other Kernel-based Learning Methods. Cambridge University Press (2000). https://doi.org/10.1017/CBO9780511801389

15. Dua, D., Graff, C.: UCI Machine Learning repository (2017), https://archive.ics.uci.edu/ml

16. Dwork, C., Hardt, M., Pitassi, T., Reingold, O., Zemel, R.S.: Fairness through awareness. In: Innovations in Theoretical Computer Science 2012. pp. 214–226. ACM (2012), https://doi.org/10.1145/2090236.2090255

17. Fish, B., Kun, J., Lelkes, Á.D.: A confidence-based approach for balancing fairness and accuracy. In: Proceedings of the 2016 SIAM international conference on data mining. pp. 144–152. SIAM (2016), https://doi.org/10.1137/1.9781611974348.17

18. Fisher, A., Rudin, C., Dominici, F.: All Models are Wrong, but Many are Useful: Learning a Variable’s Importance by Studying an Entire Class of Prediction Models Simultaneously. Journal of Machine Learning Research 20(177), 1–81 (2019), http://jmlr.org/papers/v20/18-760.html
19. Friedman, J.H.: Greedy function approximation: A gradient boosting machine. The Annals of Statistics 29(5), 1189–1232 (2001), http://www.jstor.org/stable/2699986

20. Ghorbal, K., Goubault, E., Putot, S.: The zonotope abstract domain Taylor1+. In: Computer Aided Verification, 21st International Conference, CAV 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643, pp. 627–633. Springer (2009), https://doi.org/10.1007/978-3-642-02658-4_47

21. Ghosh, B., Basu, D., Meel, K.S.: Algorithmic fairness verification with graphical models. In: Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022. pp. 9539–9548 (2022), https://doi.org/10.1609/aaai.v36i9.21187

22. Goldstein, A., Kapelner, A., Bleich, J., Pitkin, E.: Peeking Inside the Black Box: Visualizing Statistical Learning With Plots of Individual Conditional Expectation. Journal of Computational and Graphical Statistics 24(1), 44–65 (2015), https://doi.org/10.1080/10618600.2014.907095

23. Goodfellow, I., McDaniel, P., Papernot, N.: Making Machine Learning Robust Against Adversarial Inputs. Commun. ACM 61(7), 56–66 (2018). https://doi.org/10.1145/3134599

24. Hechtlinger, Y.: Interpretation of Prediction Models Using the Input Gradient. CoRR arXiv (2016), http://arxiv.org/abs/1611.07634

25. Hooker, G., Mentch, L., Zhou, S.: Unrestricted permutation forces extrapolation: Variable importance requires at least one more model, or there is no free variable importance. Statistics and Computing 31(6) (2021), https://doi.org/10.1007/s11222-021-10057-z

26. Khandani, A.E., Kim, A.J., Lo, A.W.: Consumer Credit-Risk Models via Machine-Learning Algorithms. Journal of Banking & Finance 34(11), 2767–2787 (2010). https://doi.org/https://doi.org/10.1016/j.jbankfin.2010.06.001

27. Langenberg, P., Balda, E.R., Behboodi, A., Mathar, R.: On the robustness of support vector machines against adversarial examples. In: 13th International Conference on Signal Processing and Communication Systems, ICSPCS 2019. pp. 1–6. IEEE (2019). https://doi.org/10.1109/ICSPCS47537.2019.9008746

28. Liu, C., Arnon, T., Lazarus, C., Strong, C.A., Barrett, C.W., Kochenderfer, M.J.: Algorithms for verifying deep neural networks. Found. Trends Optim. 4(3-4), 244–404 (2021), https://doi.org/10.1561/2400000035

29. Lundberg, S.M., Lee, S.: A unified approach to interpreting model predictions. In: Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017. pp. 4765–4774 (2017), https://proceedings.neurips.cc/paper/2017/hash/8a20a8621978632d76c4328b67767-Abstract.html

30. Mehrabi, N., Morstatter, F., Saxena, N., Lerman, K., Galstyan, A.: A survey on bias and fairness in machine learning. ACM Comput. Surv. 54(6) (Jul 2021). https://doi.org/10.1145/3457607

31. Messine, F.: Extentions of affine arithmetic: Application to unconstrained global optimization. J. Universal Computer Science 8(11), 992–1015 (2002). https://doi.org/10.3217/jucs-008-11-0992

32. Mladenic, D., Brank, J., Grobelnik, M., Milic-Frayling, N.: Feature selection using linear classifier weights: interaction with classification models. In: SIGIR 2004: Proceedings of the 27th Annual International ACM SIGIR Conference on Research and Development in Information Retrieval. pp. 234–241. ACM (2004). https://doi.org/10.1145/1008992.1009034

33. Pal, A., Ranzato, F., Urban, C., Zanella, M.: Abstract Feature Importance for SVMs. https://github.com/AFI-SVM (2023)

34. Park, S., Byun, J., Lee, J.: Privacy-preserving fair learning of support vector machine with homomorphic encryption. In: WWW ’22: The ACM Web Conference 2022. pp. 3572–3583. ACM (2022). https://doi.org/10.1145/3485447.3512252
35. Ranzato, F., Urban, C., Zanella, M.: Fairness-aware training of decision trees by abstract interpretation. In: Proceedings of the 30th ACM International Conference on Information & Knowledge Management, CIKM2021. pp. 1508–1517 (2021), https://doi.org/10.1145/3459637.3482342

36. Ranzato, F., Zanella, M.: Robustness Verification of Support Vector Machines. In: Proc. 26th International Static Analysis Symposium (SAS 2019). pp. 271–295. LNCS vol. 11822 (2019). https://doi.org/10.1007/978-3-030-32304-2_14

37. Ranzato, F., Zanella, M.: Saver: SVM Abstract Verifier (2019), https://github.com/abstract-machine-learning/saver

38. Ribeiro, M.T., Singh, S., Guestrin, C.: "Why should I trust you?": Explaining the predictions of any classifier. In: Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, 2016. pp. 1135–1144. ACM (2016). https://doi.org/10.1145/2939672.2939778

39. Ribeiro, M.T.C.: Local Interpretable Model-agnostic Explanations (LIME) (2016), https://lime-ml.readthedocs.io

40. Roh, Y., Lee, K., Whang, S., Suh, C.: Fr-train: A mutual information-based approach to fair and robust training. In: Proc. of the 37th Int. Conf. on Machine Learning (ICML 2020). Proceedings of Machine Learning Research, vol. 119, pp. 8147–8157. PMLR (2020), http://proceedings.mlr.press/v119/roh20a.html

41. Ruoss, A., Balunovic, M., Fischer, M., Vechev, M.T.: Learning certified individually fair representations. In: Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems (NeurIPS 2020) (2020), https://proceedings.neurips.cc/paper/2020/hash/55d491cf951b1b920900684d71419282-Abstract.html

42. Shapley, L.S.: A Value for n-Person Games. In: Kuhn, H.W., Tucker, A.W. (eds.) Contributions to the Theory of Games II, pp. 307–317. Princeton University Press, Princeton (1953)

43. Tjoa, E., Guan, C.: A survey on explainable artificial intelligence (XAI): Toward medical XAI. IEEE Trans. Neural Networks Learn. Syst. 32(11), 4793–4813 (2021), https://doi.org/10.1109/TNNLS.2020.3027314

44. Urban, C., Christakis, M., Wüstholz, V., Zhang, F.: Perfectly parallel fairness certification of neural networks. Proc. ACM Program. Lang. 4(OOPSLA), 185:1–185:30 (2020). https://doi.org/10.1145/3428253

45. Urban, C., Miné, A.: A Review of Formal Methods applied to Machine Learning. CoRR arXiv (2021), https://arxiv.org/abs/2104.02466

46. Verma, S., Rubin, J.: Fairness definitions explained. In: Proceedings of the International Workshop on Software Fairness, FairWare@ICSE 2018. pp. 1–7. ACM (2018). https://doi.org/10.1145/3194770.3194776

47. Xiao, H., Biggio, B., Nelson, B., Xiao, H., Eckert, C., Roli, F.: Support vector machines under adversarial label contamination. Neurocomputing 160, 53–62 (2015). https://doi.org/10.1016/j.neucom.2014.08.081

48. Yurochkin, M., Bower, A., Sun, Y.: Training individually fair ML models with sensitive subspace robustness. In: Proc. 8th International Conference on Learning Representations, ICLR 2020 (2020), https://openreview.net/forum?id=B1gdkxHFDH