SHF: Medium: Rearchitecting Neural Networks for Verification

SHF：中：重新架构神经网络进行验证

• 批准号: 1900676
• 负责人: Matthew Dwyer
• 金额: $ 125.55万
• 依托单位: University of Virginia Main Campus
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-07-01 至 2024-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1900676&HistoricalAwards=false
• 关键词: SHF; Medium; Rearchitecting; Neural; Networks

Machine learning has the potential to positively impact systems across society, for example, in agriculture, transportation, medicine, energy, and education. To realize that potential, however, methods for assuring the safe operation of those systems are needed. This project addresses this pressing need. Consider the increasing presence of self-driving capabilities in automobiles. They issue warnings when the car drifts outside of the lane and can initiate corrective steering actions. To do this, they employ a neural network to analyze images from a forward-facing camera to detect, for example, the lines that demark lane boundaries. A flaw in this neural network might, for instance, initiate a steering action in the wrong direction and thereby lead to vehicle damage or passenger injury. This project develops techniques for assuring that machine learning produces neural networks that come with guarantees about their behavior. Those guarantees can, in turn, be relied upon when determining that the overall system will operate safely. To achieve verifiably safe machine learning, this project leverages the growing body of work on symbolic verification algorithms for neural networks. These algorithms are cost-prohibitive when applied to existing neural networks. The approach taken in this project searches for and automatically generates an alternative neural network architecture that allows for an appropriate balance between the accuracy of the network and the tractability of verification. Once it finds such an architecture, it employs an iterative counterexample guided refinement approach to training the architecture which results in neural networks that meet essential safety guarantees. The project will organize an annual day-long "Rising Stars" forum for under-represented scholars working in formal methods, software engineering and machine learning.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.

机器学习有可能对整个社会的系统产生积极影响，例如农业、交通、医药、能源和教育。然而，为了实现这一潜力，需要确保这些系统安全运行的方法。该项目解决了这一迫切需求。想想汽车中越来越多的自动驾驶功能。当汽车偏离车道时，它们会发出警告，并启动纠正转向措施。为了做到这一点，他们使用了一个神经网络来分析来自前向摄像头的图像，以检测，例如，划定车道边界的线条。例如，这种神经网络的缺陷可能会导致错误的转向动作，从而导致车辆损坏或乘客受伤。该项目开发了一些技术，以确保机器学习产生的神经网络具有对其行为的保证。反过来，在确定整个系统是否安全运行时，可以依靠这些保证。为了实现可验证的安全机器学习，该项目利用了神经网络符号验证算法方面越来越多的工作。当应用于现有的神经网络时，这些算法的成本过高。该项目采用的方法搜索并自动生成另一种神经网络架构，该架构允许在网络的准确性和验证的可追溯性之间取得适当的平衡。一旦找到这样的架构，它就会使用迭代反例指导的改进方法来训练架构，从而产生满足基本安全保证的神经网络。该项目将为在正式方法、软件工程和机器学习领域工作的代表性不足的学者组织为期一天的年度“新星”论坛。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Systematic Generation of Diverse Benchmarks for DNN Verification

• DOI: 10.1007/978-3-030-53288-8_5
• 发表时间: 2020-06-13
• 期刊: Computer Aided Verification
• 作者: Xu D;Shriver D;Dwyer MB;Elbaum S
• 通讯作者: Elbaum S

Reducing DNN Properties to Enable Falsification with Adversarial Attacks

• DOI: 10.1109/icse43902.2021.00036
• 发表时间: 2021-05
• 期刊: 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)
• 作者: David Shriver;Sebastian G. Elbaum;Matthew B. Dwyer

DNNV: A Framework for Deep Neural Network Verification

• DOI: 10.1007/978-3-030-81685-8_6
• 发表时间: 2021-05
• 作者: David Shriver;Sebastian G. Elbaum;Matthew B. Dwyer