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.
Code (2)
Tasks
Density EstimationMethods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Floating-Point Neural Network Verification at the Software Level
The behaviour of neural network components must be proven correct before deployment in safety-critical systems. Unfortunately, existing neural network verification techniques cannot certify the absence of faults at the s…
Automated Repair of AI Code with Large Language Models and Formal Verification
The next generation of AI systems requires strong safety guarantees. This report looks at the software implementation of neural networks and related memory safety properties, including NULL pointer deference, out-of-boun…
Language ModelingLanguage ModellingLarge Language ModelPrompt EngineeringFormal Verification of End-to-End Learning in Cyber-Physical Systems: Progress and Challenges
Autonomous systems -- such as self-driving cars, autonomous drones, and automated trains -- must come with strong safety guarantees. Over the past decade, techniques based on formal methods have enjoyed some success in p…
Self-Driving CarsCan ChatGPT support software verification?
Large language models have become increasingly effective in software engineering tasks such as code generation, debugging and repair. Language models like ChatGPT can not only generate code, but also explain its inner wo…
Code GenerationvalidRethinking Autonomy: Preventing Failures in AI-Driven Software Engineering
The integration of Large Language Models (LLMs) into software engineering has revolutionized code generation, enabling unprecedented productivity through promptware and autonomous AI agents. However, this transformation …
Prompt EngineeringCode Generation