NeuroCodeBench: a plain C neural network benchmark for software verification
This addresses the need for strong guarantees in safety-critical systems with neural network components, though it is incremental as it builds on existing verification techniques by focusing on code-level faults.
The authors tackled the problem of verifying neural network implementations in safety-critical systems by introducing NeuroCodeBench, a benchmark of 32 neural networks in plain C with 607 safety properties, and found that state-of-the-art software verifiers struggle to provide correct verdicts due to incomplete C library support and network complexity.
Safety-critical systems with neural network components require strong guarantees. While existing neural network verification techniques have shown great progress towards this goal, they cannot prove the absence of software faults in the network implementation. This paper presents NeuroCodeBench - a verification benchmark for neural network code written in plain C. It contains 32 neural networks with 607 safety properties divided into 6 categories: maths library, activation functions, error-correcting networks, transfer function approximation, probability density estimation and reinforcement learning. Our preliminary evaluation shows that state-of-the-art software verifiers struggle to provide correct verdicts, due to their incomplete support of the standard C mathematical library and the complexity of larger neural networks.