权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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）在许多领域都取得了成功，包括计算机视觉、语音识别和自然语言处理。然而，由于越来越多地采用神经网络在安全关键和社会敏感的领域，如自动驾驶汽车，机器人，计算机安全，刑事司法和医疗诊断，有一个迫切需要开发验证技术，可以提供保证的可靠性和安全的神经网络应用。形式验证技术可以提供正确性的保证，然而，现有的方法是不有效的，在分析现实世界的神经网络与大量的神经元和复杂的模型结构。该项目设定了一个全面的研究议程，重点是NN的整体形式验证框架，为开发可靠和安全的NN提供系统和原则性的方法。它旨在使自动驾驶等主要机器学习应用受益，并为美国在软件工程和人工智能方面的领导地位做出贡献。研究结果正在通过开源软件包、顶级会议和期刊上的出版物、教学研讨会上的教程以及专门的K-12项目广泛传播，这些项目旨在让年轻一代了解软件验证和机器学习研究的前沿。该项目的研究团队正在整合经典计算领域的方法，如软件工程，自动验证和形式化方法，以解决NN应用程序的可靠性和安全性方面的独特研究挑战。具体的研究方向包括：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

MGG: Accelerating Graph Neural Networks with Fine-Grained Intra-Kernel Communication-Computation Pipelining on Multi-GPU Platforms

DOI：
发表时间：
2022-09
期刊：
影响因子：
0
作者：
Yuke Wang;Boyuan Feng;Zheng Wang;Tong Geng;K. Barker;Ang Li;Yufei Ding
通讯作者：
Yuke Wang;Boyuan Feng;Zheng Wang;Tong Geng;K. Barker;Ang Li;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

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