Efficient Counterexample-Guided Fairness Verification and Repair of Neural Networks Using Satisfiability Modulo Convex Programming

Efficient Counterexample-Guided Fairness Verification and Repair of Neural Networks Using Satisfiability Modulo Convex Programming

Arya Fayyazi, Yifeng Xiao, Pierluigi Nuzzo, Massoud Pedram

Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence
Main Track. Pages 367-375. https://doi.org/10.24963/ijcai.2025/42

Ensuring fairness is essential for ethical decision-making in various domains. Informally, a neural network is considered fair if and only if it treats similar individuals similarly in a given task. We introduce FaVeR (Fairness Verification and Repair), a framework for efficiently verifying and repairing pre-trained neural networks with respect to individual fairness properties. FaVeR ensures fairness via iterative search of high-sensitivity neurons and backward adjustment of their weights, guided by counterexamples generated from fairness verification using satisfiability modulo convex programming. By addressing fairness at the neuron level, FaVeR minimizes the impact of neural network repair on the overall performance. Experimental evaluations on common fairness datasets show that FaVeR achieves a 100% fairness repair rate across all models, with accuracy reduction of less than 2.27%. Moreover, its significantly lower average runtime makes it suitable for practical applications.
Keywords:
AI Ethics, Trust, Fairness: ETF: Fairness and diversity
AI Ethics, Trust, Fairness: ETF: Bias
Constraint Satisfaction and Optimization: CSO: Constraint satisfaction
Constraint Satisfaction and Optimization: CSO: Satisfiabilty