SHF: Medium: Formal Methods for Program Fairness

随着软件渗透到我们的个人生活、公司世界和官僚机构中，我们越来越多的关键决策被委托给不透明的算法。因此，这些算法已经成为一系列具有深远社会影响的重大决策的强大仲裁者。然而，执行敏感任务的算法可能存在歧视？是有意还是无意？反对某些群体。这个项目的首要目标是实现对这些决策程序的公平性的自动推理。这个项目的成果被整合到教学课程中，从而提高了人们对自动化决策公平性的认识。该项目在一个独特的跨学科环境中培养研究生。该项目受到法律和该地区最近的作品的启发，研究了各种公平的概念，并通过程序验证的正式镜头将它们投射出来。该项目开发了一些技术来证明一个程序在特定人群下是公平的，以及自动修复不公平的程序以使其公平的技术。从技术角度来看，该项目开发了新颖的概率程序验证和综合技术，这些技术在关注公平性问题的同时，具有普遍性并扩展了当前技术的范围。具体而言，该项目开发了基于体积计算的新型概率验证技术。此外，该项目还开发了概率程序的程序修复和调试技术。

As software permeates our personal lives, corporate world, and bureaucracy, more and more of our critical decisions are being delegated to opaque algorithms. These algorithms have thus become powerful arbitrators of a range of significant decisions with far-reaching societal impact. However, an algorithm carrying out a sensitive task could potentially discriminate ? advertently or inadvertently ? against certain groups. The overarching goal of this project is to enable automated reasoning about fairness of such decision-making programs. The results from this project are integrated in teaching curricula, thus raising awareness about fairness in automated decision making. The project trains graduate students in a unique and inter-disciplinary environment. This project investigates various notions of fairness, inspired by the law and recent works in the area, and casts them through the formal lens of program verification. The project develops techniques for certifying that a program is fair under a given population, and techniques for automatically repairing unfair programs to make them fair. From a technical viewpoint, this project develops novel probabilistic program verification and synthesis technologies that, while focusing on the problem of fairness, are general and expand the reach of current technologies. Specifically, the project develops novel probabilistic verification techniques based on volume computation. Furthermore, the project develops program repair and debugging techniques for probabilistic programs.