NeuralSAT: A DPLL(T) Framework for Verifying Deep Neural Networks

NeuralSAT is a high-performance verification tool for deep neural networks (DNNs). It integrates the DPLL(T) approach commonly used in SMT solving with a theory solver specialized for DNN reasoning. NeuralSAT exploits multicores and GPU for efficiency and can scale to networks with millions of parameters. It supports a wide range of neural networks and activation functions.

NEWS

• NeuralSAT is ranked 2nd overall at VNN-COMP'25
• NeuralSAT is ranked 2nd overall at VNN-COMP'24
  • Initially VNN-COMP’s script incorrectly parsed NeuralSAT’s (and another tool’s) results, and ranked it last. After fixing the issue, NeuralSAT’s results were correctly parsed and NeuralSAT was officially placed 2nd, behind ABCrown and above PyRAT. The updated VNN-COMP’24 report mentions the issue, presents the corrected rankings (see Table B.1), and includes detailed results and graphs in Appendix B.
• NeuralSAT is given the New Participation Award at VNN-COMP'23
• NeuralSAT is ranked 4th in VNN-COMP'23. This was our first participation and we look forward to next time.
  • Note: The current version of NeuralSAT adds significant improvements and fixed the implementation bugs we had during VNN-COMP'23 that produce unsound results (hence 4th place ranking).

PUBLICATIONS

• CVPR'26 research paper on verifying AI-based computer vision systems.
• FSE’26 paper on formalizing and verifying structural robustness properties of AI systems.
• NeurIPS’25 paper on generating and checking DNN verification proofs.
• NeurIPS’25 paper on compositional DNN verification (Spotlight).
• SAIV'25 competition paper on NeuralSAT.
• CAV’25 paper on NeuralSAT verification tool.
• FSE'24 paper on new optimizations developed for the NeuralSAT.
• Arxiv'24 technical report on NeuralSAT design and methodology.

INSTALLATION & USAGE

• see INSTALL.md

FEATURES

• fully automatic, ease of use and requires no tuning (i.e., no expert knowledge required)

  • NeuralSAT requires no parameter tuning (a huge engineering effort that researchers often don't pay attention to)! In fact, you can just apply NeuralSAT as is to check your networks and desired properties. The user does not have to do any configuration or tweaking. It just works!
    • But if you're an expert (or want to break the tool), you are welcome to tweak its internal settings.
  • This is what makes NeuralSAT different from other DNN verifiers (e.g., AB-Crown), which require lots of tuning to work well.

• standard input and output formats

  • input: onnx for neural networks and vnnlib for specifications
  • output: unsat for proved property, sat for disproved property (accompanied with a counterexample), and unknown or timeout for property that cannot be proved.

• versatile: support multiple types of neural types of networks and activation functions

  • layers (can be mixture of different types): fully connected (fc), convolutional (cnn), residual networks (resnet), batch normalization (bn)
  • activation functions: ReLU, sigmoid, tanh, power

• well-tested

  • NeuralSAT has been tested on a wide-range of benchmarks (e.g., ACAS XU, MNIST, CIFAR).

• fast and among the most scalable verification tools currently

  • NeuralSAT exploits and uses multhreads (i.e., multicore processing/CPUS) and GPUs available on your system to improve its performance.

• active development and frequent updates

  • If NeuralSAT does not support your problem, feel free to contact us (e.g., by openning a new Github issue). We will do our best to help.
  • We will release new, stable versions about 3-4 times a year

OVERVIEW

NeuralSAT takes as input the formula $\alpha$ representing the DNN N (with non-linear ReLU activation) and the formulae $\phi_{in}\Rightarrow \phi_{out}$ representing the property $\phi$ to be proved. Internally, it checks the satisfiability of the formula: $\alpha \land \phi_{in} \land \overline{\phi_{out}}$. NeuralSAT returns UNSAT if the formula is unsatisfiable, indicating N satisfies $\phi$, and SAT if the formula is satisfiable, indicating the N does not satisfy $\phi$.

NeuralSAT uses a DPLL(T)-based algorithm to check unsatisfiability. It applies DPLL/CDCL to assign values to boolean variables and checks for conflicts the assignment has with the real-valued constraints of the DNN and the property of interest. If conflicts arise, NeuralSAT determines the assignment decisions causing the conflicts and learns clauses to avoid those decisions in the future. NeuralSAT repeats these decisions and checking steps until it finds a full assignment for all boolean variables, in which it returns SAT, or until it no longer can decide, in which it returns UNSAT.

PERFORMANCES

VNN-COMP is an annual competition on neural network verification that has been held annually to facilitate the fair and objective comparison of SOTA neural network verification tools. The goal of VNN-COMP is to encourage the standardization of tool interfaces, and bring together the neural network verification community. To this end, VNN-COMP uses standardized formats for networks (ONNX) and specification (VNN-LIB), and evaluates tools using a common set of benchmarks (collected from various sources including previous papers and contributions from the community) on a common platform (AWS instances).

The cactus plot shows NeuralSAT and other tools performance on Regular Track benchmarks from VNN-COMP'25.

PEOPLE

• Hai Duong (GMU, main developer)
• Jahnvi (GMU)
• Thanh Le (NII)
• Lam Nguyen (HUST)
• Linhan Li (GMU)
• Nguyen Ho (GMU)
• ThanhVu Nguyen (GMU)
• Matthew Dwyer (UVA)

ACKNOWLEDGEMENTS

The NeuralSAT research is partially supported by grants from NSF (1900676, 2019239, 2129824, 2217071, 2501059, 2422036, 2319131, 2238133, 2200621) and an Amazon Research Award and an NVIDIA Academic Grant.