Justicia: A Stochastic SAT Approach to Formally Verify Fairness

Authors: Bishwamittra Ghosh, Debabrota Basu, Kuldeep S. Meel7554-7563

AAAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Experimental Our experiments validate that our method is more accurate and scalable than the distributional verifiers, such as Fair Square and Veri Fair, and more robust than the sample-based empirical verifiers, such as AIF360.
Researcher Affiliation Academia Bishwamittra Ghosh1, Debabrota Basu2,3, Kuldeep S. Meel1 1 National University of Singapore, Singapore 2 Chalmers University of Technology, G oteborg, Sweden 3 Scool, Inria Lille Nord Europe, France
Pseudocode Yes Algorithm 1 Justicia: SSAT-based Fairness Verifier
Open Source Code Yes Source code: https://github.com/meelgroup/justicia
Open Datasets Yes We have experimented on multiple datasets containing multiple protected attributes: the UCI3 Adult and German-credit dataset, Pro Publica s COMPAS recidivism dataset (Angwin et al. 2016), Ricci dataset (Mc Ginley 2010), and Titanic dataset4.
Dataset Splits No The paper mentions using k-samples from the data generating distribution for error bounds in theoretical analysis but does not specify actual training/validation/test splits for the experiments conducted on the listed datasets.
Hardware Specification No The paper states that computational work was performed on resources of 'Max Planck Institute for Software Systems, Germany and the National Supercomputing Centre, Singapore', but it does not provide specific hardware details (e.g., GPU/CPU models, memory) of these resources.
Software Dependencies No We have implemented a prototype of Justicia in Python (version 3.7.3). ... We have used the Py SAT library ... for encoding the decision function of the logistic regression classifier into a CNF formula.
Experiment Setup No The paper describes the classifiers and algorithms studied (CNF learner, decision trees, logistic regression, reweighing algorithm, optimized pre-processing algorithm) and the datasets used, but it does not provide specific hyperparameter values or other system-level training settings.