Takahisa Toda

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.

As machine learning (ML) systems are increasingly used in various fields, including tasks with high social impact, concerns about their fairness are growing. To address these concerns, individual fairness testing (IFT) has been introduced to identify individual discriminatory instances (IDIs) that indicate the violation of individual fairness in a given ML classifier. In this paper, we propose a black-box testing algorithm for IFT, named Aft (short for Approximation-guided Fairness Testing). Aft constructs approximate models based on decision trees, and generates test cases by sampling paths of the decision trees. Our evaluation by experiments confirms that Aft outperforms the state-of-the-art black-box IFT algorithm ExpGA both in efficiency (by 3.42 times) and diversity of IDIs identified by algorithms (by 1.16 times).

Individual fairness testing (Ift) is a framework to find discriminatory instances within a given classifier. In this paper, we show our idea of a Ift framework, that integrates the notion of data validity, termed "Individual Fairness Testing with Data Validity (Ift-v)". We develop a solid foundation of Ift-v and demonstrate the feasibility of Ift-v. Our preliminary evaluation with Ift-v reveals the possibility that many of discriminatory instances detected by state-of-the-art Ift algorithms are considered invalid. These findings prompt a re-think of the current Ift framework, suggesting a transition from solely focusing on the discovery of discriminatory instances to the consideration of valid ones.

This paper proposes an algorithmic framework for various reconfiguration problems using zero-suppressed binary decision diagrams (ZDDs), a data structure for families of sets. In general, a reconfiguration problem checks if there is a step-by-step transformation between two given feasible solutions (e.g., independent sets of an input graph) of a fixed search problem such that all intermediate results are also feasible and each step obeys a fixed reconfiguration rule (e.g., adding/removing a single vertex to/from an independent set). The solution space formed by all feasible solutions can be exponential in the input size, and indeed many reconfiguration problems are known to be PSPACE-complete. This paper shows that an algorithm in the proposed framework efficiently conducts the breadth-first search by compressing the solution space using ZDDs, and finds a shortest transformation between two given feasible solutions if exists. Moreover, the proposed framework provides rich information on the solution space, such as the connectivity of the solution space and all feasible solutions reachable from a specified one. We demonstrate that the proposed framework can be applied to various reconfiguration problems, and experimentally evaluate their performances.