SHF: Medium: Formal Methods for Program Fairness

SHF：媒介：程序公平性的形式化方法

• 批准号: 1704117
• 负责人: Aws Albarghouthi
• 金额: $ 100万
• 依托单位: University of Wisconsin-Madison
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-06-01 至 2021-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1704117&HistoricalAwards=false
• 关键词: SHF; Medium; Formal; Methods; Program

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.

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

项目成果

Synthesizing Coupling Proofs of Differential Privacy

• DOI: 10.1145/3158146
• 发表时间: 2018-01-01
• 期刊: PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL
• 影响因子: 1.8
• 作者: Albarghouthi, Aws;Hsu, Justin
• 通讯作者: Hsu, Justin

Training Set Debugging Using Trusted Items

• DOI: 10.1609/aaai.v32i1.11610
• 发表时间: 2018-01
• 期刊: ArXiv
• 作者: Xuezhou Zhang;Xiaojin Zhu;Stephen J. Wright

Multi-category fairness in sponsored search auctions

赞助搜索拍卖中的多类别公平性

• DOI: 10.1145/3351095.3372848
• 发表时间: 2020
• 期刊: and Transparency
• 作者: Ilvento, Christina;Jagadeesan, Meena;Chawla, Shuchi
• 通讯作者: Chawla, Shuchi

Teacher Improves Learning by Selecting a Training Subset

教师通过选择训练子集来改善学习

• 发表时间: 2018
• 期刊: Proceedings of the Twenty-First International Conference on Artificial Intelligence and Statistics
• 作者: Ma, Yuzhe;Nowak, Robert;Rigollet, Philippe;Zhang, Xuezhou;Zhu, Xiaojin
• 通讯作者: Zhu, Xiaojin

Repairing Decision-Making Programs under Uncertainty

修复不确定性下的决策程序

• 发表时间: 2017
• 期刊: Computer Aided Verification
• 作者: Albarghouthi, Aws;D'Antoni, Loris;Drews, Samuel
• 通讯作者: Drews, Samuel