FMitF:Track I: Verified Safe and Fair Machine Learning

人工智能（AI），特别是机器学习，正越来越多地应用于对人们生活产生重大影响的领域。例子包括医疗保健和社会服务的提供、法律司法系统的决策、自动驾驶汽车以及面部和语音识别。研究人员发现，机器学习的这些应用往往包含偏见，或健康、安全或经济风险。这个项目的新颖之处在于开发方法来证明机器学习系统的安全性或公平性测试在数学上是合理的，并且在计算机上正确编码，因此其测试结果是可以信赖的。因此，项目的影响将是更大的保证，即风险（缺乏安全性）和偏见（缺乏公平性）被准确而正确地了解和评估。研究人员开发了对上述总体目标所必需的几个组件的正确性进行计算机检查的证明。这些计算机检查的必要统计检验公式的证明，如Hoeffding不等式（和其他类似的不等式），被用来限制偏差或安全风险超过给定极限的概率。其中的数学原理是已知的，但计算机检验的证明是新颖的。此外，一些较新的边界有手写的证明，可能需要更严格或更强的假设，其局限性将通过尝试计算机检查的证明来揭示。其次，用于实现安全性/公平性测试的计算机代码需要类似的正确性证明。如何做到这一点的某些方面是众所周知的，但是缺少涉及的数字（浮点）计算的计算机验证证明，并且具有挑战性。最后，研究人员将通过使用机器学习来辅助这些证明，改进在某些方面仍然薄弱的计算机证明工具。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Artificial intelligence (AI), and specifically machine learning, is being used more and more in areas with significant real-world impacts on people's lives. Examples include the delivery of health care and social services, decisions in the legal-justice system, self-driving cars, and face and speech recognition. Researchers have discovered that these applications of machine learning often embody biases, or health, safety, or economic risks. This project's novelty lies in developing ways to show that a test of the safety or fairness of a machine-learning system is mathematically sound and correctly coded on a computer, so that its test results can be relied upon. The project's impacts will thus be greater assurance that risks (lack of safety) and biases (lack of fairness) are known and evaluated precisely and correctly.The investigators develop computer-checked proofs of correctness of several components necessary to the overall goals described above. These computer-checked proofs of formulations of the necessary statistical tests, such as Hoeffding's Inequality (and other such inequalities), are used to bound the probability that bias or safety risk exceeds a given limit. The mathematics of these is known, but computer-checked proofs are novel. Further, some newer bounds have hand-written proofs possibly needing more rigor or stronger assumptions, the limitations of which will be revealed by attempting computer-checked proofs. Next, computer code used to implement the safety/fairness tests needs similar proofs of correctness. Some aspects of how to do this are well-known, but computer-checked proofs for the numerical (floating-point) computations involved are lacking, and challenging. Lastly, the researchers will improve the computer proof tools, which remain weak in certain respects, by using machine learning to assist in these kinds of proofs.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.