Collaborative Research: SLES: Verifying and Enforcing Safety Constraints in AI-based Sequential Generation

人工智能（AI）已经对各种复杂的现实挑战产生了变革性的影响。在其应用中，顺序数据在人工智能直接与用户接触时的许多关键用途中普遍存在。自动驾驶汽车依靠人工智能来处理来自摄像头和雷达的传感器数据序列，并做出一系列实时决策，以确保驾驶安全。医疗监控系统使用人工智能来分析患者健康数据序列，如血压、心率等，以检测异常并预测潜在的健康问题。聊天机器人利用人工智能来理解自然语言，并以单词和句子的顺序生成安全、公平和适当的文本响应。由于序列内复杂的依赖关系，人工智能产生的序列数据使其行为难以表征，并且在这些场景中不小心应用人工智能可能会导致有害的后果，例如自动驾驶车辆的碰撞或产生有偏见或有毒的文本。本项目旨在研究具有序列数据场景下人工智能的安全性，为其在关键任务环境中的行为提供保障，并确保基于人工智能的序列生成能够遵守安全约束和社会规范。最终，这项研究将有助于减少意外的人工智能故障，防止人工智能技术中的偏见和歧视，使人工智能系统与人类价值观和社会规范保持一致，并建立公众对人工智能应用的信任。本项目的技术贡献包括三个重点。第一个推力开发了一个正式的验证框架，以确保人工智能模型在严格的数学保证下进行顺序生成任务的安全性。它包括一系列创新的验证算法，适用于序列生成模型中涉及的一般非线性函数的有界传播和分支定界。这些新的验证方法将集成到alpha-beta-CROWN神经网络验证器中，这是一个由研究人员开发的知名开源工具箱。第二个重点涉及训练和推理算法，确保顺序生成模型符合指定的安全约束，并使用独特的概率框架将安全约束分解为行动级组件，并在每个生成步骤中强制执行它们。该方法可以与模型训练相结合，利用后验正则化技术提高序列生成模型的安全性能。最后，第三个重点旨在整合上述形式验证和约束生成组件，并将它们应用于三个重要的现实世界应用：文本生成的安全性，受控系统的安全性和稳定性，以及健壮的人工智能生成的文本检测器。该项目还将为更广泛的人工智能社区提供工具，包括α - β - crown神经网络验证器，以及为评估顺序生成模型的安全性而开发的共享数据和基准。该项目由美国国家科学基金会和开放慈善组织合作支持。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Artificial intelligence (AI) has achieved transformative impacts on various complex real-world challenges. Among its applications, sequential data are prevalent in many critical usages of AI when it directly engages with its users. Self-driving cars rely on AI to process sequences of sensor data from cameras and radars, and make a sequence of real-time decisions to ensure safe driving. Healthcare monitoring systems use AI to analyze sequences of patient health data, such as blood pressure, heart rate, and others, to detect anomalies and predict potential health issues. Chatbots utilize AI to understand natural language and generate safe, fair, and appropriate text responses as sequences of words and sentences. The sequential data produced by AI make its behavior hard to characterize because of the complex dependencies within the sequence, and a careless application of AI in these scenarios may lead to harmful consequences, such as a collision of an autonomous vehicle or the generation of biased or toxic texts. This project aims to study the safety of AI under scenarios with sequential data, provide assurance for its behavior in mission-critical environments, and ensure AI-based sequential generation can adhere to safety constraints and social norms. Ultimately, this research will help with reducing unexpected AI failures, preventing bias and discrimination in AI technologies, aligning AI systems with human values and societal norms, and building up public trust for AI-enabled applications.The technical contributions of this project consist of three thrusts. The first thrust develops a formal verification framework for assuring the safety of AI models for sequential generation tasks with rigorous mathematical guarantees. It includes a series of innovative verification algorithms for bound propagation and branch-and-bound for general non-linear functions involved in sequential generation models. These new verification methods will be integrated into the alpha-beta-CROWN neural network verifier, a well-known open-source toolbox developed by investigators. The second thrust involves training and inference algorithms that ensure sequential generation models comply with specified safety constraints, with a unique probabilistic framework that decomposes a safety constraint into action-level components and enforces them at each generation step. This approach can be integrated with model training to improve the safety performance of sequential generation models using posterior regularization techniques. Lastly, the third thrust aims to integrate the formal verification and constrained generation components above and apply them to three important real-world applications: safety of text generation, safety and stability of controlled systems, and robust AI-generated text detectors. This project will also result in tools to the broader AI community, including the alpha-beta-CROWN neural network verifier, and the shared data and benchmarks developed to evaluate the safety of sequential generation models.This project is supported by a partnership with the NSF and Open Philanthropy.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.