FMitF: Collaborative Research: Formal Methods for Machine Learning System Design

FMITF：协作研究：机器学习系统设计的形式化方法

• 批准号: 1836978
• 负责人: Somesh Jha
• 金额: $ 40.6万
• 依托单位: University of Wisconsin-Madison
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1836978&HistoricalAwards=false
• 关键词: FMitF; Collaborative; Research; Formal; Methods

Machine learning (ML) algorithms, fueled by massive amounts of data, are increasingly being utilized in several critical domains, including health care, finance, and transportation. Models produced by ML algorithms, for example deep neural networks, are being deployed in these domains where trustworthiness is a big concern. It has become clear that, for such domains, a high degree of assurance is required regarding the safe and correct operation of ML-based systems. This project seeks to provide a systematic framework for the design of ML systems based on formal methods. The project seeks to review and improve almost every aspect of the design flow of ML systems, including data-set design, learning algorithm selection, training of ML models, analysis and verification, and deployment. The theory and ideas generated during the project will be implemented in a new software toolkit for the design of ML systems in the context of cyber-physical systems.The project focuses on cyber-physical systems (CPS), which is a rich domain to apply formal methods principles. Moreover, the research ideas from this project can be readily applied to other contexts. A key aspect of this research is the use of a semantic approach to the design and analysis of ML systems, where the semantics of the target application and a formal specification for the full system, comprising the ML component and other components, are cornerstones of the design methodology. The project employs a range of formal methods, including satisfiability solvers, simulation-based verification, model checking, specification analysis, and synthesis to improve all stages of the ML design flow. Formal techniques are also used for the tuning of hyper-parameters and other aspects of the training process, to aid in debugging misclassifications produced by ML models, and to monitor ML systems at run time and ensure that outputs from ML models are used in a manner that ensures safe operation at all times.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的系统的安全和正确操作需要高度的保证。该项目旨在为基于形式化方法的机器学习系统设计提供一个系统框架。该项目旨在审查和改进机器学习系统设计流程的几乎每个方面，包括数据集设计、学习算法选择、机器学习模型的训练、分析和验证以及部署。项目期间产生的理论和想法将在一个新的软件工具包中实施，用于在网络物理系统的背景下设计机器学习系统。该项目重点研究网络物理系统（CPS），这是一个应用形式化方法原理的丰富领域。此外，本项目的研究思路可以很容易地应用于其他情境。本研究的一个关键方面是使用语义方法来设计和分析机器学习系统，其中目标应用程序的语义和完整系统的正式规范，包括机器学习组件和其他组件，是设计方法的基石。该项目采用了一系列正式方法，包括满意度求解器、基于仿真的验证、模型检查、规范分析和综合，以改进机器学习设计流程的所有阶段。正式技术也用于调整超参数和训练过程的其他方面，以帮助调试ML模型产生的错误分类，并在运行时监控ML系统，并确保ML模型的输出以确保始终安全运行的方式使用。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Game redesign in no-regret game playing

游戏重新设计，让游戏不后悔

• 发表时间: 2022
• 期刊: The 31st International Joint Conference on Artificial Intelligence and the 25th European Conference on Artificial Intelligence
• 作者: Ma, Yuzhe;Wu, Young;Zhu, Xiaojin
• 通讯作者: Zhu, Xiaojin

Towards Understanding Limitations of Pixel Discretization Against Adversarial Attacks

• DOI: 10.1109/eurosp.2019.00042
• 发表时间: 2018-05
• 期刊: 2019 IEEE European Symposium on Security and Privacy (EuroS&P)
• 作者: Jiefeng Chen;Xi Wu;Vaibhav Rastogi;Yingyu Liang;S. Jha

Policy Teaching via Environment Poisoning: Training-time Adversarial Attacks against Reinforcement Learning

• 发表时间: 2020-03
• 期刊: ArXiv
• 作者: Amin Rakhsha;Goran Radanovic;R. Devidze;Xiaojin Zhu;A. Singla

The Sample Complexity of Teaching by Reinforcement on Q-Learning

• DOI: 10.1609/aaai.v35i12.17306
• 发表时间: 2021-05
• 作者: Xuezhou Zhang;S. Bharti;Yuzhe Ma;A. Singla;Xiaojin Zhu

Corruption-Robust Offline Reinforcement Learning

• 发表时间: 2021-06
• 期刊: ArXiv
• 作者: Xuezhou Zhang;Yiding Chen;Jerry Zhu;Wen Sun