Sönke Beck
email: s.beck@gsi.de

Brian Kootte

Irene Dedes

Timo Dickel

Ania A Kwiatkowski

Eleni Marina Lykiardopoulou

Wolfgang R Plaß

Moritz P Reiter

Corina Andreoiu

Julian Bergmann

Thomas Brunner

Dominique Curien

Jens Dilling

Jerzy Dudek

Eleanor Dunling

Jake Flowerdew

Abdelghafar Gaamouci

Leigh Graham

Gerald Gwinner

Andrew Jacobs

Renee Klawitter

Yang Lan

Erich Leistenschneider

Nikolay Minkov

Victor Monier

Ish Mukul

Stefan F Paul

Christoph Scheidenberger

Robert I Thompson

James L Tracy

Michael Vansteenkiste

Hua-Lei Wang

Michael E Wieser

Christian Will

Jie Yang

Mass measurements of neutron-deficient Yb isotopes and nuclear structure at the extreme proton-rich side of the N =82 shell

High-accuracy mass measurements of neutron-deficient Yb isotopes have been performed at TRI-UMF using TITAN's multiple-reflection time-of-flight mass spectrometer (MR-TOF-MS). For the first time, an MR-TOF-MS was used online simultaneously as isobar separator and as mass spectrometer, extending the measurements to two isotopes further away from stability than otherwise possible. The ground state masses of 150,153 Yb and the excitation energy of 151 Yb m were measured for the first time. As a result, the persistence of the N =82 shell with almost unmodified shell gap energies is established up to the proton dripline. Furthermore, the puzzling systematics of the h 11/2 -excited isomeric states of the N =81 isotones are unraveled using state-of-the-art mean field calculations.

Experimental and theoretical studies of exotic nuclei, i.e., very short-lived nuclei far away from the valley of stability in the chart of the nuclides, present a unique and important way to gain general understanding of the atomic nucleus and the governing interactions of its constituents. Exotic nuclei reveal novel properties, unknown in more stable nuclei, such as nuclear halos and skins, and exotic decay modes [1,2]. Deeper understanding of nuclear structure hinges on theoretical models. Extending experimental data towards the driplines is decisive for testing prediction capacities of theories, estimating the model uncertainties and thus for improving models and theories [3].

One striking effect, which may occur in exotic nuclei, is a change in the nuclear shell structure towards the proton or neutron driplines; shells can weaken or disappear, and new magic numbers appear [4,5]. On the neutron-rich side of the nuclear chart, shell closures have been shown to vanish far from stability for the neutron numbers N =20 and N =28 [6,7], and new shell closures have been found for N =32 and N =34 [8][9][10][11][12][13][14][START_REF] Leistenschneider | The LEBIT Collaboration and the[END_REF]. The N =82 shell closure has been studied for neutron-rich nuclei down to Cd [16][17][18]. The data in the neutron-deficient region are incomplete, and the evolution of the N =82 shell towards the proton dripline is not known. In this work, the N =82 shell closure is investigated by mass measurements up to the proton dripline.

Series of nuclear isomers are known to occur near shell closures. A unique sequence of isomers exists in the N =81 isotones with even Z, ranging from 131 Sn to 149 Er [19,[START_REF]From ENSDF database as of[END_REF]. This sequence is remarkable, because the excitation energies of these J π =11/2 -isomers stay approximately constant at 750 keV between 139 Ce and 149 Er [START_REF] Ketelle | [END_REF][22][23][24][25], over a range of eleven isotones. Such an effect is unique for isomers throughout the chart of the nuclides, and its origin has been considered enigmatic since its discovery more than 60 years ago [22,25,26]. The dependence of energy vs. total angular momentum within non-collective excitation regimes is usually strongly irregular according to nuclear mean-field theory [27]. Yet here, the experimental data of the series are extended, and the origin of the constant excitation energies is explained using state-of-the-art mean-field calculations.

A major challenge for experiments with exotic nuclei at radioactive ion beam facilities is isobaric contamination. Nuclei closer to stability and molecules are usually produced with rates many orders of magnitude higher than those of the nuclei of interest and hamper measurements of the exotic nuclei. Recently, multiple-reflection time-offlight mass spectrometers (MR-TOF-MS) [28,29] have been established as isobar separators [30,31] and even isomer separators [32]. They feature very high mass separation powers of several 10 5 and short cycle times, enabling access to very short-lived (≈ ms) nuclides and high ion rates (10 6 ions/s). MR-TOF-MS can also be used for direct mass measurements of exotic nuclei [12,[33][34][35] and diagnostics purposes [36][37][38]. In an MR-TOF-MS, ions are cooled in a radio-frequency (RF) ion trap (injection trap), injected into a time-of-flight (TOF) analyzer, in which the ions are stored between two ion reflectors and dispersed in TOF according to their mass-to-charge ratios. Mass separation is then achieved by the subsequent removal of the unwanted ions using a fast-switching deflector, such as a Bradbury-Nielsen gate [30], a pulsed drift tube [39], or one of the reflectors [40]. A novel method for mass separation in an MR-TOF-MS is the dynamical re-trapping of the ions in the injection trap after the TOF dispersion procedure [41]. This re-trapping technique is highly mass-selective; the ions of interest can be stored, while other ions are removed. In contrast to the other methods, it allows an MR-TOF-MS to act as an isobar separator for its own mass measurements. It has been developed for the MR-TOF-MS [42,43] at TRIUMF's Ion Trap for Atomic and Nuclear Science (TI-TAN) [44], but it could also be used to add one or several stages of isobar separation to mass measurements in other MR-TOF-MS world-wide.

In this work, mass-selective re-trapping has been employed for the first time on-line. High-accuracy mass measurements of neutron-deficient Yb isotopes were performed using TITAN's MR-TOF-MS. The nuclei were produced in spallation reactions at the ISAC facility [45] by impinging a 480 MeV proton beam with a current of 25 to 45 µA from the TRIUMF cyclotron onto a Ta target. Yb atoms that left the target were ionized by the TRI-UMF resonant ionization laser ion source TRILIS [46], using a two-step resonant laser excitation scheme into a high-lying Rydberg state [47,48]. Ions were extracted and separated using ISAC's high-resolution mass separator [49]

(J π = 1/2 + ) 151m Yb + (J π = 11/2 -) (c)
Re-trapping on isobaric beam, consisting mostly of singly-charged Eu, Dy, Ho, Er, Tm, Yb, BaF and CeO ions, was transported to the TITAN facility, cooled and bunched in the TITAN RF quadrupole (RFQ) cooler buncher [50] and injected into the MR-TOF-MS. There, the ions were transported to the injection trap, cooled and injected into the TOF analyzer, where they performed one time-focus shift turn [51] and about 330 isochronous turns (IT), corresponding to a TOF of about 8 ms. Then the ions were ejected onto a detector. A mass-resolving power of about 270,000 (FWHM) was achieved. For measurements, in which the isobaric contamination was too high to observe Yb ions, the MR-TOF-MS was first used as an isobar separator: after TOF dispersion of the ions in the analyzer, the ions of interest were re-trapped in the injection trap. Then, they were re-cooled and injected again into the analyzer for the subsequent mass measurement procedure. The overall cycle time was 20 ms. After each mass measurement, a spectrum was taken without resonant laser ionization to verify the identification of the Yb ions.

Figure 1 shows mass spectra measured without and with re-trapping. The mass separation power amounts to 35,000. To avoid deterioration of the mass measurement accuracy due to ion-ion interactions, the beam was attenuated in the ISAC beam line to about one ion per species per cycle detected in the MR-TOF-MS. Using mass-selective re-trapping, the rate of contaminant ions was reduced by at least three orders of magnitude, and the rate of incoming ions could therefore be increased by a corresponding factor by increasing the proton current on the target and by reducing the attenuation. As shown in Fig. 1, the nuclides 151 Tm and 151 Yb could only be measured with re-trapping. Similarily, the measurement of 150 Yb required re-trapping. The re-trapping increases the dynamic range of the measurement to five orders of magnitude, a value which is rarely achieved in mass spectrometry. It also reduces the total number of ions that reach the detector; this minimizes the background resulting from radioactivity implanted on the detector.

For the analysis of the data, the recorded TOF data were converted to mass data using an isobaric ion species present in the mass spectrum to provide a time-resolved calibration [53]. The mass spectra were analyzed by fitting hyper-EMG functions [52] to the unbinned mass data using weighted maximum likelihood estimation [53]. The isotopes of interest and their respective calibrants are listed in Table I. The mass values of the calibrants were taken from the Atomic Mass Evaluation AME2020 [54]. The dominating contribution to the systematic uncertainty are shifts in the TOF due to voltage ringing caused by the switching of the reflector voltages [START_REF] Will | TITAN's Multiple-Reflection Time-of-Flight Mass Spectrometer and Isobar Separator -Characterization and First Experiments[END_REF][START_REF] Reiter | [END_REF]. Its relative value amounts to 3 × 10 -7 .

The ground state masses of eight Yb isotopes were measured (Table I). For 154-157 Yb, the masses were already well known, and the present results are in good agreement with the AME2020 [54]. The masses of 151 Yb and 152 Yb were measured directly for the first time, and their uncertainties could be reduced by a factor of three. The masses of 150 Yb and 153 Yb were measured for the first time.

With these results, the N =82 shell closure can be examined in the extreme proton-rich region. Figure 2 shows the empirical two-neutron-shell gap ∆ 2n (Z, N ) = FIG. 2. Evolution of the two-neutron-shell gap ∆2n at N =82 as a function of the proton number Z and predictions of the theoretical models HFB21 [57], UNEDF0 [58], and FRDM2012 [59]. Experimental data are from the AME2020 [54] and this work. Regions of proton-unbound nuclides are indicated [54,60]. Most error bars are hidden in the symbols, lines are drawn to guide the eye.

S 2n (Z, N )-S 2n (Z, N +2), where S 2n (Z, N ) = B(Z, N )- B(Z, N -2)
is the two-neutron separation energy and B(Z, N ) is the binding energy, for different N =82 isotones. The two-neutron-shell gap shows pronounced maxima when crossing closed shells. From the proton shell closure at Z=50, the two-neutron-shell gap decreases, though from Z=58 onward, the reduction is only weak. So far, the most proton-rich nuclide, for which ∆ 2n was known, was 150 Er (Z=68). The newly determined value for 152 Yb (Z=70), despite being the lowest value found so far, clearly establishes that the shell persists with almost unmodified shell gap energy up to the proton dripline. The dripline is expected to lie between 152 Yb and 153 Lu (Z=71) [54,60]. The experimental data are compared with different theoretical models, the macroscopic-microscopic finite-range droplet model FRDM(2012) [59], and two microscopic models, the Hartree-Fock-Bogoliubov model with BSk21 Skyrme interaction (HFB-21) [57], and the energy density functional UNEDF0 [58]. Although HFB-21 comes closest to the measured values, in particular for the most protonrich isotones, none of these models fully reproduces the experimental trend. This fact highlights the importance of measurements for model improvements and model error estimates. Furthermore, the mass of 153 Yb provides an anchor point for the α decay chains from 173 Hg to 153 Yb and from 170 Au to 154 Lu and thus determines the absolute masses of nine more nuclides and fix the mass surface in this region of the chart of nuclides [61,62].

A J π =11/2 -isomer has been observed in 151 Yb previously [63][64][65], but in this work its excitation energy was measured for the first time (Fig. 1c). In total, 460 events were detected with an isomer-to-ground state ratio of 11.1(3.1), corresponding to 38 events in the ground state. The measured excitation energy is 679(105) keV; it falls in line with the excitation energy of about 750 keV of J π =11/2 -isomers in the even-Z, N =81 isotones from 139 Ce onward. The experimental data are shown in Fig. 3a. The systematic trend suggests the assignment of the measured Yb isomer as J π =11/2 - [25,64]. The J π =1/2 + , 3/2 + , and 11/2 -states are neutron-hole states below the closed shell and can be associated with the s 1/2 , d 3/2 , h 11/2 orbitals, respectively. The fact that the excitation energies are constant has not been explained so far [22,25,26].

In order to resolve this long-standing riddle, mean-field calculations were performed. The phenomenological, deformed Woods-Saxon Hamiltonian in its so-called universal parametrization, for which its parameters are fixed throughout the chart of nuclides, was employed [66][67][68][69][70]. Its use is supported by the fact that it has been successfully applied in numerous nuclear structure calculations. Furthermore, it has recently been tested extensively from the point of view of prediction uncertainties and elimination of parametric correlations [71], which are known to destroy -often completely -model prediction capacities [72].

Potential-energy calculations using the Strutinsky method [73] were performed for all even-Z isotones from Sn to Hf. Partial results are shown in Fig. 3b. The J π =3/2 + ground-states with even-Z from Sn to Gd can be associated with d 3/2 , and J π =1/2 + with s 1/2 orbitals from Dy to Hf. The latter orbital does not couple with the spin-orbit field at all, whereas the former does so only very weakly, so that their crossing at Gd and Dy reflects mainly the evolution of the central potential with Z. FIG. 4. Single proton energies as functions of the quadrupole deformation α20, calculated using the Woods-Saxon Hamiltonian. The numbers in the circles represent the numbers of protons that can fill the levels below the circles. Note a neardegeneracy of 6 levels at small prolate deformations, indicated with oval curve, cf. Nd-Hf evolution in Fig. 3 Calculations show the impact of the shell closures at Z=50 and N =82, in that the ground-state equilibrium shapes remain spherical for the Sn, Te, Xe and Ba isotones, though the potential stiffness decreases. They predict non-spherical (oblate) quadrupole equilibrium shapes for 139 Ce and heavier isotones, while predicting small but increasingly prolate shapes for the J π =11/2 - isomers. This evolution coincides with the evolution of the energies of the isomers, which increase from about 40 keV in 131 Sn to about 750 keV in 139 Ce, i.e., within the zone of spherical ground-states. Stabilization at about 750 keV, starting with Ce (Z=58), coincides with the mean-field predictions of the slightly prolate quadrupole shapes with quadrupole deformations of α 20 ≈ 0.10 at the J π =11/2 -isomeric energy minima. The calculations also show that the trend of constant J π =11/2 -isomer excitation energies continues for 153 Hf.

Below spherical closed neutron shells (here N =82), Kisomers usually correspond to nucleonic configurations with maximum alignment of the angular-momentum j, i.e. with projection m j = j, at slightly prolate quadrupole shapes [27]. Calculations suggest that h 11/2isomers have typical prolate deformations of α 20 ≈ 0.1. The underlying stabilizing structural element is the very high single-nucleonic (proton) density at α 20 ≈ 0.12 (Fig. 4), where six proton levels lie very close together. According to the Strutinsky shell-correction approach, the corresponding shell-energies are strongly negative and nearly constant, stabilizing the corresponding shapes with isomer energies at about 800 keV.

In summary, high-accuracy mass measurements of neutron-deficient Yb isotopes have been performed. They were enabled by the first-ever simultaneous online use of an MR-TOF-MS as isobar separator and as mass spectrometer, employing mass-selective re-trapping, and thus extending the measurements to two isotopes further away from stability than otherwise possible. The persistence of the N =82 shell with almost unmodified shell gap energies was established up to the expected location of the proton dripline. Furthermore, the results extend the knowledge of excitation energies of the unique J π =11/2 - isomers in even-Z, N =81 isotones. The structural properties of this sequence were analyzed, and the constant excitation energies over a range of 13 isotones was explained. Application of the mass-selective re-trapping is not limited to TITAN, but could also be employed with other MR-TOF-MS world-wide to extend the reach of mass measurements with these devices by two or more isotopes towards exoticity. Since its first use in this experiment, this technique is now regularly applied in TI-TAN's MR-TOF-MS.

FIG. 1 .

 1 FIG.1. Mass spectra at mass-to-charge ratio 151 u/e (a) without re-trapping, (b) with re-trapping set for 151 Yb, (c) zoom to the Yb region with re-trapping, showing the 151 Yb nuclear ground and isomeric state. The ions performed 335 IT in the analyzer, corresponding to a TOF of 8.14 ms. The curves represent hyper-EMG[52] fits to the data. Note the different abundance scales. For both spectra (a) and (b) the measurement time was 760 s; for (b) the incoming rate was increased; (c) contains all data taken during about 3 h with different proton currents on the target.

FIG. 3 .

 3 FIG. 3. (a) Top panel: Measured excitation energies of isomers in the even-Z N =81 isotones from Sn to Yb [19, 25]. The value for 151 Yb results from the present work. Most error bars are invisible within the scale of the figure. Note the constancy of the h 11/2 excitation energy from Ce to Yb. (b) Bottom panel: Corresponding results obtained using mean-field calculations with universal parametrization of the Woods-Saxon Hamiltonian. From Nd (Z=60) to Hf (Z=72), the filled proton levels are near-degenerate, cf. Fig. 4.

  at a mass separation power of about 2000. The

	10 4	(a)	151	Eu +			Re-trapping off
	10 3
	10 1 10 2			151	Dy +	151 Ho + 151 Er +
	10 0
	10 3	(b)	151 Eu +			Re-trapping on
	10 1 10 2			151 Dy +	151	Ho + 151 Er +	151 Tm +	151 Yb + 151m Yb +
	10 0
		150.92	150.93	150.94	150.95
			151 Yb +

  Yb 155 Eu + -50514(45) -50503(17) -11(48) 154 Yb 138 Ce 16 O + -49934(45) -49932(17) -2(48) 153 Yb 153 Dy + -47102(46) --152 Yb 136 Ce 16 O + -46061(46) -46270(150) 209(157)

	Nuclide Calibrant METITAN	MEAME20	∆ME
		(keV/c 2 )	(keV/c 2 ) (keV/c 2 )
	157 Yb	157 Tm + -53395(54) -53420(11) 25(55)
	156 Yb	156 Tm + -53331(55) -53266(9) -65(56)
	155 151 Yb	151 Er + -41297(114) -41540(300) 243(321)
	151 Yb m	151 Er + -40617(49)	-	-
	150 Yb	150 Dy + -38635(44)	-	-
	TABLE I. List of measured mass excess values of Yb isotopes,
	METITAN. Mass excess values from the AME2020, MEAME20,
	and the deviation ∆ME=METITAN-MEAME20 [54], are given
	for comparison, where available.

We would like to thank J. Lassen and the TRILIS ion source group for the excellent beam conditions. This work was supported by the German Research Foundation (DFG), grant No. SCHE 1969/2-1, by the German Federal Ministry for Education and Research (BMBF), grant No. 05P16RGFN1 and 05P19RGFN1, by the Hessian Ministry for Science and Art through the LOEWE Center HICforFAIR, by the JLU and GSI under the JLU-GSI strategic Helmholtz partnership agreement, by the Polish National Science Centre under Contract No. 2016/21/B/ST2/01227, by the Natural Sciences and Engineering Research Council of Canada (NSERC) under grants and RGPAS-2018-522453 and by the UKRI Science and Technology Facilities Council (STFC) grant No. ST/P004008/1. Support from the National Natural Science Foundation of China, grant No. 11975209, and the Physics Research and Development Program of Zhengzhou University, grant No. 32410017 are acknowledged. TRIUMF receives federal funding via NRC-CNRC. N.M. acknowledges the support by the FAIR Phase-0 project and by Bulgarian NSF contract KP-06-N48/1. E.D. acknowledges the support by the Canada-UK Foundation.


Francesco Ranzato

Marco Zanella

Fairness-Aware Training of Decision Trees by Abstract Interpretation

We study the problem of formally verifying individual fairness of decision tree ensembles, as well as training tree models which maximize both accuracy and individual fairness. In our approach, fairness verification and fairness-aware training both rely on a notion of stability of a classifier, which is a generalization of the standard notion of robustness to input perturbations used in adversarial machine learning. Our verification and training methods leverage abstract interpretation, a well-established mathematical framework for designing computable, correct, and precise approximations of potentially infinite behaviors. We implemented our fairness-aware learning method by building on a tool for adversarial training of decision trees. We evaluated it in practice on the reference datasets in the literature on fairness in machine learning. The experimental results show that our approach is able to train tree models exhibiting a high degree of individual fairness with respect to the natural state-of-theart CART trees and random forests. Moreover, as a by-product, these fairness-aware decision trees turn out to be significantly compact, which naturally enhances their interpretability.

Introduction

Nowadays, machine learning (ML) software assists or even automates decisions with far-reaching socio-economic impact, e.g., for credit scoring [START_REF] Amir | Consumer Credit-Risk Models via Machine-Learning Algorithms[END_REF], recidivism prediction [START_REF] Chouldechova | Fair Prediction with Disparate Impact: A Study of Bias in Recidivism Prediction Instruments[END_REF], or hiring tasks [START_REF] Schumann | We Need Fairness and Explainability in Algorithmic Hiring[END_REF]. The widespread and ever-increasing adoption of ML-based decision-making tools raises concerns on their fairness properties [START_REF] Barocas | Big Data's Disparate Impact[END_REF][START_REF] Mehrabi | A survey on bias and fairness in machine learning[END_REF]. A number of recent cases have indeed shown that such tools may reproduce, or even reinforce, bias directly or indirectly present in the training data [START_REF] Buolamwini | Gender shades: Intersectional accuracy disparities in commercial gender classification[END_REF][START_REF] Kay | Unequal representation and gender stereotypes in image search results for occupations[END_REF][START_REF] Obermeyer | Dissecting racial bias in an algorithm used to manage the health of populations[END_REF]. For this reason, the Artificial Intelligence Act [START_REF]Proposal for a Regulation Laying Down Harmonised Rules on Artificial Intelligence (Artificial Intelligence Act)[END_REF] -a first legal framework on machine learning software proposed by the European Commission in April 2021 -imposes strict requirements to minimize the risk of discriminatory outcomes. Our work anticipates the need for methods and tools to facilitate the development of machine learning software that complies with this newly proposed regulation.

Several fairness verification and bias mitigation approaches for machine learning systems have been proposed in recent years, e.g., [START_REF] Aghaei | Learning optimal and fair decision trees for non-discriminative decision-making[END_REF][START_REF] Grari | Achieving Fairness with Decision Trees: An Adversarial Approach[END_REF][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][START_REF] Yurochkin | Training individually fair ML models with sensitive subspace robustness[END_REF][START_REF] Bilal Zafar | Fairness beyond disparate treatment & disparate impact: Learning classification without disparate mistreatment[END_REF] among the others. However, most works focus 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][START_REF] Yurochkin | Training individually fair ML models with sensitive subspace robustness[END_REF] or on group-based notions of fairness [START_REF] Grari | Achieving Fairness with Decision Trees: An Adversarial Approach[END_REF][START_REF] Bilal Zafar | Fairness beyond disparate treatment & disparate impact: Learning classification without disparate mistreatment[END_REF], e.g., demographic parity [START_REF] Dwork | Fairness through awareness[END_REF] or equalized odds [START_REF] Hardt | Equality of opportunity in supervised learning[END_REF]. These notions of group-based fairness require some form of statistical parity (e.g., between positive outcomes) for members of different protected groups (e.g., gender or race). On the other hand, they do not provide guarantees for individuals or other subgroups. By contrast, in this paper we focus on individual fairness [START_REF] Dwork | Fairness through awareness[END_REF], which intuitively requires that similar individuals in the population receive similar outcomes, and on decision tree ensembles [START_REF] Breiman | Random Forests[END_REF][START_REF] Jerome H Friedman | Greedy Function Approximation: A Gradient Boosting Machine[END_REF], which are commonly used for tabular datasets since they are easily interpretable ML models with high accuracy rates.

Contributions

We propose an approach for verifying individual fairness of decision tree ensembles, as well as for training tree models which maximize both accuracy and individual fairness.

Our methodology is based on the well-established framework of abstract interpretation [START_REF] Cousot | Principles of Abstract Interpretation[END_REF][START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Rival | Introduction to Static Analysis: An Abstract Interpretation Perspective[END_REF] for designing computable, correct, and precise overapproximations of model computations. In this approach, model computations are over-approximated using an abstract domain, which defines a symbolic abstract representation of the concrete quantities being manipulated. Our technique over-approximates computations over input space regions containing similar individuals, and is fully parametric in the choice of the underlying abstract domain. More precisely, we use a product of two abstract domains:

(a) the well-known numerical abstract domain of hyper-rectangles (also known as boxes or intervals) [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], that represents exactly the standard notion of similarity between individuals based on the ∞ distance metric, and does not lose precision for the univariate split rules of type x i ≤ k, with x i feature and k threshold, the most common split rules used in decision trees;

(b) a specific relational abstract domain which is able to represent precisely one-hot encoded categorical features, such as a feature color ∈ {white, black} which is one-hot encoded by color white , color black ∈ {0, 1}.

Our Fairness-Aware Tree Training method, called FATT, is designed as an extension of Meta-Silvae [START_REF] Ranzato | Genetic adversarial training of decision trees[END_REF], a learning methodology for ensembles of decision trees based on a genetic training algorithm, which is able to train a decision tree for maximizing both its accuracy and its robustness to adversarial perturbations. Meta-Silvae in turn leverages a verification tool for robustness properties of decision trees based on abstract interpretation [START_REF] Ranzato | Abstract interpretation of decision tree ensemble classifiers[END_REF]. We demonstrate the effectiveness of our method FATT in training accurate and fair models on the standard datasets used in the literature on fairness in machine learning. Overall, the experimental results show that our fairness-aware tree models are on average between 35% and 45% more fair than naturally trained decision tree ensembles at an average cost of -3.6% of accuracy. Moreover, it turns out that our tree models are orders of magnitude more compact and thus naturally easier to interpret. Finally, we show how our fairness-aware models can be used as "hints" for setting the size and shape hyper-parameters (i.e., maximum tree depth and minimum number of samples per leaf) when training standard decision tree models. As a result, this hint-based strategy is capable to output models that are about 20% more fair and just about 1% less accurate than standard models.

Related Work

The most related work to ours is by Aghaei et al. [START_REF] Aghaei | Learning optimal and fair decision trees for non-discriminative decision-making[END_REF], Raff et al. [START_REF] Raff | Fair forests: Regularized tree induction to minimize model bias[END_REF] and Ruoss et al. [START_REF] Ruoss | Learning certified individually fair representations[END_REF].

By relying on the mixed-integer optimization learning approach by Bertsimas and Dunn [START_REF] Bertsimas | Optimal classification trees[END_REF], Aghaei et al. [START_REF] Aghaei | Learning optimal and fair decision trees for non-discriminative decision-making[END_REF] put forward a framework for training fair decision trees for classification and regression. The experimental evaluation shows that this approach mitigates unfairness as modeled by their notions of disparate impact and disparate treatment at the cost of a significantly higher training computational cost. Their notion of disparate treatment is distance-based and thus akin to individual fairness with respect to the nearest individuals in a given dataset (e.g., the k-nearest individuals). In contrast, we consider individual fairness with respect to the nearest individuals in the input space, thus including individuals that are not necessarily part of a given dataset.

Raff et al. [START_REF] Raff | Fair forests: Regularized tree induction to minimize model bias[END_REF] propose a regularization-based approach for training fair decision trees as well as fair random forests. They consider both group fairness as well as individual fairness with respect to the k-nearest individuals in a given dataset, similarly to Aghaei et al. [START_REF] Aghaei | Learning optimal and fair decision trees for non-discriminative decision-making[END_REF]. In their experiments they use a subset of the datasets that we consider in our evaluation (i.e., the Adult, German, and Health datasets). Our fair models have higher accuracy than theirs (i.e., between 2% and 5.5%) for all but one of these datasets (Health dataset). Interestingly, their models (in particular those with worse accuracy than ours) often have accuracy on par with a constant classifier due to the highly unbalanced label distribution of the datasets. Unfortunately, their tool does not appear to be available for further experimental comparison.

Finally, Ruoss et al. [START_REF] Ruoss | Learning certified individually fair representations[END_REF] have proposed an approach for learning individually fair data representations and training neural networks (rather than decision tree ensembles as we do) that satisfy individual fairness with respect to a given similarity notion. We use the same notions of similarity in our experiments (cf. Section 6.1).

More broadly, our work fits into the research ecosystem that is nowadays forming around the use of formal methods for the verification of machine learning software. We refer to Liu et al. [START_REF] Liu | Algorithms for verifying deep neural networks[END_REF] and Urban et al. [START_REF] Urban | A Review of Formal Methods applied to Machine Learning[END_REF] for recent surveys of this field.

The rest of the paper is organized as follows. In Section 2 we recall some basic notions on decision tree ensembles and abstract interpretation, while Section 3 provides our setting of individual fairness. In Section 4 we describe our formal verification method of the individual fairness of tree ensembles, which is then exploited in Section 5 by the fairness-aware tree training algorithm FATT. Section 6 describes our implementation of FATT and the results of our experimental evaluation. Section 7 concludes.

Background

Classifiers

Given an input space X ⊆ R d of numerical vectors and a finite set of labels L = {y 1 , . . . , y m }, a classifier C : X → ℘ + (L), where ℘ + (L) is the set of all nonempty subsets of L, associates at least one label to every input in X. A training algorithm takes as input a dataset D ⊆ X × L and outputs a classifier C D : X → ℘ + (L) which optimizes a given objective function, e.g., the Gini index or the entropy-based information gain for decision trees.

Categorical features can be converted into numerical ones by one-hot encoding, where a single feature with k ≥ 2 possible distinct categories {c 1 , ..., c k } is replaced by k new binary features with numerical values in {0, 1}. Then, each value c j of the original categorical feature is represented by a bit-value assignment to the new k binary features in which the j-th feature is set to 1 and the remaining k -1 binary features are set to 0.

Classifiers can be evaluated and compared through several metrics. A basic metric is accuracy on a test dataset: given a ground truth test dataset T ⊆ X × L, the accuracy of a classifier C on T is

acc T (C) |{(x, y) ∈ T | C(x) = {y}}| |T | .
According to a growing belief [START_REF] Goodfellow | Making Machine Learning Robust Against Adversarial Inputs[END_REF], however, accuracy is not enough in machine learning, since robustness to adversarial inputs of a ML classifier may significantly affect its safety and generalization properties [START_REF] Carlini | Towards Evaluating the Robustness of Neural Networks[END_REF][START_REF] Goodfellow | Making Machine Learning Robust Against Adversarial Inputs[END_REF]. Given an input perturbation modeled by a function P : X → ℘(X), a classifier C :

X → ℘ + (L)
is stable [START_REF] Ranzato | Abstract interpretation of decision tree ensemble classifiers[END_REF] on the perturbation attack P (x) of x ∈ X when C consistently assigns the same label(s) to every attack ranging in P (x), i.e., stable(C, x, P ) ⇔ ∀x ∈ P (x) :

C(x ) = C(x). (1)
When the sample x ∈ X has a ground truth label y x ∈ L, robustness of C on x for attacks in P (x) boils down to stability, i.e. stable(C, x, P ) holds, together with correct classification, i.e. C(x) = {y x } holds. The most common example of perturbation is induced by the ∞ norm such that ||x|| ∞ = max{x 1 , ..., x d }, where a given input x ∈ X is perturbed by considering those vectors x ∈ X such that the ∞ norm of x-x is less than or equal to a given threshold τ ∈ R ≥0 , i.e., this perturbation is defined by

P ∞ (x) {x ∈ X | ||x -x || ∞ ≤ τ }.

Decision Trees and Tree Ensembles

We consider standard decision tree classifiers commonly referred to as CARTs (Classification And Regression Trees) [START_REF] Leo Breiman | Classification and Regression Trees[END_REF]. A decision tree t : X → ℘ + (L) is defined inductively. A base tree t is a single leaf λ storing a (normalized) frequency distribution of labels for the samples of the training dataset, hence λ ∈ [0, 1] |L| , or, equivalently, λ : L → [0, 1]. Some algorithmic rule converts this frequency distribution into a set of labels, typically as arg max y∈L λ(y) ∈ ℘ + (L).

A composite tree t is Γ(split, t l , t r ), where split : X → {tt, ff } is a Boolean split criterion for the internal parent node of its left and right subtrees t l and t r , respectively; thus, for all x ∈ X, t(x) if split(x) then t l (x) else t r (x). Although split rules can be of any type, most common decision trees employ univariate hard splits of type split(x) x i ≤ k, for some feature i ∈ [1, d] and threshold k ∈ R.

Tree ensembles, also known as forests, are sets of decision trees which together contribute to formulate a unique classification output. Training algorithms as well as methods for computing the final output label(s) vary among different tree ensemble models. Random forests (RFs) [START_REF] Breiman | Random Forests[END_REF] are a major instance of tree ensemble where each tree of the ensemble is trained independently from the other trees on a random subset of the features. Gradient boosted decision trees (GBDTs) [START_REF] Jerome H Friedman | Greedy Function Approximation: A Gradient Boosting Machine[END_REF] represent a different training algorithm where an ensemble of trees is incrementally built by training each new tree on the basis of the data samples which are mis-classified by the previous trees. For RFs, the final classification output is typically obtained through a voting mechanism (e.g., majority voting), while GBDTs are usually trained for binary classification problems and use some binary reduction scheme, such as one-vs-all or one-vs-one, for multiclass classification.

Abstract Interpretation Basics

A numerical abstract domain is a tuple A, A , γ A where: A, A is at least a preordered set of abstract values and the concretization function γ A : A → ℘(R d ), mapping abstract values to sets of numerical vectors, monotonically preserves the ordering relation A , that is, a 1 A a 2 implies γ A (a 1 ) ⊆ γ A (a 2 ). The intuition is that an abstract domain A defines a symbolic abstract representation of sets of vectors ranging in the concrete domain ℘(R d ). Known examples of numerical abstract domains used in machine learning verification include intervals, zonotopes, and octagons (see the survey [START_REF] Urban | A Review of Formal Methods applied to Machine Learning[END_REF]).

Given a concrete k-ary operation on vectors f

: (R d ) k → R d , for some k ∈ N, an abstract function f A : A k → A is called a sound (or correct) (over- )approximation of f when, for all (a 1 , ..., a k ) ∈ A k , {f (x 1 , ..., x k ) | ∀i. x i ∈ γ A (a i )} ⊆ γ A (f A (a 1 , ..., a k )) holds.
When equality holds, f A is defined to be complete. In words, this means that soundness holds when f A (a 1 , ..., a k ) never misses a concrete computation of f on some input (x 1 , ..., x k ) which is abstractly represented by (a 1 , ..., a k ), while completeness implies that each abstract computation f A (a 1 , ..., a k ) is precisely a symbolic abstract representation in A of the set of computations of f on all the concrete inputs that are abstractly represented by (a 1 , ..., a k ).

We will use the well-known abstract domain of not necessarily closed real ddimensional hyper-rectangles HR d , commonly called interval or box abstraction in abstract interpretation [START_REF] Cousot | Principles of Abstract Interpretation[END_REF][START_REF] Rival | Introduction to Static Analysis: An Abstract Interpretation Perspective[END_REF]. For concrete vectors ranging in R d , the abstract values of HR d are d-dimensional vectors of type

h = x 1 ∈ [l 1 , u 1 ], . . . , x d ∈ [l d , u d ] ∈ HR d
where lower and upper bounds

l i , u i ∈ R ∪ {-∞, +∞} with l i ≤ u i . Thus, the concretization function is defined by γ HR d (h) {x ∈ R d | ∀i. l i ≤ x i ≤ u i }. Let us recall that HR d , HR d is a complete lattice for the componentwise ordering: [l 1 , u 1 ], ..., [l d , u d ] HR d [l 1 , u 1 ], ..., [l d , u d ] iff for all i, l i ≤ l i and u i ≤ u i .
More on this abstract domain can be found, e.g., in [START_REF] Cousot | Principles of Abstract Interpretation[END_REF][START_REF] Rival | Introduction to Static Analysis: An Abstract Interpretation Perspective[END_REF].

Individual Fairness

Dwork et al. [18, Section 1.1] define individual fairness as "the principle that two individuals who are similar with respect to a particular task should be classified similarly". They formalize this notion as a Lipschitz condition of the classifier, which requires that any two individuals x, y ∈ X whose distance is δ(x, y) ∈ [0, 1], are mapped to distributions D x and D y , respectively, such that the distance between D x and D y is at most δ(x, y). The intuition is that the output distributions for x and y are indistinguishable up to their distance. The distance metric δ : X × X → R ≥0 is problem specific, and for their applications Dwork et al. [18, Section 2] study the total variation or relative ∞ distances. By following Dwork et al.'s standard definition [18, Section 2], we consider a classifier C : X → ℘ + (L) to be fair when C outputs the same set of labels for every pair of individuals x, y ∈ X which satisfy a similarity relation S ⊆ X × X between input samples. Thus, S can be derived from any distance δ as (x, y) ∈ S ⇔ δ(x, y) ≤ τ , where τ ∈ R is a threshold of similarity. In order to provide a fairness metric for a classifier C, we count how often C is fair on sets of similar individuals ranging into a test dataset T ⊆ X × L:

fair T,S (C) |{(x, y) ∈ T | fair(C, x, S)}| |T | (2)
where fair(C, x, S) is defined as follows:

Definition 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 ∀x ∈ X : (x, x ) ∈ S ⇒ C(x ) = C(x).
Hence, fairness for a similarity relation S boils down to stability on the perturbation P S (x) {x ∈ X | (x, x ) ∈ S} (cf. Equation (1) in Section 2.1), namely, for all x ∈ X, fair(C, x, S) ⇔ stable(C, x, P S ).

(

) 3
Let us remark that fairness is orthogonal to accuracy since it does not depend on the correctness of the label assigned by the classifier, so that training algorithms that maximize accuracy-based metrics do not necessarily achieve fair models. Thus, this is also the case of a natural learning algorithm for CART trees and random forests, that locally optimizes split criteria by measuring entropy or Gini impurity, which are both indicators of the correct classification of training data.

It is also worth observing that fairness is anti-monotonic w.r.t. the logical implication of similarity relations, meaning that

fair(C, x, S) ∧ S ⊆ S ⇒ fair(C, x, S ). (4)
We will exploit this anti-monotonicity property, since it implies that, on one hand, fair classification is preserved for finer similarity relations and, on the other hand, fairness verification and fair training is more challenging for coarser similarity relations.

Verifying Individual Fairness

As individual fairness is equivalent to stability, we verify individual fairness of ensembles of decision trees by means of Silva [START_REF] Ranzato | Abstract interpretation of decision tree ensemble classifiers[END_REF], an abstract interpretationbased algorithm for checking stability properties of decision tree ensembles.

Sound and Complete Verification

Silva performs a static analysis of an ensemble of decision trees leveraging an abstract domain A that approximates computations on real vectors. Each abstract value a ∈ A symbolically represents a set of real vectors γ A (a) ∈ ℘(R d ).

Then, Silva over-approximates an input region P (x) ∈ ℘(R d ) for an input vector x ∈ R d by an abstract value a ∈ A such that P (x) ⊆ γ A (a), and for each decision tree t, it computes an over-approximation of the set of leaves of t that can be reached from some vector in γ A (a). This is computed by collecting the constraints of all the split nodes in each root-leaf path of t, so that each leaf λ of t stores the minimum set of constraints C λ that makes λ reachable from the root of t. The verification algorithm then checks whether this set of constraints C λ can be satisfied by the input abstract value a ∈ A: this check a |= ? C λ must be sound, meaning that if some input sample x ∈ X abstractly represented by a, i.e. x ∈ γ A (a), actually reaches the leaf λ, then a |= C λ must necessarily hold. When a |= C λ holds the leaf λ is marked as reachable from the abstract value a.

Example 1 (Sound verification). Consider the scenario in Fig. 1 where the set of split constraints for some leaf λ is depicted in blue. An hyper-rectangle abstract value such as h = x 1 ≤ 0, x 2 ≤ 0 ∈ HR 2 , depicted in green, abstractly represents some points which satisfy all the constraints in C λ , so that a |= C λ must hold. On the other hand, for a relational abstract value such as the line a ≡ x 1 + x 2 = 4, depicted in red, we have that no point in the line satisfies C λ , so that no sure information could be inferred from a merely sound check of a |= ? C λ .

C λ = {x 1 ≤ 2, ¬(x 1 ≤ -1), x 2 ≤ -1}, x 1 x 2 -1 . . . . . . 2 -1 C λ h = x 1 ≤ 0, x 2 ≤ 0 . . . . . . 4 4 a ≡ x 1 + x 2 = 4
This sound approach therefore provides an over-approximation of the set of leaves of t reachable from an abstract value a that allows us to compute a set of labels t A (a) ∈ ℘ + (L) which is an over-approximation of the actual set of labels assigned by t to all the input vectors ranging in γ A (a), i.e.,

∪ x∈γ A (a) t(x) ⊆ t A (a) (5)
holds. Thus, given a similarity relation S ⊆ X × X, it turns out that for all x ∈ X and a ∈ A,

P S (x) ⊆ γ A (a) ∧ t A (a) = t(x) ⇒ fair(t, x, S),
meaning that we have a sound verification method for individual fairness of decision trees.

For the most common classification trees with hard univariate splits of type x i ≤ k, it turns out that the abstract domain HR d guarantees that for each leaf constraint C λ and hyper-rectangle h ∈ HR d , the check h |= ? C λ is sound and complete, meaning that

h |= C λ ⇔ ∃x ∈ γ(h) reaching λ.
This noteworthy completeness property of the hyper-rectangle abstraction entails that the set of labels t HR (h) computed by the analysis on HR d coincides exactly with the set of classification labels computed by t for all the samples in γ HR d (h), i.e., the set inclusion in Equation ( 5) is strengthened to a set equality.

h x ∈ HR d such that S τ ∞ (x) = {x ∈ X | ||x -x || ∞ ≤ τ } = γ HR d (h x ) holds and, in turn, we have that t HR (h x ) = t(x) ⇔ fair(t, x, S τ ∞ ). (6)
Hence, we devised a complete verification method for individual fairness with respect to ∞ -based similarity.

Verification of Forests.

In order to analyse a forest F of trees, Silva reduces the whole forest to a single tree t F , by stacking every tree t ∈ F on top of each other, i.e., each leaf becomes the root of the next tree in F , where the ordering of this stacking operation does not affect the output of a forest verification. Then, each leaf λ of this stacked single tree t F collects all the constraints of the leaves of trees in the path from the root of t F to λ. An example is shown in Fig. 2, where the trees t 1 , t 2 , t 3 are combined into a single tree, emphasizing how the leaves of the original trees t i become internal nodes in this stacked tree t F , while their sets of constraints are collected and stored in the new leaves of t F .

Since the stacked tree t F suffers from a combinatorial explosion of the number of leaves, Silva deploys a number of optimisation strategies for performing its abstract interpretation. The most relevant ones include a best-first search algorithm to look for a pair of input samples in γ A (a) which are differently labeled. If one such pair x, x ∈ γ A (a) can be found then unfairness of the forest F in classifying x and x is proved and the analysis is terminated, otherwise fairness holds. A further optimisation consists in combining sound analyses with complete ones. While exploring an internal node n, a fast sound but possibly incomplete analysis of t F is used to estimate a superset of the leaves of t F reachable from n, which, in turn, allows us to compute a superset of the output labels.

If such superset consists of a single label, then every leaf reachable from n necessarily yields that same label, and the rest of the visit of the subtree rooted in n can be safely omitted; otherwise, that information provided by the node n is nonetheless used to refine the analysis of t F . We refer to [START_REF] Ranzato | Abstract interpretation of decision tree ensemble classifiers[END_REF] for further details on Silva.

Verification with One-Hot Enconding

As described above by the equivalence (6), when the similarity relation is defined by the ∞ norm and the abstract domain of hyper-rectangles HR d is used, our verification method for individual fairness turns out to be complete. However, completeness does not hold for classification problems involving categorical features, as shown by the following simple example.

Example 2 (Incompleteness of one-hot encoding). The following diagram depicts a toy forest F consisting of two trees t 1 and t 2 , where left/right branches are followed when the split condition is false/true. color white ≤ 0.5

{ 1 } { 2 } t 1 color black ≤ 0.5 { 2 } { 1 } t 2
Here, a categorical feature color ∈ {white, black} is one-hot encoded by color white , color black ∈ {0, 1}. Since colors are mutually exclusive, every white individual in the input space, i.e., a vector color white = 1, color black = 0 , will be labeled 1 by both trees t 1 and t 2 . Our fairness verification method on the input

∞ -based similarity relation color white ∈ [0, 1], color black ∈ [0, 1] = [0, 1]×[0, 1],
which is an hyper-rectangle, infers that the forest F is unfair on the individual in = color white = 1, color black = 0 because there exists an input sample cex ∈

[0, 1] × [0, 1] such that F (cex) = { 1 , 2 } = { 1 } = F (in)
. This is due to the counterexample cex = 0, 0 ∈ [0, 1] 2 which is therefore similar to in, although it does not represent any actual individual in the input space. Indeed, t 1 (cex) = { 2 } and t 2 (cex) = { 1 }, so that, by a majority voting, F (cex) = { 1 , 2 }, thus making F unfair on in, i.e., unfair on white individuals.

To overcome this issue with one-hot encoding, we use a refined abstract domain which is designed as reduced product1 of the underlying main abstract domain, in our case the hyper-rectangle abstraction HR d , with a relational abstract domain that keeps track of the relationships among the multiple binary features introduced by one-hot encoding categorical features. More formally, this relational abstract domain maintains the following two additional constraints on the k features x c 1 , ..., x c k introduced by one-hot encoding a categorical variable x c with k distinct values:

(a) the possible values for each x c i are restricted to the discrete set {0, 1} (rather than ranging in the continuous interval [0, 1]);

(b) the sum of all the x c i 's must satisfy the relational constraint k i=1 x c i = 1. Therefore, these conditions (a)-(b) guarantee that any abstract value for x c 1 , ..., x c k represents precisely a feasible category for x c . This abstract domain for a categorical variable x with k distinct values is denoted by OH k (x). In the example above, any hyper-rectangle color white ∈ [0, 1], color black ∈ [0, 1] is reduced by OH 2 (color), so that just two different abstract values color white = 0, color black = 1 and color white = 1, color black = 0 are allowed.

Summing up, we employed a reduced hyper-rectangle abstract domain, denoted by HR d ⊗ OH, whose generic abstract value for data vectors consisting of d numerical variables x j ∈ R and m categorical variables c j with k j ∈ N distinct categories is:

x j ∈ [l j , u j ] d j=1 × c j i ∈ {0, 1} | kj i=1 c j i = 1 m j=1 ∈ HR d ⊗ OH,
where l j , u j ∈ R ∪ {-∞, +∞} and l j ≤ u j .

Fairness-Aware Training of Trees

Several algorithms for training robust decision trees and ensembles thereof have been put forward in the literature [START_REF] Andriushchenko | Provably Robust Boosted Decision Stumps and Trees against Adversarial Attacks[END_REF][START_REF] Calzavara | Adversarial Training of Gradient-Boosted Decision Trees[END_REF][START_REF] Calzavara | TREANT: training evasion-aware decision trees[END_REF][START_REF] Chen | Robust decision trees against adversarial examples[END_REF][START_REF] Kantchelian | Evasion and Hardening of Tree Ensemble Classifiers[END_REF][START_REF] Ranzato | Genetic adversarial training of decision trees[END_REF]. These algorithms encode the robustness of a tree classifier as a loss function which is minimized either by exact methods such as MILP or by suboptimal heuristics such as genetic algorithms.

The robust learning algorithm Meta-Silvae, introduced in [START_REF] Ranzato | Genetic adversarial training of decision trees[END_REF], aims at maximizing a tunable weighted linear combination of accuracy and stability metrics, therefore, thanks to the equivalence (3), instantiating to a combination of accuracy and individual fairness for our purposes. Meta-Silvae relies on a genetic algorithm for evolving a population of decision trees t which are ranked by their accuracy acc D (t) and individual fairness fair D,S (t) w.r.t. a training dataset D, where the individual fairness metric fair D,S (t) for a similarity relation S is computed by the verification method described in Section 4.1. At the end of the genetic evolution, the best tree (or best trees are) is returned. It turns out that Meta-Silvae typically outputs significantly compact models and often achieves high accuracy and fairness already with a single decision tree rather than a forest of them. Thus, the instantiation of Meta-Silvae to the reduced product abstract domain HR d ⊗ OH described in Section 4.2 provides a learning algorithm for ensembles of decision trees, called FATT, that enhances their individual fairness.

More specifically, the objective function ϕ of FATT, for learning fair decision trees, is given by a weighted sum of the accuracy and individual fairness scores over the training dataset D, i.e., ϕ D (t) w a acc D (t) + w f fair D,S (t).

(

) 7
We use w a = 0.9 and w f = 0.1 for all our experiments (presented in the next section).

While standard learning algorithms for tree ensembles require tuning a number of hyper-parameters, such as maximum depth of trees, minimum amount of information on leaves and maximum number of trees, FATT is able to infer them automatically, so that the customary tuning process is not needed. Instead, some standard parameters are required by the underlying genetic algorithm, notably, the size of the evolving population, the maximum number of evolving iterations, the selection of crossover and mutation functions [START_REF] John | Genetic algorithms and adaptation[END_REF][START_REF] Srinivas | Genetic algorithms: a survey[END_REF]. It should be remarked that, given an objective function, the genetic algorithm of FATT converges to an optimal (or suboptimal) solution regardless of the chosen parameters of the genetic algorithm, which just affect the rate of convergence and therefore should be chosen for tuning its convergence speed only.

Crossover and mutation functions are the two main features of the genetic algorithm of FATT. The crossover function combines two parent trees t 1 and t 2 of the current evolving population by randomly substituting a subtree of t 1 with a subtree of t 2 . After a crossover operation, two types of mutation strategies are available: grow-only, which only allows trees to grow, and grow-and-prune, which also allows pruning the mutated trees. We just sketch an example of crossover and mutation functions and refer to [START_REF] Ranzato | Genetic adversarial training of decision trees[END_REF] for a detailed definition.

Example 3 (Crossover and mutation). Fig. 3 depicts a simple example of crossover, where every node is represented by a tuple (i, k, R), with i, k denoting a split x i ≤ k (therefore not relevant for leaves), while R ⊆ X represents the subset of samples in the training set reaching that node. The crossover tree t cross is built by selecting the subtree s 1 of t 1 given by the leaf (_, _, R 1 ) only, the subtree s 2 of t 2 rooted at node (2, 1, R 5 ), and by replacing s 1 with s 2 in t 1 . Selection of both subtrees can be fully random, or relies on some mixed heuristic/stochastic criteria, for example by replacing a poorly performing subtree with a better one from another tree, where subtrees are stochastically selected with a probability proportional to their Gini impurity. While the split constraints x i ≤ k are directly copied from the donor tree, the set R of reaching samples may well be different, and must therefore be recomputed. After a crossover operation, it may happen that the set of reachable samples R of some node n of t cross becomes empty, thus making n unreachable. In this case, the tree is pruned by removing these unreachable nodes and by replacing their parents with the siblings. In Fig. 3,t prune cross is the result of pruning the leaf (_, _, R 3 = ∅) of t cross . Fig. 3 also depicts two mutations of t prune cross : t mute1 is obtained from t prune cross by expanding the leaf (_, _, R 9 ), while t mute2 prunes the subtree rooted at (2, 1, R 1 ). In both cases, the leaf to grow or the subtree to prune can be selected randomly or stochastically with a probability proportional to Gini impurity.

FATT

Let us recall that the standard learning method for CART trees [START_REF] Leo Breiman | Classification and Regression Trees[END_REF] is a greedy algorithm which incrementally builds a decision tree by locally computing new split nodes or new leaves, where a new split x i ≤ k is inferred by testing every possible combination of i and k in order to locally minimize a Gini impurity or entropy index. It is also worth recalling that while this greedy learning approach yields trees which are very accurate on the training set, it often leads to overfitting, a well-known phenomenon with decision trees [START_REF] Bramer | Avoiding Overfitting of Decision Trees[END_REF].

FATT relies on an objective function that takes into account both accuracy and individual fairness, cf. Equation [START_REF] Breiman | Random Forests[END_REF]. Thus, in FATT the selection of a candidate split relies on an individual fairness index fair D,S (t) computed by the verifier described in Section 4.1 on the whole corresponding candidate tree t. This learning process is inherently not incremental and consequently could be computationally burdensome. Such a computational cost is alleviated by introducing a search aggressiveness parameter which sets up a bound on the number of new split candidates to consider or a timeout mechanism. It turns out that this optimization is effective in reducing the computational burden without sacrificing the overall generalization, because the evaluation of split candidates which are ruled out is simply delayed to later iterations of the evolutionary process.

Our fair learning method FATT uses the following basic parameters for the underlying genetic algorithm Meta-Silvae: the population size is kept fixed to 32, as our experimental evaluation showed that this provides an effective balance between achieved individual fairness and training time; the standard roulette wheel algorithm [START_REF] Neumann | Theoretical analysis of fitness-proportional selection: Landscapes and efficiency[END_REF] is employed as selection function (which is proportional to the objective function ϕ); the number of iterations of the evolutionary process is typically dataset-specific and can be estimated by running a preliminary analysis of the convergence speed, for instance by stopping after a given number of iterations with no improvement.

Experimental Evaluation

We consider the main standard datasets used in the fairness literature [START_REF] Mehrabi | A survey on bias and fairness in machine learning[END_REF] and we preprocess them by following the steps of Ruoss et al. [START_REF] Ruoss | Learning certified individually fair representations[END_REF]Section 5] for their experiments on individual fairness for deep neural networks: (1) standardize numerical attributes to zero mean and unit variance; (2) one-hot encoding of all categorical features; (3) drop rows/columns containing missing values; (4) split into train and test set. These datasets concern binary classification tasks, although our fair learning algorithm naturally extends to multiclass classification with no specific effort. The source code of FATT as well as all the datasets and preprocessing pipelines are publicly available on GitHub [START_REF] Ranzato | FATT: Fairness aware tree training[END_REF].

Adult. The Adult income dataset [START_REF] Dua | Uci machine learning repository[END_REF] is extracted from the 1994 US Census database. Every sample assigns a yearly income (below or above 50K US$) to an individual based on personal attributes such as gender, race, and occupation.

Compas. The COMPAS dataset contains data collected on the use of the COMPAS risk assessment tool in Broward County, Florida [START_REF] Angwin | Machine Bias[END_REF]. Each sample predicts the risk of recidivism for individuals based on personal attributes and criminal history.

Crime. The Communities and Crime dataset [START_REF] Dua | Uci machine learning repository[END_REF] contains socio-economic, law enforcement, and crime data for communities within the US. Each sample indicates whether a community is above or below the median number of violent crimes per population.

German. The German Credit dataset [START_REF] Dua | Uci machine learning repository[END_REF] contains samples assigning a good or bad credit score to individuals.

Health. The heritage Health dataset (https://www.kaggle.com/c/hhp) contains physician records and insurance claims. Each sample predicts the ten-year mortality (above or below the median Charlson index) for a patient.

The following table displays size and distribution of positive samples for these datasets. As noticed by Ruoss et al. [START_REF] Ruoss | Learning certified individually fair representations[END_REF], some datasets exhibit a highly unbalanced label distribution. For example, for the Adult dataset, a constant classifier C(x) = 1 would achieve 75.4% test set accuracy and 100% individual fairness with respect to any similarity relation. Hence, we follow [START_REF] Ruoss | Learning certified individually fair representations[END_REF] and we additionally evaluate and report the balanced accuracy of our FATT classifiers, i.e., 0.5 ( truePositive truePositive + falseNegative + trueNegative trueNegative + falsePositive ).

Similarity Relations

Following Ruoss et al. [START_REF] Ruoss | Learning certified individually fair representations[END_REF]Section 5.1], we consider four different types of similarity relations. In the following, let I ⊆ N denote the set of indexes of features of an individual after one-hot encoding.

noise: Two individuals x, y ∈ X are similar when a subset of their (standardized) numerical features indexed by a given subset I ⊆ I differs less than a given threshold τ ≥ 0, while all the other features are unchanged: (x, y) ∈ S noise iff |x i -y i | ≤ τ for all i ∈ I , and x i = y i for all i ∈ I I .

For our experiments, we consider τ = 0.3 in the standardized input space, e.g., for Adult two individuals are similar if their age difference is at most 3.95 years.

cat: Two individuals are similar if they are identical except for one or more categorical sensitive attributes indexed by I ⊆ I: (x, y) ∈ S cat iff x i = y i for all i ∈ I I . For Adult and German, we select the gender attribute.

For Compas, we identify race as sensitive attribute. For Crime, we consider two individuals similar regardless of their state. Lastly, for Health, neither gender nor age group should affect the final prediction.

noise-cat: Given noise and categorical similarity relations S noise and S cat , their union S noise-cat S noise ∪ S cat models a relation where two individuals are similar when some of their numerical attributes differ up to a given threshold while the other attributes are equal except some categorical features.

conditional-attribute: Here, similarity is a disjunction of two mutually exclusive cases. Consider a numerical attribute x i , a threshold τ ≥ 0 and two noise similarities S n1 , S n2 . Two individuals are defined to be similar if either their i-th attributes are similar for S n1 and are bounded by τ or these attributes are above τ and similar for S n2 :

S cond {(x, y) ∈ S n1 | x i ≤ τ, y i ≤ τ } ∪ {(x, y) ∈ S n2 | x i > τ, y i > τ }.
For Adult, we consider the median age as threshold τ = 37, and two noise similarities based on age with thresholds 0.2 and 0.4, which correspond to age differences of 2.63 and 5.26 years, respectively. For German, we also consider the median age τ = 33 and the same noise similarities on age, that correspond to age differences of 0.24 and 0.47 years.

It is worth remarking that our fairness-aware learning algorithm is not limited to support these similarity relations. Further domain-specific similarities can be defined and handled by our approach by simply instantiating the underlying fairness verifier with a suitable over-approximating abstract domain A to retain a sound verification. Moreover, if the similarity relation can be precisely represented in A, completeness is preserved as well.

Setup

Our experimental evaluation compares CART trees and Random Forests with our FATT tree models. CARTs and RFs are trained by scikit-learn. We first run a preliminary phase for tuning the hyper-parameters for CARTs and RFs. In particular, we considered both entropy-based information gain and Gini index as split criteria, and we checked maximum tree depths ranging from 5 to 100 with step 10. For RFs, we scanned the maximum number of trees ranging from 5 to 100, step 10. Cross validation inferred the optimal hyper-parameters, where the datasets have been split in 80% training and 20% validation sets. The hyper-parameters of FATT (i.e., weights of accuracy w a and fairness w f in the objective function [START_REF] Breiman | Random Forests[END_REF], type of mutation strategy, number of iterations) are inferred by assessing convergence speed, maximum fitness value and variance among fitness in the evolving population during the training phase. We report here the best results, obtained with w a = 0.9 and w f = 0.

Results

Table 1 provides a comparison between RF and FATT models by showing accuracy, balanced accuracy and individual fairness with respect to the four similarity relations of Section 6.1 computed on the test sets T . The conditionalattribute similarity relation only applies to the Adult and German datasets. As expected, FATT decision trees are slightly less accurate than RFs -about -3.6% on average, which also reflects to balanced accuracy -but outperform RFs in every fairness test. On average, the fairness increment ranges between +32.09% to +43.91% among the noise, cat, and noise-cat similarity relations. For the conditional-attribute similarity the average fairness increase of FATT models is +8.68%. Fig. 4 shows the distribution of accuracy and individual fairness for FATT trees over 1000 runs of the FATT learning algorithm. This boxplot is for fairness with respect to noise-cat similarity, as this is the most challenging relation for achieving individual fairness, as a consequence of anti-monotonicity (4). We observe a stable behaviour for accuracy, with about 50% of the observations laying within one percentile from the median. The results for fairness are similar, although for Compas we report a higher variance of the distribution, where the lowest fairness percentage is about 10% higher than the corresponding one for RFs. We claim that this may depend on the high number of features in the dataset Compas, which makes fair training a challenging task.

Table 2 compares the size of RF and FATT models, defined as total number of leaves, and their average verification time of individual fairness per input sample. It turns out that FATT tree models are orders of magnitude smaller and, therefore, more interpretable than RFs, while the average verification time per sample for our FATT models is always negligible (< 0.1 milliseconds). Finally, Table 3 compares FATT models with natural CART trees in terms of accuracy, individual fairness with respect to the noise-cat similarity, and size. While CARTs are approximately 3% more accurate than FATT models on average, they are roughly half less fair and more than 10× larger.

CART with Hints

As already recalled, decision trees frequently overfit [START_REF] Bramer | Avoiding Overfitting of Decision Trees[END_REF] due to their high number of leaves, thus yielding unstable/unfair models. Post-training techniques, such as tree pruning, are commonly used to mitigate overfitting [START_REF] Michael | A fast, bottom-up decision tree pruning algorithm with near-optimal generalization[END_REF], although they are deployed when a tree has been already fully trained and, therefore, pruning is often poorly beneficial. As a byproduct of our fairness-aware learning approach, we trained a set of natural CART trees, denoted by CART with Hints in Table 3, which exploit hyper-parameters as "hinted" by our FATT training. In particular, in this learning of CART trees with hints, the maximum tree depth and the minimum number of samples per leaf are obtained as tree depth and minimum number of samples of our best FATT models. Interestingly, the results in Table 3 show that these decision trees with hints have roughly the same size of our FATT trees, are approximately 20% more fair than natural CART trees and just 1% less accurate. Overall, it turns out that the general performance of these CARTs with hints is halfway between natural CARTs and FATT trees, both in term of accuracy and individual fairness, while having the same compactness of FATT models.

Conclusion

We believe that this work contributes to push forward the use of formal verification methods in decision tree learning, in particular a well known program analysis technique such as abstract interpretation is proved to be successful for training and verifying decision tree classifiers which are both accurate and fair, improve on state-of-the-art CART and random forest models, while being much more compact and thus interpretable. We also showed how information from our FATT trees can be exploited to tune the natural training process of decision trees.

As future work we plan to extend our fairness verification and learning method by considering alternative fairness definitions, such as group or statistical fairness, or stronger notions such as causal [START_REF] Galhotra | Fairness Testing: Testing Software for Discrimination[END_REF] or dependency [START_REF] Urban | Perfectly parallel fairness certification of neural networks[END_REF] fairness. We also aim at designing quantitative verification methods for both stability and fairness, in order to provide probabilistic guarantees on the behavior of decision tree and tree ensemble models.

(1, 0.5, R)

(_, _, R 1 ) (2, -2, R 2 ) (_, _, R 3 ) (_, _, R 4 ) t 1 (1, 1.3, R) (2, 1, R 5 ) (_, _, R 6 ) (_, _, R 7 ) (_, _, R 8 ) t 2
(1, 0.5, R)

(2, 1, R 1 ) (_, _, R 9 ) (_, _, R 10 ) (2, -2, R 2 ) (_, _, R 3 = ∅) (_, _, R

Figure 1 :

 1 Figure 1: An example of abstract check a |= ? C λ

Figure 2 :

 2 Figure 2: An example of forest to single tree reduction

1 , 1 ( 1

 111 _, R 9 ) (_, _, R 10 ) (_, _, R 4 ) R 11 ) (_, _, R 12 ) (_, _, R 13 ) (_, _, R 10 ) (_, _, R 4 ) t mute , 0.5, R) (_, _, R 1 ) (_, _, R 4 ) t mute 2

Figure 3 :

 3 Figure 3: Example of crossover and mutation

Figure 4 :

 4 Figure 4: Distribution of Accuracy (left) and Fairness (right)

Table 1 :

 1 1. The number of RF and FATT Comparison evolutionary iterations for the experiments ranges between 10 and 100. Specifically, we obtained the best results with 10 iterations for the Crime and German datasets, and with 100 iterations for Adult, Compas, and Health. It turned out that accuracy and fairness of single FATT trees, rather than forests, were already competitive, with individual fairness exceeding 85% for the most challenging similarities. We therefore concluded that ensembles of FATT trees do not introduce statistically significant benefits over single decision trees. Since FATT trees are stochastic, by relying on random seeds, each experimental test has been repeated 1000 times and the reported results refer to their median value.

	Dataset	Accuracy %	Balanced Accuracy %		cat	Individual Fairness fair T % noise noise-cat conditional-attribute
		RF	FATT	RF	FATT	RF	FATT	RF	FATT	RF	FATT	RF	FATT
	Adult	82.76	80.84	70.29	61.86 91.71 100.00 85.44 95.21 77.50 95.21 84.75	94.12
	Compas	66.57	64.11	66.24	63.83 48.01 100.00 35.51 85.98 30.87 85.98	-	-
	Crime	80.95	79.45	80.98	79.43 86.22 100.00 31.83 75.19 32.08 75.19	-	-
	German	76.50	72.00	63.62	52.54 91.50 100.00 92.00 99.50 90.00 99.50 91.50	99.50
	Health	85.29	77.87	83.27	73.59	7.84	99.99	47.66 97.04	2.91	97.03	-	-
	Average 78.41 74.85 72.88 66.25 65.06 100.00 58.49 90.58 46.67 90.58 88.13	96.81

Table 2 :

 2 Model Sizes and Verification Times

	Dataset	Model Size	cat	Average Verification Time per Sample (ms) noise noise-cat conditional-attribute
		RF	FATT RF FATT	RF	FATT	RF	FATT RF	FATT
	Adult	1427	43	0.03	0.02	0.03	0.02	0.03	0.02	0.03	0.02
	Compas	147219	75	0.36	0.07	0.47	0.07	0.61	0.07	-	-
	Crime	14148	11	0.12	0.07	2025.13	0.07	2028.47	0.07	-	-
	German	5743	2	0.06	0.03	0.06	0.02	0.07	0.03	0.06	0.02
	Health	2558676	84	1.40	0.06	0.91	0.05	3.10	0.06	-	-
	FATT Dataset Accuracy % Fairness % Size Accuracy % Fairness % Size Accuracy % Fairness % Size Natural CART CART with Hints
	Adult	80.84	95.21	43	85.32		77.56	270	84.77	87.46	47
	Compas	64.11	85.98	75	65.91		22.25	56	65.91	22.25	56
	Crime	79.45	75.19	11	77.69		24.31	48	77.44	60.65	8
	German	72.00	99.50	2	75.50		57.50	115	73.50	86.00	4
	Health	77.87	97.03	84	83.85		79.98 2371	82.25	93.64 100
	Average	74.85	90.58	43	77.65		52.32	572	76.77	70.00	43

Table 3 :

 3 Decision Trees Comparison

Readers can find more details on reduced products of abstract domains, e.g., in[START_REF] Cousot | Principles of Abstract Interpretation[END_REF].

Acknowledgments. Francesco Ranzato has been partially funded by: University of Padova, under the SID2018 project "Analysis of STatic Analyses (ASTA)"; Italian Ministry of University and Research, under the PRIN2017 project no. 201784YSZ5 "AnalysiS of PRogram Analyses (ASPRA)"; Facebook Research, under a "Probability and Programming Research Award".