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

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.