NeuroCodeBench: a plain C neural network benchmark for software verification

TL;DR

NeuroCodeBench is a new benchmark for verifying plain C neural network code, highlighting current verification tools' limitations in handling complex networks and standard math libraries.

Contribution

It introduces a comprehensive verification benchmark with diverse neural networks and safety properties, addressing a gap in verifying neural network implementations in C.

Findings

State-of-the-art verifiers struggle with complex networks

Verification tools have incomplete support for C math libraries

Larger networks pose significant verification challenges

Abstract

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.