NeuroCodeBench: a plain C neural network benchmark for software
  verification
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.
Edoardo Manino, Rafael Sá Menezes, Fedor Shmarov, Lucas C. Cordeiro
# NeuroCodeBench: a plain C neural network benchmark for software verification

###### 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.

## 1 Introduction

In contrast to classic software development, neural networks are crafted via a long process of trial and error that terminates when their predictive performance reaches a satisfactory level [7, 43]. The iterative and performance-driven nature of this process leaves neural networks vulnerable on many fronts [23]: poor performance on out-of-distribution [18] and adversarial inputs [37], misspecification of the neural architecture and training process [24], invocation of broken and deprecated libraries [35], outright software bugs [20]. Unfortunately, many of these vulnerabilities are not easy to catch early in the development process and may remain hidden until after deployment.

The most successful techniques for guaranteeing the functional correctness of neural networks operate at a high level of abstraction, where finite precision and other implementation details are not considered [27, 46, 36]. Although efforts to debug the actual implementation of neural networks exist, they are based on automatic testing and thus cannot prove correctness for all inputs [39, 20, 17]. This lack of guarantees is especially concerning for safety-critical systems since common software vulnerabilities [12] (e.g., arithmetic overflows, invalid memory accesses) can make the networks produce wrong results, expose sensitive data or corrupt the system they are executed on.

While off-the-shelf software verifiers can be used to check neural network code [42, 33], there has been no systematic attempt at assessing their performance on such tasks. Typically, state-of-the-art verification tools (e.g., CPAChecker [5], ESBMC [19], CBMC [28], UAutomizer [21]) are compared on SV-COMP [4] - the largest software verification competition with over 15'000 C programs ranging
from hand-crafted code to real-world software (e.g., drivers, Linux kernel). However, this competition lacks a dedicated benchmark for either neural networks or mathematical libraries (e.g., math.h).

This paper presents _NeuroCodeBench_ - a reasoned benchmark of neural network code in plain C. It is designed to exercise the capabilities of existing software verifiers without overwhelming them with excessively large instances. More specifically, it contains 32 neural networks with 607 safety properties in SV-COMP format divided into the following 6 categories: maths library, activation functions, error-correcting networks, transfer function approximation, probability density estimation and reinforcement learning. The last two categories are converted to C code from the VNN-COMP'22 suite [36], whereas the rest are entirely new. As a demonstration, we run the leading tools of SV-COMP 2023 in reachability, falsification and floating point arithmetic [4]. Our preliminary results show that these verifiers have incomplete support of the math.h library and struggle on larger neural networks. Lastly, we make _NeuroCodeBench_ publicly available at [31] and [30].

## 2 The Benchmark

### Design Requirements

In designing _NeuroCodeBench_, we target two main requirements. First, our benchmark must be representative of existing neural network code. Mainstream libraries like PyTorch [3] and Tensorflow [9] have an opaque multi-language interpreted structure that can be easily tested [20, 17], but does not lend itself to automated software verification. For this reason, we opt for micro-controller frameworks, where the source code of the network is fully available. We use two existing tools for converting high-level neural network specifications to standalone C code: onnx2c[45] and keras2c[14, 15].

Second, our benchmark must contain safety properties whose verdict is known, with reasonably balanced sets of safe and unsafe verdicts. Existing works rely on the verdicts of a single tool [42, 33] and thus are not a reliable source of information. Here, we establish the ground-truth verdict of our 607 safety properties in three ways (see Table 1): _A Priori_ verdicts come from the specific mathematical structure of the functions and networks we verify; _Brute Force_ verdicts come from exhaustive exploration of all possible floating point inputs; _VNN-COMP'22_ verdicts come from the independently-run neural network verification competition [36]. For the latter, we only keep unsafe properties if we can reproduce the corresponding counterexamples.

### Benchmark Description

Math Library.Typically, neural networks rely on 32-bit floating point operations1 and invoke the corresponding functions in the math.h library. More specifically, most activation functions depend on

\begin{table}
\begin{tabular}{|c|c|c|c|} \hline Benchmark Category & Safe & Unsafe & Ground Truth \\ \hline math\_functions & 33 & 11 & A Priori \\ activation\_functions & 40 & 16 & A Priori \\ hopfield\_nets & 47 & 33 & A Priori \\ poly\_approx & 48 & 48 & Brute Force \\ reach\_prob\_density & 22 & 13 & VNN-COMP’22 \\ reinforcement\_learning & 103 & 193 & VNN-COMP’22 \\ \hline \end{tabular}
\end{table}
Table 1: Overview of _NeuroCodeBench_. The “Unsafe” column comprises all properties for which a counterexample exists. The “Ground Truth” column reports the source of our verdicts.
exponential, logarithm, error function, absolute value, and max function (see activation_functions category). Similarly, positional encodings depend on sine and cosine [29], while Euclidean distances and vector normalisation depend on the square root [8].

In this light, it is worth checking whether software verifiers correctly handle calls to math.h. We write benchmarks that depend on the following functions: acosf, asinf, cosf, erff, expf, fabsf, logf, sinf and sqrtf. Since their semantics are platform-specific, we assume compliance with the IEEE 754 standard for 32-bit floating point [25] and the C99 standard for math.h[26]. We provide 44 safety properties (see Table 1) that check for a wide range of behavior: output bounds, monotonicity, periodicity, symmetry, function inversion and derivatives.

Activation Functions.Most of the non-linear behaviour in neural networks is concentrated in the activation layers [8]. These contain fairly restricted sets of activation functions whose implementation should be verified for correctness. Our benchmark includes the most popular ones [38, 22]: Elu, Gelu, Logistic, ReLU, Softmax, Softplus, Softsign and TanH. In turn, their definition depends on the functions erff, expf, expmf, fabsf, fmaxf, log1pf and tanhf. While most activation functions are univariate, the Softmax accepts multivariate inputs. To keep our verification instances small, we limit the size of Softmax input vectors to 2 and 4.

Error-Correcting Networks.For a long time, it has been known that certain types of recurrent neural networks can act as error-correcting decoders [1, 11]. The main idea is encoding a sequence of \(d\) bits into a vector \(x\in\{\pm 1\}^{d}\), and letting the neural network flip the sign of the incorrect entries.

Here, we choose Hopfield networks with Hebbian weights since their properties are well understood [1]. Specifically, we build networks reconstructing a single pattern \(x=(1,\ldots,1)\). We vary the pattern length in \(d\in\{4,8,16,32,64\}\) and the number of recursions in \(t\in[1,4]\). For compatibility with keras2c[14, 15], we use Softsign and TanH activations (see Table 2) rather than traditional sign activations [1]. Our safety properties check whether the network can reconstruct \(x\) when the first \(d/2-1\) entries can take any value in \([-1,1]\). Due to the network symmetry, we establish the ground truth by checking the extreme inputs \(x\) and \(x^{\prime}=(-1,\ldots,1)\), where \(x^{\prime}_{i}=-1\) for all \(i\in[1,d/2-1]\).

Transfer Function NetworksIn several engineering areas, neural networks are used to approximate the transfer function of electrical components [47, 32]. Here, we emulate this process by defining a hypothetical polynomial component \(f(x)=0.125x^{4}-0.25x^{3}-0.75x^{2}+x+0.5\) with oscillating transfer function. Then, we create a training set by uniformly sampling \(f(x)\) in \(x\in[-2,3]\) and train 16 different feedforward ReLU networks \(\hat{f}(x)\). The smallest has four layers with four neurons each, and the largest has a single hidden layer with 1024 neurons (see poly_approx category in Table 2).

We formally verify the approximation quality by measuring the difference between \(\hat{f}(x)\) and \(f(x)\) for each possible 32-bit floating point value in \([-2,3]\). With this information, we write 96 robustness properties (see Table 1). Specifically, we check the input domain in a small interval \(\mathcal{X}\) of size 0.1

\begin{table}
\begin{tabular}{|r|c|c|c|c|c|c|c|} \hline Neural Network Category & Inputs & Outputs & Layers & Neurons & Activations & Architecture & Conversion \\ \hline hopfield\_nets & 4–64 & 4–64 & 1 & 4–64 & Softsign/TanH & Recurrent & keras2c \\ poly\_approx & 1 & 1 & 1–4 & 16–1024 & ReLU & Feedforward & keras2c \\ reach\_prob\_density & 3–14 & 3–14 & 2–3 & 64–192 & ReLU & Feedforward & onnx2c \\ reinforcement\_learning & 4–8 & 2–8 & 2 & 128–512 & ReLU & Feedforward & onnx2c \\ \hline \end{tabular}
\end{table}
Table 2: Neural networks in _NeuroCodeBench_. The “Layers” and “Neurons” columns refer to the hidden layers only. The networks in hopfield_nets have a number of iterations between 1 and 4.
around the worst approximation error. There, we make sure that the error is always below a given threshold \(\epsilon\geq|f(x)-\hat{f}(x)|,\forall x\in\mathcal{X}\). We select six decreasing values of \(\epsilon\) for each network: three make the property hold and three yield a counterexample.

VNN-COMP NetworksSince its first edition in 2020, the International Verification of Neural Networks Competition (VNN-COMP) publishes all its benchmarks [36]. These benchmarks do not contain implementation details since they target a higher level of abstraction (real number arithmetic, no memory model). To provide a reference implementation, we propose the following conversion process: we translate the networks from ONNX format [13] to C with onnx2c[45], and the safety properties from VNN-LIB [44] to a minimal main() function with pre- and post-conditions.

Among all categories of the 2022 edition [36], we select two that contain relatively small neural networks (see Table 2): reach_prob_density are networks that approximate probability densities [34], reinforcement_learning are control networks trained via reinforcement learning [40].

### Preliminary Evaluation

Here, we use _NeuroCodeBench_ to evaluate six software verifiers which achieved top-places2 in the _Reachability_, _Falsification_ and _Floats_ categories of SV-COMP 2023 [4]. We keep our experimental setup as similar to SV-COMP as possible: we use the benchmarking tool BenchExec [6] with 2 CPU cores, 6GB of RAM and 900 seconds of total CPU time per verifier for each verification task.

Footnote 2: We omit VeriAbs [2] and VeriAbsL [16] due to licence restrictions. We omit BRICK [10] due to technical issues. We omit cooperative verifiers for clarity. We run PeSCo [41] with the CPAChecker binary from SV-COMP 2023.

Our preliminary results in Figure 1 show that all six verifiers produce a large ratio of _incorrect-to-correct_ verdicts. One of the likely reasons is incomplete support of math.h functions, which appear in the first three categories of Table 1. Indeed, CBMC, ESBMC, CPAChecker and UAutomizer produce many math-related warnings in their output, even when their verdict is correct or unknown. At the same time, approximately half of the unknown verdicts are due to timeouts on the larger neural networks of _NeuroCodeBench_, which suggests that the verifiers struggle with their complexity.

## 3 Conclusions and Future Work

_NeuroCodeBench_ is a challenging benchmark of neural network code in plain C. Our preliminary analysis demonstrates that state-of-the-art verifiers cannot produce correct verdicts on most of our safety properties. In the future, we plan to provide complete operational models for the math.h library, whose absence impacts existing verifiers. Furthermore, we plan to contribute _NeuroCodeBench_ to SV-COMP and draw the attention of that community to the challenges of verifying neural code.

Figure 1: Results of state-of-the-art software verifiers on _NeuroCodeBench_ after 900 seconds.