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

George Mason University, Fairfax VA

Investigators

Abstract

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.