CAREER: Formal Guarantees for Neurosymbolic Programs via Conformal Prediction

随着深度学习在过去十年中取得的巨大成功，深度神经网络（DNN）越来越多地被纳入安全关键系统，如医疗保健决策，教育和机器人技术。因此，迫切需要确保这些系统在实际部署时的可信度。这个项目的目标是设计新的技术来推理神经符号程序，这些程序包括DNN组件。对于传统的软件，形式化方法为程序正确性的推理提供了强大的技术。然而，这些工具与包括DNN组件的程序斗争，因为很难推理DNN的正确性属性。该项目的新颖之处是通过以严格的方式量化DNN组件的不确定性来设计可信赖的神经符号程序的算法和技术。通过这样做，下游组件可以考虑DNN预测中的不确定性;例如，如果机器人认为可能存在障碍物，它可能会谨慎行事。因此，该项目可以通过提高现代人工智能（AI）系统的可靠性来产生重大影响，这些系统在我们的世界中越来越普遍。此外，还将开设一个关于可信机器学习的新研究生班，并探索生成式人工智能在计算机科学教育中的新应用。该项目的基本思想是利用保形预测，这是一种量化任意黑盒模型的不确定性的策略，具有理论保证。广义的思想是将给定的模型转换为保形预测器，该保形预测器输出一组标签（称为预测集），该标签保证以高概率包含地面真值标签。例如，适形对象检测器可以以高概率检测图像中的所有对象，其中一些检测被标记为不确定。几种基于保形预测的程序推理技术正在探索中。首先，共形霍尔逻辑（conformal Hoare logic）的概念正在发展，这是霍尔逻辑的一个扩展，旨在对神经符号程序进行形式化推理，其中各个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.