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 software level. In this paper, we show how to specify and verify that neural networks are safe, by explicitly reasoning about their floating-point implementation. In doing so, we construct NeuroCodeBench 2.0, a benchmark comprising 912 neural network verification examples that cover activation functions, common layers, and full neural networks of up to 170K parameters. Our verification suite is written in plain C and is compatible with the format of the International Competition on Software Verification (SV-COMP). Thanks to it, we can conduct the first rigorous evaluation of eight state-of-the-art software verifiers on neural network code. The results show that existing automated verification tools can correctly solve an average of 11% of our benchmark, while producing around 3% incorrect verdicts. At the same time, a historical analysis reveals that the release of our benchmark has already had a significantly positive impact on the latter.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Exploring Approximations for Floating-Point Arithmetic using UppSAT
We consider the problem of solving floating-point constraints obtained from software verification. We present UppSAT --- a new implementation of a systematic approximation refinement framework [ZWR17] as an abstract SMT …
Formal that "Floats" High: Formal Verification of Floating Point Arithmetic
Formal verification of floating-point arithmetic remains challenging due to non-linear arithmetic behavior and the tight coupling between control and datapath logic. Existing approaches often rely on high-level C models …
Exploiting Verified Neural Networks via Floating Point Numerical Error
Researchers have developed neural network verification algorithms motivated by the need to characterize the robustness of deep neural networks. The verifiers aspire to answer whether a neural network guarantees certain p…
QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks
Deep learning has become a promising programming paradigm in software development, owing to its surprising performance in solving many challenging tasks. Deep neural networks (DNNs) are increasingly being deployed in pra…
QuantizationExploiting Binary Floating-Point Representations for Constraint Propagation: The Complete Unabridged Version
Floating-point computations are quickly finding their way in the design of safety- and mission-critical systems, despite the fact that designing floating-point algorithms is significantly more difficult than designing in…