Dnn Verification Eval

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

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

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

• arXiv: 2401.14412