NeuroCodeBench: a plain C neural network benchmark for software verification

要約

ニューラル ネットワーク コンポーネントを備えたセーフティ クリティカルなシステムには、強力な保証が必要です。
既存のニューラル ネットワーク検証技術は、この目標に向けて大きな進歩を示していますが、ネットワーク実装にソフトウェア障害がないことを証明することはできません。
この文書では、プレーン C で書かれたニューラル ネットワーク コードの検証ベンチマークである NeuroCodeBench について説明します。これには、数学ライブラリ、活性化関数、誤り訂正ネットワーク、伝達関数近似、確率密度推定、および
強化学習。
私たちの予備評価では、標準 C 数学ライブラリの不完全なサポートと大規模なニューラル ネットワークの複雑さのため、最先端のソフトウェア検証ツールが正しい判定を行うのに苦労していることがわかりました。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google