arXiv:2605.19549v1 [cs.SE] 19 May 2026
Provable Fairness Repair for Deep Neural Networks Jianan Ma
Jingyi Wang§
Hangzhou Dianzi University, China Zhejiang University, China [email protected]
Zhejiang University, China [email protected]
Qi Xuan
Zhen Wang
Zhejiang University of Technology, China [email protected]
Hangzhou Dianzi University, China [email protected]
Abstract—Deep neural networks (DNNs) are suffering from ethical issues such as individual discrimination. In response, extensive NN repair techniques have been developed to adjust models and mitigate such undesired behaviors. However, existing fairness repair methods are typically data-centric, which often lack provable guarantees and generalization to unseen samples. To overcome these limitations, we propose P RO F, a novel fairness repair framework with provable guarantees. The key intuition of P RO F is to leverage interval bound propagation (a widely used NN verification technique) to soundly capture model outputs over the whole set S(x) around a biased sample x. The derived bounds are utilized to guide fairness repair which encourages the model to produce consistent outputs on S(x). Specifically, we integrate fairness constraints and model modifications into a unified constraint-solving formulation, which can be transformed to a Mixed-Integer Linear Programming (MILP) problem solvable by off-the-shelf solvers. The solution to the MILP problem effectively induces a repaired model with guaranteed fairness over the whole set S(x). We evaluate P RO F on four widely used benchmark datasets and demonstrate that it achieves provable fairness repair, with generalization of up to 95.93% on full datasets and 93.16% on the entire input space. Notably, P RO F can be easily configured to support multiple sensitive attributes and more practical fairness definitions, while providing provable repair guarantees and delivering around 90% fairness improvement. Our code is available at https://github.com/nninjn/ProF. Index Terms—neural network repair, fairness, interval bound propagation
I. I NTRODUCTION Deep neural networks (DNNs) have demonstrated impressive performance in a wide range of applications such as computer vision [1], natural language processing [2], and autonomous driving [3]. Despite the remarkable success, their increased adoption in sensitive domains (e.g., crime risk assessment [4], public policy [5], and credit scoring [6]) has raised concerns that DNNs learning from biased data can produce unfair results. Individual discrimination has become one of the most critical problems, where input pairs differing only in sensitive attributes (e.g., gender, age, etc.) receive different predictions [7]. In response to this threat, numerous studies on DNN fairness testing [8], [9], [10], [11], [12] and verification [13], [14], [15] have been proposed. These § Corresponding author: Jingyi Wang.
techniques aim to either uncover unfairness by generating discriminatory instances or to provide guarantees through formal methods. However, their analysis results cannot provide further solutions as they do not directly mitigate the unfairness. This raises a crucial question: how to repair the model (ultimately with provable guarantee) once biased behavior is identified? A typical method for DNN fairness repair is to retrain the model with a set of discriminatory inputs. While retraining is easy to deploy, it inherently faces challenges in real-world applications due to its high costs and the necessity of accessing the original training set, which may be impractical when the model is obtained from a third party or the training data are private. For more effective and efficient repair, researchers have proposed various methods that aim to adjust the parameters of a biased NN to eliminate discriminatory behaviors. Among them, a common paradigm inspired by traditional software programs debugging is to first identify the key units in the model that are responsible for discrimination. For example, CARE [16] constructs the causal model between neurons and model outputs to pinpoint problematic neurons, followed by using a heuristic algorithm to generate neuron-level patches to modify their parameters. In addition, some other approaches achieve repair through more efficient ways: RUNNER [17] design a loss function to iteratively optimize the identified biased neurons via gradient descent, while IDNN [18] directly isolate them. NeuFair [19], on the other hand, leverages the simulated annealing algorithm to provide statistical guarantees for group fairness repair. More recently, GRFT [9] has been proposed for more effective fairness testing and repair. It achieves state-of-the-art performance by directly minimizing the distance of model outputs between discriminatory inputs and their similar instances. Research gap - While prior repair methods have shown effectiveness in certain cases, they suffer from two fundamental limitations. First, the repair techniques they employ (e.g., heuristic algorithms, gradient-based parameter tuning, or neuron isolation) are empirical in nature and lack deterministic guarantees. Even on the discriminatory pair ⟨x, x′ ⟩ used in repair, these techniques may not ensure that the model’s outputs satisfy fairness constraints. Second, these approaches
use a set of discriminatory input pairs ⟨x, x′ ⟩ to analyze and repair model behavior, where x′ is chosen from S(x) (the set of all instances similar to x). As such, they only observe and correct unfairness over a limited region of S(x). Consequently, the repaired model may still exhibit unfair behavior on unseen or unsampled inputs, resulting in limited generalization. Our insight - To address the above challenges, our key idea is to leverage interval bound propagation (a widely used NN verification technique) to soundly capture model outputs over S(x). The derived bounds can be utilized to guide fairness repair, which encourages the model to produce consistent outputs across all similar instances. To further provide guarantees for repair, our intuition is to exploit these bounds as a bridge to integrate fairness constraints and model modifications to construct a unified constraint-solving formulation. The solution to this problem can induce a repaired model with guaranteed fairness over S(x). Our solution - Based on the above insight, we propose P RO F, a novel provable NN fairness repair framework. As illustrated in Fig. 2, P RO F consists of two core components. Given a DNN f (which can be sliced as the first L − 1 layers f1:L and the last layer fL ), the first step applies interval bound propagation to calculate the concrete bounds that soundly capture the outputs of f1:L (i.e., outputs in feature space). These bounds define axis-aligned hyperrectangles, which enables us to directly tighten them to mitigate feature differences. In the second step, a naive approach would be to use these concrete bounds to construct a constraint-solving problem, where the parameter changes of the final layer fL are treated as optimization variables. However, since concrete bounds are often overly conservative, P RO F synthesizes symbolic bounds to formulate a more precise problem, thereby avoiding excessive modifications. To make the new problem solvable by off-the-shelf solvers, we introduce the dual theorem to eliminate nonlinear operations while preserving soundness. Finally, P RO F establishes a Mixed-Integer Linear Programming (MILP) problem, ensuring that the solution induces a repaired model that is provably fair over the given set S(x). We have implemented P RO F as a self-contained toolkit and evaluated it on four popular datasets involving various sensitive attributes. The results demonstrate its effectiveness in correcting the unfairness over the given set S(x) with provable guarantees, and its substantial improvements in generalization over existing state-of-the-art repair methods. On average, P RO F achieves 95.93% and 93.16% relative fairness improvement on the full dataset and the full input space, where the best baseline achieves only 71.44% and 72.67%. For the setting with multiple sensitive attributes and more practical fairness definition, P RO F also exhibits remarkable generalization, keeping around 90% fairness improvement. Additional experiments with four state-of-the-art fairness testing frameworks further confirm its consistent effectiveness. To summarize, this paper makes the following contributions: •
We present P RO F, a novel framework for provable neural network fairness repair with three key technical innovations:
1) We leverage interval bound propagation to soundly capture the model outputs, and design a bounds tightening process to effectively mitigate biased behavior. 2) We synthesize symbolic bounds to precisely encode fairness constraints and model modifications into a unified constraint-solving formulation with provable guarantees. 3) We leverage the duality theorem to eliminate nonlinearities and construct an MILP tractable by existing solvers. • We evaluate P RO F on four widely adopted benchmark datasets and demonstrate that it significantly outperforms the state-of-the-art in terms of provable guarantees and generalization to unseen samples. • We release the code and scripts for this paper at https:// github.com/nninjn/ProF to facilitate future studies.
II. P RELIMINARY DNNs. In this work, we focus on DNN models for binary classification tasks. A DNN can be represented as a function f : Rm → R, which maps a high-dimensional input x ∈ Rm to an output f (x) ∈ R. It typically consists of an input layer f1 , several hidden layers {f2 , · · · , fL−1 }, and an output layer def fL . The first L − 1 layers, denoted as f1:L = fL−1 ◦ · · · ◦ f1 , transform the input into a d-dimensional feature space, i.e., f1:L (x) ∈ Rd , while the final layer fL makes the classification. The model predicts the positive class if f (x) ≥ 0 and the negative class otherwise. Given a training dataset Dtrain , a DNN is trained by minimizing binary cross-entropy (BCE) loss ℓ: X 1 ℓ(σ(f (xi )), y i ) min f |Dtrain | i i (x ,y )∈Dtrain
i
where σ and y ∈ {0, 1} denote the sigmoid function and the true label for the input xi , respectively. Interval Bound Propagation. Owing to its efficiency in computing NN output ranges, interval bound propagation is widely used in NN verification [20], [21], [22], [23], [24], [25]. The core idea involves propagating interval bounds layer-wise through the model, starting from predefined input domains. In contrast to exact verification methods [26], [27], [28] that rely on SAT solvers, interval arithmetic offers scalable approximations by symbolizing each neuron’s value as an interval derived from its predecessor layer. Here we briefly describe how it propagates the bounds through the linear layer and the activation layer (using ReLU as an example). For a neuron h after a linear transformation with weights W and bias b, its output bounds are computed as: X h=b+ (max(0, Wi ) · zi + min(0, Wi ) · zi ) , i
h=b+
X
(max(0, Wi ) · zi + min(0, Wi ) · zi )
(1)
i
where zi , zi are the bounds of the i-th neuron in the predecessor layer. For an unstable ReLU neuron h = ReLU(z) with input interval [l, u] where l < 0 < u, a sound interval
0,8
−1, 1
−6, 14 x3 = x1 + 6x2 1
x1
1
x3
6 x2
−6
x4
0, 14 0 ≤ h1 ≤ 0.7x3 + 4.2
max x3 , 0
max x4 , 0
x4 = x1 − 6x2 −6, 14
h1
h2
−0.1
1 −1.8, 1 y y = −0.1 h + h + 1 1 2
−0.1
0 ≤ h2 ≤ 0.7x4 + 4.2 0, 14
Fig. 1: Interval bound propagation on an example NN. All neurons have zero bias except the output neuron (bias=1).
propagation can be derived via linear relaxation in various ways [21], [29]. Here we show a simple triangular form: u 0≤h≤ · (z − l), h, h = [0, u] (2) u−l Example 1. Fig. 1 illustrates interval bound propagation on a simple NN, where the brown equations denote the neurons’ symbolic bounds and the black square brackets are concrete bounds. The input x1 and x2 are bounded by [0, 8] and [−1, 1]. Using Eq. (1), the interval propagation for the first layer concretizes the symbolic expressions x3 = x1 + 6x2 and x4 = x1 − 6x2 to concrete bounds [−6, 14] and [−6, 14]. Then the triangular relaxation from Eq. (2) is used to calculate the bounds of h1 and h2 , refining both to [0, 14]. The output y finally yields the bound [−1.8, 1]. Notably, this bound is usually conservative due to the input dependencies [30], [31] of interval arithmetic, which assumes that the propagation of each neuron is independent. For example, the minimum y = −1.8 implies h1 = h2 = 14, where no valid input (x1 , x2 ) can simultaneously achieve h1 = 14 and h2 = 14. We analyze how this issue impacts the repair process and present our solution in Sec. III-C and Sec. III-D. Individual Fairness. As established in prior work [8], [12], [32], individual fairness (IF) requires a model to produce consistent predictions for similar individuals who differ only in sensitive attributes. Let x = (x1 , x2 , · · · , xm ) ∈ Rm be an input. We define S(x) as the set of all inputs similar to x: S(x) = x′ | ∃j ∈ P, xj ̸= x′j ; ∀j ∈ NP, xj = x′j where xj and x′j denote the values of the j-th attribute in x and x′ , P is the set of sensitive/protected attribute indices, and NP represent the set of non-sensitive attribute indices. Recent work [13], [33] further relaxes this notion by allowing small perturbations on non-sensitive attributes. Specifically, a relaxed neighborhood S(x) is defined as: S(x) = x′ | ∃j ∈ P, xj ̸= x′j ; ∀j ∈ NP, |xj − x′j | ≤ ϵj where ϵj > 0 limits allowable variations on non-sensitive attribute j, reflecting that small differences (e.g., age differences of a few years) may not violate the fairness relation. Building on above notions, we define an input x as an Individual Discriminatory Instance (IDI) if there exists x′ ∈ S(x) such that: (f (x) ≥ 0 ∧ f (x′ ) < 0) ∨ (f (x) < 0 ∧ f (x′ ) ≥ 0).
Such a pair ⟨x, x′ ⟩ is referred to as an IDI pair. Given a NN f , we further define U(f, x, S(x)) as the set of all inputs in S(x) that result in unfair classification under f : U(f, x, S(x)) = {x′ ∈ S(x) | (f (x) ≥ 0 ∧ f (x′ ) < 0) ∨(f (x) < 0 ∧ f (x′ ) ≥ 0)}
(3)
Example 2. Let us revisit Fig. 1. Suppose we have an input x = (4, 0) with f (x) = 0.2, where x1 is the protected attribute ranging over [0, 8], and x2 is a non-sensitive attribute with ϵ = 1. The neighborhood S(x) is thus defined as {x′ | 0 ≤ x′1 ≤ 8, −1 ≤ x′2 ≤ 1}. It is easy to verify that there exists x′ ∈ S(x) such that f (x′ ) < 0; for example, x′ = (8, 1) yields f (x′ ) = −0.6. Therefore, x constitutes an IDI, and f violates individual fairness at this input. Problem Formulation. We now formalize our repair problem. Definition 1 (The IF repair problem). Given a DNN f and a repair set Dr = {x1 , x2 , . . . , xn }, where xi denotes the i-th input. The goal of provable repair is to find a modified DNN f˜ that guarantees IF over S(xi ) for every xi ∈ Dr , that is: ∀xi ∈ Dr , ∀x ∈ S(xi ) : U(f˜, x, S(xi )) = ∅
(4)
We also aim for the repair to exhibit generalization by mitigating unfairness on inputs beyond Dr . Consistent with prior repair work [18], [16], we assume access to a small set Dc of training data to preserve the model’s original performance. III. M ETHODOLOGY A. Overview Fig. 2 presents P RO F, our provable fairness repair framework for DNNs. It consists of two main components: (1) unfair feature extractor calibration via concrete bounds tightening, and (2) provable repair through symbolic bounds synthesis and constraint-solving. The first step operates in the feature space: by propagating interval bounds through the network, P RO F establishes sound over-approximation for the features of all similar individuals. Then a progressively bounds tightening process is designed to rectify the biased feature extractor, promoting feature consistency on similar individuals. In the second step, symbolic bounds (which are tighter than concrete bounds) are synthesized and combined with the fairness constraints to formulate a more precise constraint-solving problem that provides guarantees for repair. To eliminate the nonlinear operations, we introduce the dual theorem and transform the original problem into an MILP, while preserving soundness. B. Correcting Biased Feature Extractor The objective of this phase is to calibrate the model’s feature extraction part f1:L so that it produces features as consistent as possible for all inputs in the similar set S. The ideal scenario is that for any inputs x, x′ ∈ S(xi ), f1:L produces identical features and thus f makes the same classification, i.e., ∀x, x′ ∈ S(xi ) : f1:L (x) = f1:L (x′ )
(5)
Some prior works [17], [18], [9] pursue similar goals by either: (1) biased neuron identification via differential analysis
x!
𝐱
𝐱 Biased Model Slice
x" +
All inputs similar to x
Step1: Feature Extractor Calibration h!
𝐡
𝑓!"# ∘ ⋯ ∘ 𝑓#
Interval bound propagation
min
h"
"!"# ∘⋯∘"#
3𝐡− 𝐡 %
Bounds Tightening 𝐡, 𝐡 Concrete Bounds
+ 𝑓!"# ∘ ⋯ ∘ 𝑓#
Symbolic Bound Synthesis
𝑓!
h!
Input Set
𝑓&#
min 𝑓+! 𝐡 ≥ 0 fairness or constraints max 𝑓+ 𝐡 < 0 !
Concrete Bounds h"
Symbolic Bounds
parameter changes
Duality s. t. Theory
min 𝑓(! − 𝑓! # Dual constraints Symbolic bounds MILP Solver
Provable Fair Model
Step2: Provable Repair via Constraint Solving
Exact Bounds
Fig. 2: The overview of P RO F framework. For notational simplicity, we use f1:L to denote fL−1 ◦ · · · ◦ f1 hereafter. on given IDI pairs followed by parameter modification, or (2) retraining the models to minimize the distances between features extracted from the IDI pairs. In other words, they aim to reduce the distances between specific feature pairs (discrete point pairs in the purple region in Fig. 2, Step 1). However, these approaches rely on IDI pair ⟨x, x′ ⟩ generated either by sampling within the similar input set S(x) or existing testing methods [8], [10]. This sampling-driven nature inherently suffers from incomplete coverage of S(x), as finite samples cannot exhaustively represent the entire set. Consequently, some uncovered instances may still retain large feature discrepancies and thus lead to unfair classifications. To address this problem, we propose utilizing interval bound propagation to soundly characterize and mitigate the feature differences across the neighborhood set S(x). Unlike discrete sampling methods, our approach over-approximates the model’s feature-space outputs. Specifically, we employ autoi LiRPA [34] to calculate1 the concrete bounds [hi , h ] ⊂ Rd for each set S(xi ), such that: i h i ∀i ∈ [n], x ∈ S(xi ) : f1:L (x) ∈ hi , h (6) where [n] denotes the set {1, 2, . . . , n}. As shown in Fig. 2 i (Step 1, blue region), the derived interval [hi , h ] forms an axis-aligned hyperrectangle that provably encloses the exact def feature set Hi = {f1:L (x) | x ∈ S(xi )} (purple region). The axis-aligned property enables us to upper bound the maximum distance Ldis between features in Hi : def
Ldis =
max
x, x′ ∈S(xi )
With the derived upper bounds in hand, we design a progressive bounds tightening process to mitigate the bias in f1:L . This procedure iteratively reduces the ℓ1 -norm of the concrete bounds, thereby contracting the maximum feature distance. As detailed in Alg. 1 (Lines 2–4), the process begins by computing initial concrete bounds for each input xi ∈ Dr over its neighborhood set S(xi ). It then updates the concrete bounds and minimizes a normalized objective, which measures the relative ℓ1 -norm reduction between current and original bounds. This ratio, bounded within [0, 1], directly quantifies the degree of bias mitigation, where zero corresponds to the ideal scenario described in Eq. (5). We aggregate these ratios across all inputs in Dr to construct the fairness loss Lfair (Line 8 of Alg. 1). To preserve the model’s performance, the BCE loss Lbce is computed on a small set of training data Dc . We optimize the model parameters to minimize the combined objective L = Lfair + Lbce through gradient descent. Remark: While the above process can effectively mitigate bias in the feature extractor (see Section IV-E), the fixed-number gradient descent steps do not guarantee provable repair. The repaired feature extractor may still yield Lfair > 0, indicating potential feature discrepancies within some S(xi ) that could lead to unfair classifications. To address this problem, we proceed to repair the final layer fL in the following sections. We first present a naive method that directly utilizes the concrete bounds, followed by our proposed advanced approach that incorporates symbolic bounds for enhanced precision.
∥f1:L (x) − f1:L (x′ )∥1
= max ∥h − h′ ∥1 ≤ ′ i h,h ∈H
d X j=1
max |hj − h′j |
(7)
h,h′ ∈Hi
C. A Naive Provable Repair Method with Concrete Bounds
i
≤∥h − hi ∥1 1 There are several other interval propagation tools, such as DeepPoly [20]
and DeepZ [35], which vary in precision. We choose auto-LiRPA [34] due to its balanced trade-off between efficiency and precision.
In this section, we present a naive repair method for the final classification layer fL . Our core idea is to formulate the repair as a constraint-solving problem and leverage existing solvers to obtain the solution with provable guarantees. Formally, the
i
hyperrectangle [hi , h ]. Therefore, the summations over j of Pi,j and Qi,j can provide lower and upper bounds for i (W + ∆W)h across the whole hyperrectangle [hi , h ] while avoiding the multiplication between h and ∆W, i.e., X Pi,j ≤ min h i(W + ∆W)h
Algorithm 1: Biased Feature Calibration Input: Biased NN f = fL ◦ f1:L , repair set Dr , a small set of training data Dc , maximum iteration T Output: Repaired feature extractor f˜1:L 1 for i ← 1 to |Dr | do i def i 2 S(x )= h i Set of all inputs similar to x i 3 hi , h ← C ONCRETE B OUNDS(f1:L , S(xi ))
i
X
i
4
OriDiff i ← h − hi 1
9
11
∆W,∆b
fairness repair on fL is formulated as follows: min ∥∆W∥1 + ∥∆b∥1
(8)
∆W,∆b
s.t. ∀i ∈ [n], Hi = {f˜1:L (x) | x ∈ S(xi )} ∀i ∈ [n], min f˜L (h) ≥ 0 ∨ max f˜L (h) < 0
(9) (10)
h∈Hi
Here, f˜1:L denotes the feature extractor calibrated by Alg. 1 and f˜L (h) = (W+∆W)h+b+∆b is the repaired final layer, where W + ∆W ∈ R1×d and h ∈ Rd . Eq. (8) minimizes parameter modifications while Eq. (10) and Eq. (9) enforce fairness through output consistency across all inputs in S(xi ). We identify that existing solvers cannot directly handle the formulated problem due to two inherent complexities: (1) f˜1:L includes multiple nonlinear layers and thus the exact feature set Hi is highly non-convex, and (2) the constraint in Eq. (10) introduces multiplication terms ∆Wh, which are non-linear. To address the former, a straightforward method is to use the concrete bounds again to over-approximate Hi . Specifically, we simplify Eqs. (9) and (10) as follows: min h i(W + ∆W)h ≥ 0 i h∈ hi ,h
∨ b + ∆b +
max h i(W + ∆W)h < 0
h∈
(11)
i hi ,h
i
Since [hi , h ] over-approximates Hi , Eq.(11) consists of strengthened constraints that imply Eqs.(10) and (9). Moreover, the above simplification enables us to introduce two sets of variables {Pi,j }j∈[d] and {Qi,j }j∈[d] to capture the extreme values of (W + ∆W)h in each dimension: i
Pi,j ≤ (Wj + ∆Wj )hij ∧ Pi,j ≤ (Wj + ∆Wj )hj i
Qi,j ≥ (Wj + ∆Wj )hij ∧ Qi,j ≥ (Wj + ∆Wj )hj i
(14)
s.t. ∀i ∈ [n] (12), LBi ≥ 0 ∨ UBi < 0
return f1:L
∀i ∈ [n], b + ∆b +
i
h∈ hi ,h
min ∥∆W∥1 + ∥∆b∥1
i P|Dr | h − h 1 i=1 OriDiff i P Lbce ← |D1c | (x,y)∈Dc ℓ(σ(f (x)), y) f1:L ← G RADIENT D ESCENT(f1:L ; Lfair + Lbce )
Lfair ← |D1r |
h∈Hi
max i(W + ∆W)h h
P def def Let P LBi = b + ∆b + j∈[d] Pi,j and UBi = b + ∆b + j∈[d] Qi,j , we then transform the repair problem as:
i
10
(13)
Qi,j ≥
j∈[d]
for iter ← 1 to T do 6 for ih ← 1 to i |Dr | do i 7 hi , h ← C ONCRETE B OUNDS(f1:L , S(xi )) /* Update the concrete bounds */
5
8
h∈ hi ,h
j∈[d]
(12)
where hij and hj are the j-th dimensional endpoints of the
Note that the disjunction (∨) can be handled using BigM method (detailed in the next section). The upper half of Fig. 3 revisits Example 1, where the blue values indicate the parameter modifications from solving Problem (14), which 9 9 − 0.1) × h1 + ( 140 − enforces ∀h1 ∈ [0, 14], h2 ∈ [0, 14] : ( 140 0.1) × h2 + 1 ≥ 0 to ensure fairness. The provable guarantees achieved by solving Problem (14) are formally stated as: Theorem 1. Let Dr = {xi }ni=1 be a set of inputs, each associated with a similarity neighborhood S(xi ), and let f = fL ◦f˜1:L be a DNN. Then any feasible solution (∆W, ∆b) to the problem (14) induces a repaired final layer f˜L such that the composite model f˜ = f˜L ◦ f˜1:L provably satisfies individual fairness on all S(xi ), i ∈ [n]. Proof. Consider any feasible solution (∆Ẇ, ∆ḃ) to problem (14). Recall that the sets Hi satisfy Hi = {f1:L (x) | i x ∈ S(xi )} ⊆ [hi , h ] and that the lower and upper bounds LBi , UBi are constructed via the extreme values of auxiliary optimization problems Pi,j and Qi,j to satisfy LBi ≤
min i (W + ∆Ẇ)h + b + ∆ḃ
h∈[hi ,h ]
UBi ≥
max i (W + ∆Ẇ)h + b + ∆ḃ
h∈[hi ,h ] i
Since Hi ⊆ [hi , h ], these bounds also hold over Hi . By feasibility, the repair constraints ensure that either LBi ≥ 0 or UBi < 0, which guarantees that for all h ∈ Hi , the repaired model output f˜L (h) is consistently non-negative or negative. Consequently, the composite model f˜ = f˜L ◦ f˜1:L provably satisfies individual fairness across all neighborhoods S(xi ), i ∈ [n]. D. Provable Repair with Symbolic Bounds We now identify a crucial problem of the proposed naive i method: the concrete bound [hi , h ] is typically too conservative to capture the exact feature set Hi (purple region in figure). This leads to unnecessary modifications of the final i layer in order to enforce fairness across the entire box [hi , h ] rather than just the exact set Hi . As illustrated in the upper half of Fig. 3, such conservativeness results in excessive changes
0,8
0, 14 h1
x1
However, while symbolic bounds provide tighter approximations, they consist of a set of general linear constraints on x and h, forming a polytope with fundamentally different geometric structure from hyperrectangles. Note that one of the core challenge of provable repair stems from the non-linear term ∆Wh in fairness constraint minh (W + ∆W)h ≥ 0 ∨ i b i . Although maxh (W + ∆W)h < 0, where h ∈ [hi , h ] or H Section III-C handled this issue by exploiting the axis-aligned i b i lacks this nature and renders nature of [hi , h ], the polytope H the endpoint analysis in Eq. (12) inapplicable.
14 12
1 y −1, 1
x2
𝟎, 1
2
h2
2
1214
Concrete Bound: Exact Bound:
0, 14 𝟎 ≤ 𝐡𝟏 𝐡𝟏 ≤ 𝟎. 𝟕 𝐱 𝟏 + 𝟔𝐱 𝟐 + 𝟒. 𝟐
0,8
x1
14 12
h1 1 y
−1, 1
x2
𝟎, 1
h2
5.6
5.6
𝟎 ≤ 𝐡𝟐 𝐡𝟐 ≤ 𝟎. 𝟕 𝐱 𝟏 − 𝟔𝐱 𝟐 + 𝟒. 𝟐
1214
Symbolic Bound:
Fig. 3: Comparison of repair with concrete bounds and symbolic bounds. Purple region shows the true feature set Hi .
We leverage Lagrangian duality to address this problem. In the following, we take minh∈Hb i f˜L (h) ≥ 0 as an example to illustrate. The key idea is to recast the minimization over h as a maximization over dual variables λ, thereby decoupling the multiplication between ∆W and h while preserving soundness. Specifically, we first rewrite minh∈Hb i (W+∆W)h as follows: min C⊤ p s.t. Ai p ≤ Di (17) p
that account for spurious points outside Hi . This issue is exacerbated when the repair set Dr contains multiple inputs, requiring simultaneous satisfaction of fairness constraints over multiple sets S(x) (see Section IV-E). As discussed in Example 1, the imprecision of concrete bounds fundamentally stems from their assumption of interneuron independence during propagation, which discards crucial variable dependencies. To capture Hi more precisely, we propose synthesizing symbolic bounds, where each neuron’s bounds are characterized as a linear combination of preceding variables, thereby preserving the dependencies. Given a set S(xi ), we first utilize auto-LiRPA (other bound propagation tools are also applicable) to calculate the linear bounds between h and x, and further incorporate the input bounds to synthesize the symbolic bounds for repair as: n def ≤ ≥ ≥ bi = H h α≤ i x + β i ≤ h ≤ αi x + βi , (15) SL (xi ) ≤ x ≤ SU (xi ) ≤ ≥ ≥ where α≤ i , βi , αi and βi are linear coefficients and biases, i i SL (x ) and SU (x ) denote the lower bound and upper bound of S(xi ), respectively. The brown equations in Fig. 3 denote the symbolic bounds for our running example:
b i = {h | 0 ≤ h1 ≤ 0.7(x1 + 6x2 ) + 4.2, 0 ≤ x1 ≤ 8 H 0 ≤ h2 ≤ 0.7(x1 − 6x2 ) + 4.2, −1 ≤ x2 ≤ 1} b i (the brown area) is We can see that the region formed by H more precise than the one formed by concrete bounds. Once the symbolic bounds is obtained, the repair can be bi : formulated to guarantee that fairness constraints hold over H min ∥∆W∥1 + ∥∆b∥1
∆W,∆b
s.t. min f˜L (h) ≥ 0 ∨ max f˜L (h) < 0 bi h∈H
bi h∈H
(16)
h ∈ x Rm+d . Ai ∈ R(2m+2d)×(m+d) and Di ∈ R2m+2d are constant b i , constructed as: matrices that encode the definition of H −βi≤ −Id α≤ i β≥ I −α≥ d i i , D = Ai = i −SL (xi ) 0 −Im SU (xi ) 0 Im
⊤ where C = W + ∆W, 01×m ∈ R(m+d)×1 , p =
It is evident that Ai p ≤ Di is equivalent to the definition of b i given in Eq. (15). H Recalling Eq. (17), we observe that the variable ∆W in C can be temporarily treated as a constant, since the feasible set {p | Ai p ≤ Di } is independent of ∆W. In other words, problem (16) can be viewed as first solving the worst case p∗ under a given ∆W, then optimizing ∆W accordingly. Under this observation, Eq. (17) becomes a standard linear programming (LP). We define the Lagrangian function L and the dual function g to construct the dual problem of this LP: L(p, λi ) = C⊤ p + λ⊤ i (Ai p − Di ), λi ≥ 0 g(λi ) = inf L(p, λi )
(18)
p
where λi ∈ R2m+2d are dual variables. By maximizing the dual function, we obtain the optimality condition ∂L ∂p = C + ⊤ ⊤ Ai λi = 0 ⇒ Ai λi = −C and construct the dual problem: (Primal Problem) min C⊤ p p
s.t.
Ai p ≤ D i
(Dual Problem) max − λ⊤ i Di
λi ≥0
s.t.
(19)
A⊤ i λi = −C
In the dual problem, the non-linear term ∆Wh is decoupled, as only λi are variables and both Di , Ai are constants. We further note that the primal and dual problems attain the same
strong duality [36], we have:
optimal value due to the strong duality [36] for LP: min C⊤ p =
Ai p≤Di
max
A⊤ i λi =−C λi ≥0
−λ⊤ i Di
(20)
Similar to the previous section, we now define the variable c i to soundly lower bound the model’s output over H bi : LB c i = b + ∆b + (−λ⊤ LB i Di ) ≤ b + ∆b + max −λ⊤ i Di λi ⊤
= b + ∆b + min C p
s.t.
A⊤ i λi = −C λi ≥ 0
(21)
max
A⊤ i λi =−C̊ λi ≥0
−λ⊤ i Di =
min
A⊤ i ηi =C̊ ηi ≥0
min C̊⊤ p = min (W + ∆W̊)h
Ai p≤Di
bi h∈H
ηi⊤ Di = max C̊⊤ p = max (W + ∆W̊)h Ai p≤Di
bi h∈H
c i and Thus, the model outputs over S(xi ) are bounded by LB di as: UB c i = b + ∆b̊ + (−λ̊⊤ Di ) LB i ≤ b + ∆b̊ + max −λ⊤ i Di
Ai p≤Di
λi
= b + ∆b̊ + min (W + ∆W̊)h ⊤
Note that the upper bound (for b+∆b+maxAi p≤Di C p) can similarly be derived using another set of dual variables ηi ∈ R2m+2d . We can now recast the problem (16) as following MILP: min
∆W,∆b,Z,λ,η
∀i ∈ [n]
s.t.
A⊤ i λi = −C λi ≥ 0
s.t.
A⊤ i ηi = C ηi ≥ 0
= min f˜L (h) bi h∈H
≤ min f˜L (h) = min i f˜(x) h∈Hi
x∈S(x )
di = b + ∆b̊ + (η̊i⊤ Di ) UB ≥ b + ∆b̊ + min ηi⊤ Di
∥∆W∥1 + ∥∆b∥1
h i⊤ s.t. Z ∈ {0, 1}n , C = W + ∆W, 01×m −Id α≤ −βi≤ i I β≥ ≥ d −αi i Ai = , Di = i −S (x ) 0 −I m L i 0 Im SU (x )
bi h∈H
ηi
= b + ∆b̊ + max (W + ∆W̊)h bi h∈H
= max f˜L (h) bi h∈H
(22)
A⊤ λ = −C, λ ≥ 0
i i i ⊤ A η = C, η ≥ 0 i i i c LBi = b + ∆b + (−λ⊤ i Di ) ⊤ c UB = b + ∆b + (η i i Di ) c c i < M · Zi LBi ≥ −M · (1 − Zi ) ∧ UB
In the last row we employ the Big-M method to convert the disjunction operation to conjunction, where M is a sufficiently large constant. This MILP formulation eliminates the nonlinear term ∆Wh while maintains soundness through strong duality. The provable repair guarantees achieved by solving Problem (22), along with its superiority over Problem (14) in terms of objective value, are formally stated as follows:
≥ max f˜L (h) = maxi f˜(x) h∈Hi
x∈S(x )
where the blue inequality holds due to the soundness of bi . Finally, by integrating the symbolic bounds, i.e., Hi ⊆ H c i ≥ −M · (1 − Z̊i ) ∧ UB di < M · Z̊i , the model’s outputs LB over S(xi ) are strictly confined to either positive or negative regimes, guaranteeing consistent classifications and thereby ensuring individual fairness. We next prove that the optimal solution of problem (22) is guaranteed to be no worse than that of problem (14). The key point is that any feasible solution (∆Ẇ, ∆ḃ) of the problem (14) can be extended to a feasible solution (∆W, ∆b, Z, λ, η) of the MILP problem (22). This is because the symbolic bounds encoded in problem (22) are tighter than bi ⊆ [hi , hi ], thus we the concrete bounds, which implies H have: min i (W + ∆Ẇ)h ≤ min (W + ∆Ẇ)h
h∈[hi ,h ]
bi h∈H
Theorem 2. Let Dr = {xi }ni=1 be a set of inputs, each associated with a similarity neighborhood S(xi ), and let f = fL ◦ f˜1:L be a DNN. Then any feasible solution (∆W, ∆b, Z, λ, η) to the problem (22) induces a repaired final layer f˜L such that the composite model f˜ = f˜L ◦ f˜1:L provably satisfies individual fairness on all S(xi ), i ∈ [n]. Moreover, the optimal solution of problem (22) is guaranteed to be no worse than that of problem (14) (i.e., it achieves an objective value that is no larger).
In other words, the fairness constraints in problem (22) are relaxed compared to those in problem (14). Therefore, the feasible region of problem (14) is a subset of that of problem (22). Consequently, problem (22) minimizes the same objective over a (potentially) larger feasible region, and hence its optimal value is no greater than that of problem (14).
Proof. Consider (∆W̊, ∆b̊, Z̊, λ̊, η̊) as a feasible to solution W + ∆W̊ the MILP problem (22). We denote C̊ = . 0m Recalling the dual problem constructed in Eq. (19) and the
The overall algorithm of P RO F is shown in Algorithm 2. It first calibrates the feature extractor f1:L , then synthesizes symbolic bounds to formulate an MILP problem, which is solved by Gurobi [37] to achieve provable repair. Remark: While our illustration focused on binary classifi-
max i (W + ∆Ẇ)h ≥ max (W + ∆Ẇ)h
h∈[hi ,h ]
bi h∈H
Algorithm 2: P RO F Input: Biased NN f = fL ◦ f1:L , repair set Dr , a small set of training data Dc , maximum iteration T Output: Repaired model f˜ 1 f˜1:L ← B IASED F EATURE C ALIBRATION (f, Dr , Dc , T) /* Repair f1:L by Alg. 1 */ 2 for i ← 1 to |Dr | do def 3 S(xi ) = Set of all inputs similar to xi bi ← S YMBOLIC B OUND(f˜1:L , S(xi )) 4 H
2) Repair Setup: The original datasets Dfull are divided into the training set Dtrain and the test set Dtest . Then we randomly select 100 instances from Dtrain to construct the repair set Dr . We also provide a small set Dc ⊂ Dtrain for all methods to preserve model’s performance. Table I shows the size of these sets and the original accuracy of the DNN for each dataset.
Dataset
Dfull
Dtrain
Dr
Dc
Dtest
Original Acc
Construct the MILP problem M according to Eq. (22) 6 ∆W, ∆b, Z, λ, η ← Solve(M) 7 f˜L ← Linear(W + ∆W, b + ∆b) 8 return f˜L ◦ f˜1:L
Adult Compas German Bank
48 842 6 172 1 000 45 211
38 438 4 937 700 36 168
100 100 100 100
500 500 100 500
6 784 1 235 300 9 043
85.24% 73.85% 72.67% 89.53%
5
cation, we can naturally extend P RO F to multi-class tasks by adapting the second step. For each input xi , instead of computing scalar lower/upper bounds for a single output c i , UB di ∈ RN ) for neuron, we compute vectorized bounds (LB all N classes. We then vectorize the integer variables Zi in a one-hot manner P to represent the multi-class decision, i.e., Zi ∈ {0, 1}N , j Zi,j = 1. These modifications enable us to soundly formulate the MILP for multi-class task. IV. E VALUATION In this section, we evaluate P RO F through extensive experiments and answer the following research questions. RQ1: How effective is P RO F in repairing NN unfairness? RQ2: Can P RO F handle multiple protected attributes and more practical fairness definition? • RQ3: How effective is P RO F compared to baselines when evaluated by existing fairness testing frameworks? • RQ4: How do the two key steps of P RO F contribute to the repair performance? • •
A. Experimental Setup 1) Datasets and Models: We conduct experiments on four datasets including Adult (Census Income) [38], German Credit [39], Bank Marketing [40] and Compas [41], which are commonly used in fairness testing [8], [11], [10], [12] and repair [16], [9]. ❶ Adult is a dataset to predict whether a person earns more than $50 000. The protected attributes are gender, race, and age. ❷ Bank is a dataset for predicting if the bank client will subscribe a term deposit, with age being the sensitive attribute. ❸ German Credit is a dataset to assess creditworthiness based on personal and financial records. It has two protected attributes: gender and age. ❹ Compas is a dataset for assessing the likelihood of a criminal defendant reoffending. The protected attributes are gender, race, and age. The biased NNs for repair are sourced from previous fairness verification works Fairify [13] and FairQuant [14]. These models consist of various number of layers and neurons.
TABLE I: Details of datasets involved in repair and evaluation.
3) Baselines: We select the following NN individual fairness repair methods as baselines for comprehensive comparison: ❶ Flipping-based fine-tuning. This is a basic method for flipping the protected attributes (e.g., changing the gender from female to male) in each input while maintaining the ground truth labels. Through this learning paradigm, the biased model learns to make predictions that are insensitive to variations in protected attributes. ❷ CARE [16]. This method utilizes the causal model to pinpoint key neurons that are responsible for unfairness, followed by the PSO algorithm to generate neuron-level patches for repairing the model. ❸ GRFT [9]. As the latest state-of-the-art individual fairness repair framework, GRFT designs a loss function aimed at directly reducing differences in model outputs between IDI pairs. Our method involves two hyperparameters: the number of iterations T in Step 1, and the learning rate. We fix them to 200 and 0.001 across all scenarios. 4) Evaluation Metrics: We evaluate the repaired models from two perspectives: improvement in fairness and preservation of original performance. We also record the time costs of all methods. Details of fairness metrics are described below: Fairness improvement. Three metrics are considered for the fairness evaluation. The Certified Unfair Rate (CUR) assesses the percentage of inputs x in the repair set Dr for which the repaired model f˜ still produces biased outputs over S(x): CUR =
|Dr | 1 X ˜ i I U(f , x , S(xi )) ̸= ∅ |Dr | i=1
where I is the indicator function and U is the set of all IDI instances in S(x) as defined in Eq. (3). For finite S(xi ) (e.g., the protected attribute is gender and all non-sensitive attributes are fixed), we enumerate all possible items to check whether U(f˜, xi , S(xi )) is empty. For infinite cases, we employ the method from [42] that certify the model by solving an MILP. This MILP precisely computes the model output ranges so that we can verify whether f˜ is fair over S(xi ). A provable repair must guarantee that f˜ achieves zero CUR. An effective repair should generalize to unseen inputs. We assess this using two metrics: IDI-D, the proportion of inputs in the entire dataset Dfull that are IDIs; and IDI-S, the proportion of inputs identified as IDIs in a set Dsample consisting
TABLE II: Fairness improvement results for single-attribute repair. The best values are highlighted in bold. gender
Compas race
age
gender
Adult race
age
CUR
Original FLIP CARE GRFT Ours
5.00% 0.00% 0.00% 0.00% 0.00%
9.00% 6.00% 2.00% 1.00% 0.00%
42.00% 2.00% 17.00% 16.00% 0.00%
3.00% 2.00% 2.00% 0.00% 0.00%
2.00% 4.00% 2.00% 1.00% 0.00%
IDI-D
Original FLIP CARE GRFT Ours
6.25% 1.80% 3.19% 0.00% 0.00%
8.77% 8.25% 5.75% 2.37% 0.00%
44.86% 4.83% 16.96% 19.91% 0.49%
2.74% 2.95% 1.89% 0.98% 0.79%
IDI-S
Original FLIP CARE GRFT Ours
1.76% 0.63% 0.75% 0.00% 0.00%
2.73% 1.61% 0.93% 0.50% 0.00%
10.94% 3.08% 11.36% 1.74% 0.96%
0.65% 0.43% 0.75% 0.59% 0.12%
Metrics
Methods
German gender age
Bank age
Avg (Relative Drop)
14.00% 8.00% 6.00% 7.00% 0.00%
3.00% 7.00% 0.00% 0.00% 0.00%
4.00% 1.00% 1.00% 0.00% 0.00%
1.00% 2.00% 0.00% 0.00% 0.00%
9.22% (-) 3.56% (61.45%↓) 3.33% (63.86%↓) 2.78% (69.88%↓) 0.00% (100.00%↓)
4.15% 5.56% 2.69% 0.64% 1.48%
21.64% 8.14% 5.60% 2.38% 0.83%
2.60% 4.30% 0.10% 0.20% 0.00%
2.90% 0.40% 3.30% 0.10% 0.00%
1.12% 0.93% 1.39% 0.56% 0.29%
10.56% (-) 4.13% (60.91%↓) 4.54% (56.99%↓) 3.02% (71.44%↓) 0.43% (95.93%↓)
0.53% 0.33% 0.28% 0.48% 0.30%
3.65% 1.25% 3.30% 2.51% 0.26%
7.43% 2.99% 2.46% 1.98% 0.00%
8.77% 3.76% 7.14% 2.31% 0.00%
6.67% 3.06% 4.40% 1.67% 1.31%
4.79% (-) 1.90% (60.27%↓) 3.49% (27.24%↓) 1.31% (72.67%↓) 0.33% (93.16%↓)
of 100 000 instances randomly sampled from full input space, following prior work [8], [11], [12]. To compute IDI-D and IDI-S, we enumerate all similar inputs in S(x) for each instance x ∈ Dfull or Dsample when S(x) is finite; otherwise, we conduct uniform sampling over S(x) to obtain statistically significant estimates. For both metrics, lower values indicate better fairness improvement after repair. In addition to the above metrics, we further incorporate four state-of-the-art fairness testing frameworks to evaluate P RO F and all baselines: ADF [8], EIDIG [11], NeuronFair [12], and GRFT [9]. We configured these frameworks following their technical papers and used them to generate IDIs for both the original and the repaired models. Fewer IDIs detected on the repaired models indicate better repair effectiveness. B. RQ1: How effective is P RO F in repairing NN unfairness? To answer this research question, we evaluate the performance of all repair methods. The results are summarized in Table II. As we can see, all methods lead to a notable reduction in the Certified Unfairness Rate (CUR), while P RO F consistently achieves provable fairness guarantees, reducing CUR to 0 across all settings. In contrast, existing baselines provide no theoretical guarantees and only reduce CUR by approximately 60–70%. In terms of generalization to unseen inputs, our method also outperforms all baselines. On both the full dataset Dfull and the sampled set Dsample , the models repaired by P RO F yield extremely low unfairness: the average IDI-D and IDI-S rates are reduced to just 0.43% and 0.33%, corresponding to relative reductions of 95.93% and 93.16%, respectively. The best-performing baseline, GRFT, only achieves 71.44% and 72.67% reductions in IDI-D and IDI-S. Regarding performance preservation, we present the accuracy of the repaired models in Table III. We find that all methods introduce some accuracy degradation. Among them, FLIP and P RO F exhibit more stable performance, with average accuracy losses of 1.81% and 2.27%, respectively. By comparison, CARE and GRFT can have a notable negative impact on model performance in certain scenarios. For instance, when
TABLE III: Accuracy of repaired models, where colors denote accuracy loss: green (≤3%), orange (3–5%), red (>5%). Dataset
Prot. Attr.
FLIP
CARE
GRFT
Ours
Compas Compas Compas Adult Adult Adult German German Bank
gender race age gender race age gender age age
72.39% 72.87% 70.53% 83.65% 83.58% 84.51% 68.67% 70.33% 89.28%
73.44% 71.42% 65.43% 84.39% 84.52% 80.78% 69.33% 72.67% 88.80%
72.71% 73.60% 63.24% 82.06% 81.07% 80.26% 70.00% 70.00% 89.33%
72.06% 72.47% 70.28% 82.50% 82.05% 83.67% 69.67% 69.67% 89.35%
Average Accuracy Change
77.31% - 1.81%
76.75% - 2.37%
75.81% - 3.32%
76.86% - 2.27%
repairing the Age attribute on the Compas dataset, they result in accuracy drops of nearly 10%. As for efficiency, both FLIP and GRFT introduce negligible time overheads, taking around 1 second per setting. P RO F also maintains a desirable runtime of 18 seconds on average. On the other hand, CARE incurs more time consumption (averaging 244 seconds) due to its reliance on the PSO algorithm, which often demands extensive iteration for convergence. C. RQ2: Can P RO F handle multiple protected attributes and more practical fairness definition? To answer this question, we conduct experiments on repair with multiple sensitive attributes simultaneously. CARE is excluded from this evaluation since its current implementation does not support this setting. As shown in the upper panel of Table IV, the original models exhibit higher unfairness prior to repair. This is expected since multiple protected attributes can combine to form a larger set of similar individuals, making it naturally more challenging for the model to satisfy fairness constraints. Despite this increased challenge, P RO F consistently achieves provable repair by completely eliminating unfair behaviors on the repair set (i.e., CUR = 0). Models repaired by FLIP and GRFT, however, often continue to exhibit discrimination, with CUR reductions under 70%. Our method also demonstrates
TABLE IV: Results of fairness improvements with multiple attributes and relaxed fairness properties (G, R and A denote Gender, Race and Age). Details of all relaxed fairness specifications are provided at the end of this section. Dataset
Attr.
Compas Compas Compas Adult Adult Adult German
Original
FLIP
G-R G-A R-A G-R G-A R-A G-A
19.00% 49.00% 55.00% 7.00% 16.00% 17.00% 4.00%
7.00% 13.00% 13.00% 1.00% 6.00% 8.00% 13.00%
Average Relative Drop
23.86% -
Adult Adult Adult Bank German German
G-ϕA A-ϕA R-ϕA A-ϕB G-ϕG A-ϕG
Average Relative Drop
CUR GRFT
Ours
Original
FLIP
IDI-S GRFT
6.59% 25.84% 15.04% 3.21% 7.60% 7.51% 0.40%
0.00% 1.62% 3.68% 1.78% 3.13% 2.71% 0.00%
4.49% 12.71% 13.56% 1.18% 4.31% 4.20% 16.11%
1.94% 3.57% 2.91% 0.73% 1.16% 1.36% 9.91%
1.30% 1.57% 1.91% 1.11% 3.74% 3.52% 4.39%
0.00% 1.33% 2.56% 0.39% 0.78% 0.78% 0.00%
8.74% 66.70%↓
9.46% 63.99%↓
1.85% 92.97%↓
8.08% -
3.08% 61.88%↓
2.51% 69.00%↓
0.83% 89.67%↓
3.26% 21.98% 4.70% 3.56% 3.10% 3.50%
4.97% 6.67% 6.42% 3.72% 5.30% 0.10%
1.43% 6.68% 1.78% 2.04% 0.20% 0.10%
1.22% 0.61% 1.20% 0.11% 0.00% 0.00%
0.73% 3.73% 0.62% 23.75% 7.98% 9.35%
0.52% 0.90% 0.39% 18.80% 4.01% 1.99%
0.67% 3.07% 0.60% 6.82% 2.07% 2.39%
0.18% 0.32% 0.32% 2.75% 0.00% 0.00%
6.68% -
4.53% 32.22%↓
2.04% 69.49%↓
0.52% 92.17%↓
7.69% -
4.44% 42.34%↓
2.60% 66.18%↓
0.59% 92.27%↓
Ours
Original
FLIP
3.00% 20.00% 13.00% 2.00% 6.00% 7.00% 0.00%
0.00% 0.00% 0.00% 0.00% 0.00% 0.00% 0.00%
16.92% 51.65% 55.54% 7.59% 23.01% 23.01% 6.10%
7.63% 7.57% 7.18% 6.80% 10.51% 12.62% 8.90%
8.71% 63.47%↓
7.29% 69.46%↓
0.00% 100.00%↓
26.26% -
3.00% 14.00% 2.00% 2.00% 3.00% 4.00%
6.00% 6.00% 4.00% 5.00% 8.00% 0.00%
1.00% 5.00% 1.00% 2.00% 0.00% 0.00%
0.00% 0.00% 0.00% 0.00% 0.00% 0.00%
4.67% -
4.83% -3.57%↓
1.50% 67.86%↓
0.00% 100.00%↓
remarkable generalization compared to existing approaches. It attains significantly lower IDI-D and IDI-S scores across all settings, with average mitigations of 92.97% and 89.67%, respectively, except for the “Compas + Race-Age” scenario, where its performance is only 0.6% below the best method. To further examine the effectiveness of all methods under more practical fairness definitions, we conduct a set of experiments on repairing models with relaxed fairness properties. Following Fairify [13], we define small perturbations on one non-sensitive attribute so that two individuals are considered similar even if they are not exactly equal on this attribute. These individuals are still expected to be assigned to the same class. For instance, the specification ϕA indicates that for the Adult dataset, individuals are considered similar as long as the value of “hours-per-week” attribute differ by at most 1, regardless of their values on sensitive attributes. The complete list of relaxed fairness specifications is as follows: ϕA : Two individuals are considered similar if their “hoursper-week” attribute differs by at most 1. • ϕB : Two individuals are regarded as similar when their “duration” attribute varies by no more than 1. • ϕG : This specification defines similarity between individuals whose “credit-amount” attribute lies within a fixed interval of size 100. •
The results are shown in the lower panel of Table IV. We observe that FLIP suffers a significant performance drop compared to the previous repair setting; in some cases, the unfairness of the repaired model even increases. This may be because it does not account for similarity between individuals whose non-sensitive attributes differ slightly and thus fails to enforce fairness under relaxed definitions. GRFT maintains similar performance as before, achieving around 70% reduction in unfairness metrics. In contrast, P RO F consistently outperforms existing approaches across all scenarios, achieving complete unfairness elimination on the repair set, along with
IDI-D GRFT
Ours
over 90% reduction in both IDI-D and IDI-S. In terms of accuracy, all methods exhibit slightly increased performance degradation compared to the single-attribute repair setting. Both FLIP and P RO F maintain stable performance, with average accuracy losses of 2.12% and 2.90%, respectively, which are significantly better than GRFT (5.03%). D. RQ3: How does P RO F perform under various testing frameworks? To answer this research question, we employ four stateof-the-art NN fairness testing frameworks to evaluate P RO F and all baselines. Specifically, we follow the original configurations of these frameworks and used them to generate IDIs for both the original and the repaired model. We denote the number of IDIs detected on the original model as Nori and those detected on the repaired model as Nrepair . To measure repair effectiveness under each testing framework, we report the ratio Nrepair /Nori , where a smaller ratio indicates that fewer IDIs are detected and thus better fairness improvement. The results are presented in Table V. Overall, all methods reduce model bias, broadly consistent with our earlier findings. However, we find that these testing frameworks reveal model defects more precisely and effectively than evaluation based on uniform sampling, especially in certain settings. For instance, all baseline methods especially FLIP and CARE perform poorly on the German dataset, and in some cases the repaired models even exhibit more IDIs than the original ones (ratios greater than 1). In contrast, our method shows consistently better performance, effectively reducing bias across all settings. In particular, P RO F achieves average ratios of 0.06, 0.12, 0.05, and 0.16 under the four testing tools, corresponding to 94%, 88%, 95%, and 84% reductions in IDIs, respectively. These results are in close agreement with our earlier samplingbased generalization evaluation (i.e., nearly 90% reduction). By comparison, the best-performing baseline, GRFT, reduces
TABLE V: Results of fairness evaluation with various testing frameworks. Colors indicate repair effectiveness: green for strong unfairness mitigation (ratios near 0), orange for minor change (ratios near 1), and red for increase (ratios above 1). FLIP EIDIG NF
GRFT
ADF
CARE EIDIG NF
GRFT
ADF
GRFT EIDIG NF
GRFT
ADF
P RO F EIDIG NF
GRFT
Compas
G R A G-R G-A R-A
0.28 0.53 0.28 0.29 0.70 0.30
0.24 0.63 0.34 0.32 0.72 0.38
0.36 0.59 0.28 0.29 0.64 0.38
0.33 0.37 0.25 0.17 0.51 0.31
0.28 0.42 0.92 0.32 0.79 0.48
0.36 0.45 0.95 0.34 0.72 0.47
0.45 0.35 1.04 0.29 0.72 0.36
0.42 0.22 0.91 0.17 0.57 0.29
0.00 0.17 0.21 0.44 0.21 0.22
0.00 0.18 0.20 0.44 0.23 0.25
0.00 0.18 0.16 0.29 0.13 0.14
0.00 0.11 0.14 0.17 0.10 0.12
0.00 0.00 0.12 0.00 0.15 0.22
0.00 0.00 0.13 0.00 0.15 0.31
0.00 0.00 0.09 0.00 0.10 0.19
0.00 0.00 0.08 0.00 0.08 0.15
Adult
G R A G-R G-A R-A
1.07 0.85 0.26 0.61 0.35 0.40
0.68 0.80 0.18 0.92 0.29 0.34
0.41 0.77 0.35 0.47 0.49 0.47
0.79 1.11 0.56 0.64 0.61 0.47
0.05 0.36 1.15 0.70 1.05 1.14
0.04 0.41 1.12 0.62 0.97 1.11
0.04 0.23 0.54 0.32 0.84 0.80
0.19 0.93 0.43 0.64 0.95 1.42
0.43 0.73 1.08 0.69 1.03 0.87
0.26 0.65 0.96 0.63 1.01 0.86
0.53 0.80 0.86 0.71 0.97 0.90
0.78 0.96 0.78 0.93 0.67 0.52
0.06 0.18 0.00 0.09 0.05 0.03
0.28 0.36 0.01 0.42 0.06 0.08
0.02 0.09 0.03 0.04 0.16 0.12
0.31 0.74 0.08 0.44 0.21 0.28
German
G A G-A
1.07 1.20 1.02
0.94 1.13 1.03
5.79 0.02 2.79
1.43 0.70 1.30
1.11 1.08 0.88
1.04 1.15 0.85
0.13 1.40 0.23
0.67 0.63 0.83
1.20 1.16 0.86
1.01 1.04 0.83
0.05 0.02 0.02
0.63 0.68 0.64
0.00 0.00 0.00
0.00 0.00 0.00
0.00 0.00 0.00
0.00 0.00 0.00
Bank
A
0.62
0.58
0.10
0.71
1.27
1.52
0.96
0.79
0.74
0.80
0.23
0.82
0.04
0.16
0.03
0.22
0.61
0.60
0.89
0.64
0.75
0.76
0.54
0.63
0.63
0.58
0.37
0.50
0.06
0.12
0.05
0.16
IDIs by no more than 70%, further confirming the superior generalization of our method against all baselines.
1.0
0.4 0.2
Metric Value
50
100 Epoch
150
0.6 0.4 0.2 0
50
100 Epoch
150
200
Metric Value
0.6 0.4 0.2 0
50
100 Epoch
150
0
200
50
100 Epoch
150
200
Adult - Race - Age
0.6 0.4 0.2 0
50
100 Epoch
150
Adult - Age fair bce
0
0.6 0.4 50
100 Epoch
150
200
fair bce
0.6 0.4 0.2 0
50
100 Epoch
150
200
Adult - Age - A fair bce
0
100 Epoch
0.8
0.0
200
50
Adult - Gender - Age
Adult - Race - A
0.8
0.2
1.0 0.8 0.6 0.4 0.2 0.0
1.0
fair bce
0.8
1.0
fair bce
0.8
0.4
0.0
Adult - Gender - A
1.0
0.6
1.0
fair bce
0.8
0.8
0.2
200
Adult - Gender - Race
1.0
Metric Value
To answer this question, we first examine the impact of the first step, which performs a progressive bounds tightening process. Specifically, we track the dynamics of the two losses minimized during this step: Lbce , the BCE loss computed on a small subset of training data Dc, and Lfair , a fairnessaware loss measuring the relative ℓ1 -norm reduction between the current and original bounds. Due to space limitations, we present only a subset of the results in Figure 4; the full version is shown in Appendix. We observe that Lfair steadily decreases as epochs progress, eventually reaching a relatively low level. This indicates that the concrete bounds after repair are significantly tightened compared to before, demonstrating Step 1 successfully calibrates and reduces model bias. Meanwhile, Lbce remains stable, showing that model’s knowledge is largely preserved. These results highlight that this step effectively balances fairness enhancement and accuracy retention, with Lfair playing a pivotal role in calibrating the model without sacrificing its fidelity. We further analyze the contribution of the second step in P RO F. Figure 5 compares P RO F with the naive repair method that relies on loose concrete bounds. As shown in the top panel, models repaired by P RO F consistently achieve higher accuracy, suggesting that the naive method leads to excessive modifications of the final layer as it requires fairness constraints are satisfied across the box formed by concrete bounds. This observation is further supported by the bottom panel, where we report the optimal values of the respective MILP formulations solved by Gurobi. P RO F consistently yields smaller solutions, indicating that the tighter symbolic bounds enable less adjustment to the model.
0
Metric Value
E. RQ4: How do the two key steps of P RO F impact repair?
fair bce
Metric Value
0.6
Adult - Race
1.0
fair bce
Metric Value
Adult - Gender
0.8
Metric Value
Average
Metric Value
Attr.
Metric Value
ADF
Dataset
150
200
1.0 0.8 0.6 0.4 0.2 0.0
fair bce
0
50
100 Epoch
150
200
Fig. 4: Loss dynamics during the bounds tightening in Step 1 of P RO F. Shaded areas denote the variance across 10 runs. V. D ISCUSSION Scalability to more complex models: P RO F can scale to more complex models since it only requires the final layer to be linear, which holds for most DNNs. A potential limitation when scaling to these models is computational cost, since MILP is theoretically NP-hard and its complexity grows exponentially with the number of integer variables. However, this number is irrelevant to the model size in our formulation, which could mitigate the exponential explosion issue. The remaining variables and constraints form a standard linear program solvable in polynomial time. Nevertheless, we agree that the overall MILP complexity cannot be guaranteed to be polynomial due to its inherent NP-hardness. Relation to robustness repair: P RO F achieves provable fairness repair through two carefully designed steps. The first
Accuracy
0.9 0.8 0.7 0.6 0.5 0.4 0.3 0.2
Naive method (Problem 14) ProF (Problem 22)
t pas pas pas pas e pas e pas e dul comsex comrace comage comx_rac comce_ag comex_ag a sex e s s ra
lt aduace r
lt adauge
lt lt lt adu_race adue_age adxu_age se sex rac Naive method (Problem 14) ProF (Problem 22)
t pas pas pas pas e pas e pas e dul comsex comrace comage comx_rac comce_ag comex_ag a sex s se ra
lt aduace r
lt adauge
lt lt lt adu_race adue_age adxu_age se sex rac
Optimal Value
0.4 0.3 0.2 0.1 0.0
Fig. 5: Comparison between the naive repair method and P RO F. Top: Accuracy of models repaired by the naive method and P RO F. Bottom: Optimal values of the MILP formulated by the naive method (Problem 14) and P RO F (Problem 22). step mitigates bias by tightening concrete bounds to promote feature consistency among similar individuals, regardless of the ground truth label. This method is tailored for fairness and cannot apply to robustness repair directly, which requires all perturbed inputs to be classified correctly. In the second step, we formulate a unified constraint solving problem. The key challenge here is the presence of non-linear terms in the MILP, which we address by introducing the dual theorem. This technique can also be adapted to address a similar problem in robustness repair. Beyond this issue, fairness repair exhibits another distinctive challenge: it involves disjunctive constraints that cannot be handled by existing solvers. To address this, we carefully design and introduce integer variables to transform disjunctive constraints into linear form. Overall, while some techniques in the second step can be adapted to robustness repair, the first step is fairness-specific, which makes P RO F currently unique to fairness. VI. R ELATED W ORK NN Fairness. Fairness for DNNs is commonly categorized into group fairness and individual fairness. Group fairness considers whether different demographic groups receive statistically similar outcomes [43], [44]. Despite its simplicity in metric design, it only captures statistical parity and may result in unfairness at the individual level. In contrast, individual fairness [45], [46] stipulates that similar individuals should be treated similarly by the model, typically formalized as the constraint that predictions remain consistent when only the sensitive attributes are changed. It enables finer, instance-level analysis and broader use of testing and verification techniques. Various methods have been developed to test and verify individual fairness in DNNs. ADF [8] and EIDIG [11] search for IDIs near the decision boundary by leveraging the loss function gradient. NeuronFair [12] further optimizes test generation by
computing gradients only for biased neurons identified via sensitivity analysis. More recently, [47] introduces extreme value theory to fairness testing. It models the worst case counterfactual bias and develops a randomized test-case generation algorithm to collect tail samples with statistical guarantees. Beyond testing, several works have been proposed to formally verify NN fairness. For example, [15] learns Markov Chains from a given model to formally verify group fairness with probabilistic guarantees. On the other hand, DeepGemini [48] encodes individual fairness constraints into SMT formulas but is limited in scalability. Fairify [13] improves verification efficiency by decomposing the problem and pruning neurons. FairQuant [14] further enhances scalability and precision via abstraction-refinement, and additionally quantifies the proportion of inputs that are certifiably fair or unfair. Regarding unfairness mitigation, several works [18], [9], [16], [49] use heuristic algorithms to correct model bias but lack formal guarantees. Shifty [50] presents a fairness training method, offering high-confidence fairness guarantees under demographic shift. NeuFair [19] and AutoRIC [51] are recently proposed methods that target group fairness repair: the former leverages simulated annealing to optimize repair solutions with statistical guarantees, while the latter uses constraint solving. Unlike these methods focusing on group fairness, this work aims to provide deterministic, provable guarantees for individual fairness repair. NN Repair. There exists a broader line of work on general NN repair that targets other correctness properties. Among them, non-provable methods [16], [52], [53], [54], [55], [56] typically follow a two-step pipeline: first localizing faulty neurons or parameters, then applying heuristic techniques to adjust them. These methods often rely heavily on sufficient data and lack rigorous guarantees. To provide guarantees, several recent works [57], [58], [59] leverage constraint solvers to calculate parameter changes ensuring property satisfaction. However, these methods are not specifically designed for fairness and thus cannot be directly applied to fairness repair. VII. C ONCLUSION We present P RO F, a provable fairness repair framework for DNNs. It leverages interval bound propagation to calculate concrete bounds that soundly capture the model behavior in feature space, and iteratively tightens these bounds to calibrate the biased model. P RO F further synthesizes symbolic bounds to formulate a precise constraint-solving problem and introduces the duality theorem to eliminate non-linear operations to construct an MILP that provides provable guarantees for repair. Extensive experiments demonstrate that P RO F significantly outperforms the state-of-the-art in terms of both effectiveness and generalization. Moreover, P RO F can handle multiple sensitive attributes and relaxed fairness definitions. ACKNOWLEDGMENTS This work is supported by the NSFC (No. U21B2001, No. 62402150) and the Key R&D Program of Zhejiang under Grant (No. 2025C01083).
R EFERENCES [1] M. Badar, M. Haris, and A. Fatima, “Application of deep learning for retinal image analysis: A review,” Computer Science Review, vol. 35, p. 100203, 2020. [2] J. Devlin, M.-W. Chang, K. Lee, and K. Toutanova, “Bert: Pre-training of deep bidirectional transformers for language understanding,” arXiv preprint arXiv:1810.04805, 2018. [3] Y. Deng, T. Zhang, G. Lou, X. Zheng, J. Jin, and Q.-L. Han, “Deep learning-based autonomous driving systems: A survey of attacks and defenses,” IEEE Transactions on Industrial Informatics, vol. 17, no. 12, pp. 7897–7912, 2021. [4] T. Brennan, W. Dieterich, and B. Ehret, “Evaluating the predictive validity of the compas risk and needs assessment system,” Criminal Justice and behavior, vol. 36, no. 1, pp. 21–40, 2009. [5] K. T. Rodolfa, H. Lamba, and R. Ghani, “Empirical observation of negligible fairness–accuracy trade-offs in machine learning for public policy,” Nature Machine Intelligence, vol. 3, no. 10, pp. 896–904, 2021. [6] A. E. Khandani, A. J. Kim, and A. W. Lo, “Consumer credit-risk models via machine-learning algorithms,” Journal of Banking & Finance, vol. 34, no. 11, pp. 2767–2787, 2010. [7] A. Aggarwal, P. Lohia, S. Nagar, K. Dey, and D. Saha, “Black box fairness testing of machine learning models,” in Proceedings of the 2019 27th ACM joint meeting on european software engineering conference and symposium on the foundations of software engineering, 2019, pp. 625–635. [8] P. Zhang, J. Wang, J. Sun, G. Dong, X. Wang, X. Wang, J. S. Dong, and T. Dai, “White-box fairness testing through adversarial sampling,” in Proceedings of the ACM/IEEE 42nd international conference on software engineering, 2020, pp. 949–960. [9] L. Quan, T. Li, X. Xie, Z. Chen, S. Chen, L. Jiang, and X. Li, “Dissecting global search: A simple yet effective method to boost individual discrimination testing and repair,” in 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE Computer Society, 2025, pp. 771–771. [10] Z. Wang, M. Zhang, J. Yang, B. Shao, and M. Zhang, “Maft: Efficient model-agnostic fairness testing for deep neural networks via zero-order gradient search,” in Proceedings of the IEEE/ACM 46th International Conference on Software Engineering, 2024, pp. 1–12. [11] L. Zhang, Y. Zhang, and M. Zhang, “Efficient white-box fairness testing through gradient search,” in Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2021, pp. 103–114. [12] H. Zheng, Z. Chen, T. Du, X. Zhang, Y. Cheng, S. Ji, J. Wang, Y. Yu, and J. Chen, “Neuronfair: Interpretable white-box fairness testing through biased neuron identification,” in Proceedings of the 44th International Conference on Software Engineering, 2022, pp. 1519–1531. [13] S. Biswas and H. Rajan, “Fairify: Fairness verification of neural networks,” in 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE, 2023, pp. 1546–1558. [14] B. H. Kim, J. Wang, and C. Wang, “Fairquant: Certifying and quantifying fairness of deep neural networks,” in 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE Computer Society, 2024, pp. 191–203. [15] B. Sun, J. Sun, T. Dai, and L. Zhang, “Probabilistic verification of neural networks against group fairness,” in Formal methods: 24th international symposium, FM 2021, virtual event, November 20–26, 2021, proceedings 24. Springer, 2021, pp. 83–102. [16] B. Sun, J. Sun, L. H. Pham, and J. Shi, “Causality-based neural network repair,” in Proceedings of the 44th International Conference on Software Engineering, 2022, pp. 338–349. [17] T. Li, Y. Cao, J. Zhang, S. Zhao, Y. Huang, A. Liu, Q. Guo, and Y. Liu, “Runner: Responsible unfair neuron repair for enhancing deep neural network fairness,” in Proceedings of the 46th IEEE/ACM International Conference on Software Engineering, 2024, pp. 1–13. [18] J. Chen, J. Wang, Y. Sun, P. Cheng, and J. Chen, “Isolation-based debugging for neural networks,” in Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, 2024, pp. 338–349. [19] V. A. Dasu, A. Kumar, S. Tizpaz-Niari, and G. Tan, “Neufair: Neural network fairness repair with dropout,” in Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, 2024, pp. 1541–1553.
[20] G. Singh, T. Gehr, M. Püschel, and M. Vechev, “An abstract domain for certifying neural networks,” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, pp. 1–30, 2019. [21] H. Zhang, T.-W. Weng, P.-Y. Chen, C.-J. Hsieh, and L. Daniel, “Efficient neural network robustness certification with general activation functions,” Advances in neural information processing systems, vol. 31, 2018. [22] T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev, “Ai2: Safety and robustness certification of neural networks with abstract interpretation,” in 2018 IEEE symposium on security and privacy (SP). IEEE, 2018, pp. 3–18. [23] B. Paulsen and C. Wang, “Example guided synthesis of linear approximations for neural network verification,” in International Conference on Computer Aided Verification. Springer, 2022, pp. 149–170. [24] S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana, “Formal security analysis of neural networks using symbolic intervals,” in 27th USENIX Security Symposium (USENIX Security 18), 2018, pp. 1599–1614. [25] P. Yang, R. Li, J. Li, C. Huang, J. Wang, J. Sun, B. Xue, and L. Zhang, “Improving neural network verification through spurious region guided refinement,” in TACAS 2021, ser. Lecture Notes in Computer Science, vol. 12651. Springer, 2021, pp. 389–408. [26] R. Bunel, P. Mudigonda, I. Turkaslan, P. Torr, J. Lu, and P. Kohli, “Branch and bound for piecewise linear neural network verification,” Journal of Machine Learning Research, vol. 21, no. 2020, 2020. [27] G. Katz, D. A. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zeljić et al., “The marabou framework for verification and analysis of deep neural networks,” in Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I 31. Springer, 2019, pp. 443–452. [28] G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient smt solver for verifying deep neural networks,” in Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30. Springer, 2017, pp. 97–117. [29] S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana, “Efficient formal safety analysis of neural networks,” Advances in neural information processing systems, vol. 31, 2018. [30] L. H. De Figueiredo and J. Stolfi, “Affine arithmetic: concepts and applications,” Numerical algorithms, vol. 37, pp. 147–158, 2004. [31] R. E. Moore, R. B. Kearfott, and M. J. Cloud, Introduction to interval analysis. SIAM, 2009. [32] Z. Chen, J. M. Zhang, M. Hort, M. Harman, and F. Sarro, “Fairness testing: A comprehensive survey and analysis of trends,” ACM Transactions on Software Engineering and Methodology, vol. 33, no. 5, pp. 1–59, 2024. [33] P. G. John, D. Vijaykeerthy, and D. Saha, “Verifying individual fairness in machine learning models,” in Conference on Uncertainty in Artificial Intelligence. PMLR, 2020, pp. 749–758. [34] K. Xu, Z. Shi, H. Zhang, Y. Wang, K.-W. Chang, M. Huang, B. Kailkhura, X. Lin, and C.-J. Hsieh, “Automatic perturbation analysis for scalable certified robustness and beyond,” Advances in Neural Information Processing Systems, vol. 33, pp. 1129–1141, 2020. [35] G. Singh, T. Gehr, M. Mirman, M. Püschel, and M. T. Vechev, “Fast and effective robustness certification,” in NeurIPS 2018, Montréal, Canada, 2018, pp. 10 825–10 836. [36] S. P. Boyd and L. Vandenberghe, Convex optimization. Cambridge university press, 2004. [37] Gurobi Optimization, LLC, “Gurobi Optimizer Reference Manual,” 2025. [Online]. Available: https://www.gurobi.com [38] B. Becker and R. Kohavi, “Adult,” UCI Machine Learning Repository, 1996, DOI: https://doi.org/10.24432/C5XW20. [39] H. Hofmann, “Statlog (German Credit Data),” UCI Machine Learning Repository, 1994, DOI: https://doi.org/10.24432/C5NC77. [40] S. Moro, P. Rita, and P. Cortez, “Bank Marketing,” UCI Machine Learning Repository, 2012, DOI: https://doi.org/10.24432/C5K306. [41] J. Angwin, J. Larson, S. Mattu, and L. Kirchner, “Machine bias,” 2016. [Online]. Available: https://www.propublica.org/article/ machine-bias-risk-assessments-in-criminal-sentencing [42] V. Tjeng, K. Y. Xiao, and R. Tedrake, “Evaluating robustness of neural networks with mixed integer programming,” in 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. [Online]. Available: https://openreview.net/forum?id=HyGIdiRqtm
[43] M. Feldman, S. A. Friedler, J. Moeller, C. Scheidegger, and S. Venkatasubramanian, “Certifying and removing disparate impact,” in proceedings of the 21th ACM SIGKDD international conference on knowledge discovery and data mining, 2015, pp. 259–268. [44] M. Hardt, E. Price, and N. Srebro, “Equality of opportunity in supervised learning,” Advances in neural information processing systems, vol. 29, 2016. [45] R. Zemel, Y. Wu, K. Swersky, T. Pitassi, and C. Dwork, “Learning fair representations,” in International conference on machine learning. PMLR, 2013, pp. 325–333. [46] C. Dwork, M. Hardt, T. Pitassi, O. Reingold, and R. Zemel, “Fairness through awareness,” in Proceedings of the 3rd innovations in theoretical computer science conference, 2012, pp. 214–226. [47] V. Monjezi, A. Trivedi, V. Kreinovich, and S. Tizpaz-Niari, “Fairness testing through extreme value theory,” in 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE, 2025, pp. 1501–1513. [48] X. Xie, F. Zhang, X. Hu, and L. Ma, “Deepgemini: verifying dependency fairness for deep neural network,” in Proceedings of the AAAI Conference on Artificial Intelligence, vol. 37, no. 12, 2023, pp. 15 251– 15 259. [49] T. Li, Q. Guo, A. Liu, M. Du, Z. Li, and Y. Liu, “Fairer: fairness as decision rationale alignment,” in International Conference on Machine Learning. PMLR, 2023, pp. 19 471–19 489. [50] S. Giguere, B. Metevier, Y. Brun, B. C. Da Silva, P. S. Thomas, and S. Niekum, “Fairness guarantees under demographic shift,” in Proceedings of the 10th International Conference on Learning Representations (ICLR), 2022. [51] X. Sun, W. Liu, S. Wang, T. Chen, Y. Tao, and X. Mao, “Autoric: Automated neural network repairing based on constrained optimization,” ACM Transactions on Software Engineering and Methodology, vol. 34, no. 2, pp. 1–29, 2025. [52] M. Usman, D. Gopinath, Y. Sun, Y. Noller, and C. S. Păsăreanu, “Nn repair: constraint-based repair of neural network classifiers,” in Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I 33. Springer, 2021, pp. 3–25. [53] P. Henriksen, F. Leofante, and A. Lomuscio, “Repairing misclassifications in neural networks using limited data,” in Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, 2022, pp. 1031–1038. [54] J. Sohn, S. Kang, and S. Yoo, “Arachne: Search-based repair of deep neural networks,” ACM Transactions on Software Engineering and Methodology, vol. 32, no. 4, pp. 1–26, 2023. [55] Z. Chen, J. Zhou, Y. Sun, J. Wang, Q. Xuan, and X. Yang, “Interpretability based neural network repair,” in Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, 2024, pp. 908–919. [56] J. Ma, P. Yang, J. Wang, Y. Sun, C.-C. Huang, and Z. Wang, “Vere: Verification guided synthesis for repairing deep neural networks,” in Proceedings of the 46th IEEE/ACM International Conference on Software Engineering, 2024, pp. 1–13. [57] M. Sotoudeh and A. V. Thakur, “Provable repair of deep neural networks,” in Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021, pp. 588–603. [58] F. Fu and W. Li, “Sound and complete neural network repair with minimality and locality guarantees,” in The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. [59] Z. Tao, S. Nawas, J. Mitchell, and A. V. Thakur, “Architecture-preserving provable repair of deep neural networks,” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, pp. 443–467, 2023.
100 150 Epoch
0.6 0.4 100 150 Epoch
0
50
100 150 Epoch
0.6 0.4
50
100 150 Epoch
50
100 150 Epoch
0.8 0.6 0.4
Metric Value
0.8 0.6 0.4 0.2 0
50
100 150 Epoch
200
0 1.0 0.8 0.6 0.4 0.2 0.0
50
100 150 Epoch
200
200
Adult - Gender - Race
0.8 0.6 0.4
50
100 150 Epoch
0
200
Bank - Age - B
50
100 150 Epoch
0.8 0.6 0.4 0
50
100 150 Epoch
fair 0
50
100 150 Epoch
200
0 1.0 0.8 0.6 0.4 0.2 0.0
1.0 0.8 0.6 0.4 0.2 0.0
50
100 150 Epoch
200
Bank - Age
200
0.6 0.4 0.2
0
50
100 150 Epoch
200
100 150 Epoch
200
100 150 Epoch
200
100 150 Epoch
200
Compas - Gender - Race
1.0
0
50
100 150 Epoch
0.8 0.6 0.4
200
Adult - Race - Age
0
50
100 150 Epoch
0
50
100 150 Epoch
0
200
0.8 0.6 0.4 0.2 0.0
0
50
German - Gender - G
1.0
200
50
Adult - Gender - Age
1.0
Adult - Age - A 1.0 0.8 0.6 0.4 0.2 0.0
0.8
0.2
Adult - Race - A
1.0
0.2
Metric Value
Metric Value 0
200
Adult - Gender - A
1.0
German - Age - G
100 150 Epoch
0.2 0
200
50
German - Age
1.0 0.8 0.6 0.4 0.2 0.0
1.0
0.2 0
0.2 0
200
0.4
Metric Value
200
Compas - Gender - Age
0.8
200
German - Gender - Age
1.0 Metric Value
50
Metric Value
Metric Value
0
0.0
100 150 Epoch
0.2
0.2
1.0 0.8 0.6 0.4 0.2 0.0
50
German - Gender
1.0 0.8 0.6 0.4 0.2 0.0
1.0 Metric Value
0.8
0
200
Compas - Race - Age
0.2
0.6
Metric Value
50
0.4
0.8
Adult - Race
1.0
Metric Value
0
0.6
Metric Value
200
Adult - Age
1.0 Metric Value
100 150 Epoch
0.2
Metric Value
1.0 0.8 0.6 0.4 0.2 0.0
50
Metric Value
Metric Value
0
0.4
0.8
Adult - Gender
1.0
Metric Value
0.2
Metric Value
0.4
0.6
Metric Value
0.6
0.8
Compas - Age
1.0
Metric Value
Metric Value
Metric Value
0.8
Compas - Race
1.0
Metric Value
Compas - Gender
1.0
0.8 0.6 0.4 0.2 0.0
0
50
bce
200
Fig. 6: Full results of loss dynamics during the progressive bounds tightening process in Step 1 of P RO F, with shaded areas representing the variance across multiple runs.