Machine Learning and Solvers: The Next Frontier

点击翻译按钮获取中文摘要

Software security and reliability remain one of the most important and challenging technological problems we face today. As a consequence, there is an ever-present demand for scalable and effective testing, analysis, and verification (TAV) methods. Further, as machine learning (ML) systems continue to revolutionize many areas of engineering and industry, their reliability and security have become a grave concern. Hackers have found novel ways of launching adversarial attacks against ML systems. Fortunately, successful TAV methods developed for general software can also be adapted to address the reliability and security problems of ML systems. A critical component in many scalable and effective TAV methods is a logic (aka, SAT or SMT) solver, systems that automatically solve mathematical constraints obtained from analysis of programs. Interestingly, today's leading logic solvers inherently rely on ML for improved performance, a line of research that I pioneered over the last 6 years. Conversely, one powerful way of improving the reliability and security of ML systems is via logic-guided ML systems, another line of research I have recently been developing. This Discovery Grant will fund a bleeding-edge long-term research program with the following broad directions: ML for Logic Solvers: First, we propose to develop novel ML-based methods aimed at making solver algorithms even more efficient. A logic solver can be viewed as a collection of interacting and dynamic heuristics that aim to optimally initialize, select, and sequence proof rules for a given input formula. These optimization problems are best solved using online ML methods. I propose to develop novel deep neural networks (DNNs) and deep reinforcement learning (DRL) based online and dynamic methods to initialize, sequence, and select powerful proof rules inside solvers. We will develop these methods for SMT and extended resolution solvers. Logic Solvers for ML: Second, we propose to develop a set of logic-based ML algorithms, called Logic Guided Machine Learning (LGML), that use  solvers to verify, correct, and adversarially train ML models. The key insight is to combine solvers and ML models in a corrective feedback loop in order verify the ML models, and retrain them as necessary via 'optimal' counterexamples. The proposed research will have deep fundamental scientific, technical, and commercial impact. These results will not only enable improved ML-based solver design (co-developed with cryptanalysis and TAV methods for software and ML systems), but also logic-guided ML systems that are more reliable and robust against adversarial attacks. Further, the program aims at a deeper foundational understanding of why solver work at all, and thus paving the way for a more scientific approach to solver design. Most importantly, the program aims to train at least 6 HQP in logic solvers, ML, and combinations thereof, aimed at secure and reliable software and ML systems.