FMitF:Track I: Verified Safe and Fair Machine Learning

点击翻译按钮获取中文摘要

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.