The increasing success of Machine Learning (ML) led to its massive deployment in various applications. Unfortunately, traditional methods for assessing the performance of ML models do not always provide a reliable picture of their effectiveness in practical scenarios, for instance when the robustness or the fairness of the algorithm matters.
Previous research efforts have introduced definitions of properties, such as robustness and various fairness criteria, to characterize the trustworthy behavior of ML models. Additionally, verification algorithms based on formal methods have been proposed to provide formal guarantees regarding compliance with the desired properties. However, several popular robustness and fairness properties are local or data-dependent, in the sense that they are predicated solely on specific test instances rather than on arbitrary inputs.
In this talk, I will discuss two contributions that attempt to go beyond the verification of local robustness and fairness properties. In particular, we design verification algorithms of more expressive properties for a specific class of ML classifiers, i.e., tree-based classifiers. The first contribution proposes a data-independent stability analysis to identify a subset of the feature space where the ML model does not change its predictions despite adversarial manipulations. We use this analysis to verify resilience, a new security property that generalizes the idea of robustness. The same analysis is then leveraged in our second contribution to verify a global fairness property, i.e., a property that predicates over all the possible inputs of the classifier. In particular, our analysis synthesizes sufficient conditions for fairness predicating over the entire feature space, thus providing global fairness guarantees.
9/11/2023