UCLA

The revolutionary capabilities of AI with machine learning have enabled an increasingly broad range of applications, bringing many new challenges in ensuring AI trustworthiness. This dissertation presents my research on trustworthy AI with verifiable guarantees and empirical robustness, addressing challenges posed by emerging AI models and applications. Following the introduction chapter, the first part introduces more general and scalable frameworks for the automatic formal verification of AI models as general computational graphs with general nonlinearities. I first develop a framework that not only supports regular computational graphs, but also higher-order computational graphs, enabling applications with gradients and Jacobians. I then develop a framework that enhances verification with branch-and-bound conducted on general nonlinear functions, enabling applications with various nonlinear constraints or dynamics such as autonomous systems. The second part of this dissertation introduces verification-aware training frameworks for neural networks, where verified output bounds are computed and optimized during training to produce verification-friendly AI models with stronger verifiability. I first accelerate this training by designing specific treatments on weight initialization, normalization, and regularization tailored to verification-aware training. Furthermore, I make verification-aware training more practical to handle relatively global guarantees that hold across an entire input region-of-interest rather than local robustness guarantees commonly studied previously. To do this, I develop a framework with a novel training-time branch-and-bound for verification-aware training, which is demonstrated on the application of training verification-friendly Lyapunov-stable controllers with neural networks in nonlinear dynamical systems. In the third part, I investigate the empirical reliability of AI models to complement formal guarantees, with a focus on addressing emerging challenges from large-scale pre-training. I first develop an out-of-distribution robustness evaluation that adapts to new training paradigms involving large-scale pre-training and thus scenarios comparing models trained on different datasets. I then develop a red teaming method for detectors of large language model generated texts, by generating both out-of-distribution and adversarial cases through leveraging a large language model itself. Lastly, I conclude this dissertation and discuss future directions for building more scalable and broadly applicable trustworthy AI techniques.