Repairing Decision-Making Programs Under Uncertainty


The world is uncertain. Programs can be wrong. We address the problem of repairing a program under uncertainty, where program inputs are drawn from a probability distribution. The goal of the repair is to construct a new program that satisfies a probabilistic Boolean expression. Our work focuses on loop-free decision-making programs, e.g., classifiers, that return a Boolean- or finite-valued result. Specifically, we propose distribution-guided inductive synthesis, a novel program repair technique that iteratively (i) samples a finite set of inputs from a probability distribution defining the precondition, (ii) sythesizes a minimal repair to the program over the sampled inputs using an SMT-based encoding, and (iii) verifies that the resulting program is correct and is semantically close to the original program. We formalize our algorithm and prove its correctness by rooting it in computational learning theory. For evaluation, we focus on repairing machine learning classifiers with the goal of making them unbiased (fair). Our implementation and evaluation demonstrate our approach's ability to repair a range of programs.

Computer Aided Verification (CAV)