Destabilizing Neurons to Generate Challenging Neural Network Verification Benchmarks

Neural Network Verification has made significant progress in recent years, with the development of numerous verification techniques and tools. However, the field still lacks high-quality benchmarks for systematically evaluating and improving these tools. As verification techniques advance, many existing benchmarks have become too trivial, while the harder ones often remain unsolvable. Several recent efforts have attempted to address this gap, typically by retraining or distilling neural networks to create new benchmarks. However, such approaches are computationally expensive and often produce benchmarks with unknown or unverifiable ground truth.In this paper, we introduce ReluSplitter, an automatic benchmark generation tool for DNN verifiers. ReluSplitter takes existing verification benchmarks as input and strategically destabilizes stable neurons to increase verification difficulty. This transformation is semantics-preserving by construction: every ReluSplitter -generated benchmark is guaranteed to have exactly the same ground truth as the original benchmark. This makes ReluSplitter particularly valuable for assessing verifier correctness and performance.Our evaluation demonstrates that ReluSplitter can significantly increase the difficulty of existing benchmarks, effectively challenging state-of-the-art DNN verifiers. We believe ReluSplitter offers a practical and principled way to generate benchmarks with tunable difficulty and verifiable ground truth, contributing a much-needed resource for the neural network verification community.