FairQuant: Certifying and Quantifying Fairness of Deep Neural Networks
Brian Hyeongseok Kim Jingbo Wang Chao Wang






FairQuant: Certifying and Quantifying Fairness of Deep Neural Networks
    
    
    Brian Hyeongseok Kim
    

    University of Southern California 

    Los Angeles, USA

    Jingbo Wang
    

    Purdue University

    West Lafayette, USA

    Chao Wang
    

    University of Southern California 

    Los Angeles, USA

    Received 16 July 2024; accepted 04 September 2024
==============================================================================================================================================================================================================================================================



§ ABSTRACT 
We propose a method for formally certifying and quantifying individual fairness of deep neural networks (DNN). Individual fairness guarantees that any two individuals who are identical except for a legally protected attribute (e.g., gender or race) receive the same treatment. While there are existing techniques that provide such a guarantee, they tend to suffer from lack of scalability or accuracy as the size and input dimension of the DNN increase. 

Our method overcomes this limitation by applying abstraction to a symbolic interval based analysis of the DNN followed by iterative refinement guided by the fairness property. Furthermore, our method lifts the symbolic interval based analysis from conventional qualitative certification to quantitative certification, by computing the percentage of individuals whose classification outputs are provably fair, instead of merely deciding if the DNN is fair.  

We have implemented our method and evaluated it on deep neural networks trained on four popular fairness research datasets. The experimental results show that our method is not only more accurate than state-of-the-art techniques but also several orders-of-magnitude faster. 




§ INTRODUCTION


The problem of certifying the fairness of machine learning models is more important than ever due to strong interest in applying machine learning to automated decision making in various fields from banking <cit.> and healthcare <cit.> to public policy <cit.> and criminal justice <cit.>. Since the decisions are  socially sensitive, it is important to certify that the machine learning model indeed treats individuals or groups of individuals fairly. 

However, this is challenging when the model is a deep neural network (DNN) with a large number of hidden parameters and complex nonlinear activations. 

The challenge is also exacerbated as the network size and input dimension increase.

In this work, we aim to overcome the challenge by leveraging abstract interpretation techniques to certify fairness both qualitatively and quantitatively.


Our work focuses on individual fairness which, at a high level, requires that similar individuals are treated similarly <cit.>.

Here, similar individuals are those who differ only in some legally protected input attribute (e.g., gender or race) but agree in the unprotected attributes[This notion can be understood as counterfactual fairness <cit.>

explained in more detail in Section <ref>.]

and being treated similarly means that the DNN generates the same classification output. 

Let the DNN be a function f: X→ Y from input domain X to output range Y, where an individual x∈ X is an input and a class label y∈ Y is the output.

Assume that each input x=⟨ x_1,…,x_D⟩ is a D-dimensional vector, and  x_j, where 1≤ j ≤ D, is a protected attribute.

We say that the DNN is provably fair (certified) for the entire input domain X if f(x)=f(x') holds for any two individuals x ∈ X and x' ∈ X that differ only in x_j but agree in the unprotected attributes (∀ x_i where i≠ j).


Conversely, the DNN is provably unfair (falsified) for input domain X if f(x) ≠ f(x') holds for any two individuals (x ∈ X and x'∈ X) that differ only in the protected attribute.

If the DNN is neither certified nor falsified, it remains undecided.








Given a DNN f, a protected attribute x_j, and an input domain X, a qualitative certification procedure aims to determine whether f is fair, unfair, or undecided for all x ∈ X.  

Qualitative analysis is practically important because, if f is provably fair, the model may be used as is, but if f is provably unfair, the model should not be used to make decision for any x∈ X. 

When the result of qualitative analysis is undecided, however, there is a need for quantitative analysis, to compute the degree of fairness.  For example, the degree of fairness may be measured by the percentage of individuals in input domain X whose classification outputs  are provably fair.


Both qualitative certification and quantitative certification are hard problems for deep neural networks. 

While there are many verification tools for deep neural networks, existing verifiers such as ReluVal <cit.>, DeepPoly <cit.>, and α-β-CROWN <cit.> focus on certifying perturbation robustness, which is a fundamentally different property, and cannot certify individual fairness. 


To the best of our knowledge, the only existing technique for certifying individual fairness of a DNN is  <cit.>. However, since it directly analyzes the behavior of a DNN in the concrete domain using the SMT solver, the computational cost is extremely high; as a result,  can only certify tiny networks.  

Furthermore, it cannot quantify the degree of fairness.

Prior works on quantitative analysis of fairness focus on either testing <cit.>, which do not lead to sound certification, or statistical parity <cit.> that concerns another type of fairness,  group fairness, which differs significantly from individual fairness. 



To fill the gap, we propose the first scalable method for certifying and quantifying individual fairness of a DNN. 

Our method, named , takes a certification problem (consisting of the DNN f, protected attribute x_j, and input domain X) as input and returns one of the following three outputs:

(1) certified (fair) for all input x∈ X; 

(2) falsified (unfair) for all input x∈ X;

or (3) undecided, meaning that f is neither 100% fair nor 100% unfair.

In the third case, our method also computes the percentage of inputs in X whose classification outputs are provably fair.

More specifically, our method provides a lower bound of the certified percentage, which can guarantee that the DNN meets a certain requirement, e.g., the DNN is individually fair for at least 80% of all inputs in X.


As shown in Fig. <ref>,   iterates through three steps: abstraction (forward analysis), refinement (backward analysis), and quantification (rate computation). 

Assuming that the legally protected attribute x_j has two possible values (e.g., male and female), forward analysis tries to prove that, for each x in the input partition P (which is the entire input domain X initially), flipping the value of the protected attribute of x does not change the model's output.

This is accomplished by propagating two symbolic input intervals I (∀ x∈ P that are male) and I' (∀ x'∈ P that are female) to compute the two corresponding output intervals that are overapproximated. 
If the classification labels (for all x and x') are the same, our method returns certified (fair). 

On the other hand, if the classification labels (for all x and x') are different, our method returns falsified (unfair). 

In these two cases, 100% of the inputs in the partition P are resolved. 
 




Otherwise,  we perform refinement (backward analysis) by splitting P into partitions P_l and P_u and apply forward analysis to each of these new partitions. 

Since smaller partitions often lead to smaller approximation errors, refinement has the potential to increase the number of certified (or falsified) inputs and decrease in the number of undecided inputs.






To ensure that our method terminates quickly, we propose two early termination conditions based on the refinement depth of each partition P⊆ X.  The refinement depth is the number of times X is partitioned to produce P.

There are two predefined thresholds.




Once the refinement depth exceeds the higher threshold, we classify the partition P as undecided and avoid splitting it further.


But if the refinement depth exceeds the lower threshold without exceeding the higher threshold, we use random sampling to try to find a concrete example x∈ P  that violates the fairness property. If such a counterexample is found, we classify P as undecided and avoid splitting it further.


Otherwise, we keep splitting P into smaller partitions.


Our method differs from the vast majority of existing techniques for neural network verification, which focus on robustness verification of a single neural network <cit.>. In contrast, our method focuses on certifying individual fairness by simultaneously executing the network twice symbolically, once for ∀ x∈ X and another for ∀ x'∈ X (we further explain in Section <ref> why directly using existing robustness verifiers to certify fairness does not work in practice).

Our method also differs from prior works on differential verification <cit.> or equivalence verification <cit.>, which focus on proving the behavioral difference or equivalence of two different networks, given the same input. In our case, we deal with only one network model f, with different inputs defined by our fairness property.



We have evaluated  our method on a large number of deep neural networks trained using four widely-used datasets for fairness research: Bank <cit.> (for predicting marketing), German <cit.> (for predicting credit risk), Adult <cit.> (for predicting earning power), 
and Compas <cit.> (for predicting recidivism risk).


For comparison, we apply  <cit.> since it represents the current state-of-the-art in certifying individual fairness; we also apply α-β-CROWN since it is currently the best robustness verifier for deep neural networks. 


Our results show that α-β-CROWN is not effective in certifying individual fairness. As for ,  our method  significantly outperforms  in terms of both accuracy and speed for all DNN benchmarks. 

In fact,  often completes certification in seconds, whereas  often times out after 30 minutes and certifies nothing or only a tiny fraction of the entire input domain.



To summarize, this paper makes the following contributions:


  * We propose the first scalable method for certifying and quantifying individual fairness of DNNs using symbolic interval based analysis techniques.
  
  
  * For forward analysis,  we propose techniques for more accurately deciding if the DNN is fair/unfair for all inputs in an input partition. 
  
  * For refinement, we propose techniques for more effectively deciding how to split the input partition. 
  
  * For quantification, we propose techniques for efficiently computing the percentages of inputs whose outputs can be certified and falsified.
  

  * We demonstrate the advantages of our method over the current state-of-the-art on a large number of DNNs trained using four popular fairness research datasets.


The remainder of this paper is organized as follows.  First, we motivate our work in Section <ref> using examples.  Then, we present the technical background in Section <ref>.  Next, we present the high-level procedure of our method in Section <ref>, followed by detailed algorithms of the abstraction, refinement, and quantification subroutines in Sections <ref>, <ref> and <ref>. We present the experimental results in Section <ref>, review the related work in Section <ref>, and finally give our conclusions in Section <ref>.



§ MOTIVATION




In this section, we use an example to illustrate the limitations of existing methods. 



 §.§ The Motivating Example


Fig. <ref> (left) shows a DNN for making hiring decisions.  It has three input nodes (i_1,i_2 and i_3), two hidden neurons (h_1 and h_2) and one output node (o). 

The values of h_1 and h_2 are computed in two steps:  first, the values of i_1,i_2 and i_3 are multiplied by the edge weights before they are added up; then, the result is fed to an activation function. For instance, the activation function may be ReLU(z) = max(0,z). 

The output of the entire network f is based on whether the value of o is above 0; that is, positive label is generated if o > 0; otherwise, negative label is generated.






The DNN takes an input vector x with three attributes: 

x_1 is the interview score of the job applicant, 

x_2 is the gender (0 for female and 1 for male), and 

x_3 is the number of years of experience. 

Furthermore, x_2 is the protected attribute while x_1 and x_3 are unprotected attributes.

In general, the input domain may be unbounded, e.g., when some attributes are real-valued variables.
However, for illustration purposes, we assume that the input domain is X = {x  |  x_1∈{1,2,3,4,5}, x_2∈{0,1},  x_3∈{0,1,2,3,4,5}}, meaning that X has a total of 5× 2× 6 = 60 individuals.  














Consider the individual x = ⟨ 5, 0, 5⟩, meaning that x_1=5, x_2=0 and x_3=5.  According to the DNN in Fig. <ref>, the output is the positive label.  

After flipping the value of the protected attribute x_2 from 0 to 1, we have the individual x' = ⟨ 5, 1, 5⟩, for which the DNN's output is also the positive label.

Since the DNN's output is oblivious to the gender attribute, we say that it is fair for this input x. 


Consider another individual x = ⟨ 1, 0, 5 ⟩ whose gender-flipped counterpart is x' = ⟨ 1, 1, 5 ⟩. Since the DNN produces the negative label as output for both, it is still fair for this input x. 

To summarize, the DNN f may be fair regardless of whether a particular x ∈ X receives a positive or negative output; as long as x receives the same label as its counterpart x', the DNN is considered fair.

In contrast, since the individual x = ⟨ 1, 0, 3 ⟩ and its counterpart x' = ⟨ 1, 1, 3 ⟩ receive different outputs from f, where x gets the positive label but x' gets the negative label, the DNN is not fair for this input x.  Furthermore, this pair (x, x') serves as a counterexample.



In general, a machine learning model may be fair for some, but not all, individuals of the input domain. 



However, this observation seems to be overlooked by prior work on certifying individual fairness, which focuses on searching for counterexamples or proving that they do not exist. 

Such qualitative techniques may not be useful if almost all of the DNNs in practice are simply declared as “not fair”.

In contrast, we emphasize in this work the need to  quantitatively measure the degree of fairness when a DNN is neither 100% fair nor 100% unfair, by computing the percentages of inputs whose classification outputs we can prove as fair or unfair. 





 §.§ Limitations of Prior Work


One possible solution to the fairness certification problem as defined above would be explicit enumeration of the (x,x') pairs. For each x∈ X, we may flip its protected attribute to generate x' and then check if f(x)=f(x').  

However, since the size of the input domain X may be extremely large  or infinite, this method would be prohibitively expensive in practice. 

Another possible solution is to leverage existing DNN robustness verifiers, such as ReluVal <cit.>, DeepPoly <cit.>, and α-β-CROWN <cit.>. However, since robustness and individual fairness are fundamentally different properties,  applying a robustness verifier would not work well in practice. 

The reason is because a robustness verifier takes an individual x and tries to prove that small perturbation of x (often defined by ||x-x'||<δ, where δ is a small constant) does not change the output label.

However, during fairness certification, we are not given a concrete individual x; instead, we are supposed to check for all x ∈ X and x' ∈ X, where x_j ≠ x'_j.

If we force a robustness verifier to take a symbolic input I (∀ x∈ X), it would try to prove that the DNN produces the same output label for all inputs in X (implying that the DNN makes the same decision for all inputs in X). 


Recall our example network f in Fig. <ref>. While our method can prove that f is fair for an input domain that contains x=⟨ 5,0,5 ⟩ and x'=⟨ 5,1,5⟩ (both receive a positive outcome) as well as x=⟨ 1,0,5 ⟩ and x'=⟨ 1,1,5⟩ (both receive a negative outcome), this cannot be accomplished by a robustness verifier (since it is almost never possible for all individuals in the input domain to have the same outcome).


The only currently available method for (qualitatively) certifying individual fairness of a DNN is  <cit.>, which relies on the SMT solver and may return one of the following results:

SAT (meaning that there exists a counterexample that violates the fairness property),  UNSAT (meaning that there is no counterexample), or UNKNOWN (meaning that the result remains inconclusive). 

The main problem of  is that it works directly in the concrete domain by precisely encoding the non-linear computations inside the DNN as logical formulas and solving these formulas using the SMT solver.

Since each call to the SMT solver is NP-complete, the overall computational cost is high.

Although  attempts to reduce the computational cost by partitioning input domain a priori and  heuristically pruning logical constraints, it does not scale as the network size and input dimension increase.  Indeed, our experimental evaluation of  shows that only tiny networks (with ≤ 100 neurons) can be certified.








 §.§ Novelty of Our Method




We overcome the aforementioned (accuracy and scalability) limitations by developing a method that is both scalable and able to quantify the degree of fairness.


First,   relies on abstraction to improve efficiency/scalability while maintaining the accuracy of symbolic forward analysis.  This increases the chance of quickly certifying more input regions as fair or falsifying them as unfair, and decreases the chance of leaving them as undecided.

Specifically, we use symbolic interval analysis, instead of the SMT solver used by . The advantage is that symbolic interval analysis focuses on the behavior of the DNN in an abstract domain, which is inherently more efficient and scalable than analysis in the concrete domain.  


Second,  relies on iterative refinement (partitioning of the input domain) to improve the accuracy of forward analysis. Instead of creating input partitions a priori, it conducts iterative refinement on a “need-to” basis guided by the fairness property to be certified.  


This makes it more effective than the static partitioning technique of , which divides the  input domain into a fixed number of equal chunks even before verifying any of them. 


To see why iterative refinement can improve accuracy, consider our running example in Fig. <ref>.  Initially, forward analysis is applied to the DNN in the entire input domain X, for which the certification result is undecided.

During refinement, our method would choose x_1 (over x_3) to split, based on its impact on the network's output.  After splitting x_1∈{1,2,3,4,5} into x_1∈{1,2,3} and x_1∈{4,5}, we apply forward analysis to each of these two new partitions. 


As shown in Fig. <ref>, while the partition for x_1∈{1,2,3} remains undecided, the  partition for x_1∈{4,5} is certified as fair.   This partition has 12 pairs of x ∈ X and x' ∈ X, where x_2 ≠ x'_2. Therefore, from the input domain X which has 30 (x, x') pairs, we certify 12/30 = 40% as fair.

Next, we split the undecided partition x_1∈{1,2,3} into x_1∈{1,2} and x_1∈{3} and apply forward analysis to each of these two new partitions.  While the first new partition remains undecided, the second one is certified as fair.  Since this partition has six (x, x') pairs, it represents 6/30=20% of the input domain.







This iterative refinement process continues until one of the following two termination conditions is satisfied:  either there is no more partition to apply forward analysis to, or a predetermined time limit (e.g., 30 minutes) is reached.



§ PRELIMINARIES




In this section, we review the fairness definitions as well as the basics of neural network verification. 




 §.§ Fairness Definitions


Let f:X→ Y be a classifier, where X is the input domain and Y is the output range.  Each input x∈ X is a vector in the D-dimensional attribute space, denoted x=⟨ x_1,…,x_D⟩, where 1,…,D are vector indices.  Each output y∈ Y is a class label. 

Some attributes are legally protected attributes (e.g., gender and race) while others are unprotected attributes. Let 𝒫 be the set of vector indices corresponding to protected attributes in x. We say that x_j is a protected attribute if and only if j ∈𝒫.



Given a classifier f, an input x ∈ X, and a protected attribute j ∈𝒫, we say that f is individually fair for x if and only if f(x) = f(x') for any x' ∈ X that differs from x only in the protected attribute x_j. 


This notion of fairness is local in the sense that it requires the classifier to treat an individual x in a manner that is oblivious to its protected attribute x_j of x. 







Given a classifier f, an input domain X, and a protected attribute j ∈𝒫, we say that f is individually fair  for the input domain X if and only if, for all x∈ X,  f(x)=f(x') holds for any x'∈ X that differs from x only in the protected attribute x_j. 


This notion of fairness is global since it requires the classifier to treat all x∈ X in a manner that is oblivious to the protected attribute x_j of x. 

The method of explicit enumeration would be  prohibitively expensive since the number of individuals in X may be astronomically large or infinite.




 §.§ Connecting Robustness to Fairness



Perturbation robustness, which is the most frequently checked property by existing DNN verifiers, is closely related to the notion of adversarial examples. The idea is that, if the DNN's classification output were robust, then applying a small perturbation to a given input x should not change the classifier's output for x.



Given a classifier f, an input x ∈ X, and a small constant δ,  we say that f is robust against δ-perturbation if and only if f(x)=f(x') holds for all x' ∈ X such that ||x-x'||≤δ. 


By definition, perturbation robustness is a local property defined for a particular input x, where the set of inputs defined by ||x-x'||≤δ is not supposed to be large. 

While in theory, a robustness verifier may be forced to check individual fairness by setting δ to a large value (e.g., to include the entire input domain X), it almost never works in practice. 

The reason is because, by definition, such a global robustness property requires that all inputs to have the same classification output returned by the DNN –  such a classifier f would be practically useless.


This observation has been confirmed by our experiments using α-β-CROWN <cit.>, a state-of-the-art DNN robustness verifier.  Toward this end, we have created a merged network that contains two copies of the same network, with one input for one protected attribute group (e.g., male) and the other input for the other group (e.g., female). While the verifier finds counterexamples in seconds (and thus falsifies fairness of the DNN), it has the same limitation as : it merely declares the DNN as unsafe (unfair, in our context) as soon as it finds a counterexample, but does not provide users with any meaningful, quantitative information.  

In contrast, our method provides a quantitative framework for certified fairness by reasoning about all individuals in the input domain.






§ OVERVIEW OF OUR METHOD



In this section, we present the top-level procedure of our method; detailed algorithms of the subroutines will be presented in subsequent sections.



Let the DNN y = f(x) be implemented as a series of affine transformations followed by nonlinear activations, where each affine transformation step and its subsequent nonlinear activation step constitute a hidden layer. 

Let l be the total number of hidden layers, then f=f_l(f_l-1(...f_2(f_1(x · W_1) · W_2)... · W_l-1).  For each k∈ [1,l], W_k denotes the affine transformation and f_k() denotes the nonlinear activation.

More specifically, W_1 consists of the edge weights at layer 1 and x · W_1 = Σ_i x_iw_1,i.  Furthermore, f_1 is the activation function, e.g.,  ReLU(x · W_1) = max(0, x · W_1). 



 §.§ The Basic Components


Similar to existing symbolic interval analysis based DNN verifiers <cit.>, our method consists of three basic components: forward analysis, classification, and refinement.



  
Forward Analysis

The goal of forward analysis is to compute upper and lower bounds of the network's output for all inputs. 

It starts by assigning a symbolic interval to each input attribute.  For example, in Fig. <ref>, i_1=[x_1,x_1] is symbolic, where x_1∈{0,1,2,3,4,5}. 


Compared to concrete values, symbolic values have the advantages of making the analysis faster and more scalable.  They are also sound in that they overapproximate the possible concrete values. 





  
Classification

In a binary classifier, e.g., the DNN in Fig. <ref> for making hiring decisions, the output is a singular node o whose numerical values needs to be turned to either the positive or the negative class label based on a threshold value (say 0).



For example, if o ∈ [0.3, 0.4], the output label is guaranteed to be positive since o>0 always holds, 

and if o ∈ [-0.7, -0.6], the output label is guaranteed to be negative since o<0 always holds.



However, if o ∈ [-0.7, 0.4], the output label  remains undecided – this is when our method needs to conduct refinement. 





  
Refinement

The goal of refinement is to partition the input domain of the DNN to improve the (upper and lower) symbolic bounds computed by forward analysis. 

Since approximation error may be introduced when linear bounds are pushed through nonlinear activation functions (e.g., unless ReLU is always on or always off), by partitioning the input domain, we hope to increase the chance that activation functions behave similar to their linear approximations for each of the new (and smaller) input partitions, thus reducing the approximation error. 









 §.§ The Top-Level Procedure



Algorithm <ref> shows the top-level procedure, whose input consists of the network f, the protected attribute x_j, and the input domain X. 

Together, these three parameters define the fairness certification problem, denoted ⟨ f, x_j, X ⟩.




Within the top-level procedure, we first initialize the input partition P as X and push it into the stack S. Each input partition is associated with a refinement depth.  Since P is initially the entire input domain X, its refinement depth is set to 0.  Subsequently, the refinement depth increments every time P is bisected to two smaller partitions.  In general, the refinement depth of P⊆ X is the number of times that X is bisected to reach P.


In Lines 4-10 of Algorithm <ref>, we go through each partition stored in the stack S, until there is no partition left or a time limit is reached. For each partition P, we first apply symbolic forward analysis (Line 6) to check if the DNN f is fair for all individuals in P. There are three possible outcomes:

(1) fair (certified), meaning that f(x)=f(x') for all x∈ P and its counterpart x';

(2) unfair (falsified), meaning that f(x)≠ f(x') for all x∈ P and its counterpart x'; or

(3) undecided.

Next, if the result is undecided (Line 7), we apply backward refinement by splitting P into two disjoint new partitions P_l and P_u.  By focusing on each of these smaller partitions in a subsequent iteration step, we hope to increase the chance of certifying it as fair (or falsifying it as unfair). 


Finally, we quantify fairness (Line 10) by updating the percentages of certified (r_cer), falsified (r_fal) and undecided (r_und) inputs of X.

Specifically, if the previously-undecided partition P is now certified as fair, we decrease the undecided rate r_und by |P|/|X| and increase the certified rate r_cer by the same amount.

On the other hand, if P is falsified as unfair, we decrease r_und by |P|/|X| and increase the falsified rate r_fal by the same amount.



In the next three sections, we will present our detailed algorithms for forward analysis (Section <ref>), backward refinement (Section <ref>), and quantification (Section <ref>).





 §.§ The Correctness



Before presenting the detailed algorithms, we would like to make two claims about the correctness of our method.

The first claim is about the qualitative result of forward analysis, which may be fair, unfair, or undecided.


When forward analysis declares an input partition P⊆ X as fair, the result is guaranteed to be sound in that f(x)=f'(x) holds for all x∈ P and its counterpart x', 

Similarly, when forward analysis declares P as unfair, the result is guaranteed to be sound in that 
 f(x)≠ f'(x) holds for all x∈ P and its counterpart x'.



The above soundness guarantee is because SymbolicForward soundly overapproximates the DNN's actual behavior.

That is, the upper bound UB is possibly-bigger than the actual value, and the lower bound LB is possibly-smaller than the actual value. As a result, the symbolic interval [LB, UB] computed by SymbolicForward guarantees to include all concrete values.

In the next three sections, we shall discuss in more detail how the symbolic interval is used to decide if P is fair, unfair, or undecided.

When an input partition P is undecided, it means that some individuals in P may be treated fairly whereas others in P may be treated unfairly.



This brings us to the second claim about the quantitative result of our method, represented by the rates r_cer, r_fal and r_und.


The certification rate r_cer computed by our method is guaranteed to be a lower bound of the percentage of inputs whose outputs are actually fair. 

Similarly, the falsified rate r_fal is a lower bound of the percentage of inputs whose outputs are actually unfair.



In other words, when our method generates the percentages of fair and unfair inputs, it guarantees that they are provable lower bounds of certification and falsification, respectively.

The reason is because SymbolicForward soundly overapproximates the actual value range. When the output intervals indicate that the model is fair (unfair) for all inputs in P,  it is definitely fair (unfair). Thus, both r_cer and r_fal are guaranteed to be lower bounds.


Since the sum of the three rates is 1, meaning that r_und = 1 - r_cer - r_fal, the undecided rate r_und is guaranteed to be an upper bound.



§ SYMBOLIC FORWARD ANALYSIS




Algorithm <ref> shows our forward analysis subroutine, which takes the subproblem ⟨ f, x_j, P ⟩ as input and returns the certification result as output.  






 §.§ The Two Steps


Our forward analysis consists of two steps.  

First, a standard symbolic interval based analysis is invoked twice, for the symbolic inputs I and I', to compute the corresponding symbolic outputs O and O'.  

Second, O and O' are used to decide if the certification result is fair, unfair, or undecided.




In the first step, the symbolic input I = P|_x_j∈[0,0] is defined as the subset of input partition P where all inputs have the protected attribute x_j set to 0. 

In contrast, I' = P|_x_j∈[1,1] is defined as the subset of P where all inputs have x_j set to 1. 

The output O is a sound overapproximation of f(x) for x∈ I, whereas the output O' is a sound overapproximation of f(x') for x'∈ I'.

The subroutine ForwardPass used to compute O and O' is similar to any state-of-the-art neural network verifier based on symbolic interval analysis; in our implementation, we used the algorithm of ReluVal <cit.>. 



In the second step,  the two output intervals,
 O=[O_lb,O_ub] and 
 O'=[O'_lb,O'_ub], 
are used to compute the certification result. 

To understand how it works, recall that in the concrete domain, the numerical value of the DNN's output node is compared against a threshold, say 0, to determine if the output label should be positive or negative.

In the symbolic interval abstract domain,  the upper and lower bounds of the numerical values are used to determine if the model is fair, unfair, or undecided.

Below are the five scenarios:

    
  * If O_lb > 0 and O'_lb > 0,  both O and O' have the positive label, meaning that f is fair for P.
    
  * If O_ub < 0 and O'_ub < 0,  both O and O' have the  negative label, meaning that f is fair for P.
    
  * If O_lb > 0 and O'_ub < 0,  O is positive but O' is negative, meaning that f is unfair for P.
    
  * If O_ub < 0 and O'_lb > 0,  O is negative but O' is positive, meaning that f is unfair for P.
    
  * Otherwise,  f remains undecided for P.


Fig. <ref> illustrates the first four scenarios above. Specifically, the horizontal line segments represent the value intervals of O and O', whose upper/lower bounds may be either >0 or <0.  The vertical lines represent the threshold value 0. 








We can extend out method from two protected attribute (PA) groups (e.g., male and female) to more than two PA groups.

For example, if the protected attribute x_j has three values, we will have three symbolic inputs (I,I' and I”) and three corresponding symbolic outputs (O,O' and O”).

To decide if f is fair (or unfair) in this multi-PA group setting, we check if (1) individuals in each PA group receive the same output label; and (2) the output labels for the three PA groups are the same. 


We can also extend our method from binary classification to multi-valued classification.

For example, if there are three possible output labels, we will have O_1, O_2, and O_3 as the symbolic intervals for the three values for one PA group (I) and O'_1, O'_2 and O'_3 for the other PA group (I').

To decide if f is fair (or unfair) for this multi-valued classification, we check (1) which output labels are generated for  I and I'; and (2) whether these two output labels (O and O') are the same.




 §.§ The Running Example



For our running example in Fig. <ref>, consider the initial input partition P = X. For ease of understanding, we denote the symbolic expressions for a neuron n as S_in(n) after the affine transformation, and as S(n) after the ReLU activation. 

Furthermore, S will be used for I, and S' will be used  for I'.

Let 
I = P|_x_j=0 and I' = P|_x_j=1.
After affine transformation in the hidden layer, we have S_in(h_1) = 2x_1 + 1.2x_3 and S'_in(h_1) = 2x_1 + 1.2x_3 + 0.5. If we concretize these symbolic expressions, we will have S_in(h_1) = [2, 16] and S'_in(h_1) = [2.5, 16.5]. Based on these concrete intervals, we know that h_1 is always active for both I and I'. Since the activation function is ReLU, we have S(h_1) = S_in(h_1) and S'(h_1) = S'_in(h_1).

For the hidden neuron h_2, we have S_in(h_2) = -0.2x_1 + 0.4x_3 and S'_in(h_2) = -0.2x_1 + 0.4x_3 + 0.7, whose corresponding concrete bounds are [-1, 1.8] and [-0.3, 2.5], respectively. 

In both cases, since h_2 is nonlinear (neither always-on nor always-off), we must approximate the  values using linear expressions to obtain S(h_2) and S'(h_2). 

While we  use the sound overapproximation method of Wang et al. <cit.>,  other techniques (e.g., <cit.>) may also be used. 

After overapproximating the ReLU behavior of h_2, we obtain S(h_2) = [-0.128 x_1 + 0.257 x_3, -0.128 x_1 + 0.257 x_3 + 0.643] and S'(h_2) = [-0.178 x_1 + 0.357 x_3 + 0.625, -0.178 x_1 + 0.357 x_3 + 0.893].

Finally, we compute  S_in(o) = [0.528 x_1 - 0.017 x_3 - 0.643, 0.528 x_1 - 0.017 x_3] and S'_in(o) = [0.578 x_1 - 0.117 x_3 - 0.793, 0.578 x_1 - 0.117 x_3 - 0.525]. From these symbolic bounds, we  obtain the concrete bounds of O = [-0.2, 2.64] and O' = [-0.8, 2.368]. Since these output intervals are not tight enough to determine the output labels for I and I', which are needed to decide if the model is fair or unfair for the partition P, the model remains undecided. 

To improve the accuracy, we need to split P into smaller input partitions and then apply symbolic forward analysis to each partition again. How to split P will be addressed by the iterative backward refinement method presented in the next section.





§ ITERATIVE BACKWARD REFINEMENT



The goal of iterative backward refinement is to split the currently-undecided input partition P into smaller partitions, so that for each of these smaller partitions, symbolic forward analysis will obtain a more accurate result. Algorithm <ref> shows the pseudo code, which takes the network f and the partition P as input and returns two smaller partitions P_l and P_u as output. Inside this procedure, Lines 7-14 are related to splitting P, and Lines 2-6 are related to early termination conditions.









 §.§ Early Termination Conditions


In Lines 2-6 of Algorithm <ref>, we  check if P.depth exceeds the predefined max_refinement_depth. If the answer is yes,  we avoid splitting  P further. For example, if max_refinement_depth=20, it means the current partition P occupies only |P|/|X|= 1/2^20 of the entire input domain X. 

By increasing the refinement depth, we can decrease the percentage of undecided inputs over X.

If P.depth has not exceeded the maximal refinement depth, we check if P.depth exceeds the predefined min_sample_depth, which is set to a value (e.g., 15) smaller than max_refinement_depth.  When P.depth exceeds this threshold, we start searching for counterexamples in P via random sampling. 

Inside the random sampling subroutine SampledCEX(P) shown in Line 4, we sample up to 10 concrete inputs in P and check if x and its counterpart x' satisfy f(x) ≠ f(x'). If this condition is satisfied, a counterexample is found (but P remains undecided); in this case, we increment cex_count and stop splitting P. If no counterexample is found, we continue splitting P into smaller partitions.


Note that in both early termination cases (Lines 3 and 6), the partition P will be marked as undecided since  we are not able to decide whether the DNN model is fair or unfair to all individuals in P.





 §.§ Splitting Input Intervals


In Lines 7-14 of Algorithm <ref>, we split P into smaller partitions P_l and P_u by first identifying the input attribute x_i that has the largest influence on the output (Lines 8-12) and then bisecting its input interval x_i∈[lb,ub].


Our method for identifying the input attribute x_i is based on maximizing the impact of an input attribute on the network's output.  One way to estimate the impact is taking the product of the gradient g(x_i) and the input range |ub(x_i)-lb(x_i)|.  In the literature, the product is often called the smear value <cit.>.

Unlike existing methods such as Wang et al. <cit.>, however, our computation of the smear value is different because we must consider both inputs I and I', which may have different gradients. 


Specifically, during forward analysis, we store the neuron activation information in two gradient mask matrices denoted R and R', where R[i][j] is [1,1] if the j-th neuron at i-th layer is always active, [0,0] if it is always inactive, and [0,1] if it is unknown.  The neuron activation information is used later to perform backward refinement for this partition P.


During refinement, we first compute the two gradients g_I and g_I' and then take the average. Our goal is to identify the input attribute that has the largest overall influence on the network's output. 












 §.§ The Running Example


Consider our running example in Fig. <ref> again.  

To compute the smear value, we start with the output layer's edge weights, which are 0.2 for h_1 and -1 for h_2.

Since the ReLU associated with h_1 is always-on, g_I(h_1) and g_I'(h_1) are set to the interval [0.2,0.2].

However, since the ReLU associated with h_2 is nonlinear, as indicated by the gradient mask matrices R and R', g_I(h_2) and g_I'(h_2) are set to the interval [-1.0, 0].

Then, we propagate these gradient intervals backwardly, to get g_I(i_1) = g_I'(i_1) = [(0.2×2)+(0×-0.2), (0.2×2)+(-1×-0.2)] = [0.4, 0.6] and g_I(i_2) = g_I'(i_2) = [-0.6, 0.1] and g_I(i_3) = g_I'(i_3) = [-0.16, 0.24]. 

Next, we compute the average g, based on which we compute the smear values. Since x_1 has the smear value of 0.6 × 4 = 2.4  and x_3 has the smear value of 0.24 × 5 = 1.2, we choose to partition P by bisecting the input interval of x_1. 

This leads to the smaller partitions shown in  Fig. <ref>.



 §.§ Generalization


While we only consider ReLU networks in this paper, our refinement technique can be extended to non-ReLU activations. Recall that, by definition, ReLU(z)=0 (inactive) if z<0, and ReLU(z)=1 (active) if z>0. Let σ(z) be a non-ReLU activation function. To compute the gradient mask matrices R and R', we use thresholds (ϵ_1,ϵ_2) to approximate the on/off behavior:

the mask is [0,0] (inactive) if z<ϵ_1 and [1,1] (active) if z>ϵ_2. 


Although the approximate on/off behavior of non-ReLU activation function σ(z) is not the same as the on/off behavior of ReLU(z), it serves as a practically-useful heuristic to rank the input attributes. Furthermore, this generalization will not affect the soundness of our method, since the gradient masks computed in this manner are only used for picking which input attribute to split first.



§ FAIRNESS QUANTIFICATION



We now present our method for updating the percentages of certified and falsified inputs, when the DNN model is found to be fair or unfair for the current input partition P.  The pseudo code is shown in Algorithm <ref>.




There are three cases.  

First, if the current partition P is found to be fair, meaning that all inputs in P are treated fairly,  we compute the percentage of input domain X covered by the partition P, denoted r_P, and then add r_P to r_cer, the percentage of certified inputs.

Second, if the current partition P is found to be unfair, meaning that all inputs in P are treated unfairly, we add r_P to r_fal, the percentage of falsified inputs.

In both cases, we also subtract r_p from r_und. 

Otherwise, the current partition P remains undecided and the percentages remain unchanged. 






Consider our running example with input partition P defined as x_1 ∈ [4,5] ∧ x_2 ∈ [0,1] ∧  x_3 ∈ [0,5],  as shown by the right child of the root node in Fig. <ref>. This partition has a total of 24 individuals, and its corresponding I = P|_x_2 = 0 and I'= P|_x_2 = 1 contain 12 individuals each. In contrast, the entire input domain X has 60 individuals, or 30 pairs of x and its counterpart x' (where x_2 ≠ x'_2). 

For this input partition P,  O = [1.49, 2.65] and O' = [1.0, 2.36] are the output intervals.   Assuming that the decision threshold is 0, the bounds of O and O' imply that the DNN model will generate the positive label for both I and I', meaning that the DNN model is fair for all individuals in P.

Since the input partition size is 12 and the input domain size is 30, the rate r_P = 12/30 = 40%.  After certifying P to be fair, we can add 40% to r_cer, the certification rate, and consequently subtract 40% from r_und, the undecided rate.


While the above computation assumes that population distribution for each feature is uniform and thus the percentage (e.g., 40%) is computed directly from the partition size (e.g., 12) and the domain size (e.g., 30), the method can be easily extended to consider a non-uniform population distribution.

Furthermore, note that the method works regardless of whether the input attributes have integer or real values.



§ EXPERIMENTS



We have implemented  in a software tool written in C, by leveraging the OpenBlas[http://www.openblas.net] library for fast matrix multiplication and symbolic representation of the upper and lower bounds.  Our forward analysis follows that of Wang et al. <cit.>.

For experimental comparison, we also run  which is the only currently-available tool for DNN individual fairness certification. 

Since  cannot quantify the degree of fairness, we compute the certified/falsified/undecided rates based on its reported statistics.


It is worth noting that  and our method () have a fundamental difference in falsification.  stops and declares an input partition as SAT as soon as it finds a  counterexample in that partition; thus, the number of counterexamples that it finds is always the same as the number of SAT partitions it reports. However, SAT partitions are not necessarily unfair partitions, since unfair partitions require all inputs to be counterexamples, but a SAT partition, excluding the one counterexample, still remains undecided.

 checks if an entire partition is unfair. Moreover, when the partition is undecided, it can minimize the amount of undecided inputs by only sampling for counterexamples after it reaches a deep enough refinement depth. This is made possible through our iterative refinement.

For example, in a DNN model named GC-3,  finds 194 SAT partitions (together with 6 UNSAT and 1 UNKNOWN partitions).  However, none of these 194 SAT partitions are unfair partitions. 

Instead, the percentage of falsified inputs is close to being 0% (representing 194 counterexamples out of over 435 trillion individuals in the input domain), the percentage of certified inputs is 2.985% (6 UNSAT partitions out of 201 partitions), and the rest remains undecided.

, on the other hand, finds 25,963 counterexamples; furthermore, it is able to formally certify 58.44% of the inputs as fair. 








 §.§ Benchmarks


Table <ref> shows the statistics of the benchmarks, including 32 deep neural networks trained on four popular datasets for fairness research.

Among the 32 networks, 25 came from  <cit.> and the other 7 were trained by ourselves using TensorFlow. All of these networks have a single node in the output layer, to determine the binary classification result. 


Columns 1-2 show the name of each dataset with its considered protected attribute (PA) and the number of input attributes.
Columns 3-6 show the name of each DNN model, its number of hidden layers, number of hidden neurons, and classification accuracy.
The accuracy for DNNs trained on  Bank, German, and Adult was provided by the  paper. For the models we trained using Compas, we have reserved 10% of the data for testing.


All the networks coming directly from  on Bank, German, and Adult datasets are small, where the largest has only 200 hidden neurons. Moreover, most of them have only 1 or 2 hidden layers. Thus, we additionally trained much larger networks, with up to 10,000 hidden neurons, using the Compas dataset. 


Details of the four datasets are given as follows.

Bank <cit.> is a dataset for predicting if a bank client will subscribe to its marketing; it consists of 45,000 samples.

German <cit.> is a dataset for predicting the credit risk of a person; it consists of 1,000 samples.

Adult <cit.> is a dataset for predicting if a person earns more than $50,000; it consists of 32,561 samples.

Finally,
Compas <cit.> is a dataset for predicting the risk of recidivism; it consists of 6,172 samples.[We used the preprocessed Compas data provided by <cit.>.] 



We evaluate our method using three legally-protected input attributes.

For Bank and German, we use age; 
for Adult, we use gender; 
and for Compas, we use race.[
For Bank and German, we use binarized age attribute provided by . For Compas, we binarize race attribute as {white, non-white} as in <cit.>.
]

These are consistent with  and other prior works in the fairness research. 




 §.§ Experimental Setup


We ran all experiments on a computer with 2 CPU, 4GB memory, and Ubuntu 16.04 Linux operating system.   

We set a time limit of 30 minutes for each DNN model. 


Our experiments were designed to answer three research questions:

 
  * Is  more accurate than the current state-of-the-art in certifying individual fairness of a DNN model?

  * Is  more scalable than the current state-of-the-art in handling DNN models, especially when the network size increases? 

  * Is  more effective than the current state-of-the-art in providing feedback, e.g., by quantitatively measuring the percentages of certified, falsified, and undecided inputs?



 requires a parameter MS (maximum size of an input attribute) based on which it creates a fixed number of input partitions prior to certification.

On the DNN models trained for Bank, German, and Adult, we used the default MS values (100, 100, and 10) for  to create 510, 201, and 16000 partitions, respectively.

On the new DNN models trained for Compas, we set MS to a small value of 2 to create 20 partitions for .

This was done to maximize 's performance such that it does not “choke” in verifying each input partition.

By default,  uses 100 seconds as  “soft timeout” for each input partition and uses 30 minutes as “hard timeout” for the entire DNN. This means that it takes at most 100 seconds to verify a single input partition, and if unsolved, it just moves to the next partition, until the entire 30 minutes runs out.

To run , we set the parameters min_check_depth to 15 and max_refinement_depth to 20 for all DNN models. We also use 30 minutes as “hard timeout”, but  always finished before the limit.









 §.§ Experimental Results


Table <ref> shows the results of our method () in comparison with [The order in which  sorts the partitions before running the verification query is random and non-deterministic, so there may be minor difference in the reported counterexamples in the original evaluation and ours.].

Columns 1-2 show the names of the dataset and the DNN model.  

Columns 3-5 show the statistics reported by , including the time taken, whether a counterexample is found (Cex) and the number of counterexamples found (#Cex). T/O or M/O in Column 3 respectively means that  either spent all 30m or ran out of memory in the network pruning step prior to verifying any input partition.

Columns 6-8 show the percentage of certified, falsified and undecided inputs (Cer%, Fal%, Und%).

Columns 9-14 show the corresponding results from . 





  §.§.§ Results for  RQ 1


To answer the first research question (RQ 1), i.e., whether our method is more accurate than the current state-of-the-art,  we need to compare the results shown in Columns 4-5 (for ) with the results shown in Columns 10-11 (for ).  

Specifically, Columns 4 and 10 indicate whether the tool is able to find a counterexample () or not () within the time limit. 

While our method () found counterexamples for all 32 DNNs,  found counterexamples for only 20 of the 32 models. In addition, it found counterexamples for only one of the 7 newly added models.

Moreover, Columns 5 and 11 show that, on models where both tools found counterexamples, the number of counterexamples found by  is often thousands of times more.  For example, the largest number of counterexamples found by  is 194 (for GC-3) but the large number of counterexamples found by  is 71,012 (for AC-5). 




  §.§.§ Results for RQ 2


To answer the second research question (RQ 2), i.e., whether our method is more scalable than the current state-of-the-art, we need to compare the running time shown in Column 3 (for ) with the running time shown in Column 9 (for ).   

While our method () always finished within the time limit of 30 minutes,  timed out on compas-5 and ran out of memory on compas-6 and compas-7.

Even on the models where both tools finished, the time taken by  is significantly longer. 



To illustrate the scalability advantage of our method, we took a subset of the models for which both  and  finished, and plot the running time in a bar chart, shown on the left side of Fig. <ref>.  Here, the red bars represent the time taken by  and the blue bars represent the time taken by .  The results show that  is many orders of magnitude faster, and can certify DNN models that are well beyond the reach of .




  §.§.§ Results for RQ 3


To answer the third research question (RQ 3), i.e., whether our method is more effective in providing feedback to the user, we need to compare the results in Columns 6-8  (for ) with the results in Columns 12-14 (for ), which show the certified, falsified, and undecided percentages. 

Since  was not designed to quantitatively measure the degree of fairness, it did poorly in almost all cases. Except for a few DNN models for Bank, GC-4, and compas-1, its certified percentages are either 0 or close to 0, and its undecided percentages are almost 100%.  It means that, for the vast majority of individuals in the input domain, whether they are treated by the DNN model fairly or not remains undecided. 

In contrast, the certified percentages reported by our method () are significantly higher. For the models trained using the Compas dataset, in particular, the certified percentages are around or above 90%, and more importantly, the undecided percentages are always 0.  It means that  has partitioned the input domain in such a way that each partition is either certified as being fair, or falsified as being unfair. Even on the subset of DNN models where some inputs remain undecided by , the undecided percentages reported by our method are significantly lower than , as shown on the right side of Fig. <ref>. 




 §.§ Summary


The results show that our method is more accurate and more scalable than the current state-of-the-art techniques for qualitative certification. In addition, our method is able to formally quantify the degree of fairness, which is a capability that existing methods do not have. 

For some DNN models,  still has a significant percentage of inputs left undecided. This is because we set min_check_depth=15 and max_refinement_depth=20 for all benchmarks.  Thus, as soon as  reaches the refinement depth 15 (see the refinement tree shown in Fig. <ref>) and finds a counterexample in the input partition, it will stop refining further; at that moment, all inputs in the partition are treated conservatively as undecided.  


In general, a smaller refinement depth allows  to terminate quickly. During our experiments,  terminated after 0.29s and 1.24s for GC-4 and GC-5, respectively, compared to the 4 minutes and 30 minutes taken by  and yet returned better results.  

In fact, for GC-5,  spent 30 minutes but failed to find any counterexample. 

If we increase the refinement depth, by increasing the two threshold values of , its quantification results will get even better.





§ RELATED WORK



Our method is the first scalable method for certifying and quantifying individual fairness of a deep neural network, and it outperforms the most closely related prior work,  <cit.>, which is the only tool currently available for certifying individual fairness of a DNN. 

To the best of our knowledge, no other methods can match the accuracy, scalability, and functionality of our method.

Our method differs from existing techniques for verifying other types of individual fairness properties for neural networks. 


For example, techniques in <cit.> and <cit.> tackle a different type of fairness property proposed in <cit.> that allows some perturbation for the non-protected attributes. They are orthogonal to our certification and quantification techniques. 




Other techniques <cit.> locally verify a type of property known as ε-fairness which, similar to robustness, is defined using a given input x and a small constant for perturbation. 

Group fairness is yet another type of fairness property, which can be verified using probabilistic techniques <cit.>. 

The difference between individual fairness and group fairness is that, while individual fairness requires similar individuals to be treated similarly, group fairness requires similar demographic groups to be treated similarly.

Furthermore, dependency fairness is studied in <cit.> and <cit.>.

All of these fairness properties are different from one another in varying degrees. 


There are other prior works related to fairness of machine learning models.

For example, existing works like <cit.>, <cit.>, and <cit.> proposed fairness verification techniques for other types of machine learning models, but they are not applicable to deep neural networks.

Testing techniques can quickly detect fairness violations in machine learning models <cit.>, 

but it does not provide formal guarantee that is important for certain applications. 

There are also techniques for improving fairness of machine learning models <cit.>, but they differ significantly from our method, which focuses on certifying and quantifying fairness of existing DNN models. 


At a high level, our method is related to the large number of robustness verifiers for deep neural networks based on interval analysis <cit.>, SMT solving <cit.> and mixed-integer linear programming <cit.>.

While these verifiers can decide if a model is robust against adversarial perturbation, as explained earlier in Section 2, they cannot directly certify individual fairness.  

Other neural network verifiers  that deal with differential verification <cit.> or equivalence verification <cit.> are also different, since they evaluate over two networks instead of one network. 




§ CONCLUSION



We have presented , a scalable method for certifying and quantifying individual fairness of a deep neural network over the entire input domain.  It relies on sound abstraction during symbolic forward analysis to improve scalability, and iterative refinement to improve accuracy.  In addition to certifying fairness, it is able to quantify the degree of fairness by computing the percentages of inputs whose  classification outputs can be certified as fair or falsified as unfair. 

We have evaluated the method on a large number of DNN models trained using four popular fairness research datasets. The experimental results show that the method significantly outperforms state-of-the-art techniques in terms of both accuracy and scalability, as well as the ability to quantify the degree of fairness.




§ ACKNOWLEDGMENTS


This research was supported in part by the U.S. National
Science Foundation (NSF) under grant CCF-2220345. 

We thank the anonymous reviewers for their constructive feedback.





*

ieeetr


