CAREER: Formal Guarantees for Neurosymbolic Programs via Conformal Prediction

随着深度学习在过去十年中的巨大成功，深度神经网络(DNN)正越来越多地被纳入医疗决策、教育和机器人等安全关键系统。因此，迫切需要确保这些系统在实际部署时的可信性。这个项目的目标是设计关于神经符号程序的新的推理技术，这些程序包括DNN组件。对于传统软件来说，形式化方法为程序正确性的推理提供了强大的技术。然而，由于难以对DNN的正确性属性进行推理，这些工具难以处理包含DNN组件的程序。这个项目的新颖性是通过严格量化DNN组件的不确定性来设计值得信赖的神经符号程序的算法和技术。通过这样做，下游组件可以解释DNN预测中的不确定性；例如，如果机器人认为可能存在障碍，它可能会谨慎行事。因此，该项目可以通过提高现代人工智能(AI)系统的可靠性产生重大影响，现代人工智能(AI)系统在我们的世界越来越普遍。此外，正在创建一个关于可信机器学习的新研究生课程，并正在探索生成性人工智能在计算机科学教育中的新应用。该项目的基本思想是利用共形预测，这是一种量化任意黑盒模型的不确定性的策略，具有理论保证。其主要思想是将给定的模型转换为共形预测器，该共形预测器输出一组标签(称为预测集)，该标签集保证高概率地包含基本事实标签。例如，保形目标检测器可以高概率地检测图像中的所有目标，其中一些检测被标记为不确定。目前正在探索几种基于保角预测的程序推理技术。首先，共形Hoare逻辑的概念正在发展中，它是Hoare逻辑的扩展，旨在从形式上对神经符号程序进行组合推理，其中单个DNN组件都是带有共形保证的共形预测器。其次，正在开发一种将传统的神经符号程序转换为保形程序的策略，该策略通过对单个DNN组件应用保形预测，然后在整个程序中传播不确定性。第三，正在开发合成具有共形正确性保证的神经符号程序的保形综合策略。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.