Collaborative Research: FMitF: Track-1: Correctness at Both Ends: Rigorous ML Meets Efficient Sparse Implementations

协作研究:FMitF:Track-1:两端的正确性:严格的 ML 满足高效的稀疏实现

基本信息

  • 批准号:
    2124205
  • 负责人:
  • 金额:
    $ 30万
  • 依托单位:
  • 依托单位国家:
    美国
  • 项目类别:
    Standard Grant
  • 财政年份:
    2021
  • 资助国家:
    美国
  • 起止时间:
    2021-10-01 至 2024-09-30
  • 项目状态:
    已结题

项目摘要

This project called CBE (correctness at both ends) addresses the growing concern that on one hand systems based on deep neural networks (DNNs) are playing an increasing role in critical applications, but on the other hand these systems can do significant damage if they harbor software defects. These defects go beyond the familiar logic bugs, including also semantic bugs such as misclassifying medical images. Traditionally, attempts to make DNNs more efficient by sparsifying them have often resulted in increased levels of semantic bugs. The project's novelties are its integrated approach to sparsify networks while preserving semantic correctness as well as helping eliminate logic bugs. The project's impacts are in making DNNs energy-efficient, permitting their deployment in edge devices, while also helping eliminate their defects.CBE employs a knowledge-distillation paradigm wherein a sparsified network is trained by imitating the parent network's classification behavior. Sparsification steps that meet higher level semantic objectives may unfortunately lead to an inefficient sparse implementation -- especially in newly introduced GPUs for which hand-tuned sparse libraries are unavailable. The CBE project supports the developers of such libraries by also providing low-level implementation verification tools. The investigators are domain experts in DNN semantics and optimization, and also in softwareverification. Their three-year collaborative research project is taking case studies of DNNs from critical areas such as medical imaging, and showing how DNNs can be sparsifed to ensure correctness at both ends. The main impact of this project is to develop prototype software tools that can help spur further research and technology development. Another major impact is the training of students who will fill critical roles in the fast-growing area of deployable machine-learning systems where talent shortage can cripple the nation's economy and security.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.
这个名为CBE(两端正确性)的项目解决了人们日益关注的问题,即一方面基于深度神经网络(DNN)的系统在关键应用中发挥着越来越大的作用,但另一方面,如果这些系统存在软件缺陷,它们可能会造成重大损害。这些缺陷超出了常见的逻辑错误,还包括语义错误,如错误分类医学图像。 传统上,通过稀疏化DNN来提高DNN效率的尝试通常会导致语义错误的增加。 该项目的新颖之处在于它的集成方法,可以在保持语义正确性的同时使网络稀疏化,并帮助消除逻辑错误。 该项目的影响是使DNN节能,允许其在边缘设备中部署,同时也有助于消除其缺陷。CBE采用知识蒸馏范式,其中通过模仿父网络的分类行为来训练稀疏网络。满足更高层次语义目标的稀疏化步骤可能会导致低效的稀疏实现-特别是在新引入的GPU中,手动调整的稀疏库不可用。CBE项目通过提供低级实现验证工具来支持这些库的开发人员。调查人员是DNN语义和优化领域的专家,也是软件验证领域的专家。他们为期三年的合作研究项目正在从医学成像等关键领域进行DNN的案例研究,并展示如何稀疏DNN以确保两端的正确性。 该项目的主要影响是开发原型软件工具,有助于推动进一步的研究和技术开发。另一个重要影响是培养学生,他们将在快速增长的可部署机器学习系统领域担任关键角色,人才短缺可能会削弱国家的经济和安全。该奖项反映了NSF的法定使命,并通过使用基金会的智力价值和更广泛的影响审查标准进行评估而被认为值得支持。

项目成果

期刊论文数量(1)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
An HPC Practitioner’s Workbench for Formal Refinement Checking
用于形式化细化检查的 HPC 从业者工作台
  • DOI:
  • 发表时间:
    2023
  • 期刊:
  • 影响因子:
    0
  • 作者:
    Benavides, J.;Baugh, J.;Gopalakrishnan, G.
  • 通讯作者:
    Gopalakrishnan, G.
{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ monograph.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ patent.updateTime }}

John Baugh其他文献

STRETCHED INDUCED B-TYPE NATRIURETIC PEPTIDE ALTERS HUMAN CARDIAC FIBROBLAST RESPONSE TO TRANSFORMING GROWTH FACTOR BETA AND MAY BE PROTECTIVE AGAINST MYOCARDIAL FIBROSIS
  • DOI:
    10.1016/s0735-1097(11)60363-x
  • 发表时间:
    2011-04-05
  • 期刊:
  • 影响因子:
  • 作者:
    Dermot Phelan;Chris Watson;Mark Ledwidge;John Baugh;Ken McDonald
  • 通讯作者:
    Ken McDonald
Black English: A seminar
Automatic modelling and verification of span class="small-caps"Autosar/span architectures
自动建模和验证“Autosar”架构的跨度类
  • DOI:
    10.1016/j.jss.2023.111675
  • 发表时间:
    2023-07-01
  • 期刊:
  • 影响因子:
    4.100
  • 作者:
    Miaomiao Zhang;Yu Teng;Hui Kong;John Baugh;Yu Su;Junri Mi;Bowen Du
  • 通讯作者:
    Bowen Du

John Baugh的其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

{{ truncateString('John Baugh', 18)}}的其他基金

Reusable Engineering Software Components: Interface Issues
可重用工程软件组件:接口问题
  • 批准号:
    9201697
  • 财政年份:
    1992
  • 资助金额:
    $ 30万
  • 项目类别:
    Continuing Grant
Reliability of Real-Time Engineering Software
实时工程软件的可靠性
  • 批准号:
    9201687
  • 财政年份:
    1992
  • 资助金额:
    $ 30万
  • 项目类别:
    Continuing Grant
Linguistic Diversity, Literacy, and Related Consequences forHuman Health and Environmetal Change
语言多样性、读写能力以及对人类健康和环境变化的相关影响
  • 批准号:
    9196039
  • 财政年份:
    1990
  • 资助金额:
    $ 30万
  • 项目类别:
    Standard Grant
Linguistic Diversity, Literacy, and Related Consequences forHuman Health and Environmetal Change
语言多样性、读写能力以及对人类健康和环境变化的相关影响
  • 批准号:
    8915933
  • 财政年份:
    1990
  • 资助金额:
    $ 30万
  • 项目类别:
    Standard Grant

相似国自然基金

Research on Quantum Field Theory without a Lagrangian Description
  • 批准号:
    24ZR1403900
  • 批准年份:
    2024
  • 资助金额:
    0.0 万元
  • 项目类别:
    省市级项目
Cell Research
  • 批准号:
    31224802
  • 批准年份:
    2012
  • 资助金额:
    24.0 万元
  • 项目类别:
    专项基金项目
Cell Research
  • 批准号:
    31024804
  • 批准年份:
    2010
  • 资助金额:
    24.0 万元
  • 项目类别:
    专项基金项目
Cell Research (细胞研究)
  • 批准号:
    30824808
  • 批准年份:
    2008
  • 资助金额:
    24.0 万元
  • 项目类别:
    专项基金项目
Research on the Rapid Growth Mechanism of KDP Crystal
  • 批准号:
    10774081
  • 批准年份:
    2007
  • 资助金额:
    45.0 万元
  • 项目类别:
    面上项目

相似海外基金

FMitF: Collaborative Research: RedLeaf: Verified Operating Systems in Rust
FMITF:协作研究:RedLeaf:经过验证的 Rust 操作系统
  • 批准号:
    2313411
  • 财政年份:
    2023
  • 资助金额:
    $ 30万
  • 项目类别:
    Standard Grant
Collaborative Research: FMitF: Track I: Game Theoretic Updates for Network and Cloud Functions
合作研究:FMitF:第一轨:网络和云功能的博弈论更新
  • 批准号:
    2318970
  • 财政年份:
    2023
  • 资助金额:
    $ 30万
  • 项目类别:
    Standard Grant
Collaborative Research: FMitF: Track I: Knitting Semantics
合作研究:FMitF:第一轨:针织语义
  • 批准号:
    2319182
  • 财政年份:
    2023
  • 资助金额:
    $ 30万
  • 项目类别:
    Standard Grant
Collaborative Research: FMitF: Track I: Towards Verified Robustness and Safety in Power System-Informed Neural Networks
合作研究:FMitF:第一轨:实现电力系统通知神经网络的鲁棒性和安全性验证
  • 批准号:
    2319242
  • 财政年份:
    2023
  • 资助金额:
    $ 30万
  • 项目类别:
    Standard Grant
Collaborative Research: FMitF: Track I: DeepSmith: Scheduling with Quality Guarantees for Efficient DNN Model Execution
合作研究:FMitF:第一轨:DeepSmith:为高效 DNN 模型执行提供质量保证的调度
  • 批准号:
    2349461
  • 财政年份:
    2023
  • 资助金额:
    $ 30万
  • 项目类别:
    Standard Grant
Collaborative Research: FMitF: Track I: Towards Verified Robustness and Safety in Power System-Informed Neural Networks
合作研究:FMitF:第一轨:实现电力系统通知神经网络的鲁棒性和安全性验证
  • 批准号:
    2319243
  • 财政年份:
    2023
  • 资助金额:
    $ 30万
  • 项目类别:
    Standard Grant
Collaborative Research: FMitF: Track I: Synthesis and Verification of In-Memory Computing Systems using Formal Methods
合作研究:FMitF:第一轨:使用形式方法合成和验证内存计算系统
  • 批准号:
    2319400
  • 财政年份:
    2023
  • 资助金额:
    $ 30万
  • 项目类别:
    Standard Grant
Collaborative Research: FMitF: Track I: Synthesis and Verification of In-Memory Computing Systems using Formal Methods
合作研究:FMitF:第一轨:使用形式方法合成和验证内存计算系统
  • 批准号:
    2319399
  • 财政年份:
    2023
  • 资助金额:
    $ 30万
  • 项目类别:
    Standard Grant
Collaborative Research: FMitF: Track I: Simplifying End-to-End Verification of High-Performance Distributed Systems
合作研究:FMitF:第一轨:简化高性能分布式系统的端到端验证
  • 批准号:
    2318954
  • 财政年份:
    2023
  • 资助金额:
    $ 30万
  • 项目类别:
    Standard Grant
Collaborative Research: FMitF: Track I: The Phlox framework for verifying a high-performance distributed database
合作研究:FMitF:第一轨:用于验证高性能分布式数据库的 Phlox 框架
  • 批准号:
    2319167
  • 财政年份:
    2023
  • 资助金额:
    $ 30万
  • 项目类别:
    Standard Grant
{{ showInfoDetail.title }}

作者:{{ showInfoDetail.author }}

知道了