EAGER: SHF: Verified Audit Layers for Safe Machine Learning

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

• 批准号: 2318724
• 负责人: Joseph Tassarotti
• 金额: $ 19.95万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-03-15 至 2023-11-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2318724&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）系统存在许多与隐私、公平性和对抗对手的鲁棒性相关的问题。解决这些问题是大量研究的重点。然而，正在开发的解决方案往往是复杂的，证明它们是正确的涉及微妙的数学论证。这些复杂性使得错误有可能出现，特别是在从理论算法到可执行程序的翻译中。该项目通过为ML系统开发机器检查的正确性证明来解决这些问题。该项目的新奇之处在于，通过证明一个更小、更简单的称为审计器的程序的正确性，使这一点变得可行，该程序旨在检查和控制复杂ML系统的输出。这个项目的预期影响是一个可重用的框架，用于验证这些审计员，以及教育材料，对构建机器检查的证明随机algorithm.The技术的审计算法验证已成功地应用于其他领域的验证，如编译器的正确性和安全沙箱。然而，尽管在这些其他领域取得了成功，但在ML系统的背景下追求这种方法提出了新的挑战。首先，ML系统的正确性证明通常涉及复杂的概率参数，因此需要来自测度论概率理论的机器检查结果库。其次，在定理证明器中指定这些系统的行为是困难的，特别是因为审计算法通常是高阶的，这意味着它们的规范由它们正在检查其行为的底层算法参数化。该项目建立在早期的经验，开发一个库的离散概率理论验证随机算法和数据结构。在开发框架和验证示例审计算法的过程中，调查人员解决了以模块化方式构建这些正确性证明的额外挑战，这样，审计人员就可以重新该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查进行评估，被认为值得支持的搜索.

项目成果

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

高阶分离逻辑中的异步概率耦合

• DOI: 10.1145/3632868
• 发表时间: 2024
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Gregersen, Simon Oddershede;Aguirre, Alejandro;Haselwarter, Philipp G.;Tassarotti, Joseph;Birkedal, Lars
• 通讯作者: Birkedal, Lars