Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Compositional Neural Network Verification via Assume-Guarantee Reasoning
Authors: Hai Duong, David Shriver, ThanhVu Nguyen, Matthew Dwyer
NeurIPS 2025 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | An evaluation using 7 neural networks and a total of 140 property specifications demonstrates that Co Ve NN can verify nearly 7 times more problems than state-of-the-art verifiers. |
| Researcher Affiliation | Academia | Hai Duong George Mason University Fairfax, VA 22030 EMAIL David Shriver Carnegie Mellon University Pittsburgh, PA 15213 EMAIL Thanh Vu Nguyen George Mason University Fairfax, VA 22030 EMAIL Matthew B. Dwyer University of Virginia Charlottesville, VA 22904 EMAIL |
| Pseudocode | Yes | Alg. 1: Co Ve NN algorithm. input :Verifier V, DNN N, property ϕin ϕout, number of neurons P, scale factor F and rounds r output :unsat if the property is valid and unknown otherwise |
| Open Source Code | Yes | Co Ve NN is part of the Neural SAT verification project: https://github.com/dynaroars/neuralsat. |
| Open Datasets | Yes | An evaluation using 7 neural networks and a total of 140 property specifications demonstrates that Co Ve NN can verify nearly 7 times more problems than state-of-the-art verifiers. An evaluation using 7 neural networks and a total of 140 property specifications demonstrates that Co Ve NN can verify nearly 7 times more problems than state-of-the-art verifiers. Fig. 1 shows the memory-consumption of the two top performing verifiers in VNN-COMP 24: αβ-CROWN and Neural SAT, as they check 10 randomly generated local robustness properties of Res Net models trained on CIFAR10, with an increasing number of residual blocks in each model. |
| Dataset Splits | Yes | Fig. 1 shows the memory-consumption of the two top performing verifiers in VNN-COMP 24: αβ-CROWN and Neural SAT, as they check 10 randomly generated local robustness properties of Res Net models trained on CIFAR10, with an increasing number of residual blocks in each model. For Res Nets these are local robustness classification properties and for VAEs these are local reconstruction robustness properties (Apdx. A). Across the 140 combinations of networks and properties: 98 are known to be unsat (U), none of them are sat (S), and of the remaining 42 instances no verifier in our study was able to solve the problem (?). |
| Hardware Specification | Yes | Our experiments were run on a Linux machine with an AMD Ryzen Threadripper PRO 5975WX 32-Core, 128 GB RAM, and an NVIDIA Ge Force RTX 4090 GPU with 24 GB VRAM. |
| Software Dependencies | No | The paper mentions software like "Neural SAT verifier", "αβ-CROWN", "Py Torch", and "Pytorch Image Models (timm)" but does not provide specific version numbers for these software components. |
| Experiment Setup | Yes | Timeout for a single instance is set to 3600 seconds or the maximum number of rounds r is 4. ... Fig. 5 compares Co Ve NN s performance across different parameter configurations using Neural SAT as the underlying verifier. We explore variations in P (number of assumptions per round) and F (interpolation factor)... |