EAGER: SHF: Verified Audit Layers for Safe Machine Learning

EAGER：SHF：用于安全机器学习的经过验证的审计层

• 批准号: 2035314
• 负责人: Joseph Tassarotti
• 金额: $ 19.95万
• 依托单位: Boston College
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-10-01 至 2023-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2035314&HistoricalAwards=false
• 关键词: EAGER; SHF; Verified; Audit; Layers

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.

现有的机器学习（ML）系统存在许多与隐私、公平性和针对对手的鲁棒性相关的问题。解决这些问题是大量研究的重点。然而，正在开发的解决方案通常很复杂，并且证明它们正确性涉及微妙的数学论证。这些复杂性使得可能出现错误，特别是在从理论算法到可执行程序的转换过程中。该项目通过开发机器检查的机器学习系统正确性证明来解决这些问题。该项目的新颖之处在于通过证明一个更小、更简单的程序（称为审计程序）的正确性来实现这一目标，该程序旨在检查和控制复杂机器学习系统的输出。该项目的预期影响是一个用于验证这些审计员的可重用框架，以及有关构建随机算法的机器检查证明的教育材料。验证审计算法的技术已成功应用于其他验证领域，例如作为编译器的正确性和安全沙箱。然而，尽管在这些其他领域取得了成功，但在机器学习系统的背景下追求这种方法提出了新的挑战。首先，机器学习系统的正确性证明通常涉及复杂的概率论证，因此需要经过机器检查的测度概率论结果库。其次，在定理证明器中指定这些系统的行为很困难，特别是因为审核算法通常是高阶的，这意味着它们的规范是由它们正在检查其行为的底层算法参数化的。该项目建立在早期开发离散概率论库以验证随机算法和数据结构的经验基础上。在开发框架和验证示例审核算法的过程中，研究人员解决了以模块化方式构建这些正确性证明的额外挑战，以便审核员可以重复使用并组合在一起以强制执行多种类型的正确性属性。该奖项反映了通过使用基金会的智力价值和更广泛的影响审查标准进行评估，NSF 的法定使命被认为值得支持。

项目成果

A Separation Logic for Negative Dependence

• DOI: 10.1145/3498719
• 发表时间: 2022-01-01
• 期刊: PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL
• 影响因子: 1.8
• 作者: Bao，Jialu;Gaboardi，Marco;Tassarotti，Joseph
• 通讯作者: Tassarotti，Joseph