CAREER: Formal Guarantees for Neurosymbolic Programs via Conformal Prediction

With the enormous success of deep learning over the past decade, deep neural networks (DNNs) are increasingly being incorporated into safety-critical systems, such as healthcare decision making, education and robotics. As a consequence, there is an urgent need to ensure trustworthiness of these systems when deployed in practice. The goal of this project is to design novel techniques for reasoning about neurosymbolic programs, which are programs that include DNN components. For traditional software, formal methods have provided powerful techniques for reasoning about program correctness. However, these tools struggle with programs that include DNN components due to the difficulty in reasoning about correctness properties of DNNs. This project's novelties are algorithms and techniques for designing trustworthy neurosymbolic programs by quantifying uncertainty of DNN components in a rigorous way. By doing so, downstream components can account for uncertainty in the DNN predictions; for instance, a robot may act cautiously if it believes an obstacle might be present. As a consequence, this project can have significant impacts by improving the reliability of modern artificial intelligence (AI) systems, which are increasingly pervasive in our world. Further, a new graduate class on trustworthy machine learning is being created, and novel applications of generative AI in computer science education are being explored. The fundamental idea of the project is to leverage conformal prediction, a strategy for quantifying uncertainty of arbitrary blackbox models that comes with theoretical guarantees. The broad idea is to convert a given model into a conformal predictor that outputs a set of labels (called a prediction set) that is guaranteed to contain the ground truth label with high probability. For example, a conformal object detector can detect all objects in an image with high probability, with some of the detections marked as uncertain. Several techniques for reasoning about programs based on conformal prediction are being explored. First, the notion of conformal Hoare logic, an extension of Hoare logic designed to formally reason compositionally about neurosymbolic programs where the individual DNN components are all conformal predictors that come with conformal guarantees, is being developed. Second, a strategy for converting a traditional neurosymbolic program into a conformal one, by applying conformal prediction to the individual DNN components and then propagating uncertainty through the whole program, is being developed. Third, conformal synthesis strategies for synthesizing neurosymbolic programs that come with conformal correctness guarantees is being developed. 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.