  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 classification
model, which is a variant of standard robustness under input perturbations used
in adversarial machine learning. Our verification and training methods leverage
abstract interpretation, a well established technique for static program
analysis which is able to automatically infer assertions about stability
properties of decision trees. By relying on a tool for adversarial training of
decision trees, our fairness-aware learning method has been implemented and
experimentally evaluated on the reference datasets used to assess fairness
properties. The experimental results show that our approach is able to train
tree models exhibiting a high degree of individual fairness w.r.t. the natural
state-of-the-art CART trees and random forests. Moreover, as a by-product,
these fair decision trees turn out to be significantly compact, thus enhancing
the interpretability of their fairness properties.
