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

University Of Illinois At Urbana-Champaign, Urbana IL

Investigators

Abstract

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.