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

由大量数据推动的机器学习（ML）算法越来越多地用于几个关键领域，包括医疗保健，金融和交通。由ML算法产生的模型，例如深度神经网络，正在部署在这些值得信赖的领域。很明显，对于这些领域，需要高度保证基于ML的系统的安全和正确操作。该项目旨在为基于形式化方法的ML系统设计提供一个系统框架。该项目旨在审查和改进ML系统设计流程的几乎每个方面，包括数据集设计，学习算法选择，ML模型训练，分析和验证以及部署。 在项目过程中产生的理论和想法将在一个新的软件工具包中实现，用于在网络物理系统的背景下设计ML系统。该项目侧重于网络物理系统（CPS），这是一个应用形式方法原理的丰富领域。此外，该项目的研究思路可以很容易地应用于其他背景。这项研究的一个关键方面是使用语义方法来设计和分析ML系统，其中目标应用程序的语义和完整系统的正式规范，包括ML组件和其他组件，是设计方法的基石。该项目采用了一系列形式化方法，包括可满足性求解器、基于仿真的验证、模型检查、规范分析和综合，以改进ML设计流程的所有阶段。形式化技术还用于调整超参数和训练过程的其他方面，以帮助调试ML模型产生的错误分类，并在运行时监控ML系统，并确保ML模型的输出以一种确保始终安全运行的方式使用。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的知识产权进行评估来支持。优点和更广泛的影响审查标准。

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.