Fairify: Fairness Verification of Neural Networks

Overview

We built Fairify, an SMT-based approach that verifies individual fairness of deep neural networks in production. Individual fairness requires that any two individuals who differ only in protected attributes such as race, sex, or age receive similar predictions; unlike group metrics, it captures worst-case discrimination. The property is hard to verify because it must be checked globally over the input domain and because of the non-linear computation nodes in the network.

We encoded individual fairness as pre- and post-conditions of the network and made verification tractable in three steps: input partitioning, sound neural pruning, and heuristic-based neural pruning. The key observation was that many neurons remain inactive when only a smaller part of the input domain is considered, so Fairify assigns a copy of the network to each partition and prunes it using interval arithmetic and layer-wise analysis before invoking the SMT solver.

Key Results

• Encoded individual fairness as SMT pre- and post-conditions, so each verification query returns either a fairness certificate or a concrete counterexample.
• Made global verification tractable by partitioning the input domain and applying sound pruning (interval arithmetic, layer-wise analysis) plus activation-heuristic pruning to each partition’s copy of the network.
• Verified 25 real-world neural networks collected from four different sources, showing better effectiveness, scalability, and performance than baseline and closely related work.
• Supported relaxed and targeted fairness queries and partial certification, and located violations with counterexamples that make fairness repair explainable; published at ICSE 2023.