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.

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

TC-GNN: Bridging Sparse GNN Computation and Dense Tensor Cores on GPUs

DOI：
发表时间：
2021-12
期刊：
影响因子：
0
作者：
Yuke Wang;Boyuan Feng;Zheng Wang;Guyue Huang;Yufei Ding
通讯作者：
Yuke Wang;Boyuan Feng;Zheng Wang;Guyue Huang;Yufei Ding

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