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，并可能在高性能计算和硬件加速中进行其他优化任务。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.