We introduce CertiFair, a framework for certified global fairness of NNs. This framework consists of two components. First, a verifier that can prove whether the NN satisfies the fairness property or produce a concrete counterexample that violates the fairness property. This verifier is motivated by the recent results in the “relational verification” problem [1]} where the goal is to verify hyperproperties that are defined over pairs of program traces. Our approach is based on the observation that the global individual fairness property (REF ) can be seen as a hyperproperty and hence we can generalize the concept of product programs to product NNs that accepts a pair of inputs \((x,x^{\prime })\) , instead of a single input \(x\) , and generates two independent outputs for each input. A global fairness property for this product NN can then be verified using existing NN verifiers. Moreover, and inspired by methods in certified robustness, we also propose a training procedure for certified fairness of NNs. Thanks again to the product NN, mentioned above, one can establish upper bounds on fairness and use it as a regularizer during the training of NNs. Such a regularizer will promote the fairness of the resulting model, even if the data used for training is biased and can lead to an unfair classifier. While such fairness regularizer will enhance the fairness of the model, one needs to check if the fairness property holds globally using the sound and complete verifier mentioned above.
