論文の概要: NeuroCodeBench: a plain C neural network benchmark for software
verification
- arxiv url: http://arxiv.org/abs/2309.03617v1
- Date: Thu, 7 Sep 2023 10:19:33 GMT
- ステータス: 処理完了
- システム内更新日: 2023-09-08 13:29:04.990132
- Title: NeuroCodeBench: a plain C neural network benchmark for software
verification
- Title(参考訳): NeuroCodeBench: ソフトウェア検証のための普通のCニューラルネットワークベンチマーク
- Authors: Edoardo Manino, Rafael S\'a Menezes, Fedor Shmarov, Lucas C. Cordeiro
- Abstract要約: 本稿では,通常のC言語で記述されたニューラルネットワークコードの検証ベンチマークであるNeuroCodeBenchを提案する。
そこには、数学ライブラリ、アクティベーション関数、エラー修正ネットワーク、転送関数近似、確率密度推定、強化学習の6つのカテゴリに分けられる607の安全性特性を持つ32のニューラルネットワークが含まれている。
- 参考スコア(独自算出の注目度): 4.9975496263385875
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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.
- Abstract(参考訳): ニューラルネットワークコンポーネントを持つ安全クリティカルシステムは、強力な保証を必要とする。
既存のニューラルネットワーク検証技術はこの目標に向けて大きな進歩を見せているが、ネットワーク実装におけるソフトウェア欠陥の欠如を証明することはできない。
本稿では,平易なc言語で記述されたニューラルネットワークコードの検証ベンチマークであるneurocodebenchについて述べる。計算ライブラリ,アクティベーション関数,誤り訂正ネットワーク,伝達関数近似,確率密度推定,強化学習の6つのカテゴリに,607の安全性特性を持つ32のニューラルネットワークが含まれている。
予備評価の結果,標準c数式ライブラリの不完全なサポートと大規模ニューラルネットワークの複雑さにより,最先端のソフトウェア検証者が正しい判断を下すのに苦労していることが判明した。
関連論文リスト
- Verified Neural Compressed Sensing [58.98637799432153]
精度の高い計算タスクのために、初めて(私たちの知識を最大限に活用するために)証明可能なニューラルネットワークを開発します。
極小問題次元(最大50)では、線形および双項線形測定からスパースベクトルを確実に回復するニューラルネットワークを訓練できることを示す。
ネットワークの複雑さは問題の難易度に適応できることを示し、従来の圧縮センシング手法が証明不可能な問題を解く。
論文 参考訳(メタデータ) (2024-05-07T12:20:12Z) - Set-Based Training for Neural Network Verification [8.97708612393722]
小さな入力摂動はニューラルネットワークの出力に大きな影響を与える。
安全クリティカルな環境では、入力はノイズの多いセンサーデータを含むことが多い。
我々は、堅牢なニューラルネットワークをトレーニングして正式な検証を行う、エンドツーエンドのセットベーストレーニング手順を採用している。
論文 参考訳(メタデータ) (2024-01-26T15:52:41Z) - Quantization-aware Interval Bound Propagation for Training Certifiably
Robust Quantized Neural Networks [58.195261590442406]
我々は、逆向きに頑健な量子化ニューラルネットワーク(QNN)の訓練と証明の課題について検討する。
近年の研究では、浮動小数点ニューラルネットワークが量子化後の敵攻撃に対して脆弱であることが示されている。
本稿では、堅牢なQNNをトレーニングするための新しい方法であるQA-IBP(quantization-aware interval bound propagation)を提案する。
論文 参考訳(メタデータ) (2022-11-29T13:32:38Z) - Robust Training and Verification of Implicit Neural Networks: A
Non-Euclidean Contractive Approach [64.23331120621118]
本稿では,暗黙的ニューラルネットワークのトレーニングとロバスト性検証のための理論的および計算的枠組みを提案する。
組込みネットワークを導入し、組込みネットワークを用いて、元のネットワークの到達可能な集合の超近似として$ell_infty$-normボックスを提供することを示す。
MNISTデータセット上で暗黙的なニューラルネットワークをトレーニングするためにアルゴリズムを適用し、我々のモデルの堅牢性と、文献における既存のアプローチを通じてトレーニングされたモデルを比較する。
論文 参考訳(メタデータ) (2022-08-08T03:13:24Z) - CheckINN: Wide Range Neural Network Verification in Imandra [0.0]
我々は,関数型プログラミング言語Imandraと定理証明器が,ニューラルネットワーク検証のための総合的な基盤を提供する方法を示す。
We developed a novel library CheckINN that formals neural network in Imandra, and covers different important facets of neural network verification。
論文 参考訳(メタデータ) (2022-07-21T16:06:58Z) - Neural Network Quantization for Efficient Inference: A Survey [0.0]
ニューラルネットワークの量子化は、最近、ニューラルネットワークのサイズと複雑さを減らすというこの要求を満たすために発生した。
本稿では,過去10年間に開発された多くのニューラルネットワーク量子化技術について検討する。
論文 参考訳(メタデータ) (2021-12-08T22:49:39Z) - The mathematics of adversarial attacks in AI -- Why deep learning is
unstable despite the existence of stable neural networks [69.33657875725747]
固定アーキテクチャを用いた分類問題に対するニューラルネットワークのトレーニングに基づくトレーニング手順が,不正確あるいは不安定なニューラルネットワーク(正確であれば)を生み出すことを証明している。
鍵となるのは、安定かつ正確なニューラルネットワークは入力に依存する可変次元を持つ必要があり、特に、可変次元は安定性に必要な条件である。
我々の結果は、正確で安定したニューラルネットワークが存在するというパラドックスを示しているが、現代のアルゴリズムはそれらを計算していない。
論文 参考訳(メタデータ) (2021-09-13T16:19:25Z) - Building Compact and Robust Deep Neural Networks with Toeplitz Matrices [93.05076144491146]
この論文は、コンパクトで、訓練が容易で、信頼性があり、敵の例に対して堅牢なニューラルネットワークを訓練する問題に焦点を当てている。
Toeplitzファミリーの構造化行列の特性を利用して、コンパクトでセキュアなニューラルネットワークを構築する。
論文 参考訳(メタデータ) (2021-09-02T13:58:12Z) - Provably Training Neural Network Classifiers under Fairness Constraints [70.64045590577318]
過パラメータのニューラルネットワークが制約を満たしていることを示す。
公平なニューラルネットワーク分類器を構築する上で重要な要素は、ニューラルネットワークの非応答解析を確立することである。
論文 参考訳(メタデータ) (2020-12-30T18:46:50Z) - Scalable Verification of Quantized Neural Networks (Technical Report) [14.04927063847749]
ビットベクトル仕様を持つ量子化ニューラルネットワークのビットエクササイズ実装はPSPACEハードであることを示す。
量子化されたニューラルネットワークのSMTに基づく検証をよりスケーラブルにするための3つの手法を提案する。
論文 参考訳(メタデータ) (2020-12-15T10:05:37Z) - Towards Repairing Neural Networks Correctly [6.600380575920419]
本稿では,ニューラルネットワークの正確性を保証するための実行時検証手法を提案する。
実験結果から,本手法は特性を満たすことが保証されたニューラルネットワークを効果的に生成することが示された。
論文 参考訳(メタデータ) (2020-12-03T12:31:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。