To check the emptiness of the set \(\mathcal {C}_p\)  in (REF ) (and hence certify the global individual fairness property), we need to search the space \(D_\phi \times D_\phi \)  to find at least one counterexample that violates the fairness property, i.e., a pair \(x_p = (x,x^{\prime })\)  that represent similar individuals who are classified differently by the NN. Finding such a counterexample is, in general, NP-hard due to the non-convexity of the ReLU NN \(f_{\theta _p}\) . To that end, we use PeregriNN [1]} as our NN verifier. Briefly, PeregriNN overapproximates the highly non-convex NN with a linear convex relaxation for each ReLU activation. This is done by introducing two optimization variables for each ReLU, a pre-activation variable \(\hat{y}\)  and a post-activation variable \(y\) . The non-convex ReLU function can then be overapproximated by a triangular region of three constraints; \(y \ge 0\) , \(y \ge \hat{y}\) , and \(y \le \frac{u}{u-l}(\hat{y} - l)\) , where \(l\text{,}u\)  are the lower and upper bounds of \(\hat{y}\)  respectively. The solver tries to check whether the approximate problem has no solution or iteratively refine the NN approximation until a counterexample that violates the fairness constraint is found. PeregriNN employs other optimizations in the objective function to guide the refinement of the NN approximation but the details of these methods are beyond the scope of this paper. We refer the reader to the original paper [1]} for more details on the internals of the solver.
