CAREER: Robustness Verification and Certified Defense for Machine Learning Models

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

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.