CAREER: Formal Guarantees for Neurosymbolic Programs via Conformal Prediction

职业：通过保形预测对神经符号程序提供正式保证

• 批准号: 2338777
• 负责人: Osbert Bastani
• 金额: $ 59.8万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-07-01 至 2029-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2338777&HistoricalAwards=false
• 关键词: CAREER; Formal; Guarantees; Neurosymbolic; Programs

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.

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