Machine Learning and Solvers: The Next Frontier

软件安全和可靠性仍然是我们今天面临的最重要和最具挑战性的技术问题之一。因此，对可扩展且有效的测试、分析和验证(TAV)方法的需求一直存在。此外，随着机器学习(ML)系统继续给工程和工业的许多领域带来革命性的变化，其可靠性和安全性已成为一个严重的问题。黑客发现了对ML系统发动对抗性攻击的新方法。幸运的是，为通用软件开发的成功的TAV方法也可以适用于解决ML系统的可靠性和安全性问题。在许多可扩展和有效的TAV方法中，一个关键组件是逻辑(又名、SAT或SMT)求解器，它是自动求解从程序分析中获得的数学约束的系统。有趣的是，今天领先的逻辑解算器天生就依赖ML来提高性能，这是我在过去6年中开创的一条研究路线。相反，提高ML系统可靠性和安全性的一种有效方法是通过逻辑制导的ML系统，这是我最近开发的另一项研究。这笔发现基金将资助一项前沿的长期研究计划，其主要方向如下：逻辑求解器的ML：首先，我们建议开发基于ML的新方法，旨在使求解器算法更加高效。逻辑解算器可以被视为旨在针对给定输入公式最佳地初始化、选择和排序证明规则的交互和动态启发式的集合。这些优化问题最好使用在线ML方法来解决。我建议开发新的基于深度神经网络(DNN)和深度强化学习(DRL)的在线和动态方法来初始化、排序和选择强大的求解器内的证明规则。我们将为SMT和扩展分辨率解算器开发这些方法。ML的逻辑解算器：其次，我们建议开发一套基于逻辑的ML算法，称为逻辑制导机器学习(LGML)，它使用逻辑解算器来验证、纠正和相反地训练ML模型。关键的洞察力是将求解器和ML模型组合在一个校正反馈循环中，以便验证ML模型，并根据需要通过‘最佳’反例对它们进行重新训练。拟议中的研究将产生深远的基础性科学、技术和商业影响。这些结果不仅将使改进的基于ML的求解器设计(与密码分析和软件和ML系统的TAV方法共同开发)成为可能，而且还将使逻辑制导的ML系统对对手攻击更可靠和更健壮。此外，该计划旨在更深入地了解求解器为什么工作，从而为更科学地进行求解器设计铺平道路。最重要的是，该计划旨在培训至少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.