Dnn Verification Eval

---
name: dnn-verification-eval
description: Evaluates the scalability and correctness of DNN verification tools by measuring their ability to prove safety or robustness properties within a strict time limit across diverse network architectures and property types. Use when the user wants to benchmark on VNN-COMP'22 & MNIST_GDVB, or asks about evaluating this task. Reports verification_success_rate.
metadata:
  skill_kind: dataset_eval
  source_arxiv: 2401.14412
  bibtex_key: duong2024veristable
  confidence: high
---

# dnn-verification-eval

> Harnessing Neuron Stability to Improve DNN Verification — Duong et al. (2024) (arXiv:2401.14412, 2024)

## What this evaluates

Evaluates the scalability and correctness of DNN verification tools by measuring their ability to prove safety or robustness properties within a strict time limit across diverse network architectures and property types.

## Datasets

- **VNN-COMP'22 & MNIST_GDVB** — total 580; splits: test (580); repo https://github.com/ChristopherBrix/vnncomp2022_benchmarks

## Metrics

- `verification_success_rate` **(primary)** — range: [0, 1]
  - Count of instances solved (SAT or UNSAT) within a 900-second per-instance timeout, divided by the total number of evaluable instances (excluding unknowns).

## Input / output format

**Input**: Neural network architecture (weights, biases, layer types) paired with a formal safety or robustness property specification (input constraints and output bounds).

**Output**: Verdict: SAT, UNSAT, or TIMEOUT.

## Scoring recipe

```python
def compute_success_rate(predictions, gold, timeout=900):
    solved = 0
    for pred in predictions:
        if pred != 'TIMEOUT':
            solved += 1
    return solved / len(gold)
```

## Common pitfalls

- Excluding unknown instances from the denominator changes the success rate calculation.
- Timeouts are per-instance (900s), not global, which heavily impacts multi-threaded scaling comparisons.
- Hardware differences across tools are normalized via timeout, but GPU/CPU utilization varies significantly.

## Evidence (verbatim from paper)

> In total, we have 713 problem instances (an instance is the verification task of a property of a network). Among these instances, 444 are known to be unsat (U), 136 are sat (S), and 133 are unknown (?) because no existing verifiers, in this study or in VNN-COMP, can solve them. We exclude unknown instances from our study because they do not contribute to our evaluation or comparison to other tools.

## Citation

```bibtex
@misc{duong2024veristable,
  title={Harnessing Neuron Stability to Improve DNN Verification},
  author={Duong et al. (2024)},
  year={2024},
  note={arXiv:2401.14412}
}
```

- arXiv: 2401.14412