EAGER: SHF: Verified Audit Layers for Safe Machine Learning

Boston College, Chestnut Hill MA

Investigators

Abstract

Existing machine learning (ML) systems have many issues related to privacy, fairness, and robustness against adversaries. Addressing these problems is the focus of a great deal of research. However, the solutions being developed are often complex, and the proofs that they are correct involve subtle mathematical arguments. These complexities make it possible for errors to arise, particularly in the translation from theoretical algorithms into executable programs. This project addresses these issues by developing machine-checked proofs of correctness for ML systems. The project's novelty is in an approach for making this feasible by proving the correctness of a smaller, simpler program called an auditor, which is designed to check and control the output of a complex ML system. The expected impact of this project is a re-usable framework for verifying these auditors, as well as educational material on constructing machine-checked proofs about randomized algorithms. The technique of verifying an auditing algorithm has been successfully applied in other areas of verification, such as compiler correctness and security sandboxing. However, despite successes in these other domains, pursuing this approach in the context of ML systems raises new challenges. First, proofs of correctness for ML systems often involve complex probabilistic arguments, so that machine-checked libraries of results from measure-theoretic probability theory are needed. Second, specifying the behavior of these systems in a theorem prover is difficult, particularly because auditing algorithms are often higher-order, meaning that their specification is parameterized by the underlying algorithms whose behavior they are checking. The project builds on earlier experience developing a library for discrete probability theory for verifying randomized algorithms and data structures. In the course of developing the framework and verifying example auditing algorithms, the investigator addresses additional challenges about structuring these correctness proofs in a modular way, so that auditors can be re-used and composed together to enforce multiple types of correctness properties. 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.