FMitF: Track I: Scalable and Quantitative Verification for Neural Network Analysis and Design

FMITF：第一轨：神经网络分析和设计的可扩展和定量验证

基本信息

批准号：
2124039
负责人：
Tevfik Bultan
金额：
$ 74.92万
依托单位：
University of California-Santa Barbara
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2021
资助国家：
美国
起止时间：
2021-10-01 至 2025-09-30
项目状态：
未结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2124039&HistoricalAwards=false
关键词：
FMitF Track Scalable Quantitative Verification

项目摘要

Neural Networks (NNs) have been successful in many areas including computer vision, speech recognition, and natural language processing. However, due to the increasing adoption of NNs in safety-critical and socially sensitive domains such as self-driving cars, robotics, computer security, criminal justice, and medical diagnosis, there is a pressing need for developing verification techniques that can provide guarantees about dependability and safety of NN applications. Formal-verification techniques can provide guarantees of correctness; however, existing approaches are not effective in analyzing real-world NNs with large numbers of neurons and complicated model structures. This project sets a comprehensive research agenda focusing on a holistic formal-verification framework for NNs that will provide a systematic and principled approach for developing dependable and safe NNs. It is intended to benefit major machine-learning applications such as autonomous driving and contribute to the leadership of the United States in software engineering and artificial intelligence. The research findings are being widely disseminated through open-source software packages, publications in premier conferences and journals, tutorials at teaching workshops, as well as specialized K-12 programs for exposing the young generation to the frontiers of software verification and machine-learning research. The team of researchers working on this project are integrating methods from the classical computing fields such as software engineering, automated verification, and formal methods to address the unique research challenges in the dependability and safety of NN applications. Specific research directions include 1) novel symbolic quantitative analysis techniques that provide sound results for establishing dependability and safety of the state-of-the-art NN models; 2) a set of effective system-level optimizations for computation/memory efficient NN verification with sufficient cross-framework portability and high verification efficiency; 3) advanced neural architecture design and training support for exploring and developing neural network models with verifiable robustness. The success of this research agenda is intended to enable a more complete and efficient software stack for improving the scalability of NN verification techniques and the robustness of NN applications.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.

神经网络 (NN) 在计算机视觉、语音识别和自然语言处理等许多领域取得了成功。然而，由于神经网络在自动驾驶汽车、机器人、计算机安全、刑事司法和医疗诊断等安全关键和社会敏感领域越来越多地采用，迫切需要开发能够为以下方面提供保证的验证技术：神经网络应用的可靠性和安全性。形式验证技术可以提供正确性的保证；然而，现有方法在分析具有大量神经元和复杂模型结构的现实世界神经网络时并不有效。该项目制定了一个全面的研究议程，重点关注神经网络的整体形式验证框架，该框架将为开发可靠和安全的神经网络提供系统和原则性的方法。旨在使自动驾驶等主要机器学习应用受益，并为美国在软件工程和人工智能领域的领导地位做出贡献。研究成果正在通过开源软件包、顶级会议和期刊上的出版物、教学研讨会上的教程以及专门的 K-12 项目广泛传播，让年轻一代接触软件验证和机器学习研究的前沿。从事该项目的研究人员团队正在集成软件工程、自动验证和形式化方法等经典计算领域的方法，以解决神经网络应用的可靠性和安全性方面的独特研究挑战。具体研究方向包括1）新颖的符号定量分析技术，为建立最先进的神经网络模型的可靠性和安全性提供良好的结果； 2）一套有效的系统级优化，用于计算/内存高效的神经网络验证，具有足够的跨框架可移植性和高验证效率； 3）先进的神经架构设计和训练支持，用于探索和开发具有可验证鲁棒性的神经网络模型。该研究议程的成功旨在实现更完整、更高效的软件堆栈，以提高 NN 验证技术的可扩展性和 NN 应用的稳健性。该奖项反映了 NSF 的法定使命，并通过使用基金会的评估进行评估，被认为值得支持。智力价值和更广泛的影响审查标准。

项目成果

期刊论文数量（8）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

ZENO: A Type-based Optimization Framework for Zero Knowledge Neural Network Inference

DOI：
10.1145/3617232.3624852
发表时间：
2024-04
期刊：
Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1
影响因子：
0
作者：
Boyuan Feng;Zheng Wang;Yuke Wang;Shu Yang;Yufei Ding
通讯作者：
Boyuan Feng;Zheng Wang;Yuke Wang;Shu Yang;Yufei Ding

APNN-TC: Accelerating Arbitrary Precision Neural Networks on Ampere GPU Tensor Cores

DOI：
10.1145/3458817.3476157
发表时间：
2021-06
期刊：
SC21: International Conference for High Performance Computing, Networking, Storage and Analysis
影响因子：
0
作者：
Boyuan Feng;Yuke Wang;Tong Geng;Ang Li;Yufei Ding
通讯作者：
Boyuan Feng;Yuke Wang;Tong Geng;Ang Li;Yufei Ding

Faith: An Efficient Framework for Transformer Verification on GPUs

Faith：GPU 上 Transformer 验证的高效框架

DOI：
发表时间：
2022
期刊：
Proceedings of the 2022 USENIX Annual Technical Conference
影响因子：
0
作者：
Feng, Boyuan;Tang, Tianqi;Wang, Yuke;Chen, Zhaodong;Wang, Zheng;Yang, Shu;Xie, Yuan;Ding, Yufei
通讯作者：
Ding, Yufei

DOTA: detect and omit weak attentions for scalable transformer acceleration

DOI：
10.1145/3503222.3507738
发表时间：
2022-02
期刊：
Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems
影响因子：
0
作者：
Zheng Qu;L. Liu;Fengbin Tu;Zhaodong Chen;Yufei Ding;Yuan Xie
通讯作者：
Zheng Qu;L. Liu;Fengbin Tu;Zhaodong Chen;Yufei Ding;Yuan Xie

QGTC: accelerating quantized graph neural networks via GPU tensor core

DOI：
10.1145/3503221.3508408
发表时间：
2021-11
期刊：
Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming
影响因子：
0
作者：
Yuke Wang;Boyuan Feng;Yufei Ding
通讯作者：
Yuke Wang;Boyuan Feng;Yufei Ding