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算法产生的模型，例如深神经网络，正在这些域中部署在这些域中，在这些领域中，值得信赖是一个很大的问题。很明显，对于此类领域，基于ML的系统的安全和正确操作需要高度保证。该项目旨在为基于正式方法的ML系统设计提供系统的框架。该项目旨在审查和改善ML系统设计流的几乎所有方面，包括数据集设计，学习算法选择，ML模型培训，分析和验证以及部署。 项目期间产生的理论和思想将在一个新的软件工具包中实施，用于在网络物理系统的背景下设计ML系统。该项目着重于网络物理系统（CPS），这是应用正式方法原理的丰富领域。此外，该项目的研究思想可以很容易地应用于其他情况。这项研究的一个关键方面是使用语义方法来设计和分析ML系统，其中目标应用程序的语义以及包含ML组件和其他组件的完整系统的正式规范是设计方法的基石。该项目采用了一系列形式的方法，包括满足性求解器，基于仿真的验证，模型检查，规范分析和合成，以改善ML设计流的所有阶段。正式技术还用于调整超参数和培训过程的其他方面，以帮助调试由ML模型产生的错误分类，并在运行时监视ML系统，并确保以任何时间的方式使用ML模型的输出，以确保这些奖项的范围来确保NSF的合法任务和支持的范围，以表现出良好的依据，并具有良好的构建。 标准。

项目成果

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

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

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

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

Adaptive Reward-Poisoning Attacks against Reinforcement Learning

• 发表时间: 2020-03
• 期刊: ArXiv
• 作者: Xuezhou Zhang;Yuzhe Ma-;A. Singla;Xiaojin Zhu