PaperlayerView exact revision on arXiv

Source-linked AI summary

Fairify: Fairness Verification of Neural Networks

Sumon Biswas, Hridesh Rajan

arXiv:2212.06140v2cs.LGcs.AI

TL;DR

Formal fairness guarantees for machine-learning models remain difficult because neural-network verification involves nonlinear computations and global checks. Fairify applies SMT verification with input partitioning and neuron pruning to check individual fairness. On an AC3 partition, it reported SAT counterexamples after 86.27% compression; the conservative heuristic-pruned networks had no accuracy loss.

  • Problem

    Formal fairness guarantees for neural networks are difficult because verification involves nonlinear computations and individual fairness requires global checking.

    Source: §I · p. 1

  • Method

    Fairify applies SMT verification to partitioned input regions and prunes inactive neurons, using activation heuristics for further pruning.

    Source: §I · pp. 1–2, C. Input Partitioning · p. 5

  • Results

    On an AC3 partition, Fairify achieved 86.27% compression and reported SAT counterexamples in 21.47 seconds; conservative heuristic pruning caused no accuracy loss.

    Source: 1) Utility · p. 8, 3) Performance · p. 10

  • Takeaways & Limitations

    Fairify can provide individual-fairness verification results and counterexamples for real-world neural networks, including partition-specific evidence useful for defect localization.

    Source: 1) Utility · p. 8, §VIII · p. 11

    The evaluation covers structured datasets and ReLU-based networks; verifying CNNs or LSTMs remains a potential future improvement.

    Source: §VI · p. 10

Abstract

from arXiv · show

Fairness of machine learning (ML) software has become a major concern in the recent past. Although recent research on testing and improving fairness have demonstrated impact on real-world software, providing fairness guarantee in practice is still lacking. Certification of ML models is challenging because of the complex decision-making process of the models. In this paper, we proposed Fairify, an SMT-based approach to verify individual fairness property in neural network (NN) models. Individual fairness ensures that any two similar individuals get similar treatment irrespective of their protected attributes e.g., race, sex, age. Verifying this fairness property is hard because of the global checking and non-linear computation nodes in NN. We proposed sound approach to make individual fairness verification tractable for the developers. The key idea is that many neurons in the NN always remain inactive when a smaller part of the input domain is considered. So, Fairify leverages whitebox access to the models in production and then apply formal analysis based pruning. Our approach adopts input partitioning and then prunes the NN for each partition to provide fairness certification or counterexample. We leveraged interval arithmetic and activation heuristic of the neurons to perform the pruning as necessary. We evaluated Fairify on 25 real-world neural networks collected from four different sources, and demonstrated the effectiveness, scalability and performance over baseline and closely related work. Fairify is also configurable based on the domain and size of the NN. Our novel formulation of the problem can answer targeted verification queries with relaxations and counterexamples, which have practical implications.

I. INTRODUCTION

Fairify targets the gap between fairness testing and practical formal guarantees by using SMT verification for individual fairness in trained neural networks. It combines partitioning and pruning to make verification more tractable, with activation heuristics offering an additional efficiency option.

I. INTRODUCTION

  • Fairify uses SMT verification to check individual fairness in production neural networks and can return counterexamples or verify relaxed queries.The authors contrast this with Libra, which cannot check relaxed fairness queries or provide counterexamples for violations.Source: §I · p. 1
  • Formal fairness guarantees remain difficult because neural networks have nonlinear activation functions and individual fairness requires global rather than local checking.The introduction reports that state-of-the-art SMT solving could not verify the models’ fairness in days, while Fairify verified most queries within an hour.Source: §I · p. 1
  • Fairify combines input partitioning and neuron pruning to make global individual-fairness verification of neural networks more tractable.The method uses sound analysis to identify inactive neurons within partitions, then applies heuristic pruning as an optional further efficiency improvement.Source: §I · p. 2
  • The evaluation reports significant improvement over the baseline in utility, scalability, and performance.The models include real-world networks collected from Kaggle and prior work.Source: §I · p. 2

II. PRELIMINARIES

  • The paper considers fully connected, ReLU-based neural networks represented as layered directed acyclic graphs with weighted-sum computations.A neuron applies a nonlinear activation after its weighted sum; ReLU outputs zero for nonpositive inputs and the input value for positive inputs.Source: §II · p. 2

III. FAIRNESS VERIFICATION

This section defines individual fairness verification as a global check over pairs of similar inputs, distinguishing it from group fairness and local robustness. It also introduces relaxed and targeted fairness queries that support more specific verification questions.

A. Individual Fairness

  • Individual fairness requires similar individuals who differ in protected attributes to receive the same prediction, whereas group fairness compares outcomes across protected groups.Individual fairness is a worst-case property over input pairs; group fairness can miss bias when discrimination is equal across groups.Source: A. Individual Fairness · p. 3
  • Unlike local robustness, individual fairness checks pairs of inputs across the full domain, making it a harder global property to verify.The paper states that local robustness verifiers cannot directly verify this property; its static verification does not require labeled training data or an oracle.Source: A. Individual Fairness · p. 3, §III · p. 3
  • ϵ-fairness relaxes equality on non-protected attributes to allow bounded differences, and certification for it also implies certification for basic individual fairness.The relaxed query therefore requires stronger certification than the basic definition.Source: A. Individual Fairness · p. 3
  • Targeted fairness restricts verification to inputs satisfying arbitrary additional constraints, such as specified education, work hours, and occupation.The paper motivates targeted verification and counterexamples as useful for diagnosing and auditing fairness problems.Source: A. Individual Fairness · p. 3

IV. APPROACH

The section formulates the fairness verification problem and describes the proposed verification approach.

  • This section formulates the fairness verification problem and describes the approach used to verify the property.Source: §IV · p. 3

A. Problem Formulation

Fairify encodes fairness verification using input preconditions and output postconditions for a trained network. Its formulation handles paired inputs, transfers output constraints through activation functions, and uses SMT solving to check for violations or certification.

A. Problem Formulation

  • The verification query combines input preconditions and a neural-network output postcondition to check fairness on a trained model with white-box access.Input bounds may come from domain knowledge, including bounds obtained from training data.Source: A. Problem Formulation · p. 3
  • For a sigmoid classifier, Fairify transfers the output-mismatch postcondition to a condition on the pre-activation outputs.The weakest-precondition computation simplifies the query by reasoning at the output layer before applying Sigmoid.Source: A. Problem Formulation · p. 4
  • Fairness verification uses two input copies and two network outputs, and the query can also encode relaxed and targeted fairness constraints.This requires twice as many input variables and network copies as local robustness verification.Source: A. Problem Formulation · p. 4
  • SMT verification can provide counterexamples for violations and check ϵ-fairness and targeted fairness, while pruning inactive neurons reduces query complexity.The paper notes that branching over neuron activation choices grows as 2^n for n neurons and cannot be parallelized.Source: A. Problem Formulation · p. 4

B. Solution Overview

Fairify preprocesses the fairness query, partitions the input domain, and prunes a network for each partition before solving. The pipeline combines sound pruning with heuristic pruning when needed, and can return partition-level results within a time budget.

B. Solution Overview

  • Fairify preprocesses the query, partitions the input domain, applies sound pruning, and uses heuristic pruning if a soft timeout is reached.The heuristic stage may also support partial verification of a subset of partitions.Source: B. Solution Overview · pp. 4–5

C. Input Partitioning

D. Sound Pruning

  • For each partition, Fairify uses white-box weights and biases to bound neuron values, then verifies neurons layer by layer and removes those proven inactive.Pruning reduces network size before the SMT solver checks the query on the pruned network.Source: B. Solution Overview · p. 4, D. Sound Pruning · p. 5

C. Input Partitioning

  • A maximum attribute size controls partitioning; Fairify creates a network copy per region, enabling region-specific pruning and parallel query processing.A SAT result in any partition gives a counterexample, while UNSAT for one partition certifies only that region; all partitions must be UNSAT to establish whole-query UNSAT.Source: C. Input Partitioning · p. 5

D. Sound Pruning

  • Sound pruning analyzes activation patterns using partition-specific input bounds, removing neurons and associated edges when they do not affect network values.The network is represented for symbolic execution and constraint checking.Source: D. Sound Pruning · p. 5

1) Interval analysis:

Interval analysis propagates neuron bounds through the network using the preceding layer’s bounds. These bounds can prove a neuron inactive or show that its ReLU activation can be removed.

1) Interval analysis:

  • For each neuron, interval arithmetic combines upper or lower bounds from the preceding layer with positive and negative incoming weights to calculate bounds.The maximum uses upper bounds for positive weights and lower bounds for negative weights; the minimum uses the opposite bounds.Source: 1) Interval analysis · p. 5
  • If a neuron's weighted-sum upper bound is at most zero, it is always inactive and can be removed with its edges.The bounds are calculated without including activation functions, and the passage states that interval arithmetic on multiplication loses no accuracy.Source: 1) Interval analysis · pp. 5–6
  • If the lower bound is positive, Fairify removes the neuron's ReLU function; bounds may be too loose to prove inactivity, especially in deep layers.The latter case motivates an additional individual-verification step.Source: 1) Interval analysis · pp. 5–6

2) Individual verification:

Individual verification uses an SMT query for neurons that interval analysis has not already pruned. The checks proceed layer by layer using only the immediately preceding layer.

2) Individual verification:

  • For each remaining neuron, Fairify formulates an individual verification query with a precondition containing the neuron's lower bound.The query checks the condition that the neuron value is below zero.Source: 2) Individual verification · p. 6
  • Fairify checks neurons in increasing layer order, using only the immediately preceding layer and omitting ReLU activation functions from each query.Only neurons not already pruned by interval analysis receive these checks.Source: 2) Individual verification · p. 6
  • The individual queries can identify additional inactive neurons that interval analysis did not prove inactive.The passage attributes their speed to the restricted inputs and omission of nonlinear activations.Source: 2) Individual verification · p. 6

E. Heuristic Based Pruning

Fairify uses neuron-profile simulations and magnitude distributions to select additional pruning candidates conservatively. The approach targets smaller networks with little or no accuracy loss, while verification and deployment apply to the pruned model.

E. Heuristic Based Pruning

  • For structured-data fairness models, sparse input domains can leave many neurons never activated or active only in particular regions.The passage contrasts 13-feature Adult Census instances with 28-by-28 MNIST inputs.Source: E. Heuristic Based Pruning · p. 6
  • With 1,000 simulated valid inputs, Fairify marks neurons never observed active as candidates, then compares candidate and non-candidate magnitude distributions.The simulations profile neuron values; a candidate could still activate on an unobserved valid input.Source: E. Heuristic Based Pruning · p. 6
  • In first hidden layers, non-candidates' mean and median positive magnitudes were each at least 10 times larger than candidates'.The reported distribution difference informs candidate selection.Source: E. Heuristic Based Pruning · p. 6
  • Fairify selects candidates below the 5th percentile of non-candidate magnitudes using a 5% tolerance, with comparisons performed layer by layer.Magnitude differences are described as more prominent in deep than shallow layers.Source: E. Heuristic Based Pruning · p. 6
  • Heuristic pruning does not guarantee the original network's outcome, so the certified pruned model is the one intended for production.The authors report that conservative selection can enable faster verification with negligible accuracy effects.Source: E. Heuristic Based Pruning · p. 6

V. EVALUATION

The evaluation uses a benchmark designed for fairness verification in development pipelines, drawing on real-world neural networks from theory and practice. It covers 25 models across three fairness datasets and four sources.

1) Benchmarks:

  • The benchmark was designed to support fairness verification in development pipelines using models from theory and practice.Source: 1) Benchmarks · p. 7
  • The benchmark contains 25 neural networks collected from four sources for the Bank Marketing, Adult Census, and German Credit datasets.The networks are fully connected and use ReLU activations.Source: 1) Benchmarks · p. 7
  • Bank Marketing has 45,000 instances and 16 attributes, German Credit has 1,000 instances and 20 attributes, and Adult Census has 32,561 individuals and 13 attributes.The datasets concern term-deposit subscription, credit risk, and income above $50,000, respectively.Source: 1) Benchmarks · p. 7

2) Experiment setup:

Fairify is evaluated against SMT baselines on fairness-verification tasks, with configurable timeouts and partition sizes. The results assess utility through verification outcomes, pruning, and partition-level information that can support defect localization.

2) Experiment setup:

  • Fairify partitions inputs and returns a verification status for each partition, including a counterexample when SAT and the pruned network.The experiment considered utility, scalability to relaxed queries, and performance in time and accuracy.Source: 2) Experiment setup · p. 7, B. Results · p. 7

1) Utility:

  • In 30 minutes, Fairify verified 19 of 25 models, while the baseline verified only AC6 within 30 hours.Source: 1) Utility · p. 8, Table II · p. 8
  • Baseline verification encoded fairness constraints and sent them with the original network to an SMT solver; adding input partitioning produced the same results.Fairify combines partitioning with network pruning to reduce network complexity.Source: 1) Utility · p. 8
  • The soft timeout was 100 seconds per solver run, with another run after heuristic pruning when sound verification returned UNKNOWN.The hard timeout was 30 minutes; partition size and timeout were configurable.Source: 1) Utility · pp. 8–9
  • For AC3 with race as the protected attribute, a partition was pruned by 86.27% and yielded two unfair-credit-class counterexamples in 21.47 seconds.The individuals differed only in race and were classified as bad versus good credit risk.Source: 1) Utility · p. 8
  • Heuristic pruning was attempted 13.98% of the time and produced SAT or UNSAT results in 19.38% of those attempts.It was applied only when sound pruning did not produce a result within the soft timeout.Source: 1) Utility · p. 8
  • For BM3, Fairify reported SAT for 27 partitions and UNSAT for 108, which can help developers localize fairness defects and guide repair.Developers may also choose to deploy the pruned network versions.Source: 1) Utility · p. 9

2) Scalability:

Fairify was tested on more complex models and on relaxed and targeted fairness queries. The evaluation also reports the time required by its partitioning and pruning steps.

2) Scalability:

  • With a one-hour hard timeout and doubled soft timeout, Fairify verified 3 of the 6 remaining complex networks.The setup also reduced maximum partition size.Source: 2) Scalability · p. 9
  • Under relaxed fairness queries, 21/25 models were verified for φr1 and 22/25 for φr2 within one hour; targeted queries also yielded counterexamples or certifications for many partitions.Relaxation permits small perturbations to non-protected attributes while requiring the same class, making the fairness requirement stricter.Source: 2) Scalability · p. 9
  • Partitioning and pruning took no more than 10 seconds for any model, excluding SMT solving of the final constraints.The reported total includes partitioning and pruning, whose added time was negligible relative to SMT solving.Source: 3) Performance · p. 9

3) Performance:

Fairify’s reported performance is qualified by lower coverage than under differing verification properties and experimental settings, while conservative heuristic pruning incurred no accuracy loss. The paper also limits its evaluation to structured, ReLU-based models and describes outputs that can support fairness testing and repair.

3) Performance:

  • Fairify verified all queries for Libra models AC8–12 except AC11–12, which were verified for only two of four queries; reported coverage was below under different properties, configurations, and setups.The table covers verification of relaxed and targeted fairness queries.Source: 3) Performance · pp. 9–10, Table IV · p. 10
  • Conservative heuristic pruning caused no accuracy loss in the pruned networks, although less-conservative heuristic pruning may reduce accuracy.Without heuristic pruning, the paper reports no accuracy loss; the developer may choose to deploy a pruned network despite a small reduction.Source: 3) Performance · p. 10

VI. THREATS TO VALIDITY

  • Soundness is grounded in interval arithmetic and SMT solving, complete disjoint input partitions, and symbolic Python functions reconstructed from extracted model weights and biases.The paper notes that individual fairness can fall short in bias quantification and suggests certified-partition counts for future quantification.Source: §VI · p. 10
  • The evaluation covers structured datasets and ReLU networks; unstructured data may require a different approach, while CNN and LSTM verification remains future work.Source: §VI · p. 10

VII. RELATED WORKS

  • Prior work includes fairness testing, individual-fairness verification for non-neural models, dependency-fairness certification, and fairness-aware training.Other neural-network verification work has focused on properties such as robustness and adversarial inputs [44].Source: §VII · pp. 10–11

VIII. CONCLUSION AND FUTURE WORK

  • Fairify verifies individual fairness and its relaxations on real-world neural networks, with counterexamples and targeted results that can guide test generation and interactive repair.Source: §VIII · p. 11
  • Future work could prioritize verification partitions, dynamically allocate time, and extend provable repair and fairness-aware software design.Source: §VIII · p. 11

Related papers

Loading 2212.06140v2…