Fairness as a Program Property
This work addresses fairness verification for decision-making programs, which is an incremental step in applying formal methods to algorithmic fairness.
The paper tackles the problem of determining whether a decision-making program is fair by framing algorithmic fairness questions as program verification problems, and it presents an automated verification technique to prove or disprove fairness with respect to a probabilistic population model.
We explore the following question: Is a decision-making program fair, for some useful definition of fairness? First, we describe how several algorithmic fairness questions can be phrased as program verification problems. Second, we discuss an automated verification technique for proving or disproving fairness of decision-making programs with respect to a probabilistic model of the population.