Research map / Large language models / AI and society
NN4SysBench: Characterizing Neural Network Verification for Computer Systems
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Introduces NN4SysBench, a neural network verification benchmark suite built from six computer-systems ML applications (learned index, bloom filter, cardinality estimation, congestion control, adaptive bitrate, learned scheduler), with vanilla and verifier-compatible versions, evaluated with αβ-CROWN and Marabou.
Problem
Neural network verifiers do not well support the unique characteristics of neural networks for computer systems (NN4Sys), such as many specification entries, monotonicity, probabilistic, and temporal specifications, and hierarchical models.
Approach
A benchmark suite of real NN4Sys applications with safety specifications in four categories, plus a compatible version built with dual-models (for monotonicity), chain-models (for k-step temporal properties), unit-counting (for probabilistic specs), and single-network approximations of RMIs so that existing verifiers can run them.
Key results
- Each benchmark is verified by at least one of αβ-CROWN or Marabou, and runtimes vary widely across benchmarks (from about 0.03 s to 180 s timeout).
- Marabou solves some small networks more efficiently while αβ-CROWN solves large networks Marabou cannot handle.
- Monotonicity specifications are harder to verify than reachability specifications, and safe specs are harder than unsafe specs for CongestCtrl and AdaptBitrate.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Increase model size | αβ-CROWN verification of CongestCtrl and AdaptBitrate · CongestCtrl and AdaptBitrate | verification runtime | Hurt |
| Use monotonicity specifications instead of reachability specifications | αβ-CROWN verification of CongestCtrl and AdaptBitrate · CongestCtrl and AdaptBitrate | verification runtime | Hurt |
| Use safe specifications instead of unsafe specifications | αβ-CROWN verification · CongestCtrl | verification runtime | Hurt |
| Use larger networks | αβ-CROWN and Marabou · NN4SysBench | verification runtime | Mixed |
Surprising findings
- Some compatible benchmarks are verified by neither verifier due to unsupported operators such as scatter in chain-models.
Limitations
- Compatible versions approximate the original NN4Sys (e.g., RMI as single network, probabilistic specs via unit counting, conservative), so results do not reflect original proposals' safety.
- Specifications are subjective and not claimed to be what NN4Sys must satisfy.
- Verifier comparison is not apples-to-apples since αβ-CROWN uses GPU and Marabou does not.
Experimental setup
Datasets: 150K-key lognormal dataset geolocation dataset for bloom filter database query trace data for cardinality estimation
Benchmarks: NN4SysBench
Metrics: end-to-end verification runtime (s) solved/unsolved status
Baselines: αβ-CROWN Marabou
Builds on: VNN-COMP benchmarks Aurora congestion control learned index / RMI Ouroboros
Closest papers by meaning
- Training Verification-Friendly Neural Networks via Neuron Behavior Consistency (AAAI 2025 · similarity 0.86)
- Certified but Private: Scalable Zero-Knowledge Proofs for the Formal Verification of Neural Networks (NeurIPS 2026 · similarity 0.85)
- Provably Safe Neural Network Controllers via Differential Dynamic Logic (NeurIPS 2024 · similarity 0.85)
- VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees (ICML 2024 · similarity 0.85)
- DeepBern-Nets: Taming the Complexity of Certifying Neural Networks Using Bernstein Polynomial Activations and Precise Bound Propagation (AAAI 2024 · similarity 0.85)
- Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification (NeurIPS 2025 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.