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.