Machine Learning and Solvers: The Next Frontier

软件安全性和可靠性仍然是我们今天面临的最重要和最具挑战性的技术问题之一。因此，对可伸缩且有效的测试、分析和验证（TAV）方法的需求一直存在。此外，随着机器学习（ML）系统不断改变工程和工业的许多领域，它们的可靠性和安全性已经成为一个严重的问题。黑客已经找到了针对机器学习系统发起对抗性攻击的新方法。幸运的是，为一般软件开发的成功的TAV方法也可以用于解决机器学习系统的可靠性和安全性问题。在许多可扩展和有效的TAV方法中，一个关键的组成部分是逻辑（即SAT或SMT）求解器，即自动求解从程序分析中获得的数学约束的系统。有趣的是，当今领先的逻辑求解器本质上依赖于ML来提高性能，这是我在过去6年里率先开展的一系列研究。相反，提高机器学习系统可靠性和安全性的一个有效方法是通过逻辑引导的机器学习系统，这是我最近正在开发的另一个研究方向。这项发现基金将资助一项前沿的长期研究计划，该计划具有以下广泛的方向：逻辑求解器的ML：首先，我们建议开发基于ML的新颖方法，旨在使求解器算法更加高效。逻辑求解器可以看作是一组相互作用的动态启发式算法，其目的是为给定的输入公式最佳地初始化、选择和序列证明规则。这些优化问题最好使用在线ML方法来解决。我建议开发新的基于在线和动态方法的深度神经网络（dnn）和深度强化学习（DRL）来初始化、排序和选择求解器内部的强大证明规则。我们将为SMT和扩展分辨率求解器开发这些方法。机器学习的逻辑求解器：其次，我们建议开发一套基于逻辑的机器学习算法，称为逻辑引导机器学习（LGML），它使用求解器来验证、纠正和对抗性训练机器学习模型。关键的见解是将求解器和ML模型结合在一个纠正反馈循环中，以验证ML模型，并在必要时通过“最优”反例重新训练它们。拟议的研究将产生深刻的基础科学、技术和商业影响。这些结果不仅可以改进基于机器学习的求解器设计（与软件和机器学习系统的密码分析和TAV方法共同开发），还可以使逻辑引导的机器学习系统更可靠，更强大，抵御对抗性攻击。此外，该计划旨在加深对求解器工作原理的基础理解，从而为更科学的求解器设计方法铺平道路。最重要的是，该项目旨在培训至少6名HQP，包括逻辑解算器、ML及其组合，旨在开发安全可靠的软件和ML系统。

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.