Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Quantitative Verification of Fairness in Tree Ensembles

Zhenjiang Zhao, Takahisa Toda, Takashi Kitamura

TL;DR

This work tackles the challenge of quantitatively verifying fairness and robustness in tree ensembles by introducing BoxQTE, a SMT-based framework that exploits the box-structured input partitioning inherent to trees to compute any-time upper and lower bounds on fairness measures. It formalizes confidence-based fairness and robustness (epsilon-kappa) for tree ensembles, defines path-tuple boxes, and shows how to encode the problem to discover counterexample regions without exhaustive search. BoxQTE delivers superior efficiency and accuracy compared to CegarQuant, aided by enhancements like task priority, decomposition, and box blocking, and it demonstrates notable improvements in fairness testing by identifying many more discriminatory instances in substantially less time. The approach holds promise for model debugging and bias mitigation in tabular-data applications, with extensions to multi-class ensembles and integration with surrogate-based testing envisaged for future work.

Abstract

This work focuses on quantitative verification of fairness in tree ensembles. Unlike traditional verification approaches that merely return a single counterexample when the fairness is violated, quantitative verification estimates the ratio of all counterexamples and characterizes the regions where they occur, which is important information for diagnosing and mitigating bias. To date, quantitative verification has been explored almost exclusively for deep neural networks (DNNs). Representative methods, such as DeepGemini and FairQuant, all build on the core idea of Counterexample-Guided Abstraction Refinement, a generic framework that could be adapted to other model classes. We extended the framework into a model-agnostic form, but discovered two limitations: (i) it can provide only lower bounds, and (ii) its performance scales poorly. Exploiting the discrete structure of tree ensembles, our work proposes an efficient quantification technique that delivers any-time upper and lower bounds. Experiments on five widely used datasets demonstrate its effectiveness and efficiency. When applied to fairness testing, our quantification method significantly outperforms state-of-the-art testing techniques.

Quantitative Verification of Fairness in Tree Ensembles

TL;DR

This work tackles the challenge of quantitatively verifying fairness and robustness in tree ensembles by introducing BoxQTE, a SMT-based framework that exploits the box-structured input partitioning inherent to trees to compute any-time upper and lower bounds on fairness measures. It formalizes confidence-based fairness and robustness (epsilon-kappa) for tree ensembles, defines path-tuple boxes, and shows how to encode the problem to discover counterexample regions without exhaustive search. BoxQTE delivers superior efficiency and accuracy compared to CegarQuant, aided by enhancements like task priority, decomposition, and box blocking, and it demonstrates notable improvements in fairness testing by identifying many more discriminatory instances in substantially less time. The approach holds promise for model debugging and bias mitigation in tabular-data applications, with extensions to multi-class ensembles and integration with surrogate-based testing envisaged for future work.

Abstract

This work focuses on quantitative verification of fairness in tree ensembles. Unlike traditional verification approaches that merely return a single counterexample when the fairness is violated, quantitative verification estimates the ratio of all counterexamples and characterizes the regions where they occur, which is important information for diagnosing and mitigating bias. To date, quantitative verification has been explored almost exclusively for deep neural networks (DNNs). Representative methods, such as DeepGemini and FairQuant, all build on the core idea of Counterexample-Guided Abstraction Refinement, a generic framework that could be adapted to other model classes. We extended the framework into a model-agnostic form, but discovered two limitations: (i) it can provide only lower bounds, and (ii) its performance scales poorly. Exploiting the discrete structure of tree ensembles, our work proposes an efficient quantification technique that delivers any-time upper and lower bounds. Experiments on five widely used datasets demonstrate its effectiveness and efficiency. When applied to fairness testing, our quantification method significantly outperforms state-of-the-art testing techniques.

Paper Structure

This paper contains 40 sections, 3 theorems, 27 equations, 6 figures, 4 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Our contributions.
  3. Preliminary
  4. Fairness and Robustness
  5. Decision Trees and Tree Ensembles
  6. Basics
  7. Box of path
  8. Semantics of tree ensembles in terms of box
  9. Methodology and Theory
  10. Quantitative Verification Problem
  11. Theory Basics
  12. Intution of Our Quantification Method
  13. SMT Encoding for Tree Ensembles
  14. Proposed Quantification Method: BoxQTE
  15. Parallelization.
  16. ...and 25 more sections

Key Result

Lemma 1

Let $f$ be a tree ensemble, and $X$ be its input space. The following statements hold: (1) $\bigcup_{\text{path tuple }\vec{\pi} \text{ in } f}B^{(\vec{\pi})} = X$, (2) for any two path tuples $\vec{\pi}$ and $\vec{\pi'}$, if $\vec{\pi} \neq \vec{\pi'}$, then $B^{(\vec{\pi})} \cap B^{(\vec{\pi'})} =

Figures (6)

  • Figure 1: An example of GBDT tree ensemble classifier for predicting loan eligibility. The input attributes are ordered as 'income', 'race' and 'age'. Among them, income takes real values over the range $[0, 1000]$, race takes categorical values over the range $[0, 4]$, and age takes integer values over the range $[0, 100]$.
  • Figure 2: Overview of our quantification method, BoxQTE.
  • Figure 3: Two examples of partial counterexample regions (in red) obtained from box pairs.
  • Figure 4: Evolution of bounds over time of BoxQTE and CegarQuant with time limit of 600s.
  • Figure 5: Evolution of bounds over time of BoxQTE and its three enhancements with time limit of 600s.
  • ...and 1 more figures

Theorems & Definitions (14)

  • Definition 1: Global $\epsilon$-Robustness with Classifier Confidence $\kappa$: a. k. a . , $\epsilon$-$\kappa$-Robustness
  • Definition 2: $\epsilon$-Fairness with Classifier Confidence $\kappa$: a. k. a . , $\epsilon$-$\kappa$-Fairness
  • Example 1: Tree Ensemble
  • Example 2: Tree Ensemble
  • Definition 3: Individual Fairness Measure
  • Definition 4: $\epsilon$-$\kappa$-Fairness Measure
  • Definition 5: $\epsilon$-$\kappa$-Robustness Measure
  • Lemma 1
  • Lemma 1
  • Theorem 1: Any-Time Lower and Upper Bounds
  • ...and 4 more