CAREER: Robustness Verification and Certified Defense for Machine Learning Models

机器学习模型在许多重要任务上表现得非常好；然而，由于这些模型的黑箱性质，并不能保证它们总是安全的。当将模型部署到现实世界的系统中时，这成为一个关键的挑战。例如，飞机控制系统在探测到附近的入侵者时必须执行一定的动作。即使在很小的干扰下，自动驾驶汽车也必须识别停车标志。该项目将开发一个框架来验证和提高机器学习模型的安全性。所提出的验证方法将是有效的，并支持广泛的结构。此外，该框架可用于训练保证满足某些安全规范的模型。这些功能将为小型神经网络之外的更广泛应用提供安全模型。该项目通过招募多元化的团队来支持教育和多元化。研究成果将被整合到人工智能安全相关的教科书、课程和宣传活动中。该项目的目标是为更通用的模型启用机器学习验证，并使其易于应用于应用程序领域的用户。为了实现这一目标，我们将构建一个基于凸松弛框架的自动验证算法。在这个框架中，模型验证可以作为一个优化问题，并使用（凸或线性）松弛来获得有效的解决方案。通过将该框架推广到一般计算图，我们将设计一个自动验证算法。该算法将自动运行用户指定的任何模型，而无需为每个新模型重新推导新的验证程序。除了允许更广泛的模型之外，该项目还将能够验证更复杂的语义扰动。研究者还将在基于优化的框架下研究离散模型（例如，KNN或树集成）的验证。最后，提出的研究将使训练模型具有可验证的属性，可以通过跨学科合作应用于许多现实世界的应用。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Machine learning models perform very well on many important tasks; however, those models are not guaranteed to be always safe due to their black-box nature. This becomes a critical challenge when deploying models into real world systems. For example, an aircraft control system has to perform a certain action when detecting a nearby intruder. A self-driving car has to recognize stop signs even under small perturbations. This project will develop a framework to verify and improve the safety of machine learning models. The proposed verification methods will be efficient and support a wide range of structures. Further, the framework can be used to train models that are guaranteed to meet some safety specifications. These functionalities will enable safe models for a much broader range of applications beyond small neural networks. The project supports education and diversity through the recruitment of a diverse team. The research results will be integrated into textbooks, courses, and outreach activities on AI safety.The goal of this project is to enable machine learning verification for more general models and to make it easily applicable to users in the application domains. To achieve this goal, we will build an automatic verification algorithm based on a convex relaxation framework. In this framework, model verification can be posed as an optimization problem, and (convex or linear) relaxations are used to get an efficient solution. By generalizing this framework to a general computational graph, we will design an automatic verification algorithm. The algorithm will run automatically for any model specified by a user, without the need of re-deriving a new verification procedure for each new model. In addition to allowing a wider range of models, the project will also enable verification of more complex semantic perturbations. The investigator will also study verification of discrete models (e.g., KNN or tree ensembles) under an optimization-based framework. Finally, the proposed research will enable training models with verifiable properties that can be applied to many real-world applications through interdisciplinary collaborations.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.