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

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

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.