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

这个名为CBE(两端正确性)的项目解决了人们日益关注的问题，即一方面基于深度神经网络(DNN)的系统在关键应用中发挥着越来越重要的作用，但另一方面，如果这些系统存在软件缺陷，可能会造成重大破坏。这些缺陷超越了常见的逻辑错误，还包括错误分类医学图像等语义错误。传统上，试图通过稀疏DNN来提高DNN的效率，往往会导致语义错误水平的增加。该项目的新奇之处在于它集成了一种方法来稀疏网络，同时保持语义正确，并帮助消除逻辑错误。该项目的影响在于使DNN变得能效，允许它们部署在边缘设备中，同时也有助于消除它们的缺陷。CBE采用了一种知识蒸馏范式，其中稀疏网络是通过模仿父网络的分类行为来训练的。不幸的是，满足更高级别语义目标的精简步骤可能会导致低效率的稀疏实现--特别是在新引入的GPU中，对于这些新引入的GPU，手动调优的稀疏库不可用。CBE项目还通过提供低级实现验证工具来支持这类库的开发人员。研究人员是DNN语义和优化领域的专家，也是软件验证方面的专家。他们为期三年的合作研究项目正在从关键领域(如医学成像)获取DNN的案例研究，并展示如何稀疏DNN以确保两端的正确性。该项目的主要影响是开发有助于推动进一步研究和技术开发的原型软件工具。另一个主要影响是培训学生，他们将在快速增长的可部署机器学习系统领域担任关键角色，在该领域，人才短缺可能会削弱国家经济和安全。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.