首次在软件层验证神经网络浮点实现安全性，构建可测试基准
Floating-Point Neural Network Verification at the Software Level
- 通过显式建模浮点运算，从代码层面验证神经网络正确性
- 8款主流工具平均仅能正确处理11%的测试用例，3%给出错误结论
- 适用于安全关键系统开发与验证工具评估，推动领域发展
神经网络在部署至安全关键系统前必须确保行为正确。然而，现有验证方法无法在软件层面证明其无故障。本文提出在浮点实现层面显式推理神经网络安全性，并构建了NeuroCodeBench 2.0基准，包含912个验证实例，覆盖激活函数、常见层及最大达17万参数的完整神经网络。验证套件采用纯C语言编写，兼容国际软件验证竞赛（SV-COMP）格式。基于此，首次对八款前沿软件验证器进行严格评估：结果显示，现有自动化工具平均仅能正确求解11%的案例，且约3%产生错误判定。同时，历史分析表明该基准已显著促进相关工具改进。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。