# NeuroCodeBench: a plain C neural network benchmark for software verification

arXiv: https://arxiv.org/abs/2309.03617 · HTML: https://mlsanity.com/paper/2309.03617/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 45 references that are in the map.
- First posted on arXiv 7 Sep 2023.

## Builds on (most cited first, 14 of 14)

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Exploring the Limits of Out-of-Distribution Detection](https://mlsanity.com/paper/2106.03004/) (2021)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [A Framework for Understanding Sources of Harm throughout the Machine Learning Life Cycle](https://mlsanity.com/paper/1901.10002/) (2019)
- [Activation Functions: Comparison of trends in Practice and Research for Deep Learning](https://mlsanity.com/paper/1811.03378/) (2018)
- [Taxonomy of Real Faults in Deep Learning Systems](https://mlsanity.com/paper/1910.11015/) (2019)
- [TensorFuzz: Debugging Neural Networks with Coverage-Guided Fuzzing](https://mlsanity.com/paper/1807.10875/) (2018)
- [CAPE: Encoding Relative Positions with Continuous Augmented Positional Embeddings](https://mlsanity.com/paper/2106.03143/) (2021)
- [Pitfalls in Machine Learning Research: Reexamining the Development Cycle](https://mlsanity.com/paper/2011.02832/) (2020)
- [Bugs in Machine Learning-based Systems: A Faultload Benchmark](https://mlsanity.com/paper/2206.12311/) (2022)
- [CBMC: The C Bounded Model Checker](https://mlsanity.com/paper/2302.02384/) (2023)
- [Learning Density Distribution of Reachable States for Autonomous Systems](https://mlsanity.com/paper/2109.06728/) (2021)
- [Verifying Quantized Neural Networks using SMT-Based Model Checking](https://mlsanity.com/paper/2106.05997/) (2021)
- [CEG4N: Counter-Example Guided Neural Network Quantization Refinement](https://mlsanity.com/paper/2207.04231/) (2022)

## Built on by (most cited first, 3 of 3)

- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Automated Repair of AI Code with Large Language Models and Formal Verification](https://mlsanity.com/paper/2405.08848/) (2024)
- [Floating-Point Neural Network Verification at the Software Level](https://mlsanity.com/paper/2510.23389/) (2025)

## Abstract (arXiv)

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.