Michele Diego
email: michele.diego@univ-lyon1.fr

Marco Gandolfi

Stefano Giordano

Fabien Vialla

Aurélien Crut

Fabrice Vallée

Paolo Maioli

Natalia Del Fatti

Francesco Banfi

Tuning photoacoustics with nanotransducers via thermal boundary resistance and laser pulse duration

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

The photoacoustic effect in liquids, generated by metal nanoparticles excited with short laser pulses, offers high contrast imaging and promising medical treatment techniques. Understanding the role of the thermal boundary resistance (TBR) and the laser pulse duration in the generation mechanism of acoustic waves is essential to implement efficient photoacoustic nanotransducers. This work theoretically investigates, for the paradigmatic case of water-immersed gold nanocylinders, the role of the TBR and of laser pulse duration in the competition between the launching mechanisms: the thermophone and the mechanophone. In the thermophone, the nanoparticle acts as a nanoheater and the wave is launched by water thermal expansion. In the mechanophone, the nanoparticle directly acts as a nanopiston. Specifically, for a gold-water interface, the thermophone prevails under ns light pulse irradiation, while the mechanophone dominates shortening the pulse to the 10 ps regime. For a graphene-functionalized gold-water interface, instead, the mechanophone dominates over the entire range of explored laser pulse durations. Results point to high-TBR, liquidimmersed nanoparticles as potentially efficient photoacoustic nanogenerators, with the advantage of keeping the liquid environment temperature unaltered.

Nanoscale photoacoustics generation in liquids, owing to its potential in nanoimaging and therapeutic applications, is a flourishing topic at the cross-road of condensed matter physics, nanomedicine and material science [START_REF] Emelianov | Photoacoustics for molecular imaging and therapy[END_REF][START_REF] Li | Photoacoustic tomography and sensing in biomedicine[END_REF][START_REF] Xu | Photoacoustic imaging in biomedicine[END_REF][START_REF] Wang | Photoacoustic imaging and spectroscopy[END_REF][START_REF] Li | Gold nanoparticles for photoacoustic imaging[END_REF] . In this context, liquid-immersed metal nanoparticles have proven to be efficient photoacoustic generators due to their tunable optical absorption properties [START_REF] Yang | Nanoparticles for photoacoustic imaging[END_REF][START_REF] Mantri | Engineering plasmonic nanoparticles for enhanced photoacoustic imaging[END_REF][START_REF] El-Brolossy | Shape and size dependence of the surface plasmon resonance of gold nanoparticles studied by photoacoustic technique[END_REF][START_REF] Garcia-Alvarez | Optimizing the geometry of photoacoustically active gold nanoparticles for biomedical imaging[END_REF] , high contrast imaging features [START_REF] Luke | Biomedical applications of photoacoustic imaging with exogenous contrast agents[END_REF][START_REF] Pan | Molecular photoacoustic imaging of angiogenesis with integrin-targeted gold nanobeacons[END_REF] and biocompatibility [START_REF] Shukla | Biocompatibility of gold nanoparticles and their endocytotic fate inside the cellular compartment: a microscopic overview[END_REF][START_REF] Craciun | Surface plasmon resonance or biocompatibility-key properties for determining the applicability of noble metal nanoparticles[END_REF] . Great efforts have been devoted to optimise the parameters allowing a more efficient photoacoustic conversion, such as size, geometry [START_REF] Garcia-Alvarez | Optimizing the geometry of photoacoustically active gold nanoparticles for biomedical imaging[END_REF][START_REF] Verawaty | Simulating photoacoustic waves from individual nanoparticle of various shapes using k-wave[END_REF][START_REF] Guiraud | Thermoacoustic wave generation in multilayered thermophones with cylindrical and spherical geometries[END_REF][START_REF] Ronchi | Discrimination of nano-objects via cluster analysis techniques applied to time-resolved thermo-acoustic microscopy[END_REF] and transducer materials [START_REF] Lee | Efficient photoacoustic conversion in optical nanomaterials and composites[END_REF] . Yet, despite its relevance for applications, the combined effects of the pulse temporal width, τ L , [START_REF] Gandolfi | Optical wavelength dependence of photoacoustic signal of gold nanofluid[END_REF][START_REF] Prost | Photoacoustic generation by a gold nanosphere: From linear to nonlinear thermoelastics in the long-pulse illumination regime[END_REF][START_REF] Diego | Ultrafast nano generation of acoustic waves in water via a single carbon nanotube[END_REF] and the thermal boundary resistance [START_REF] Chen | Silica-coated gold nanorods as photoacoustic signal nanoamplifiers[END_REF][START_REF] Repenko | Strong photoacoustic signal enhancement by coating gold nanoparticles with melanin for biomedical imaging[END_REF][START_REF] Cavigli | Impact of kapitza resistance on the stability and efficiency of photoacoustic conversion from gold nanorods[END_REF] (TBR) tunabilities remain relatively unexplored and lack a thorough rationalization.

In brief, the photoacoustic effect of an individual liquidimmersed metal nanoparticle consists of three steps: (i) absorption of the laser pulse by the nanoparticle and its temperature rise, (ii) thermal interaction between the nanoparticle and the liquid environment and (iii) generation of the acoustic wave in liquid. The acoustic wave in liquid is triggered by two launching mechanisms: the mechanophone and the thermophone effects. The former is due to the thermal expansion of the metal nanoparticle, the latter mechanism to that of the liquid environment with the nanoparticle acting as a nanoheater. The photoacoustic generation in these systems is typically investigated under ns laser pulses irradiation, in which case the mechanophone contribution is, in most instances, disregarded [START_REF] Gandolfi | Optical wavelength dependence of photoacoustic signal of gold nanofluid[END_REF][START_REF] Chen | Environmentdependent generation of photoacoustic waves from plasmonic nanoparticles[END_REF][START_REF] Shahbazi | Photoacoustics of core-shell nanospheres using comprehensive modeling and analytical solution approach[END_REF][START_REF] Guiraud | Multilayer modeling of thermoacoustic sound generation for thermophone analysis and design[END_REF][START_REF] Guiraud | Two temperature model for thermoacoustic sound generation in thick porous thermophones[END_REF] . Nevertheless, the mechanophone effect cannot be neglected in general, as recently demonstrated for the case of carbon nanotubes immersed in water [START_REF] Diego | Ultrafast nano generation of acoustic waves in water via a single carbon nanotube[END_REF] . Once the size and composition of the nanoparticles and of the surrounding liquid are fixed by the specific application constraints, the relative contributions of the thermophone vs Left axis: pressure time evolution in water at r = R gnc + 5 nm for τ L = 1 ns, R = 1 × 10 -7 m 2 K/W. The curves are normalized to the total pressure maximum. Right axis: I(t) (red dashed curve). This is the author's peer reviewed, accepted manuscript. However, the online version of record will be different from this version once it has been copyedited and typeset. Right axis: I(t) (red dashed line) maximized at the time t 0 . δ T gnc : difference between the GNC peak temperatures between the cases of τ T BR /τ L ∼ 100 and 0.01. Panel (c): normalized mechanical energy generated in water by the thermophone and the mechanophone effects for different τ T BR /τ L (bottom axis) and the corresponding TBRs (top axis). The ratios τ T BR /τ L are rounded to the first significant figure. Values for Au/water and graphene-functionalized Au/water interface are identified by the two round sketches.

PLEASE CITE THIS ARTICLE AS

mechanophone effects may be tuned upon varying the TBR at the nanoparticle/liquid interface (interface engineering) and τ L , their interplay making the focus of the present work. We theoretically investigate the role of the thermophone and mechanophone effects in acoustic wave generation for the paradigmatic case of a water-immersed gold nanocylinder (GNC) of radius R gnc =10 nm and of high aspect ratio, because of their relevance in bio-medical applications [START_REF] He | Application of gold nanoparticles in photoacoustic imaging[END_REF][START_REF] Manohar | Gold nanorods as molecular contrast agents in photoacoustic imaging: the promises and the caveats[END_REF][START_REF] Cavigli | Size affects the stability of the photoacoustic conversion of gold nanorods[END_REF][START_REF] Cavigli | Photostability of gold nanorods upon endosomal confinement in cultured cells[END_REF][START_REF] Chen | Miniature gold nanorods for photoacoustic molecular imaging in the second nearinfrared optical window[END_REF][START_REF] Dhada | Gold nanorods as photoacoustic nanoprobes to detect proinflammatory macrophages and inflammation[END_REF][START_REF] Knights | Optimising gold nanorods for photoacoustic imaging in vitro[END_REF] . Formally, the GNC is assumed infinitely extended along its axis, the problem thus being radially symmetric with r the radial coordinate. The model, detailed in SI, comprises three steps: optics, thermics and mechanics. As for the optics, the system, at equilibrium at t = 0 s, is excited with a laser pulse at 530 nm wavelength, i.e. within water transparency window. The light intensity (W/m 2 ) has a Gaussian intensity profile,

I(t) = 2 ln (2) π Φ τ L exp -4 ln (2) (t-t 0 ) 2 τ 2 L
, where Φ = 10 J/m 2 is the pulse fluence, which is kept constant for all τ L values, with τ L =1 ns, 100 ps, 10 ps its temporal full-width-half-maximum, while the pulse temporal peak occurs at t 0 = 3τ L . Via the GNC absorption cross section we then calculate the absorbed power density. The latter serves as the source term for the thermics. The temperature T (r,t) throughout the system (both GNC and water) is then obtained solving the thermal diffusion equation while imposing the continuity of the heat flux at the GNC/water interface, q = 1 R [T (R gnc -,t) -T (R gnc +,t)]r, which is controlled by the TBR, R, with T (R gnc ±,t) the temperature at the inner (-) and outer (+) side of the interface and r its normal vector. T (r,t) serves as the source terms for the mechanics via the thermal expansion coefficients of both the GNC and water, ultimately yielding the pressure, p(r,t), and the radial velocity field, v r (r,t) in water. With p and v r at hand, the acoustic Poynting vector, P (W/m 2 ), and from it the mechanical energy radiated in water, U, are retrieved. The thermophone and mechanophone contribution to the total p(r,t) and U are calculated forcing to zero the GNC and water thermal expansion coefficients, respectively.

The first conclusion that can be drawn from simulations results is that the mechanophone effect needs to be accounted for. Fig. 1 shows p(t) in water, 5 nm from the GNC/water interface, together with the thermophone and mechanophone contributions. Results are for the case of τ L = 1 ns and R = 1 × 10 -7 m 2 K/W. The latter is representative of the general cases that might be encountered: its order of magnitude falls between that of the Au/water, 1 × 10 -8 m 2 K/W [START_REF] Gandolfi | Optical wavelength dependence of photoacoustic signal of gold nanofluid[END_REF][START_REF] Plech | Laser-induced heating and melting of gold nanoparticles studied by timeresolved x-ray scattering[END_REF][START_REF] Stoll | Time-resolved investigations of the cooling dynamics of metal nanoparticles: impact of environment[END_REF][START_REF] Wilson | Curvature and temperature-dependent thermal interface conductance between nanoscale gold and water[END_REF] , and that of the graphene-functionalized Au/water interface [START_REF] Herrero | Ultra-high liquid-solid thermal resistance using nanostructured gold surfaces coated with graphene[END_REF] , 1 × 10 -6 m 2 K/W. The thermophone and the mechanophone contributions have similar amplitudes, thus both contributing to the total pressure signal.

We now address the role played by the TBR and τ L in the relative contribution between these two launching mechanisms. On the thermal side, upon absorption of the laser pulse, the GNC raises its temperature on a time scale τ L . It cools down on a time scale τ th transferring heat to the proximal water and raising the temperature of the latter. Finally, the GNC and the proximal water diffuse heat to distant water, relaxing to the initial temperature. The timescale τ th has contributions from the TBR and heat diffusion effects arising from the GNC This is the author's peer reviewed, accepted manuscript. However, the online version of record will be different from this version once it has been copyedited and typeset. and proximal water thermal impedances 39 . We now discuss what might be intuitively foreseen in the two extreme-case scenarios.

PLEASE CITE THIS ARTICLE AS

For τ th ≫ τ L , energy from the laser pulse is delivered to the GNC on a time scale τ L , and, only after a time ∼ τ th , the GNC temperature decreases substantially, while delivering heat to the proximal water. That is, on a time scale τ th we should expect a high-temperature GNC, thermally isolated from the surrounding water still at its ambient temperature. On the mechanics side, the thermal expansion of the GNC should be at its maximum. On the contrary, the contribution of water thermal expansion should be at a minimum and set in on a timescale exceeding τ th . The relevance of the mechanophone effect with respect to the thermophone should thus be highest for cases in which τ th ≫ τ L . For τ th ≪ τ L the situation is the opposite. The laser feeds energy to the GNC on a time scale τ L , whereas the GNC delivers energy to the proximal water on a much faster time scale, τ th : the GNC absorbs energy from the laser pulse and concomitantly delivers it to the proximal water. In this scenario the peak GNC temperature should be at its minimum, whereas the proximal water temperature should reach its greatest value. Accordingly, on the mechanics side, the peak thermal expansion of the GNC should be at its minimum, and that of proximal water at its maximum. The relevance of the mechanophone effect with respect to the thermophone should thus be lowest for τ th ≪ τ L . In first instance, the ratio τ th /τ L therefore appears as a meaningful metric to inspect the thermophone to mechanophone transition. The TBR is though the only material parameter that can be tuned [START_REF] Han | Thermal transport at solidliquid interfaces: High pressure facilitates heat flow through nonlocal liquid structuring[END_REF][START_REF] Pham | Pressure dependence of kapitza resistance at gold/water and silicon/water interfaces[END_REF][START_REF] Barisik | Temperature dependence of thermal resistance at the water/silicon interface[END_REF][START_REF] Vera | Temperature and heat flux dependence of thermal resistance of water/metal nanoparticle interfaces at sub-boiling temperatures[END_REF][START_REF] Banfi | Temperature dependence of the thermal boundary resistivity of glass-embedded metal nanoparticles[END_REF][START_REF] Wu | Thermal transport across surfactant layers on gold nanorods in aqueous solution[END_REF][START_REF] Caplan | Analytical model for the effects of wetting on thermal boundary conductance across solid/classical liquid interfaces[END_REF][START_REF] Ramos-Alvarado | Solid-liquid thermal transport and its relationship with wettability and the interfacial liquid structure[END_REF][START_REF] Kim | Molecular dynamics simulations of thermal resistance at the liquid-solid interface[END_REF][START_REF] Vo | Nano-scale liquid film sheared between strong wetting surfaces: Effects of interface region on the flow[END_REF][START_REF] Barrat | Kapitza resistance at the liquid-solid interface[END_REF][START_REF] Hu | Effect of nanopatterns on kapitza resistance at a watergold interface during boiling: A molecular dynamics study[END_REF][START_REF] Wang | Role of wetting and nanoscale roughness on thermal conductance at liquid-solid interface[END_REF][START_REF] Hasan | Manipulating thermal resistance at the solid-fluid interface through monolayer deposition[END_REF][START_REF] Yenigun | Effect of nano-film thickness on thermal resistance at water/silicon interface[END_REF][START_REF] Cao | Enhanced thermal transport across multilayer graphene and water by interlayer functionalization[END_REF][START_REF] Tian | Enhancing solid-liquid interface thermal transport using self-assembled monolayers[END_REF] , the thermal properties of the GNC and water being fixed. Under a practical stand-point it is therefore desirable to parameterize the prob-lem in terms of a thermal decay time linked to the TBR only, rather than to τ th , which comprises also the effect of proximal water and GNC thermal impedances. To this end, we link the TBR to the thermal decay time through the expression τ T BR =RR gnc c p ρ/2, with c p and ρ the Au specific heat and mass density, respectively. This relation is somewhat approximate [START_REF] Formally | the GNC cooling is mono-exponential with a decay given by this formula, only for a Biot number Bi≪1 and for isothermal water[END_REF] , nevertheless, it has the merit of providing a rule-of-thumb estimate. In the following, we therefore parameterize simulations results in terms of τ T BR /τ L rather than τ th /τ L . We now inspect what happens varying the TBR for a fixed laser pulse duration.

Nanosecond regime. Fig. 2 shows the GNC (panel (a)) and the proximal water (panel (b)) temperature dynamics. The curves are calculated for a fixed value of τ L =1 ns while varying the TBR, from 10 -5 to 10 -9 m 2 K/W, so as to cover the range of τ T BR /τ L from 10 -2 to 10 2 . For increasing τ T BR /τ L the GNC maximum temperature, max{T gnc (t)}, increases from 305 K to 377 K, whereas that of proximal water, max{T w (t)}, decreases from 300 K to 293 K. The implications of the thermal problem on the competition between the thermophone and mechanophone contributions are shown in panel (c). The histogram shows the mechanical energy radiated in water by the sole thermophone (azure) and sole mechanophone (mustard) effects as a function of τ T BR /τ L (bottom axis) and TBR (top axis). Energies are normalized to the maximum mechanical energy observed in water in our simulations (i.e. the thermophone contribution of the τ L = 10 ps, τ T BR /τ L = 10 -11 case that will be described later). For increasing values of the TBR, acoustic wave generation in water switches from thermophone-dominated for τ T BR /τ L 1, to mechanophone-dominated for τ T BR /τ L ≫ 1, τ T BR /τ L ≈ 1 being a cross-over value between the two regimes.

In real case scenarios, the TBR can be tuned engineering the This is the author's peer reviewed, accepted manuscript. However, the online version of record will be different from this version once it has been copyedited and typeset. FIG. 4. Laser pulse: τ L = 10 ps. Same caption as for Fig. 2. The TBR values are varied so as to span the same values of τ T BR /τ L as for the 1 ns pulse case. In panel (c) the case of the graphene-functionalized Au/water interface is here by the mechanophone effect and is hence not reported. GNC/water interface, and the acoustic wave launching mechanism accordingly, switching for instance from the thermophone for the bare Au/water interface, to the mechanophone for the graphene-functionalized Au/water interface, which cases are indicated by the two inset sketches.

PLEASE CITE THIS ARTICLE AS

So far we spanned τ T BR /τ L for a fixed value of τ L while varying the TBR. The question then arises as to whether a similar physics holds true also for shorter laser pulses, thus eventually allowing for an additional knob, τ L , to select the launching mechanism.

Picosecond regime. Fig. 3 and Fig. 4 are analogous to Fig. 2 but for the cases of τ L =100 ps and 10 ps, respectively. For sake of comparison, the TBR is now varied from 10 -6 to 10 -10 m 2 K/W and from 10 -7 to 10 -11 m 2 K/W for the case τ L =100 ps and 10 ps, respectively. These changes allow covering the same range of τ T BR /τ L as for the case of the 1 ns laser pulse. On the thermal side, Fig. 3(a,b) and Fig. 4(a,b) encompass the general trend observed in Fig. 2(a,b): for increasing τ T BR /τ L , max{T gnc (t)} increases whereas max{T w (t)} decreases. While reducing τ L , a relevant parameter for the following discussion is δ T gnc , defined as the difference between the GNC peak temperatures between the cases of τ T BR /τ L =10 2 and 10 -2 . δ T gnc ranges from 72 K for τ L =1 ns, to 27 K for τ L =10 ps, because of the increase of the peak temperature for the case of τ T BR /τ L =10 -2 while transitioning from Fig. 2(a), across Fig. 3(a) to Fig. 4(a). Among the physical reasons behind this trend, is that reducing τ L for a fixed value of τ T BR /τ L =10 -2 implies reducing the TBR, eventually to a point where the interfacial heat transfer is no more the limiting process, the GNC and the proximal water thermal impedances remaining as the only factors controlling the thermal dynamics 58 .

The implications of the thermal problem on the competition between the thermophone and mechanophone contributions are shown in panel (c) of Fig. 3 and Fig. 4, for τ L =100 ps ans 10 ps, respectively. The striking difference, comparing Fig. 2(c), 3(c) and 4(c), is that the mechanophone contribution dependence on τ th /τ L weakens substantially upon reducing the pulse temporal width; not so for the thermophone contribution. Indeed, for the τ L =1 ns case, the mechanophone contribution changes by more than an order of magnitude when increasing τ T BR /τ L from 10 -2 to 10 2 , whereas it changes by a factor of ∼2 for the τ L =10 ps case. The physical reason stands in the thermal problem. The mechanophone effect is triggered by the GNC thermal expansion. The shorter the laser pulse, the smaller is δ T gnc , implying that the peak GNC temperature becomes rather uniform regardless of τ T BR /τ L , and the GNC thermal expansion accordingly.

When exciting with a 100 ps laser pulse, the mechanophone effect contribution to the radiated acoustic energy in water raises to 23% for the Au GNC/water interface, and dominates the graphene-functionalized GNC/water interface, see Fig. 3(c). Further reducing the pulse duration to 10 ps, the mechanophone effect becomes the prevailing mechanism also for the Au GNC/water interface, see Fig. 4(c). 59 In conclusion, we showed, for the case of a water-immersed Au nanocylinder, that the TBR and the laser pulse duration are two valuable control knobs, allowing to switch the acoustic wave launching mechanism in water from the thermophone to the mechanophone. The Au/water and graphenefunctionalized Au/water interfaces were discussed as realistic show-case scenarios. Importantly, when the mechanophone is the dominant launching effect, the surrounding water temperature increase is minimized. These findings thus bare particu-This is the author's peer reviewed, accepted manuscript. However, the online version of record will be different from this version once it has been copyedited and typeset.

PLEASE CITE THIS ARTICLE AS DOI: 10.1063/5.0135147 lar importance in situations requiring high frequency acoustic wave generation in water (i.e. short τ L ) while avoiding heating effects of the latter, as is the case for in-vivo bioimaging and theranostics applications at the nanoscale. Noteworthy, these findings may be expanded to include other nanosystems [START_REF] Bertolotti | A note on the history of photoacoustic, thermal lensing, and photothermal deflection techniques[END_REF][START_REF] Gandolfi | Ultrafast photoacoustic nanometrology of inas nanowires mechanical properties[END_REF] .

  FIG.1. Left axis: pressure time evolution in water at r = R gnc + 5 nm for τ L = 1 ns, R = 1 × 10 -7 m 2 K/W. The curves are normalized to the total pressure maximum. Right axis: I(t) (red dashed curve).

FIG. 2 .

 2 FIG.2. Laser pulse: τ L = 1 ns. Panels (a,b): temperature time evolution, for increasing values of τ T BR /τ L and the corresponding TBR values, in the GNC (r = 0 nm): panel (a); in proximal water (r = R gnc + 5 nm): panel (b). Right axis: I(t) (red dashed line) maximized at the time t 0 . δ T gnc : difference between the GNC peak temperatures between the cases of τ T BR /τ L ∼ 100 and 0.01. Panel (c): normalized mechanical energy generated in water by the thermophone and the mechanophone effects for different τ T BR /τ L (bottom axis) and the corresponding TBRs (top axis). The ratios τ T BR /τ L are rounded to the first significant figure. Values for Au/water and graphene-functionalized Au/water interface are identified by the two round sketches.

FIG. 3 .

 3 FIG.3. Laser pulse: τ L = 100 ps. Same caption as for Fig.2. The TBR values are varied so as to span the same values of τ T BR /τ L as for the 1 ns pulse case.

2 )

 2 This is the author's peer reviewed, accepted manuscript. However, the online version of record will be different from this version once it has been copyedited and typeset.PLEASE CITE THIS ARTICLE AS DOI: 10.1063/5This is the author's peer reviewed, accepted manuscript. However, the online version of record will be different from this version once it has been copyedited and typeset. PLEASE CITE THIS ARTICLE AS DOI: 10.1063/5.0135147

DATA AVAILABILITY STATEMENT

The data that support the findings of this study are available from the corresponding author upon reasonable request.

SUPPLEMENTARY MATERIAL

See the supplementary material for the details on the simulations design.

This work was partially supported by the LABEX iMUST (ANR-10-LABX-0064) of Université de Lyon within the program "Investissements d'Avenir" (ANR-11-IDEX-0007), by ANR through project 2D-PRESTO (ANR-19-CE09-0027) and through project ULTRASINGLE (ANR-20-CE30-0016). F.B. acknowledges financial support from CNRS through Délégation CNRS 2021-2022.

AUTHOR DECLARATIONS

Conflict of Interest

The authors have no conflicts to disclose. This is the author's peer reviewed, accepted manuscript. However, the online version of record will be different from this version once it has been copyedited and typeset.

PLEASE CITE THIS ARTICLE AS DOI: 10.1063/5.0135147


Abhinandan Pal

Francesco Ranzato

Caterina Urban

Marco Zanella

Abstract Interpretation-Based Feature Importance for SVMs

We propose a symbolic representation for support vector machines (SVMs) by means of abstract interpretation, a well-known and successful technique for designing and implementing static program analyses. We leverage this abstraction in two ways: (1) to enhance the interpretability of SVMs by deriving a novel feature importance measure, called abstract feature importance (AFI), that does not depend in any way on a given dataset of the accuracy of the SVM and is very fast to compute, and (2) for verifying stability, notably individual fairness, of SVMs and producing concrete counterexamples when the verification fails. We implemented our approach and we empirically demonstrated its effectiveness on SVMs based on linear and nonlinear (polynomial and radial basis function) kernels. Our experimental results show that, independently of the accuracy of the SVM, our AFI measure correlates much more strongly with the stability of the SVM to feature perturbations than feature importance measures widely available in machine learning software such as permutation feature importance. It thus gives better insight into the trustworthiness of SVMs.

Introduction

Machine learning (ML) software is increasingly being employed in high stakes or sensitive applications [START_REF] Chouldechova | Fair Prediction with Disparate Impact: A Study of Bias in Recidivism Prediction Instruments[END_REF]Khandani et al., 2010, etc.). This poses important challenges for safety, privacy, and non-discrimination [START_REF] Buolamwini | Gender shades: Intersectional accuracy disparities in commercial gender classification[END_REF][START_REF] Obermeyer | Dissecting racial bias in an algorithm used to manage the health of populations[END_REF]. As a consequence, research in ML verification rapidly gained popularity [START_REF] Liu | Algorithms for verifying deep neural networks[END_REF][START_REF] Urban | A Review of Formal Methods applied to Machine Learning[END_REF] and demand for interpretable ML models is more and more pronounced [START_REF] Tjoa | A Survey on Explainable Artificial Intelligence (XAI): Toward Medical XAI[END_REF]. Notably, interpretability is needed to meet the requirements of recent legal regulations on sensitive automated decision-making applications, such as the General Data Protection Regulation (GDPR) and the Artificial Intelligence Act in the EU.

There is a tradeoff between interpretability and performance of a ML model: non-linear models generally deliver much better predictions but they do not provide explanations. The most prominent interpretability technique is feature importance, measuring the contribution of each input feature to a model prediction [START_REF] Bhatt | Explainable Machine Learning in Deployment[END_REF].

Permutation feature importance (PFI) [START_REF] Breiman | Random Forests[END_REF][START_REF] Fisher | All Models are Wrong, but Many are Useful: Learning a Variable's Importance by Studying an Entire Class of Prediction Models Simultaneously[END_REF], the most widely used and understood importance measure, 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. PFI is easy to explain, implement, and use, making it widely available in ML software (e.g., the scikit-learn Python library, etc.). On the other hand, the result may greatly vary depending on the dataset. Second, the result depends on shuffling and must be averaged across repetitions to stabilize, thus becoming resource intensive when the number of features is large. Third, PFI yields misleading results when features are correlated [START_REF] Hooker | Unrestricted permutation forces extrapolation: Variable importance requires at least one more model, or there is no free variable importance[END_REF]. Finally, and more importantly, the quality of the result heavily depends on the accuracy of the model! Notably, model variance to feature perturbations [START_REF] Goodfellow | Making Machine Learning Robust Against Adversarial Inputs[END_REF] and PFI are strongly correlated only when the model generalizes well.

Contributions. In this work, we propose a novel feature importance measure for SVMs, called abstract feature importance (AFI), that: (a) does not depend on a given dataset or the accuracy of the model, and (b) is extremely fast to compute, independently of the number of input features. We support both linear and non-linear kernels, in particular the polynomial and the radial basis function (RBF) kernels.

We derive our importance measure from a symbolic representation of a SVM based on abstract interpretation [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Cousot | Principles of Abstract Interpretation[END_REF], a wellestablished framework for designing computable and correct over-approximations of model computations. Specifically, the concrete quantities being manipulated by model computations are represented using an abstract domain, which defines their abstract counterparts and their datastructure representations, as well as algorithms to manipulate them according to the semantics of the computations.

We leverage existing abstract domains such as hyperrect-angles [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] and reduced affine forms [START_REF] Messine | Extentions of Affine Arithmetic: Application to Unconstrained Global Optimization[END_REF] 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 combination in verifying model stability against feature perturbations. In particular, we focus on verifying individual fairness [START_REF] Dwork | Fairness through awareness[END_REF].We evaluate our approach by verifying SVMs trained on the reference datasets in the literature on ML fairness (Mehrabi et al., 2021a) and considering different similarity relations.

Our approach is sound, meaning that an individually fair abstract representation of a SVM implies that the SVM is also fair. Thus, the fraction of successful fairness verifications over a test dataset is a lower bound on individual fairness of a SVM. On the other hand, our approach is not complete as there are cases in which the SVM is fair but the verification of its abstract representation fails due to imprecisions introduced by the abstraction. Our third contribution in this work is a way to leverage this abstract representation to generate concrete counterexamples when unable to verify fairness, i.e., 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 thus, by complement, an upper bound on individual fairness of a SVM.

Finally, we conduct an extensive experimental comparison between our proposed importance measure AFI and the standard and popular PFI and we 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 ML model. We also distinguish modelagnostic measures, which can be applied to any model, and model-specific measures. Finally, we classify importance measures in performance-based, i.e., measuring importance with respect to the predictive performance of the model (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 [START_REF] Breiman | Random Forests[END_REF][START_REF] Fisher | All Models are Wrong, but Many are Useful: Learning a Variable's Importance by Studying an Entire Class of Prediction Models Simultaneously[END_REF] is a global, model-agnostic, performance-based measure. AFI, our novel feature importance measure, is specific for SVMs but can be used both as global and local measure, and is effect-based. Several other model-agnostic importance measures have been proposed in the literature. Prominent effect-based measures are visual tools such as partial dependence (PD) [START_REF] Friedman | Greedy Function Approximation: A Gradient Boosting Machine[END_REF], individual conditional expectation (ICE) [START_REF] Goldstein | Peeking Inside the Black Box: Visualizing Statistical Learning With Plots of Individual Conditional Expectation[END_REF], and accumulated local effects (ALE) [START_REF] Apley | Visualizing the Effects of Predictor Variables in Black Box Supervised Learning Models[END_REF] plots. Other notable effect-based measures are Shapley values [START_REF] Strumbelj | Explaining Prediction Models and Individual Predictions with Feature Contributions[END_REF], and local measures such as local interpretable model-agnostic explanations (LIME) [START_REF] Ribeiro | Why Should I Trust You?": Explaining the Predictions of Any Classifier[END_REF], and SHapley Additive exPlanations (SHAP) [START_REF] Lundberg | A Unified Approach to Interpreting Model Predictions[END_REF]. Visual tools, such as individual conditional importance (ICI) and partial importance (PI) curves [START_REF] Casalicchio | Visualizing the Feature Importance for Black Box Models[END_REF], are also proposed for local performance-based measures. [START_REF] Casalicchio | Visualizing the Feature Importance for Black Box Models[END_REF] additionally propose a Shapley feature importance (SFIMP) measure that allows comparing feature importances across different models. Input gradient [START_REF] Hechtlinger | Interpretation of Prediction Models Using the Input Gradient[END_REF]) is a local measure that can be both effect-based and performancebased. Feature importance measures specific for SVMs are typically limited to linear SVMs or face scalability issues with the number of features, e.g. [START_REF] Mladenić | Feature selection using linear classifier weights: interaction with classification models[END_REF][START_REF] Chang | Feature ranking using linear svm[END_REF]. By contrast, our AFI measure also supports non-linear kernels and has no scalability issues.

Our work generally contributes to the research ecosystem around the verification of ML models using formal methods [START_REF] Liu | Algorithms for verifying deep neural networks[END_REF][START_REF] Urban | A Review of Formal Methods applied to Machine Learning[END_REF]. Most approaches have focused on neural networks [START_REF] Roh | Fr-train: A mutual information-based approach to fair and robust training[END_REF][START_REF] Ruoss | Learning certified individually fair representations[END_REF][START_REF] Urban | Perfectly parallel fairness certification of neural networks[END_REF]Yurochkin et al., 2020, etc.) while here we focus on SVMs. Our work leverages the SVM verifier SAVer [START_REF] Ranzato | Robustness verification of support vector machines[END_REF]. In addition, we introduce here a more precise abstraction for one-hot encoded features. Our fairness analysis is closely in line with the approach by [START_REF] Ranzato | Fairnessaware training of decision trees by abstract interpretation[END_REF], who evaluated the individual fairness of decision tree ensembles trained by a new fairness-aware learning technique. Similar works either consider a very different notion of fairness or a different "threat model", in most cases both. [START_REF] Xiao | Support vector machines under adversarial label contamination[END_REF] evaluate security against flipping a few labels to maximize classification error. [START_REF] Ghosh | Algorithmic fairness verification with graphical models[END_REF] consider group and causal fairness metrics. [START_REF] Langenberg | On the robustness of support vector machines against adversarial examples[END_REF] deal with robustness of SVMs against adversarial attacks [START_REF] Fish | A confidencebased approach for balancing fairness and accuracy[END_REF] propose a new fairness metric where they add a new feature with random values and bias individuals on this feature: the model is fair when it recovers the original labels. [START_REF] Park | Privacy-preserving fair learning of support vector machine with homomorphic encryption[END_REF] put forward a protocol to protect sensitive information and train a fair model using homomorphic encryption. [START_REF] Mehrabi | A survey on bias and fairness in machine learning[END_REF] and [START_REF] Verma | Fairness definitions explained[END_REF] discuss several fairness metrics used to verify a variety of ML models.

Background

Support Vector Machines. SVMs [START_REF] Cristianini | An Introduction to Support Vector Machines and Other Kernel-based Learning Methods[END_REF] are 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 an hyperplane w • z -b = 0, where w ∈ R d and b ∈ R are learned parameters, that determines whether an input z falls above/below (i.e., sgn(w • z -b) = ±1) w.r.t. the hyperplane. This approach is extended to non-linear SVMs through a projection to a high-dimensional space via a kernel function where k(x, z) = e -γ x-z 2 2 , for some positive hyperparameter γ > 0. In multi-classification for a set of labels L = {y 1 , ..., y m }, m > 2, the standard approach is a reduction into multiple binary classification problems combined by leveraging a voting procedure over different labels.

k : R d × R d → R. Given a training dataset T = {(x 1 , y 1 ), ...., (x n , y n )} ⊆ X × {-1, +1}, kernel function k and learned parameters c i , b ∈ R, i ∈ [1, n], a non-linear SVM C T is
Abstract Interpretation. A tuple A, A , γ A is a numerical abstract domain (or abstraction) when A, A is an partially ordered set of abstract values and γ A : A → ℘(R n ) is a concretization function which maps abstract values to sets of numerical vectors and monotonically preserves the ordering relation, i.e., a 1 A a 2 implies γ A (a 1 ) ⊆ γ A (a 2 ). Intuitively, an abstract domain defines a symbolic representation of sets of vectors in ℘(R n ).

Given a k-ary operation

f : (R d ) k → R d , for some k > 0, a corresponding abstract function f A : A k → A is a sound (over-)approximation of f on (a 1 , ..., a k ) ∈ A k when {f (x 1 , ..., x k ) | x i ∈ γ A (a i )} ⊆ γ A (f A (a 1 , ..., a k ))
holds. Morever, f A is a complete (over-)approximation of f on its input (a 1 , ..., a k ) when equality holds.

Abstract Domains. We consider the well-known abstract domain of hyperrectangles (or intervals) [START_REF] Cousot | Principles of Abstract Interpretation[END_REF][START_REF] Rival | Introduction to Static Analysis: An Abstract Interpretation Perspective[END_REF]. The hyperrectangle abstract domain HR n consists of n-dimensional vectors h of real intervals h = [l 1 , u 1 ], . . . , [l n , u n ] ∈ HR n , with lower and upper bounds l

i , u i ∈ R ∪ {-∞, +∞} such that l i ≤ u i . Hence, the concretization function γ HR : HR n → ℘(R n ) is de- fined by γ HR (h) {x ∈ R n | ∀i. l i ≤ x i ≤ u i }.
Abstract operations are defined by extending the following abstract additions and multiplications of intervals:

[l 1 , u 1 ] + HR [l 2 , u 2 ] [l 1 + l 2 , u 1 + u 2 ] and [l 1 , u 1 ] * HR [l 2 , u 2 ] [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 exp can be imprecise, e.g., the evaluations of the simple expressions x -x and x • x on an input interval [-c, c], with c > 0, yield, respectively, [-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 polynomial/RBF SVM classifier. Therefore, following [START_REF] Ranzato | Robustness verification of support vector machines[END_REF], for our SVM abstract representations, we leverage the relational reduced affine form (RAF) ab-straction. A RAF for vectors in R n is given by an expression a 0 + n i=1 a i i + a r r , where the i 's are symbolic variables ranging in the real interval [-1, 1] representing a dependence from the i-th component of the vector, while r is a further symbolic variable in [-1, 1] which accumulates all the approximations introduced by non-linear operations. Thus,

RAF n {a 0 + n i=1 a i i + a r a | a 0 , a 1 , ..., a n ∈ R, a r ∈ R ≥0 }. The concretization map γ RAF : RAF n → ℘(R) is defined by γ RAF (a 0 + n i=1 a i i + a r a ) {x ∈ R | a 0 - n i=1 |a i | -|a r | ≤ x ≤ a 0 + n i=1 |a i | + |a r |}.
Moreover, RAF n also has a top element RAF representing the lack of information, i.e., such that γ RAF ( RAF ) = R. Linear operations, namely additions and scalar multiplications, admit a complete approximation on the RAF abstraction. Thus, RAFs settle the dependency problem for linear expressions. Instead, non-linear abstract operations, such as multiplication, must necessarily be approximated for RAFs. We will use an optimal abstract multiplication of RAFs defined by [START_REF] Skalna | A new algorithm for Chebyshev minimum-error multiplication of reduced affine forms[END_REF].

Robustness. We consider an input space X ⊆ R d , a set of classification labels L = {y 1 , ..., y m }, and a dataset

T = {(x 1 , y 1 ), ...., (x n , y n )} ⊆ X × L. A classifier trained on the dataset T is modeled as a map C T : X → L.
An adversarial region for an input sample x ∈ X is designated by a perturbation P (x) ⊆ X such that x ∈ P (x). Usually, a perturbation function P : X → ℘(X) is defined through a metric m to measure similarity between inputs as their distance w.r.t. m. The most common metric is induced by the ∞ maximum norm [START_REF] Carlini | Towards Evaluating the Robustness of Neural Networks[END_REF] defined as x ∞ max {x 1 , . . . , x d }, so that the corresponding perturbation P ∞ (x) includes all the vectors z ∈ X whose ∞ distance from x is bounded by a thresh-

old ∈ R + , that is, P ∞ (x) {z ∈ X | x -z ∞ ≤ }.
A classifier C is robust (or stable) for a perturbation function P on an input x, denoted by robust(C, x, P ), when for all z ∈ P (x), C(z) = C(x) holds. Robustness to a perturbation P is used as a major metric [START_REF] Goodfellow | Making Machine Learning Robust Against Adversarial Inputs[END_REF] to assess a classifier C on a testing set T ⊆ X × L as follows:

rob T (C, P ) |{(x,y)∈T | robust(C,x,P )}| |T | .
SAVer. Our work leverages SAVer (SVM Abstract Verifier), an automatic tool for robustness verification of SVMs introduced by [START_REF] Ranzato | Robustness verification of support vector machines[END_REF]. Given an SVM C : X → L, SAVer leverages an abstraction A n of ℘(R n ) to first achieve a sound abstraction P (x) ∈ A n of an adversarial region P (x), i.e., P (x) ⊆ γ A (P (x)), and then applies sound abstract versions of the transfer functions occurring in C to design an abstract SVM C : A → ℘(L) that computes an over-approximation of the labels assigned to inputs in P (x), i.e., {C(z) ∈ L | z ∈ P (x)} ⊆ C (P (x)). If C (P (x)) = {y i }, then every input in P (x) is classified as y i , so C is proved robust over P (x). In the binary case L = {-1, +1}, C consists of an abstract function A C : A n → A 1 that computes an over-approximation A C (P (x)) of the set of distances between samples in P (x) and the separation curve, and then over-approximates the set of labels:

C (P (x)) if γ A1 (A C (P (x))) ⊆ R <0 then {-1} elseif γ A1 (A C (P (x))) ⊆ R >0 then {+1} else {-1, +1}.
In multi-classification, the voting also needs to be soundly approximated [START_REF] Ranzato | Robustness verification of support vector machines[END_REF].

Abstract Feature Importance

We can now define our abstract feature importance (AFI).

Definition 3.1 (Abstract Feature Importance). Let C : R n → L be a SVM classifier and let A RAF C : (RAF n ) n → RAF n be its abstraction in the RAF abstract domain. Let A RAF C (f 1 , . . . , f n ) a 0 + n i=1 a i i +a r r be the abstract computation output for an abstract input (f 1 , . . . , f n ), f i ∈ RAF n . The importance of every input feature i ∈ [1, n] is defined as the absolute value |a i | ≥ 0.
The definition purposely approximates by ignoring the accumulative error due to the approximations of all non-linear operations performed by C, i.e., the term a r r , influenced by all input features. When (f 1 , . . . , f n ), f i ∈ RAF n , abstracts the whole input space X ⊆ R n , AFI measures the global feature importance. Otherwise, AFI measures the local importance on the output label.

Example 3.2. Let us consider a toy linear SVM

C over a space X ⊆ R 2 of values normalized to [-1, +1], thus X = {x ∈ R 2 | -1 ≤ x 1 , x 2 ≤ +1}.
We consider two support vectors v 1 = (-0.5, 1), v 2 = (0.5, -1) ∈ X labeled respectively as -1, +1 with weights w 1 = w 2 = 0.5 and bias b = 0, so that C sgn (x) = -0.5(v 1 • x) + 0.5(v 2 • x). We express X as the RAF a = (0 ± 1 , 0 ± 2 ) ∈ (RAF 2 ) 2 . By performing the abstract computations of A RAF C on this input we obtain:

A RAF C (a) = -0.5(v 1 • RAF a)+0.5(v 2 • RAF a) = -0.5(-0.5(0 ± 1 ) + 1(0 ± 2 )) + 0.5(0.5(0 ± 1 ) - 1(0 ± 2 )) = -0.5(0 ± (-0.5) 1 ± 2 ) + 0.5(0 ± 0.5 1 ± (-1) 2 ) = 0 ± 0.5 1 ± (-1) 2 .
We therefore infer the importance indices |a 1 | = 0.5 and |a 2 | = 1 for, respectively, x 1 and x 2 , and conclude that x 2 is twice as important as x 1 . Note that, since we considered a linear SVM, it can be rewritten in primal form as:

C sgn (x) = -0.5(v 1 • x) + 0.5(v 2 • x) = -0.5(-0.5x 1 + x 2 ) + 0.5(0.5x 1 -x 2 ) = 0.5x 1 -x 2 = (0.5, -1)•x,
thus obtaining an explicit weight w = (0.5, -1) for the input features, whose absolute values 0.5, 1 exactly match our importance indices.

Our importance indices depend on the size of the input, which can make results harder to read and interpret, especially when the number of features is high. We use a simple clustering strategy to assign them a score: we consider the distribution of feature importances and compute its mean µ and standard deviation σ, and we assign to each feature x i the score score i ∈ Z such that µ + score i σ ≤ ai-µ σ < µ + (score i + 1)σ, which has the same effect of standardizing the distribution into a normal N (0, 1) and slicing the distribution at every unit, labeling every slice with a progressive number. By doing so, features moderately influencing the result will have a score close to zero, while relevant feature will have higher scores, and those not influencing the outcome will have a negative score. Last, we suggest to shift and clip such distribution in order to obtain grades, e.g., in [3,10], which can be achieved by a simple transformation: grade i = max(min(10, score i + 6), 3). For instance, let us consider a distribution of indices a i given by (1,6,2,5,6,1,6,7,8,9), where µ = 5.1 and σ = 2.85: we compute gradei i as (5,7,5,6,7,5,7,7,8,8). In this case it becomes easy to see that x 1 and x 3 have similar impact on the classification, although having different scores.

Last, we emphasize the fact that AFI does not require any knowledge on the ground truth values, nor the actual output of the classifier, as it focuses on the computation process performed by the classifier, rather than how the result of such computation is used to assign a label to a point, thus making this approach feasible in scenarios where the correct output is not known in advance.

An Abstraction for One-Hot Encoding

ML algorithms need a way to represent categorical data in numeric form. Let F = {c 1 , c 2 , . . . , c k } be the set of values of a categorical feature f . Assigning a number to each value in F introduces an unwanted ordering relation among features. A better approach is one-hot encoding, that is, replacing f with k binary features

(x f 1 , x f 2 , . . . , x f k ) ∈ {0, 1} k such that ∀i ∈ [1, k]. x f i = 1 ⇔ f = c i .
This sequence of bits is also referred to as a tier of f . Abstractions such as the hyperrectangle and RAF abstract domains, are likely to suffer from a significant loss of precision when dealing with one-hot encoded features, as they are not able to keep track of the relationship existing between the binary features resulting from the encoding. Example 4.1. Let us consider a categorical feature f ∈ F = {red , green, blue} and let (x r , x g , x b ) ∈ {0, 1} 3 be the corresponding one-hot encoded tiers. Consider the set {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 ∈ [0, 1], x g ∈ [0, 1], x b ∈ [0, 0]) ∈ HR 3 .
Observe that h also represents infinitely many vectors in R 3 that do not belong to X and are illegal encodings, such as (0.3, 0.7, 0), (1, 1, 0) or (0, 0, 0).

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

Let us first recall the constant propagation abstract domain CP R ∪ {⊥ CP , CP }, ordinarily used by modern compilers [START_REF] Aho | Compilers: Principles, Techniques, and Tools (2nd Edition)[END_REF][START_REF] Wegman | Constant propagation with conditional branches[END_REF]. CP is a flat domain whose partial order CP is defined by ⊥ CP CP z CP CP , for all z ∈ R. The concretization γ CP : CP → ℘(R) is: γ CP (z) {z}, for all z ∈ R, meaning that a given numerical feature can only assume a constant value z, γ CP ( CP ) R representing no constancy information, while γ CP (⊥ CP ) ∅ encodes unfeasibility. CP also has an abstraction map α CP : ℘(R) → CP that provides the best approximation in CP, i.e. least w.r.t. the order CP , of a set of values, which is: α CP (∅) ⊥ CP , α CP ({z}) z, and α CP (X)

CP otherwise.

, a b ⇔ ∀i ∈ [1, k]. a i,f CP b i,f & a i,t CP b i,t . Then, for each component i ∈ [1, k], the map γi : OH k → ℘(R k ) is defined as: γi (a) {x ∈ R k | x i ∈ γ CP (a i,t ), ∀j = i. x j ∈ γ CP (a j,f )}.
Thus, a ∈ OH k represents through γi the set of tiers whose i-th component was originally set to true. Note that if, for some

i ∈ [1, k], either a i,f = ⊥ CP or a i,t = ⊥ CP , then γi (a) = ∅. A value a ∈ OH k such that, for all i ∈ [1, k] and u ∈ {f, t}, a i,u ∈ CP { CP } is called top-less.
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

γ OH k : OH k → ℘(R k ) is: γ OH k (a) ∪ k
i=1 γi (a). Example 4.2. Let us continue Example 4.1 by considering a = (0, 1), (0, 1), (0, ⊥ CP ) ∈ OH 3 as an abstraction of X = {(1, 0, 0), (0, 1, 0)}. Its concretization is:

γ OH3 (a) = γ1 (a) ∪ γ2 (a) ∪ γ3 (a) = {x ∈ R 3 | x 1 ∈ {1}, x 2 ∈ {0}, x 3 ∈ {0}} ∪ {x ∈ R 3 | x 1 ∈ {0}, x 2 ∈ {1}, x 3 ∈ {0}} ∪ {x ∈ R 3 | x 1 ∈ {0}, x 2 ∈ {0}, x 3 ∈ ∅} = {(1, 0, 0), (0, 1, 0)}. Thus a precisely represents X.
Example 4.2 is not fortuitous. In fact, for any set X of onehot encoded tiers there always exists an abstract value a in OH which precisely represents this set, i.e., γ OH (a) = X.

Theorem 4.3. If X ∈ ℘(R k
) is such that every vector of X is a one-hot encoded tier (0, ..., 0, 1, 0, ...0), then the abstract value a X ∈ OH k defined as a

X i α CP ({x i | x ∈ X, x i = 0}), α CP ({x i | x ∈ X, x i = 1}) , for all i ∈ [1, k], precisely represents X.
Remark 4.4. a X is always top-less because the components of each pair a X i range in {0, 1, ⊥ CP }.

Given a function f : R → R, its abstract counterpart f CP : CP → CP on the CP domain is [START_REF] Wegman | Constant propagation with conditional branches[END_REF]:

f CP (z) f (z), for all z ∈ R, f CP (⊥ CP ) ⊥ CP , and f CP ( CP ) CP .
In turn, f CP allows us to define a sound abstract counterpart of f on our OH abstraction:

Theorem 4.5. A sound approximation of f on OH k is f OH : OH k → OH k defined, for all i ∈ [1, k], as (f OH (a)) i f CP (a i,f ), f CP (a i,t ) .
Example 4.6. Let us carry on Example 4.2. We apply f (x)

x 2 -3x + 1 to every component in γ OH3 (a):

f (γ OH3 (a)) = {(f (1), f (0), f (0)), (f (0), f (1), f (0))} = {(-1, 1, 1), (1, -1, 1)}. By applying Theorem 4.5 to a, we obtain a f OH (a) = (f CP (0), f CP (1)), (f CP (0), f CP (1)), (f CP (0), f CP (⊥ CP ) = (1, -1), (1, -1), (1, ⊥ CP ) , whose concretization is: γ OH3 (a ) = γ1 (a ) ∪ γ2 (a ) ∪ γ3 (a ) = {x ∈ R 3 | x 1 ∈ {-1}, x 2 ∈ {1}, x 3 ∈ {1}} ∪ {x ∈ R 3 | x 1 ∈ {1}, x 2 ∈ {-1}, x 3 ∈ {1}} ∪ {x ∈ R 3 | x 1 ∈ {1}, x 2 ∈ {1}, x 3 ∈ ∅} = {(-1, 1, 1), (1, -1, 1)}. Then, notice that soundness holds because f (γ OH3 (a)) ⊆ γ OH3 (f OH (a)).
Note that in Example 4.6, f (γ OH3 (a)) = γ OH3 (f OH (a)) also holds, i.e., f OH is a complete approximation of f on a. This is as a consequence of the following general result.

Corollary 4.7. Let a ∈ OH k be top-less. Then (i) f OH is a complete abstraction of f on a; and (ii) given

f 1 , f 2 , . . . , f p : R → R, f OH 1 • f OH 2 • • • • • f OH p is a com- plete abstraction of f 1 • f 2 • • • • • f p on a.
We implemented this OH abstraction on top of (the interval and) RAF abstraction in SAVer. Given a categorical feature f we first perform one-hot encoding, obtaining (x f 1 , x f 2 , . . . , x f k ) ∈ {0, 1} k . When perturbing one-hot encoded values we allow every binary feature in the encoding to be either 0 or 1, so their abstract value is always in the shape (0 CP , 1 CP ) k . As a consequence each abstract binary feature a i can be represented as the RAF 0.5 ± 0.5 i . We keep track of the relation between features and tiers using a global lookup table. After computing the abstract kernel, the resulting RAF a contains information both from the regular and the OH analysis. For verification purposes, we condense the latter to a single interval representing the behavior of the categorical feature f : we compute γ OH k over each tier and we select the values minimizing and maximizing the RAF expression a, thus computing a sound approximation of the interval of variation induced by f . Then, we build a RAF a by transferring numerical features as they are, and replacing tier information with the newlycomputed intervals, expressed in RAF form. Finally, the resulting a allows to compute the superset of output labels as before. Both the RAF a or the condensed RAF a are suitable for our importance measure AFI: in the former case, unlike PFI, we are additionally able to measure the importance of tiers of a one-hot encoded feature.

Individual Fairness

Several formal models of fairness have been investigated in the literature. [START_REF] Dwork | Fairness through awareness[END_REF] point out several weak-nesses of group fairness and therefore study individual fairness defined as "the principle that two individuals who are similar with respect to a particular task should be classified similarly" (Dwork et al., 2012, Section 1.1). This is formalized as a Lipschitz condition of the classifier, that is, by requiring that two individuals x, y ∈ X whose distance is δ(x, y), are mapped, respectively, to distributions D x and D y whose distance is at most δ(x, y). Intuitively, the output distributions for x and y are indistinguishable up to their distance. Several distance metrics δ : X × X → R ≥0 can be used in this context, where [START_REF] Dwork | Fairness through awareness[END_REF], Section 2) studies the total variation or relative ∞ distances.

Following [START_REF] Dwork | Fairness through awareness[END_REF], a classifier C : X → L is (individually) fair when C outputs the same label for all pairs of individuals x, y ∈ X satisfying a similarity relation S ⊆ X × X between input samples. This relation S can be derived from a distance δ as follows: (x, y) ∈ S ⇔ δ(x, y) ≤ , where ∈ R is a similarity threshold. Definition 5.1 (Individual Fairness). A classifier C : X → L is fair on an individual x ∈ X with respect to a similarity relation S ⊆ X × X, denoted by fair(C, x, S),

when ∀z ∈ X. (x, z) ∈ S ⇒ C(z) = C(x).
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 ⊆ X × L: fair T,S (C)

|{(x,y)∈T | fair(C,x,S)}| |T |
. Hence, individual fairness for a similarity relation S boils down to robustness on the perturbation P S (x) {z ∈ X | (x, z) ∈ S} induced by S, i.e., for all x ∈ X, fair(C, x, S) ⇔ robust(C, x, P S ).

Mitigating Incompleteness

The abstract framework described in Sec. 2 and 4 is sound, thus a classifier C verified as robust over a region P (x) guarantees that every point x ∈ P (x) receives the same label. The converse is generally not true for non-linear kernels, due to lack of completeness: when the abstract verification is not able to assert robustness, it may be either due to a loss of precision or an actual point in P (x) which receives a different label. We refer to the latter as a counterexample. In case of an inconclusive analysis we can mitigate the effect of incompleteness by searching for counterexamples: if at least one is found the classifier can be marked as not robust. Finding a counterexample within a possibly infinite set of points however is a daunting task. Let a ∈ RAF n be a sound abstraction for P (x), C a classifier, and A RAF C its abstraction. We define an informed heuristic search approach which leverages our AFI measure: 1. let a out = a 0 + n i=1 a i i + a r r be the output of the abstract computation on RAF (cf. Sec. 3); 2. if C(x) < 0, we look for a potential counterexample x * by maximizing a out , i.e., selecting the maximum possible value for every x i when a i > 0, and the minimum when

a i < 0 (the converse if C(x) > 0); 3. if C(x * ) = C(x)
, then x * is a counterexample for x, and the classifier is not robust; 4. otherwise we select the most influential feature x M , and its mean value in P (x) given by m =

min{x M | x∈P (x)}+max{x M | x∈P (x)} 2
, and we partition P (x) using the cutting hyperplane x M ≤ m, obtaining left and right sets P l (x), P r (x) ⊆ P (x); 5. we consider a l , a r ∈ RAF abstracting P l (x), P r (x), respectively, and we recursively repeat from step 1 until a counterexample is found, or a user-defined timeout is met.

Maximization in step 2 requires additional care for features obtained through one-hot encoding, as exactly one 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 5 does not introduce any loss of precision, as RAF represent hyperrectangles, and partitioning one using a cutting hyperplane of the form x i ≤ k yields two smaller hyperrectangles.

Step 1 and 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 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 (x) while leaving all the vertices on the same side. We therefore proceed to step 4 and 5 partitioning P (x) into two smaller components P l (x) and P r (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 definitively marked as not robust. Otherwise, we set a timeout mechanism, such as a limit on the recursion depth, to avoid non-termination.

Example 6.1. Let s = (0, -√ 2), t = (-1, 1), v = (1, 1) be the support vectors of an SVM with polynomial kernel k(x, y) = (x • y + 1) 2 , -α s = α t = α v = 1 their weights, and b = 0 the bias. Classifier C is therefore given by C

(x) = -(s•x+1) 2 +(t•x+1) 2 +(v •x+1
) 2 and can be rewritten to its primal form 2x 2 1 + 2(2 + √ 2)x 2 + 1, allowing to see the separation plane as the parabola Γ :

x 2 = -1 2+ √ 2 x 2 1 - 1 2(2+ √
2) . We now consider x = (0.5, -0.5) and P (x ) the hyperrectangle of radius 0.5 centered in x :

P (x) = {x ∈ R 2 | 0 ≤ x 1 ≤ 1, -1 ≤ x 2 ≤ 0}.
We observe that C(x ) ≈ -1.91, but every point x ∈ P (x ) having x 2 = 0 will evaluate to the positive expression 2x 2 1 + 1, hence C is not robust over P (x). Visually, Γ crosses P (x) leaving some vertices on different sides of the space.

We consider a = (0.5 ± 0.5 1 , -0.5 ± 0.5 2 ) ∈ RAF 2 2 abstracting P (x ), and compute a out = c ± 0.5

1 ± (1 + √ 2) 2 ± d r ,
where the values of the center c ∈ R and the non linear accumulation term d ∈ R are omitted as not relevant for this example. As a result we obtain the fea-ture importance gradient (0.5, 1 + √ 2) having both components positive. Since C(x ) < 0 we are looking for positive counterexamples and, following step 3, we build x * ∈ P (x ) by selecting the maximum values for x 1 , x 2 in P (x ), which yields x * = (1, 0). Then compute C(x * ) = 2(1) 2 + 2(2 + (2)(0) + 1 = 3 > 0, hence a counterexample is found and C can be marked as not robust.

(x ) = {x ∈ R 2 | -1 ≤ x 1 ≤ +1, -1 2+ √ 2 ≤ x 2 ≤ 0}
, as depicted by Fig. 1. It is easy to observe that every vertex of P (x ) is on the same side of Γ and thus receives the same label, while a small region in the bottom lays on the other side making C not robust. We repeat the counterexample search process obtaining the importance gradient (0,

3+2 √ 2 (2+ √
2) 2 ), this time looking for a negative counterexample hence moving in the opposite direction with respect to the gradient. By doing so we compute x * = (-1, -1 2+ √

2 ) as the bottom-left corner, but C(x * ) = 1 which does not produce a counterexample. We therefore follow steps 4 and 5 partitioning P (x ) with

x 2 < -1 2(2+ √
2) as shown in the picture, and starting the recursion. After the first recursive step, none of the rectangles have counterexamples in their vertices, so another recursive call is started on the lowest one after partitioning on x 1 < 0. Both the resulting rectangles have now counterexamples in their vertices, which can be found by step 1 and 2. C can thus be marked as non robust.

Experimental Evaluation

We consider datasets standard to the fairness literature (Mehrabi et al., 2021a) (a) Adult [START_REF] Dua | Uci machine learning repository[END_REF], which labels yearly incomes (above or below 50K US$) based on personal attributes. (b) Compas [START_REF] Angwin | Machine Bias[END_REF], which labels recidivism risk based on personal attributes and criminal history. (c) Crime [START_REF] Dua | Uci machine learning repository[END_REF], which labels communities below or above the median per capita violent crime rate based on socio-economic, law enforcement, and crime data. (d) German [START_REF] Dua | Uci machine learning repository[END_REF], which labels (good or bad) credit scores [START_REF] Dua | Uci machine learning repository[END_REF]. (e) Health (https://www.kaggle. com/c/hhp), which labels ten-year mortality (above or below the median Charlson index) for a patient based on physician records and insurance claims. The data is preprocessed following (Ruoss et al., 2020, Section 5). Some of these datasets exhibit a highly unbalanced label distribution, leading to high accuracy and 100% individual fairness for a constant classifier like C(x) = 1. Thus, following [START_REF] Ruoss | Learning certified individually fair representations[END_REF] we also report the balanced accuracy, i.e., 1 2 truePos truePos+falseNeg + trueNeg trueNeg+falsePos .

Similarity Relations. Let I ⊆ N denote the set of features after one hot encoding and x, y ∈ X be two individuals. Following (Ruoss et al., 2020, Section 5.1), we consider three similarity relations.

NOISE: S noise (x, y) iff |x i -y i | ≤ for all i ∈ I , and x i = y i for all i ∈ I I , where I ⊆ I is a subset of numerical features. For our experiments, we consider = 0.05 which leads upto a 10% perturbation for data normalised to [0,1].

CAT: S cat (x, y) iff x i = y i for all i ∈ I I , where I ⊆ I represent sensitive categorical attributes. For Adult and German, we select the gender attribute. For Compas, its race. For Crime, we consider state. Lastly, for Health, we consider gender and age group.

NOISE-CAT: S noise-cat (x, y) = S noise ∪ S cat (x, y)
Further domain-specific similarities can be defined and handled by our approach by simply instantiating the underlying static analyzer with a suitable abstract domain.

Setup. We trained the SVMs used in our experiments with scikit-learn [START_REF] Pedregosa | Scikit-learn: Machine learning in Python[END_REF]. Hyperparameters were chosen by hit-and-trial and observing trends. For instance, Fig. 2 shows trends in balanced accuracy and individual fairness with different hyperparameters for SVMs with polynomial and RBF kernels trained on the Crime dataset. Individual fairness is calculated with respect to the NOISE-CAT similarity relation using the RAF+OH abstract domain. The plots show that balanced accuracy and individual fairness are inversely correlated and the change in fairness is steeper than accuracy. Similar trends occur for SVMs trained on the other datasets. The final chosen hyperparameters for each kernel for each dataset were those that lead to SVMs with high balanced accuracy. Our implementation, the datasets with preprocessing pipelines, our we could find substantially more counterexamples.

Feature Importance. We now compare our feature importance measure AFI with PFI (as implemented in sklearn.inspection with n_repeat = 10). As a representative example, we show in Table 2, a comparison on SVMs trained on the Compas dataset. For each SVM model, in line 'LB', we order the numerical features in the datasets (i.e., 'priors_count', 'juv_fel_count', etc.) based on the verified individual fairness score with respect to the NOISE perturbation (with = 0.3 in order to amplify the difference in score between the features). In lines 'AFI' and 'PFI' we show the order of these features based on the importance measured by AFI and PFI, respectively. We also indicate in parenthesis the time it took to compute these measures. We used the RAF+OH abstraction for AFI. We can see that AFI better correlates with model variance to feature perturbations. In fact, the correlation is perfect in the linear SVM case. In the polynomial SVM case, the lower individual fairness scores indicate that the abstraction loses precision and this explains why AFI is less accurate (but still better than PFI, at least in identifying the least important feature). Note also that AFI is computed in a small fraction of time compared to PFI. We show similar or better results for other datasets in Appendix A.2.

Finally, we recall that AFI can also measure the importance of tiers of a feature (cf. Section 4). Thus, it offers another way to detect potential bias issues starting from discrepancies between tier importances (e.g., we observed that the tier 'wife' of the 'relationship' feature of the Adult dataset results has a different importance from the tier 'husband').

Conclusion

We put forward a novel abstract feature importance measure based on an abstract interpretation for SVMs tailored for achieving a precise symbolic representation of one-hot encoded features. We showed that our abstraction is effective for verifying 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 ver-ify alternative or stronger fairness notions. We also aim to design quantitative verification methods to provide probabilistic guarantees on the behavior of SVM models.

A Appendix

A.1 Proofs

Proof of Theorem 4.3. We must show that X = γ OH k (a).

Since we required values in X to be the result of a one-hot encoding, values other than f, t cannot occur. We start by calling

F i = {x i |x ∈ X ∧ x i = f } and T i = {x i |x ∈ X ∧ x i =
t} the sets of false and true values occurring the i-esim component, for every 1 ≤ i ≤ k. We observe that F i can be either the singleton of f or the empty set, the latter if and only if the i-esim member of the tier is never false in X. The same is true for T i being either the singleton of t or the empty set.

We now show that X ⊆ γ OH k (a), that is, every element of the former also belongs to the latter. If X is the empty set condition is trivially satisfied. Otherwise, we consider a generic element x ∈ X. Since x is the result of a onehot encoding procedure, there exists 1 ≤ i ≤ k such that x i = t, while x j = f for every 1 ≤ j ≤ k, j = i. As a consequence, T i cannot be the empty set, and must be T i = {t}, similarily we obtain F j = {f } for every j = i. This implies that a i,t = t and a j,f = f , allowing to explicitly compute

γi (a) ={x ∈ R k |x i ∈ γ CP (a i,t )∧ ∀j = i : x j ∈ γ CP (a j,f )} ={x ∈ R k |x i ∈ γ CP (t) ∧ ∀j = i : x j ∈ γ CP (f )} ={x ∈ R k |x i ∈ {t} ∧ ∀j = i : x j ∈ {f }} ={x ∈ R k |x i = t ∧ ∀j = i : x j = f } ={x } which in turns implies x ∈ γi (a) ⊆ k j=1 γj (a) = γ OH k (a), hence X ⊆ γ OH k (a).
Last, we show that γ OH k (a) ⊆ X by arguing that every element of the former also belongs to the latter. If γ OH k (a) is the empty set implication is trivially satisfied, otherwise we consider a generic element x ∈ γ OH k (a). Since γ OH k (a) = k i=1 γi (a), there must exists some 1 ≤ z ≤ k such that x ∈ γz (a), which can be written as

γz (a) ={x ∈ R k |x z ∈ γ CP (a z,t ) ∧ ∀j = z : x j ∈ γ CP (a j,f )} ={x ∈ R k |x z ∈ γ CP (α CP (T z )) ∧ ∀j = z : x j ∈ γ CP (α CP (F j ))} if T z = ∅, or ∃j = z : F j = ∅ then γz (a) = ∅,
which is not acceptable and thus must not be considered. As a consequence, it must be T z = ∅ and ∀j = z : F j = ∅, which in turns implies T z = {t} and ∀j = z : F j = {f }.

This allows to rewrite

γz (a) ={x ∈ R k |x z ∈ γ CP (α CP (T z )) ∧ ∀j = z : x j ∈ γ CP (α CP (F j ))} ={x ∈ R k |x z ∈ γ CP (α CP ({t})) ∧ ∀j = z : x j ∈ γ CP (α CP ({f }))} ={x ∈ R k |x z ∈ γ CP (t) ∧ ∀j = z : x j ∈ γ CP (f )} ={x ∈ R k |x z ∈ {t} ∧ ∀j = z : x j ∈ {f }} ={x ∈ R k |x z = t ∧ ∀j = z : x j = f }
which is a singleton. Since x ∈ γz (a), we can write γz (a) = {x }. On the other hand, T z = {t} also implies ∃x ∈ X : x z = t. Moreover, it must be x j = f for all j = i, as x is the result of a one-hot encoding, hence x = x and x ∈ X, which leads to the conclusion that every γi (a) ⊆ X, hence γ OH k (a) ⊆ X.

Since both X ⊆ γ OH k (a) and γ OH k (a) ⊆ X hold at the same time, we can conclude that X = γ OH k (a) and a precisely X without loss of precision.

Proof of Theorem 4.5. It must be shown that, for any f : R → R and for any a

∈ OH k , f (γ OH k (a)) ⊆ γ OH k (f OH (a)). f (γ OH k (a)) = f k i=1 γi (a) = k i=1 f (γ i (a)) = k i=1 {f (x)|x i ∈ γ CP (a i,t )∧ ∀j = i : x j ∈ γ CP (a j,f )} = k i=1 {x|x i ∈ f (γ CP (a i,t ))∧ ∀j = i : x j ∈ f (γ CP (a j,f ))} ⊆ k i=1 {x|x i ∈ γ CP (f CP (a i,t ))∧ ∀j = i : x j ∈ γ CP (f CP (a j,f ))} = k i=1 γi (f OH (a)) = γ OH k (f OH (a))
Proof of Corollary 4.7. (i) By assuming no CP value occurs in a, then f (γ BC (a i,z )) = γ BC (f BC (a i,z )) for any 1 ≤ i ≤ k and z ∈ {f, t}. This equivalence can be exploited in proof of Th. 4.5, yielding f (γ OH k (a)) = γ OH k (f OH (a)).

(ii) We will prove the stronger property that analysis is complete and no CP values can be generated. Proof is by induction on the number n ∈ N of applications of functions f i . P (0) Due to Th.4.3, it is possible to abstract X with some a 0 ∈ OH k without loss of precision. Remark 4.4 also applies and guarantees that no CP can occur in a 0 . P (n) ⇒ P (n + 1) By inductive hypotheses we have an intermediate abstract value a n ∈ OH k which represents its concrete counterpart without loss of precision, and we also know that a n does not contain any CP values. We can therefore compute a n+1 = f OH k n+1 (a n ) and, due to Corollary 4.7, no loss of precision can occur in a n+1 . Also, by definition of f OH in Th.4.5, CP cannot be introduced unless already present in a n , which is not the case thanks to inductive hypotheses.

Alternatively, it is possible to consider f = f 1 • f 2 • . . . • f n and directly apply Corollary 4.7, although this appears more restrictive as it does not allow for composition with other complete transfer functions in between.

A.2 Additional Experimental Data

Table 3 shows accuracy, balanced accuracy, and individual fairness scores for SVMs with linear kernels (represented as L(reg. param.)), polynomial kernels (represented as P(reg. param, degree, base)), and RBF kernels (represented as R(reg. param, γ)). Individual fairness scores are computed with respect to the NOISE (N), CAT (C), and NOISE-CAT (NC) similarity relations. The table also compares results with and without the OH abstraction.

We show further comparisons between our proposed AFI and PFI in Table 4 andTable 5. We compute individual fairness scores with respect to the NOISE perturbation. We choose different values to amplify the difference in score between the features. Note the much better correlation of AFI with fairness scores than PFI. We do not report results for the Crime dataset as it has dozens of numerical features. PFI timed out after executing for several hours on Health. 4 42.4 37.2 94.8 97.9 95.4 97.5 P(0.01,3,3) 83.9 76.7 0.0 0.0 0.0 0.0 0.0 0.0 0.5 .03 0.5 0.5 0.03 0.5 Compas L(1) 64.7 64.1 99.5 94.9 95.5 99.5 94.9 95.5 99.5 94.9 95.5 99.5 94.9 95.5 R(0.05,0.01) 64.5 63.1 42.5 1.0 54.3 42.5 1.0 54.3 71.6 66.9 91.8 97.5 89.

  represented in its dual form by the function C T (z) sgn ( n i=1 (c i y i k(x i , z)) -b). Most common kernels are: (i) linear, where k(x, z) = x • z; (ii) polynomial, where k(x, z) = (x • z + c) p , for some hyperparameters c ∈ R and p ∈ N; (iii) radial basis function (RBF),

Figure 1 :

 1 Figure 1: Recursion while searching for counterexamples.

Figure 2 :

 2 Figure 2: Trends on hyperparameters for SVMs with polynomial (left) and RBF (right) kernels trained on Crime.

Figure 3 :

 3 Figure 3: Comparison of individual fairness using different abstract domains for SVMs trained on Crime.

  .5 91.3 90.6 99.4 96.1 95.5 99.4 91.3 90.6 99.4 96.1 95.5 99.4 R(0.1,0.01) 82.3 76.4 0.68 0.65 1.26 3.38 2.87 4.71 0.82 0.81 80.1 94.1 29.4 82.0 P(0.1,3,0.01) 71.0 61.0 0.0 0.0 .005 0.0 0.0 .005 0.03 0.02 6.62 0.03 0.02 6.62

  The One-Hot abstract domain for a k-dimensional one-hot encoded feature space is: OH k (CP × 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. 0, or true, i.e. 1. Given a ∈ OH k and a component i ∈ [1, k], let a i,f /t ∈ CP denote, resp., the first/second element of the i-th pair in a. The partial order of OH k is induced componentwise by CP , i.e., for all a, b ∈ OH k

Table 1 :

 1 Bounds on fairness with respect to the NOISE-CAT similarity relation using the RAF+OH abstraction. On the other hand, the gap is much wider in the other cases, notably for SVMs with polynomial kernels, mostly due to a lower precision of the abstraction. Using partitioning up to 3.125% of the original input size, yields similar upper bound values, which indicates the presence of few additional counterexamples. Only partitioning up to 0.1% of the original size input size,

		Linear	Polynomial		RBF
	Dataset LB	UB	LB	UB	LB	UB
	Crime	29.6 58.4 39.1 72.9 91.0 92.5
	Health	95.5 99.6 0.02 98.7 29.4 97.4
	Compas 94.9 94.9 0.09 71.4 89.3 93.0
	German 81.5 81.5 10.0 76.0 0.0	84.0
	Adult	91.6 0.03 89.5 92.2 95.4
	SVM models and experiment scripts will be made avail-
	able on GitHub upon publication of this work.
	Individual Fairness. We show a summary of individual
	fairness and balanced accuracy scores obtained for SVMs
	trained on the Crime dataset in Fig. 3. We can see that
	the RAF abstraction typically outperforms intervals, and
	our OH abstraction always yields equal or higher individ-
	ual fairness score. The full raw data for each dataset shows
	the same trend. It is shown in Table 3 in Appendix A.2.
	In Table 1, for each dataset, we show bounds on individual
	fairness with respect to the NOISE-CAT similarity rela-
	tion using the RAF+OH abstraction: the lower bound is the
	verified individual fairness score (cf. Section 5) and the up-
	per bound is the estimate obtained with our counterexam-
	ple search without input partitioning (cf. Section 6), e.g.,
	an upper bound of 76% indicates that we found concrete
	counterexamples to individual fairness for 48 over 200 test
	data points. The gap between bounds is quite narrow for
	linear SVMs as well as for SVMs with RBF kernels trained
	on the Crime, Compas, and Adult datasets: in these cases,
	our RAF+OH abstraction is precise and our counterexam-
	ple search heuristic is strong.

Table 2 :

 2 Comparison of our AFI and PFI on Compas.

	Linear	LB 87.2 93.3 97	97.1 97.7 99	100
	AFI (0.225s) 1	2	3	4	5	6	7
	PFI (1976s) 1	2	5	4	3	7	6
	Polynomial LB 1.23 1.32 1.32 12.5 16.2 34.5 48.7
	AFI (0.199s) 4	6	5	3	2	1	7
	PFI (5166s) 3	1	5	7	4	2	6
	RBF	LB 69	71.5 73.7 74	75.4 76	76.7
	AFI (0.267s) 1	2	4	3	5	6	7
	PFI (11776s) 2	1	4	3	5	7	6

Table 3 :

 3 Accuracy, balanced accuracy, and individual fairness scores for SVMs trained on each dataset.

	Dataset Kernel	Acc.	Bal. Acc	C	Interval NC N	C	Interval OH NC N	C	RAF NC N	C	RAF OH NC N
		L(1)	84.6 75.6 95.2 91.6 96.5 95.2 91.6 96.5 95.2 91.6 96.5 95.2 91.6 96.5
	Adult	R(0.05,0.01) 83.8 72.0 2.8 0.0 2.4 2.8 0.0 2.

Table 4 :

 4 Comparison of our AFI and PFI on Adult.

	Linear ( = 0.3)	LB	83.4	96	98.37 98.37 98.44 99.2
		AFI 1	2	3	4	5	6
		PFI 1	2	6	4	5	3
	Polynomial ( = 0.1) LB	23.2	23.9	24.5	28.3	29.5	95.2
		AFI 2	5	6	3	4	1
		PFI 6	5	4	2	3	1
	RBF ( = 0.3)	LB	50.3	53.5	56.4	56.6	57.7	57.9
		AFI 1	2	3	4	5	6
		PFI 2	1	4	5	6	3

Table 5 :

 5 Comparison of our AFI and PFI on German.

	Linear ( = 0.3)	LB 78	83.5 87	89.5 90	90	98.5 98.5 99.5
		AFI 1	2	3	4	5	6	7	8	9
		PFI 3	7	1	6	4	2	8	5	9
	Polynomial ( = 0.3) LB 83	86	86.5 87	92.5 92.5 93	94.5 94.5
		AFI 1	6	5	3	2	9	4	7	8
		PFI 2	3	4	5	9	1	6	7	8
	RBF ( = 0.1)	LB 54	54	54.5 55	56.5 57	57.5 58	58.5
		AFI 1	2	3	4	5	6	8	7	9
		PFI 1	3	7	9	4	5	8	2	6

Acknowledgements

Francesco Ranzato has been partially funded by the Italian MIUR, under the PRIN2017 project no. 201784YSZ5 "AnalysiS of PRogram Analyses (ASPRA)", by Facebook Research, under a "Probability and Programming Research Award", by an Amazon Research Award for "AWS Automated Reasoning", and by a WhatsApp Research Award for "Privacy aware program analysis".