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.