Probabilistic Verification of Neural Networks Against Group Fairness

In this step, we construct a Discrete-Time Markov Chain (DTMC) which approximates $N$ (i.e., line 2 of Algorithm 1). DTMCs are widely used to model the behavior of stochastic systems [10], and they are often considered reasonably human-interpretable. Example DTMCs are shown in Figure 1. The definition of DTMC is presented in Appendix 0.A.2. Algorithm 2 shows the details of this step. The overall idea is to construct a DTMC, based on which we can perform various analysis such as verifying fairness. To make sure the analysis result on the DTMC applies to the original $N$, it is important that the DTMC is constructed in such a way that it preserves properties such as probabilistic reachability analysis (which is necessary for verifying fairness as we show later). Algorithm 2 is thus base on the recent work published in [10], which develops a sampling method for learning DTMC. To learn a DTMC which satisfies our requirements, we must answer three questions.

(1) What are the states $S$ in the DTMC? The choice of $S$ has certain consequences in our approach. First, it constrains the kind of properties that we are allowed to analyze based on the DTMC. As we aim to verify fairness, the states must minimally include states representing different protected features, and states representing prediction outcomes. The reason is that, with these states, we can turn the problem of verifying fairness into probabilistic reachability analysis based on the DTMC, as we show in Section 3.2. What additionally are the states to be included depends on the level of details that we would like to have for subsequent analysis. For instance, we include states representing other features at the input layer, and states representing the status of hidden neurons. Having these additional states allows us to analyze the correlation between the states and the prediction outcome. For instance, having states representing a particular feature (or the status of a neuron of a hidden layer) allows us to check how sensitive the prediction outcome is with respect to the feature (or the status of a neuron). Second, the choice of states may have an impact on the cost of learning the DTMC. In general, the more states there are, the more expensive it is to learn the DTMC. In Section 4, we show empirically the impact of having different sizes of $S$. We remark that to represent continuous input features and hidden neural states using discrete states, we discretize their values (e.g., using binning or clustering methods such as Kmeans [42] based on a user-provided number of clusters).

(2) How do we identify the transition probability matrix? The answer is to repeatedly sample inputs (by sampling based on a prior probability distribution) and then monitor the trace of the inputs, i.e., the sequence of transitions triggered by the inputs. After sampling a sufficiently large number of inputs, the transition probability matrix then can be estimated based on the frequency of transitions between states in the traces. In general, the question of estimating the transition probability matrix of a DTMC is a well-studied topic and many approaches have been proposed, including frequency estimation, Laplace smoothing [10] and Good-Turing estimation [26]. In this work, we adopt the following simple and effective estimation method. Let $W$ be a set of traces which can be regarded as a bag of transitions. We write $n_{p}$ where $p\in S$ to denote the number transitions in $W$ originated from state $p$. We write $n_{pq}$ where $p\in S$ and $q\in S$ to be the number of transitions observed from state $p$ to $q$ in $W$. Let $m$ be the total number of states in $S$. The transition probability matrix $A_{W}$ (estimated based on $W$) is: $A_{W}(p,q)=\left\{\begin{array}[]{ll}\frac{n_{pq}}{n_{p}}&\mbox{if $n_{q}\neq 0$}\\ \frac{1}{m}&\mbox{otherwise}\end{array}\right.$. Intuitively, the probability of transition from state $p$ to $q$ is estimated as the number of transitions from $p$ to $q$ divided by the total number of transitions taken from state $p$ observed in $W$. Note that if a state $p$ has not been visited, $A_{W}(p,q)$ is estimated by $\frac{1}{m}$; otherwise, $A_{W}(p,q)$ is estimated by $\frac{n_{pq}}{n_{p}}$.

(3) How do we know that the estimated transition probability matrix is accurate enough for the purpose of verifying fairness? Formally, let $A_{W}$ be the transition probability matrix estimated as above; and let $A$ be the actual transition probability matrix. We would like the following to be satisfied.

where $\epsilon>0$ and $\delta>0$ are constants representing accuracy and confidence; $\emph{Div}(A,A_{W})$ represents the divergence between $A$ and $A_{W}$; and $P$ is the probability. Intuitively, the learned DTMC must be estimated such that the probability of the divergence between $A_{W}$ and $A$ greater than $\epsilon$ is no larger than the confidence level $\delta$. In this work, we define the divergence based on the individual transition probability, i.e.,

Intuitively, we would like to sample traces until the observed transition probabilities $A_{W}(p,q)=\frac{n_{pq}}{n_{p}}$ are close to the real transition probability $A(p,q)$ to a certain level for all $p,q\in S$. Theorem 1 in the recently published work [10] shows that if we sample enough samples such that for each $p\in S$, $n_{p}$ satisfies

where $\delta^{\prime}=\frac{\delta}{m}$, we can guarantee the learned DTMC is sound with respect to $N$ in terms of probabilistic reachability analysis. Formally, let $H(n)=\frac{2}{\epsilon^{2}}log(\frac{2}{\delta^{\prime}})[\frac{1}{4}-(max_{q}|\frac{1}{2}-\frac{n_{pq}}{n_{p}}|-\frac{2}{3}\epsilon)^{2}]$,

Appendix 0.A.3 provides the proof. Intuitively, the theorem provides a bound on the number of traces that we must sample in order to guarantee that the learned DTMC is PAC-correct with respect to any CTL property, which provides a way of verifying fairness as we show in Section 3.2.

We now go through Algorithm 2 in detail. The loop from line 3 to 8 keeps sampling inputs and obtains traces. Note that we use the uniform sampling by default and would sample according to the actual distribution if it is provided. Next, we update $A_{W}$ as explained above at line 6. Then we check if more samples are needed by monitoring if a sufficient number of traces has been sampled according to Theorem 3.1. If it is the case, we output the DTMC as the result. Otherwise, we repeat the steps to generate new samples and update the model.

In this step, we verify $N$ against the fairness property $\phi$ based on the learned $D$. Note that $D$ is PAC-correct only with respect to CTL properties. Thus it is infeasible to directly verify $\phi$ (which is not a CTL property). Our remedy is to compute $P(Y=l\>|\>F=f_{i})$ and $P(Y=l\>|\>F=f_{j})$ separately and then verify $\phi$ based on the results. Because we demand there is always a state in $S$ representing $F=f_{i}$ and a state representing $Y=l$, the problem of computing $P(Y=l\>|\>F=f_{i})$ can be reduced to a probabilistic reachability checking problem $\psi$, i.e., the probability of reaching the state representing $Y=l$ from the state representing $F=f_{i}$. This can be solved using probabilistic model checking techniques. Probabilistic model checking [39] of DTMC is a formal verification method for analyzing DTMC against formally-specified quantitative properties (e.g., PCTL). Probabilistic model checking algorithms are often based on a combination of graph-based algorithms and numerical techniques. For straightforward properties such as computing the probability that a U (Until), F (Finally) or $\textbf{G}(Globally)$ path formula is satisfied, the problem can be reduced to solving a system of linear equations [39]. We refer to the readers to [39] for a complete and systematic formulate of the algorithm for probabilistic model checking.

Next we verify the fairness property $\phi$ based on the result of probabilistic model checking. First, the following is immediate based on Theorem 3.1.

Appendix 0.A.4 provides the proof. Hence, given an expected accuracy $\mu\epsilon$ and a confidence level $\mu\delta$ on fairness property $\phi$ , we can derive $\epsilon$ and $\delta$ to be used in Algorithm 2 as: $\epsilon=\frac{\mu\epsilon}{2}$ and $\delta=1-\sqrt{1-\mu\delta}$. We compute the probability of $P(Y=l\>|\>F=f_{i})$ and $P(Y=l\>|\>F=f_{j})$ based on the learned $D$ (i.e., line 3 of Algorithm 1). Next, we compare $|P(Y=l\>|\>F=f_{i})-P(Y=l\>|\>F=f_{j})|$ with $\xi$. If the difference is no larger than $\xi$, fairness is verified. The following establishes the correctness of Algorithm 1.

Appendix 0.A.5 provides the proof.

The overall time complexity of model learning and probabilistic model checking is linear in the number of traces sampled, i.e., $\textbf{O}(n)$ where $n$ is the total number of traces sampled. Here $n$ is determined by $H(n)$ as well as the probability distribution of the states. Contribution of $H(n)$ can be determined as $\textbf{O}(\frac{\log m}{\mu\epsilon^{2}\log\mu\delta})$ based on Equation 6, where $m$ is the total number of states. In the first case, for a model with only input features and output predictions as states, the probability of reaching each input states are statistically equal if we apply uniform sampling to generate IID input vectors. In this scenario the overall time complexity is $\textbf{O}(\frac{m\log m}{\mu\epsilon^{2}\log\mu\delta})$. In the second case, for a model with states representing the status of hidden layer neurons, we need to consider the probability for each hidden neuron states when the sampled inputs are fed into the network $N$. In the best case, the probabilities are equal, we denote $m^{\prime}$ as the maximum number of states in one layer among all layers included, the complexity is then $\textbf{O}(\frac{m^{\prime}\log m}{\mu\epsilon^{2}\log\mu\delta})$. In the worst case, certain neuron is never activated (or certain predefined state is never reached) no matter what the input is. Since the probability distribution among the hidden states are highly network-dependent, we are not able to estimate the average performance.

In the case that the verification result shows $\phi$ is satisfied, our approach outputs $D$ and terminates successfully. We remark that in such a case $D$ can be regarded as the evidence for the verification result as well as a human-interpretable explanation on why fairness is satisfied. In the case that $\phi$ is not satisfied, a natural question is: how do we improve the neural network for fairness? Existing approaches have proposed methods for improving fairness such as by training without the protected features [55] (i.e., a form of pre-processing) or training with fairness as an objective [16] (i.e., a form of in-processing). In the following, we show that a post-processing method can be supported based on the learned DTMC. That is, we can identify the neurons which are responsible for violating the fairness based on the learned DTMC and “mutate” the neural network slightly, e.g., adjusting its weights, to achieve fairness.

We start with a sensitivity analysis to understand the impact of each probabilistic distribution (e.g., of the non-protected features or hidden neurons) on the prediction outcome. Let $F$ be the set of discrete states representing different protected feature values. Let $I$ represent a non-protected feature or an internal neuron. We denote $I_{i}$ as a particular state in the DTMC which represents certain group of values of the feature or neuron. Let $l$ represent the prediction result that we are interested in. The sensitivity of $I$ (with respect to the outcome $l$) is defined as follows.

where $reach(s,s^{\prime})$ for any state $s$ and $s^{\prime}$ represents the probability of reaching $s^{\prime}$ from $s$. Intuitively, the sensitivity of $I$ is the summation of the ‘sensitivity’ of every state $I_{i}$, which is calculated as $\max_{f,g}\big{(}reach(f,I_{i})-reach(g,I_{i})\big{)}$, i.e., the maximum probability difference of reaching $I_{i}$ from all possible protected feature states. The result is then multiplied with the probability of reaching $I_{i}$ from start state $S_{0}$ and the probability of reaching $l$ from $I_{i}$. Our approach analyzes all non-protected features and hidden neurons and identify the most sensitive features or neurons for improving fairness in step 4.

In this step, we demonstrate one way of improving neural network fairness based on our analysis result, i.e., by adjusting weight parameters of the neurons identified in step 3. The idea is to search for a small adjustment through optimization techniques such that the fairness property is satisfied. In particular, we adopt the Particle Swarm Optimization (PSO) algorithm [37], which simulates intelligent collective behavior of animals such as flocks of birds and schools of fish. In PSO multiple particles are placed in the search space and the optimization target is to find the best location, where the fitness function is used to determine the best location. We omit the details of PSO here due to space limitation and present it in Appendix LABEL:A:PSO.

In our approach, the weights of the most sensitive neurons are the subject for optimization and thus are represented by the location of the particles in the PSO. The initial location of each particle is set to the original weights and the initial velocity is set to zero. The fitness function is defined as follows.

where $Prob_{diff}$ represents the maximum probability difference of getting a desired outcome among all different values of the sensitive feature; $accuracy$ is the accuracy of repaired network on the training dataset and constant parameter $\alpha\in(0,1)$ determines the importance of the accuracy (relative to the fairness). Intuitively, the objective is to satisfy fairness and not to sacrifice accuracy too much. We set the bounds of weight adjustment to $(0,2)$, i.e., 0 to 2 times of the original weight. The maximum number of iteration is set to 100. To further reduce the searching time, we stop the search as soon as the fairness property is satisfied or we fail to find a better location in the last 10 consecutive iterations.

In the following, we evaluate our method in order to answer multiple research questions (RQs) based on multiple neural networks trained on 4 datasets adopted from existing research [54, 4, 58, 28], i.e., in addition to the Census Income [18] dataset as introduced in Example 1, we have the following three datasets. First is the German Credit [19] dataset consisting of 1k instances containing 20 features and is used to assess an individual’s credit. Age and gender are the two protected features. The labels are whether an individual’s credit is good or not. Second is the Bank Marketing [17] dataset consisting of 45k instances. There are 17 features, among which age is the protected feature. The labels are whether the client will subscribe a term deposit. Third is Jigsaw Comment [1] dataset. It consists of 313k text comments with average length of 80 words classified into toxic and non-toxic. The protected features analysed are race and religion.

Following existing approaches [54, 4, 58, 28], we train three 6-layer feed-forward neural networks (FFNN) on the first three dataset (with accuracy 0.88, 1 and 0.92 respectively) and train one recurrent neural network, i.e., 8-cell Long Short Term Memory (LSTM), for the last dataset (with accuracy 0.92) and analyze their fairness against the corresponding protected attributes. For the LSTM model, we adopt the state-of-the-art embedding tool GloVe [44]. We use the 50-dimension word vectors pre-trained on Wikipedia 2014 and Gigaword 5 dataset.

Recall that we need to sample inputs to learn a DTMC. In the case of first three datasets, inputs are sampled by generating randomly values within the range of each feature (in IID manner assuming a uniform distribution). In the case of the Jigsaw dataset, we cannot randomly generate and replace words as the resultant sentence is likely invalid. Inspired by the work in [41, 7, 33], our approach is to replace a randomly selected word with a randomly selected synonym (generated by Gensim [46]).

The other measurement is the number of traces that we are required to sample using Algorithm 2. For each model and protected feature, the number of traces generated in Algorithm 2 depends on number of categorical values defined for this protected feature and the number of predictions. That is, more categories and predictions result in more states in the learn a DTMC model, which subsequently lead to more traces required. Furthermore, the number of traces required also depends on the probabilistic distribution from each state in the model. As described in Algorithm 2, the minimum number of traces transiting from each state must be greater than $H(n)$. This is evidenced by results shown in Table 1, where the number of traces vary significantly between models or protected features, ranging from 2K to 35K. Although the number of traces is expected to increase for more complicated models, we believe that this is not a limiting factor since the sampling of the traces can be easily paralleled.

We further conduct an experiment to monitor the execution time required for the same neural network model with a different numbers of states in the learned DTMC. We keep other parameters (i.e., $\mu\epsilon$, $\mu\delta$ and $\phi$) the same. Note that hidden neurons are not selected as states to reduce the impact of the state distribution. We show one representative result (based on the mode trained on the Census Income dataset with attribute race as the protected feature) in Figure 2. As we can see the total execution time is bounded by $n\log n$ which tally with our time complexity analysis in Section 3.