In This Story
The team’s NeuralSAT advanced the frontiers of trustworthy artificial intelligence, earning second place in a highly competitive field of international teams advancing the formal verification of AI systems.
NeuralSAT is an open-source verification tool developed by experts in Formal Methods/AI Hai Duong and ThanhVu Nguyen, both of George Mason University. It analyzes whether deep neural networks behave as intended, even under adversarial or uncertain conditions. The International Neural Network Verification Competition (VNN-COMP) gathers international research teams working on formal methods for AI safety—methods that are increasingly important as neural networks are deployed in autonomous systems, healthcare, finance, and other mission-critical systems.
"Our goal with NeuralSAT is to bring precision and robustness to AI systems,” said Nguyen, an associate professor in computer science, “especially as they are increasingly used in safety-critical settings."
Each year, the participating VNN-COMP tools are evaluated across a wide set of benchmarks that test scalability, correctness, and performance. The 2024 competition’s results were recently released.
"This year’s benchmarks pushed the boundaries of what verification tools could handle—both in terms of scale and complexity," said Duong, a third-year computer science PhD candidate. "We’re proud that NeuralSAT remained among the top performers, showing strong results across both safety and robustness categories."
NeuralSAT was developed in close collaboration with researchers across multiple institutions, including the University of Virginia’s Matt Dwyer. It builds on recent advances in symbolic reasoning, SAT solving, and abstraction. In its inaugural appearance at VNN-COMP in 2023, NeuralSAT placed fourth overall and received the New Participant Award. In addition to competitions, the tool has been featured at top-tier conferences such as the Symposium on the Foundations of Software Engineering and Computer Aided Verification.
Nguyen, who serves as an organizer and program chair of VNN-COMP 2025, emphasized the significance of the competition in shaping the research landscape.
"The field of neural network verification is rapidly maturing, and VNN-COMP has become the standard for evaluating progress," he said. "Many research papers now compare their tools against VNN-COMP results or use its benchmarks for evaluation. It's exciting to be involved in shaping the competition while also contributing a tool that pushes the research frontier."
David Rosenblum, chair of the Department of Computer Science, was thrilled with ROARS Lab’s achievement. "ThanhVu Nguyen is an established research leader on problems at the intersection of formal methods and deep learning. This team’s outstanding achievement has demonstrated the great potential impact of verification technologies for AI safety," he said.
The long-term goal of NeuralSAT, supported in part by Nguyen’s NSF CAREER Award and Amazon Research Award, is to remain at the forefront of AI verification research while evolving into a practical, scalable, and potentially commercial-grade solution for industry use.
George Mason is advancing a bold vision for the future of safe and robust AI and is further expanding its leadership with the launch of Virginia's first master’s program in artificial intelligence in fall 2025. This program reflects the university’s deep commitment to cutting-edge education and the development of trustworthy, high-impact AI technologies.