CAREER: NeuralSAT: A Constraint-Solving Framework for Verifying Deep Neural Networks

深度神经网络（dnn）已经成为解决现实世界问题的有效方法。然而，就像传统软件一样，深度神经网络也会有“漏洞”并受到攻击。这自然提出了dnn应该如何测试、验证并最终验证以满足相关鲁棒性和安全性标准的要求的问题。为了解决这个问题，研究人员开发了强大的形式化方法和工具来验证深度神经网络。然而，尽管最近取得了许多进展，现有的方法和工具在实现良好的精度和可扩展性方面仍然存在挑战。此外，它们可能产生不可靠的结果，并且不适用于图神经网络（gnn）等dnn。该项目旨在解决这些挑战。该项目的新颖之处在于将学习和抽象能力集成到现代约束求解器中，用于精确和可扩展的深度神经网络验证，对深度神经网络验证器进行压力测试并验证其结果，并通过其他深度神经网络方法的透镜处理gnn。该项目的影响是开发新的理论，先进的方法和实用工具，以确保深度神经网络系统的准确性和质量。该项目有四个技术研究组成部分。第一部分开发了NeuralSAT，这是一个dnn的约束求解器，它结合了现代SAT求解的冲突驱动子句学习能力和SMT求解中基于抽象的理论求解器。第二个组件通过开发非凸抽象和利用现代SAT求解器中的启发式和优化，使NeuralSAT在规模上更加精确和高效。第三个组件使用子句学习和变形测试来帮助开发人员在生产期间发现DNN验证器中的错误，并在部署期间验证其结果。第四部分通过将GNN简化为前馈神经网络（FNN）来探索GNN，这是一个强大的深度学习模型，但现有的正式技术和工具很少，这允许将FNN分析仪应用于GNN。该项目将通过提高嵌入深度神经网络的系统的可靠性来造福社会。该研究通过开发有效的技术来验证dnn，从而为ML做出贡献，使AI/ML研究人员和用户能够改进他们的dnn并充满信心地部署它们。这项研究支持了研究生和本科生的研究人员，并为弗吉尼亚州北部威廉王子县的K-12学生提供了推广活动。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Deep Neural Networks (DNNs) have emerged as an effective approach to tackling real-world problems. However, just like traditional software, DNNs can have "bugs" and be attacked. This naturally raises the question of how DNNs should be tested, validated, and ultimately verified to meet the requirements of relevant robustness and safety standards. To address this question, researchers have developed powerful formal methods and tools to verify DNNs. However, despite many recent advances, existing approaches and tools still have challenges in achieving good precision and scalability. Moreover, they could produce unsound results and do not apply to DNNs such as Graph Neural Networks (GNNs). This project aims to address these challenges. The project's novelties are the integration of learning and abstraction ability in modern constraint solvers for accurate and scalable DNN verification, stress-testing DNN verifiers and certifying their results, and tackling GNNs through the lenses of other DNN approaches. The project's impacts are the development of new theories, advanced methods, and practical tools to ensure the accuracy and quality of DNN systems.The project has four technical research components. The first component develops NeuralSAT, a constraint-solver for DNNs that combines the conflict-driven clause learning ability of modern SAT solving and abstraction-based theory solver in SMT solving. The second component makes NeuralSAT more precise and efficient at scale by developing non-convex abstractions and leveraging heuristics and optimizations in modern SAT solvers. The third component uses clause learning and metamorphic testing to help developers find bugs in their DNN verifiers during production and certify their results during deployment. The fourth component explores GNNs, a powerful model in deep learning but with few existing formal techniques and tools by reducing GNN to Feed-forward Neural Network (FNN), which allows for the applications of FNN analyzers to GNNs. The project will benefit society by improving the reliability of systems embedding DNNs. The research contributes to ML by developing effective techniques to verify DNNs, allowing AI/ML researchers and users to improve their DNNs and deploy them with confidence. The research is supporting graduate and undergraduate student researchers and outreach activities for K-12 students in Prince William county of Northern Virginia.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.