Qnn Smt Verification Eval

qnn-smt-verification-eval

Verifying Quantized Neural Networks using SMT-Based Model Checking — Sena et al. (2021) (arXiv:2106.05997, 2021)

What this evaluates

This evaluation protocol tests the scalability and correctness of SMT-based formal verification for quantized neural networks. It measures how well an SMT model-checking framework can prove safety properties or find counterexamples across different quantization levels, network architectures, and SMT solvers.

Datasets

• Iris dataset — total 150; splits: full (-1)
• Vocalic dataset — total 200; splits: full (-1)
• AcasXu benchmark — total 45; splits: full (-1)

Metrics

• verification_time (primary) — range: other
  • CPU time in seconds measured via the times system call until the SMT solver (ESBMC) returns a result (safe/unsafe) or hits a resource limit.

Input / output format

Input: C code representation of the fixed-point quantized ANN, annotated with FRAMA-C reachable intervals, plus SMT constraints defining hyper-rectangular/hypercubic input safety regions.

Output: SMT solver result: 'safe' (property holds), 'unsafe' with counterexample, or 'timeout' (due to memory exhaustion).

Scoring recipe

def evaluate(qnn_c_code, safety_property, solver='yices'):
    cmd = f'esbmc {qnn_c_code} -I <path> --force-malloc-success --no-div-by-zero-check --no-pointer-check --{solver} --no-bounds-check --interval-analysis --fixedbv'
    start = time.time()
    result = run(cmd)  # Returns 'safe', 'unsafe', or 'timeout'
    elapsed = time.time() - start
    return {'status': result, 'time_seconds': elapsed}

Common pitfalls

• Quantization bit-width must be carefully chosen to avoid overflow; incorrect quantization invalidates verification results.
• Timeouts are frequently caused by memory exhaustion rather than solver inefficiency, so memory limits should be monitored.
• Solver performance varies drastically (e.g., Z3 is orders of magnitude slower than Yices), making solver choice critical.

Evidence (verbatim from paper)

Here, we are interested in comparing the performance of such solvers in verifying ANN implementations. All presented execution times are CPU times, i.e., only the elapsed periods spent in allocated CPUs, which was measured with the times system call. In general, we let ESBMC run without time or memory limits. The timeouts reported in the following experiments are all due to exceedingly high memory consumption. There, we can see that solvers Bitwuzla and Boolector have nearly identical performance, in terms of verification time (Fig. 10(a)). In contrast, Yices exhibits a considerable advantage across the whole verification suite, being, in some specific cases, even two orders of magnitude faster.

Citation

@misc{sena2021verifying,
  title={Verifying Quantized Neural Networks using SMT-Based Model Checking},
  author={Sena et al. (2021)},
  year={2021},
  note={arXiv:2106.05997}
}

• arXiv: 2106.05997