Source-linked AI summary
Verifying Individual Fairness in Machine Learning Models
Philips George John, Deepak Vijaykeerthy, Diptikalyan Saha
TL;DR
The paper asks how to verify individual fairness for classifiers on structured data, where fairness requires similar valid inputs to receive sufficiently similar outputs. It develops verification algorithms using relaxations and reports sound verification with incompleteness in some cases, alongside acceptable evaluation times and scaling costs.
Problem
Individual-fairness verification requires checking a global property over all sufficiently close input pairs, unlike group-fairness or local-robustness verification.
Source: §1 · pp. 1–2Method
The paper develops a verification framework and algorithms for linear and kernelized classifiers, using relaxations to handle the verification problem.
Source: §1 · p. 2, §4.1 · p. 5Results
Verification times were reported as acceptable even for reasonably complex models, while sum-of-squares relaxations scaled poorly as data dimension increased.
Source: §5.3 · p. 9Takeaways & Limitations
The work provides a first approach to individual-fairness verification for machine-learning models, with an exact linear-classifier case available at worst-case exponential cost.
Source: §6 · p. 9Relaxation-based verification can remain incomplete, potentially failing indefinitely to find an existing bias instance, and no upper bound is known for the SOS degree needed to approach tight bounds.
Source: §4.1 · p. 5, §4.2.2 · p. 6
Abstract
from arXiv · showhide
We consider the problem of whether a given decision model, working with structured data, has individual fairness. Following the work of Dwork, a model is individually biased (or unfair) if there is a pair of valid inputs which are close to each other (according to an appropriate metric) but are treated differently by the model (different class label, or large difference in output), and it is unbiased (or fair) if no such pair exists. Our objective is to construct verifiers for proving individual fairness of a given model, and we do so by considering appropriate relaxations of the problem. We construct verifiers which are sound but not complete for linear classifiers, and kernelized polynomial/radial basis function classifiers. We also report the experimental results of evaluating our proposed algorithms on publicly available datasets.
1 INTRODUCTION
The paper defines individual fairness for structured inputs using metric-based closeness and develops verification methods for checking whether classifiers treat close inputs differently.
1 INTRODUCTION
- The paper measures input closeness with coordinate-wise thresholds assigned to feature subsets, accommodating structured data rather than relying only on an ℓp metric.Source: §1 · p. 1
- The threshold scheme subsumes protected-attribute testing by allowing arbitrary changes to protected features while fixing non-protected features.Source: §1 · pp. 1–2
- Individual fairness checks all sufficiently close input pairs, unlike group fairness’s average-case parity and local robustness’s neighborhood around one nominal input.Source: §1 · p. 2
- The paper presents the first technique for verifying individual fairness as a global robustness property of machine-learning models.Source: §1 · p. 2
- Its framework covers linear classifiers and kernelized polynomial or RBF classifiers, with sound but incomplete algorithms except for exact linear verification at worst-case exponential cost.Source: §1 · p. 2
2 RELATED WORK
Prior work addressed fairness testing, group-fairness verification, and local robustness verification, but these approaches do not provide the global individual-fairness verification considered here.
2 RELATED WORK
- Fairness-testing tools use random search or systematic decision-space exploration, but none guarantees the absence of individual bias.THEMIS uses random testing (Galhotra et al. 2017), AEQUITAS combines global search with perturbations near a discriminating sample (Udeshi et al. 2018), and Aggarwal et al. (2019) use symbolic execution and model explainability.Source: §2 · p. 2
- Prior verification work on fairness considered group measures such as disparate impact, while adversarial-robustness verification typically targets local rather than global robustness.Group-fairness examples include (Bastani et al. 2019); Zhang et al. (2019) surveys local robustness.Source: §2 · p. 2
- SMT/MILP approaches can be sound and complete for certain model classes at worst-case exponential or superexponential cost, whereas convex relaxations are efficient but sacrifice completeness.The cited SMT/MILP examples include linear models, decision trees, and piecewise-linear neural networks (Katz et al. 2017; Bunel et al. 2018).Source: §2 · p. 2
- Raghunathan et al. (2018) verify local robustness of ReLU networks by relaxing the problem to polynomial optimization and using semidefinite relaxations for lower bounds.Source: §2 · p. 2
3 PRELIMINARIES
The preliminaries specify the model assumptions, valid structured inputs, and distance-based criteria used to define individual fairness and bias.
3 PRELIMINARIES
- The assumed prediction function is known, twice continuously differentiable, and used directly for regression or through its sign for binary classification.Source: §3 · p. 3
- Input features may be continuous or discrete within fixed intervals, and an input is valid when every feature satisfies its domain constraint.Source: §3 · p. 3
- Individual fairness requires close inputs to have outputs within a chosen tolerance; classification uses unchanged labels, while regression can use bounded absolute output error.Source: §3 · p. 3
- Structured-data closeness is defined by partitioning features into subsets and assigning each subset a nonnegative perturbation threshold.Source: §3 · p. 3
- A model is individually biased when a valid, sufficiently close input pair produces an output difference greater than δ.Source: §3 · p. 3
- Linear models use an affine score, while polynomial kernels permit curved decision boundaries and RBF kernels use a Gaussian form.Source: §3 · p. 3
4 VERIFYING INDIVIDUAL BIAS
The section develops an optimization-based verifier for individual bias, then specializes it to linear, polynomial-kernel, and RBF models. The guarantees range from exact but potentially expensive linear verification to sound, incomplete relaxations for kernelized models.
4.1 A META-ALGORITHM
- The meta-algorithm searches for a close input pair with output difference beyond δ, using lower bounds to certify NO BIAS; relaxations preserve soundness but may prevent termination or yield spurious witnesses.It fixes selected discrete attributes, may relax others, and refines bounds when they leave bias possible.Source: §4.1 · pp. 4–5
4.2.1 Linear Models
- Linear models admit exact verification: continuous-attribute regression is solvable in polynomial time, while MILP/MIQP handles categorical attributes with worst-case exponential time.The resulting verifier is sound and complete, modulo computational issues.Source: §4.2.1 · pp. 5–6
4.2.2 Kernelized Polynomial Models
- Polynomial-kernel verification uses sum-of-squares lower bounds and runs in n^O(2d) time with ±O(1/2^n) error, but successive relaxation refinement leaves the verifier incomplete.The method is sound when it reports NO BIAS; convergence is known, but no upper bound is known for the degree needed to approach the tight bound.Source: §4.2.2 · pp. 6–7
4.3 RBF Kernelized Classifiers
- For RBF classifiers, the verifier runs in poly(n, M) time and returns either a bias pair with g(x, x′) < −2ε or a lower bound L ≥ −2ε for all valid pairs, for fixed sufficiently small ε.The stated coverage relies on assumptions about minimum model-weight and attribute magnitudes.Source: §4.3 · pp. 7–8
5 EXPERIMENTAL RESULTS
Experiments evaluate verification on publicly available datasets, finding generally acceptable verification times but poor scaling for sum-of-squares relaxations as data dimension grows. A comparison with random testing finds testing can take comparable or longer time without finding a bias instance.
5.1 SETUP
- Experiments ran on a 32-processor, 128-GB-RAM cloud virtual machine, with at most 32 parallel jobs; CPLEX, quadprog, and SDPA solved the optimization programs.The machine had no dedicated GPU; SDPA was used for sum-of-squares relaxation SDPs.Source: §5.1 · p. 8
5.2.1 Datasets
- Four public datasets were used, including a dimension-reduced Modified Adult variant; protected attributes received arbitrary perturbations while other attributes were fixed.Protected attributes were sex and marital status for German Credit, race for Adult, ethnicity for Fraud Detection, and gender and ethnicity for Credit.Source: §5.2.1 · pp. 8–9, Table 3 · p. 9
5.2.2 Models
- Linear models used logistic regression, while RBF and degree-2 polynomial models used SVC; masked variants trained with protected attributes set to zero.The RBF and polynomial models included both unmasked and masked configurations.Source: §5.2.2 · p. 9
5.3 EVALUATION OF VERIFICATION
- Verification times were described as acceptable even for complex real-world models, but sum-of-squares relaxations scaled poorly as data dimension increased.Table 1 reports results for the relaxed problem; Bias = Yes denotes a valid bias instance, No a no-bias proof, and Possible neither outcome.Source: Table 1 · p. 8, §5.3 · p. 9
5.4 COMPARISON WITH TESTING
- Random testing took comparable or longer time than verification, even without generating a bias instance.The comparison used 50,000 THEMIS samples; Table 2 presents the testing results.Source: Table 2 · p. 8, §5.4 · p. 9
6 CONCLUSION AND DISCUSSION
The paper presents individual-fairness verification for structured-data models and discusses further analysis of bias instances. Wider model classes, other fairness definitions, and refinement schemes are proposed as future directions.
6 CONCLUSION AND DISCUSSION
- The paper presents a meta-algorithm and specific verification algorithms for linear and polynomial/RBF-kernel models, describing this as the first work on ML individual-fairness verification.The algorithms return either a no-bias certificate or a bias instance; further analysis can tighten feature constraints or add domain-knowledge-based linear constraints.Source: §6 · p. 9
- The verifier alone cannot identify regions where bias exists for every input, and the proposed bias-analysis options have no reported experimental results.The options are to tighten input-feature constraints or add linear constraints to bias instances.Source: §6 · p. 9
- Future work includes wider model classes, other individual and group fairness definitions, and counterexample-driven refinement schemes.Source: §6 · p. 9
SUPPLEMENTARY MATERIAL
The supplementary material introduces polynomial and sum-of-squares terminology, then describes semidefinite relaxations for polynomial optimization. These relaxations provide lower bounds, but their non-negativity verification is incomplete.
PRELIMINARIES
- A polynomial is a finite sum of monomials, and its degree is the largest degree among monomials with nonzero coefficients.Source: PRELIMINARIES · p. 10
SUM-OF-SQUARES RELAXATIONS
- A sum-of-squares polynomial is a sum of squared polynomials; a degree-d sum-of-squares has a positive-semidefinite Gram-matrix representation.The matrix representation characterizes degree-d sum-of-squares polynomials.Source: SUM-OF-SQUARES RELAXATIONS · p. 10
- Sum-of-squares semidefinite programs produce increasing lower bounds for polynomial minima, and checking for a degree-d sum-of-squares gives a sound but incomplete non-negativity verifier.For constant d, the stated SDP has O(n^2d) variables and O(nd) constraints.Source: SUM-OF-SQUARES RELAXATIONS · pp. 10–11
- For constrained optimization, no degree upper bound is known for the required sum-of-squares relaxations, and the hierarchy does not always reach the true optimum.The stated degree upper bound applies to unconstrained minimization, not the constrained case.Source: SUM-OF-SQUARES RELAXATIONS · p. 11