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

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

• 批准号: 1837132
• 负责人: Sanjit Seshia
• 金额: $ 29.4万
• 依托单位: University of California-Berkeley
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-10-01 至 2023-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1837132&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的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Parallel and Multi-objective Falsification with Scenic and VerifAI

使用 Scenic 和 VerifAI 进行并行和多目标证伪

• DOI: 10.1007/978-3-030-88494-9_15
• 发表时间: 2021
• 期刊: 21st International Conference on Runtime Verification
• 作者: Viswanadha, K.;Kim, E.;Indaheng, F.;Fremont, D. J.;Seshia, S. A.
• 通讯作者: Seshia, S. A.

Scenic: a language for scenario specification and data generation

• DOI: 10.1007/s10994-021-06120-5
• 发表时间: 2020-10
• 期刊: Machine Learning
• 影响因子: 7.5
• 作者: Daniel J. Fremont;Edward J. Kim;T. Dreossi;Shromona Ghosh;Xiangyu Yue;A. Sangiovanni-Vincentelli;S. Sesh

Semantic Adversarial Deep Learning

• DOI: 10.1109/mdat.2020.2968274
• 发表时间: 2018-04
• 期刊: IEEE Design & Test
• 影响因子: 2
• 作者: S. Seshia;S. Jha;T. Dreossi