Collaborative Research: FMitF: Track I: DeepSmith: Scheduling with Quality Guarantees for Efficient DNN Model Execution

最近，深度学习的空前增长导致了计算机视觉、语言翻译、自动驾驶和金融欺诈检测等多种尖端技术的快速发展。然而，基于深度神经网络(DNN)的现实深度学习模型通常具有很高的计算和存储需求，这极大地限制了它们在资源受限环境下的训练和部署。拟议的研究旨在采用正式方法显著提高DNN执行的性能，同时提供有用的质量保证，使深度学习能够得到更广泛的部署。该项目将制作开源软件和会议教程，以促进多学科社区中的技术转让和富有成效的产业界与学术界的互动。该项目提出了DeepSmith，一个基于可满足性模理论(SMT)的高效DNN模型执行调度框架。该项目的核心包括一种新的资源受限调度公式和组合理论，该公式使用SMT来精确编码丰富的性能和资源约束集，以及一系列高级的特定于领域的SMT求解算法。此外，还将开发一种特定领域的编程语言，以便能够使用SMT快速开发准确的调度和高度的代码可重用性。由此产生的DeepSmith框架将允许在DNN执行中高效地探索和部署SMT，并可能在高性能计算和硬件加速中执行其他优化任务。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

The recent unprecedented growth of deep learning has led to rapid advances in a multitude of cutting-edge technologies such as computer vision, language translation, autonomous driving, and financial-fraud detection. However, realistic deep-learning models based on deep neural networks (DNNs) typically have substantial computational and memory requirements, which greatly limit their training and deployment in resource-constrained settings. The proposed research aims to employ formal methods to significantly improve the performance of DNN execution while providing useful quality guarantees that will enable a wider deployment of deep learning. This project will produce open-source software and conference tutorials to facilitate technology transfer and fruitful industry-academia interactions in a multidisciplinary community. This project proposes DeepSmith, a scheduling framework for efficient DNN model execution based on satisfiability modulo theories (SMT). The core of the proposed project includes a novel resource-constrained scheduling formulation with combined theories using SMT to exactly encode a rich set of performance and resource constraints, and a collection of advanced domain-specific SMT-solving algorithms. Moreover, a domain-specific programming language will be developed to enable the rapid development of exact scheduling using SMT and high code reusability. The resulting DeepSmith framework will allow productive exploration and deployment of SMT in DNN execution and potentially other optimization tasks in high-performance computing and hardware acceleration.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.