Counting Worlds Branching Time Semantics for Post-Hoc Bias Mitigation in Generative AI

Generative AI systems are known to amplify biases present in their training data. While several inference-time mitigation strategies have been proposed, they remain largely empirical and lack formal guarantees. We introduce CTLFS, a branching-time logic designed to reason about bias in series of outputs by a generative AI. CTLFS defines modal operators that, based on a counting worlds semantics, allow us to verify whether the current generation process respects intended properties. These include: satisfaction of an intended probability distribution over a protected attribute; prediction of the likelihood of remaining within acceptable bounds as new outputs are generated; and required output elimination to restore fairness. We illustrate the framework on a toy example of biased image generation.