Nguyen to receive NSF CAREER Award for NeuralSAT: A constraint-solving framework for verifying deep neural networks

Thanhvu Nguyen, Assistant Professor, Computer Science, is set to receive funding for the project: "CAREER: NeuralSAT: A Constraint-Solving Framework for Verifying Deep Neural Networks." 

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 Machine Learning by developing effective techniques to verify DNNs, allowing Artificial Intelligence/Machine Learning 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. 

Nguyen will receive $510,509 from the National Science Foundation for this award. Funding will begin in July 2023 and will end in late June 2028. 

###

About George Mason University

George Mason University is Virginia's largest public research university. Located near Washington, D.C., Mason enrolls 38,000 students from 130 countries and all 50 states. Mason has grown rapidly over the last half-century and is recognized for its innovation and entrepreneurship, remarkable diversity and commitment to accessibility. Learn more at http://www.gmu.edu.

END