FairSquare: Probabilistic Verification for Program Fairness

With the range and sensitivity of algorithmic decisions expanding at a break-neck speed, it is imperative that
we aggressively investigate fairness and bias in decision-making programs. First, we show that a number of
recently proposed formal definitions of fairness can be encoded as probabilistic program properties. Second,
with the goal of enabling rigorous reasoning about fairness, we design a novel technique for verifying
probabilistic properties that admits a wide class of decision-making programs. Third, we present FairSquare,
the first verification tool for automatically certifying that a program meets a given fairness property. We
evaluate FairSquare on a range of decision-making programs. Our evaluation demonstrates FairSquare’s
ability to verify fairness for a range of different programs, which we show are out-of-reach for state-of-the-art
program analysis techniques.