Researchers Tackle Floating-Point Bugs in Neural Networks With New Verification Benchmark

Before deploying neural networks in safety-critical systems—like autonomous vehicles or medical devices—developers need guarantees that the code will behave correctly. Yet existing verification methods struggle to certify the actual software implementation, particularly when floating-point arithmetic introduces rounding errors and numerical instabilities.

A new research effort addresses this gap by developing NeuroCodeBench 2.0, a comprehensive benchmark designed to verify neural networks at the code level, accounting for the real-world complexities of how floating-point math works in practice.

The Problem with Current Approaches#

Most neural network verification tools focus on the abstract mathematical properties of networks—proving that a model will make the right decision given certain inputs—but they ignore what actually happens when that network runs on real hardware and software. Floating-point operations introduce precision losses, rounding, and subtle numerical behaviors that can cascade through a computation and lead to unexpected results.

By contrast, this work explicitly reasons about floating-point implementations, treating the actual C code as the object of verification rather than an idealized mathematical model.

Building a Verification Benchmark#

The researchers constructed NeuroCodeBench 2.0 to contain 912 verification examples spanning:

• Activation functions (ReLU, sigmoid, tanh, etc.)
• Common layer types (fully connected, convolutional)
• Complete neural networks up to 170,000 parameters

The entire suite is written in plain C and formatted to be compatible with the International Competition on Software Verification (SV-COMP), a major evaluation framework for automated verification tools.

Evaluating State-of-the-Art Tools#

For the first time, researchers systematically tested eight leading automated software verifiers against neural network code. The results underscore the challenge: on average, these tools correctly solved only 11% of the benchmark, while also producing around 3% false verdicts—cases where the verifier reached an incorrect conclusion.

Despite these sobering initial numbers, the release of the benchmark has already spurred improvements in the field, with participating tools showing measurable progress in subsequent versions.