SHF: Small: SMT Reasoning for Tensors and Data

Sri International, Menlo Park CA

Investigators

Abstract

Our society is increasingly more dependent on computing systems that include components built from tensor models and rely on them to make critical decisions, like for example airplane controllers built from MATLAB code, or neural networks in self-driving cars. The surge in size and complexity of these systems has made their development, testing, and verification extremely costly and time consuming. To address this challenge, this project develops novel automated reasoning techniques that can support the development cycle of tensor-based systems, at scale, from design to verification, with the potential to increase both performance and reliability of the resulting systems, while broadening the applicability of symbolic reasoning to new domains. The goal of the project is to develop new automated reasoning and symbolic optimization techniques needed for reasoning about complex systems that rely on tensors and data as the underlying model of computation. The current generation of automated reasoning techniques focuses solely on scalar domains, and they are inadequate for reasoning about large tensor systems with data. This project develops new reasoning techniques, in the context of satisfiability modulo theories, that can operate at the level of tensors. The key novel ideas explored in this project include high-level modeling and representation of tensor models, data-aware reasoning and optimization techniques for both linear and non-linear tensor models, and combination of numerical optimization and symbolic reasoning techniques. The project integrates the new techniques into machine learning and software analysis tools and evaluates their effectiveness. 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.