α,β-CROWN Reproducibility Study

Formal verification only matters if its results can be trusted — and reproduced. During my research internship at the Digital Research Center of Sfax (CRNS), I evaluated α,β-CROWN, a multi-year VNN-COMP winner, by re-running the CIFAR2020 benchmark in an independent environment.

The benchmark asks whether ResNet-style CNNs trained on CIFAR-10 stay robust under L∞ perturbations of ε = 2/255 and 8/255: 147 properties, each pairing an ONNX model with a VNN-LIB specification, under a 300-second timeout.

I built the tooling around the runs: a parser that turns raw verifier logs into structured CSVs, scripts that extract the official per-benchmark results, and a notebook that compares verdicts with confusion matrices and solved-over-time curves.

The study confirmed that α,β-CROWN reproduces well. All 103 certified-safe (UNSAT) verdicts matched, 34 of 35 counterexamples (SAT) matched, and the remaining divergences clustered on the slowest instances near the timeout.