Technical Summary: Floating-Point Neural Network Verification at the Software Level

Problem Statement

While neural network verification has advanced significantly in providing formal guarantees for idealized, real-valued models, these approaches often fail to account for the specific implementation details of deployed systems. In safety-critical applications (e.g., CPS, IoT), neural networks are implemented using finite-precision floating-point arithmetic (typically 32-bit IEEE 754) and rely on standard mathematical libraries (e.g., math.h). These low-level details introduce rounding errors and non-associative behaviors that can invalidate safety proofs derived from infinite-precision models. For instance, the paper demonstrates that the SoftSign activation function, which is non-decreasing in real arithmetic, ceases to be so when implemented in 32-bit floating point.

Existing attempts to verify neural network code at the software level have yielded mixed results. Software verifiers often struggle to scale to large neural network instances, forcing practitioners to revert to unsound infinite-precision models or abandon verification for testing. Furthermore, existing tools have been observed to produce incorrect results in certain settings, casting doubt on their reliability as safety oracles for floating-point implementations. There is a lack of rigorous, standardized evaluation of automated software verifiers specifically on neural network code.

Methodology

To address these gaps, the authors conducted a rigorous evaluation of eight state-of-the-art automated software verifiers on neural network code. The methodology involved three primary components:

1. Benchmark Construction (NeuroCodeBench 2.0): The authors constructed a comprehensive benchmark comprising 912 verification examples. This benchmark covers:

   • Mathematical Functions: 58 instances testing properties (e.g., monotonicity, periodicity, linear bounds) of standard math.h functions.
   • Activation Functions: 57 instances testing properties of common activations (e.g., ReLU, TanH, SoftSign, GELU).
   • Neural Layers: 86 instances covering affine transformations, normalization, pooling, and SoftMax layers.
   • Full Neural Networks: 711 instances including Hopfield networks, SAT-encoded ReLU networks, polynomial approximation networks, Lipschitz-bounded networks, and networks derived from VNN-COMP (Probability Density and Reinforcement Learning tasks).
   • Ground Truth: Every instance is pre-labeled as "safe" or "unsafe" using techniques such as brute-force testing, exhaustive construction, or counterexample generation, ensuring a known correct verdict for evaluation.

2. Standardization and Compatibility: To ensure fair comparison and reproducibility, the authors converted all benchmark instances into the format used by the International Competition on Software Verification (SV-COMP). This involved creating self-contained C files that include the model implementation, safety properties, and necessary dependencies. The workflow utilized the BenchExec framework to manage resource limits and execution, ensuring the tools were run with the same configurations used in the 2024 SV-COMP edition.

3. Experimental Evaluation: The study evaluated eight tools (2LS, CBMC, CPAChecker, DIVINE, ESBMC, PeSCo, Pinaka, UAutomizer) under two conditions:

   • Baseline: Running verifiers on the plain benchmark instances.
   • Operational Models: Providing explicit C implementations of the math.h library (using MUSL and CORE-MATH) to see if supplying the function definitions improves verification outcomes.
   • Historical Analysis: The authors also analyzed the historical performance of one tool (ESBMC) from 2018 to 2026 to observe trends in the field.

Key Contributions

• NeuroCodeBench 2.0: The creation of a large-scale, ground-truth benchmark specifically designed for software-level verification of floating-point neural networks. It includes 912 instances ranging from simple functions to full networks with up to 170K parameters.
• SV-COMP Integration: The benchmark was formatted to be compatible with the SV-COMP infrastructure, making it part of the official benchmark set for the 2026 edition. This allows for automated, reproducible evaluation using standard tool configurations.
• Rigorous Evaluation: The first systematic study comparing eight state-of-the-art software verifiers on neural network code, revealing significant variance in performance and correctness.
• Operational Model Analysis: An investigation into whether supplying explicit implementations of mathematical libraries (MUSL, CORE-MATH) improves verifier performance, finding that the impact is tool-dependent and often negligible or negative.

Results

The evaluation yielded several critical findings regarding the current state of software verification for neural networks:

• Low Correctness and Scalability: The results were described as "rather underwhelming." The tools exhibited a large variance across the benchmark, with the best-performing tool (CBMC) solving 371 out of 912 instances correctly, while others solved significantly fewer. The average solution rate across categories varied, with some complex categories (e.g., Reinforcement Learning) seeing solution rates as low as 3%. Most tools failed to verify more than a single neural layer at a time.
• Incorrect Verdicts: Several tools produced a high rate of incorrect results. For example, CBMC produced nearly 25% incorrect definitive verdicts (mostly false positives), and Pinaka and UAutomizer also showed significant error rates. Only ESBMC produced no incorrect verdicts among the tools that solved a substantial number of instances.
• Impact of Operational Models: Providing explicit implementations of math.h (MUSL or CORE-MATH) did not lead to visible improvements overall. For some tools (CBMC, ESBMC, Pinaka), performance actually decreased due to the added complexity of verifying the library code. For others (CPAChecker, PeSCo), the number of solved instances increased, but this often came with a surge in incorrect verdicts.
• Scalability Limits: Tools struggled significantly with full neural networks. The solution rate dropped to single digits for complex categories like Reinforcement Learning and Probability Density. Even for synthetic networks, tools like ESBMC could only solve instances with very small widths (e.g., width 4) before timing out.
• Historical Progress: The analysis of ESBMC from 2018 to 2026 showed non-monotonic but generally constant improvements. A notable spike in incorrect verdicts in 2022-2023 was traced to an implementation error in a k-induction algorithm, which was fixed following the release of the earlier NeuroCodeBench 1.0. The introduction of NeuroCodeBench 1.0 in 2024 led to a drastic reduction in incorrect verdicts across the community, though the impact of NeuroCodeBench 2.0 (late 2025) was more moderate.

Significance and Claims

The paper claims that while verifying neural networks at the software level is conceptually feasible, existing state-of-the-art software verifiers are not yet ready to handle this task effectively. The study highlights that current tools cannot reliably check more than a single layer, frequently return incorrect results, and lack full support for standard mathematical libraries.

The authors argue that their work serves as a necessary "reality check" for the verification community. By providing a rigorous benchmark with known ground truth, they demonstrate that the gap between idealized verification and software implementation is currently too wide for existing tools to bridge without significant improvements. The paper posits that the release of NeuroCodeBench has already stimulated progress, evidenced by the reduction in incorrect verdicts following its initial release. However, the authors conclude that certifying the full implementation of neural networks against worst-case numerical deviations remains a long-term challenge requiring native support for mathematical libraries and custom decision procedures adapted for floating-point arithmetic.