論文の概要: Scaling Model Checking for DNN Analysis via State-Space Reduction and
Input Segmentation (Extended Version)
- arxiv url: http://arxiv.org/abs/2306.17323v1
- Date: Thu, 29 Jun 2023 22:18:07 GMT
- ステータス: 処理完了
- システム内更新日: 2023-07-03 13:51:34.682526
- Title: Scaling Model Checking for DNN Analysis via State-Space Reduction and
Input Segmentation (Extended Version)
- Title（参考訳）: 状態空間削減と入力セグメンテーションによるDNN解析のためのスケーリングモデル検査(拡張版)
- Authors: Mahum Naseer and Osman Hasan and Muhammad Shafique
- Abstract要約: 既存のフレームワークは、トレーニングされたNNに対して堅牢性と/または安全性を保証する。
我々は、広範囲のNNプロパティを分析するための最初のモデルチェックベースのフレームワークであるFANNetを提案した。
本研究は,形式的NN解析のスケーラビリティとタイミング効率を向上させるために,状態空間の削減と入力セグメント化手法を開発する。
- 参考スコア（独自算出の注目度）: 12.272381003294026
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: Owing to their remarkable learning capabilities and performance in real-world
applications, the use of machine learning systems based on Neural Networks
(NNs) has been continuously increasing. However, various case studies and
empirical findings in the literature suggest that slight variations to NN
inputs can lead to erroneous and undesirable NN behavior. This has led to
considerable interest in their formal analysis, aiming to provide guarantees
regarding a given NN's behavior. Existing frameworks provide robustness and/or
safety guarantees for the trained NNs, using satisfiability solving and linear
programming. We proposed FANNet, the first model checking-based framework for
analyzing a broader range of NN properties. However, the state-space explosion
associated with model checking entails a scalability problem, making the FANNet
applicable only to small NNs. This work develops state-space reduction and
input segmentation approaches, to improve the scalability and timing efficiency
of formal NN analysis. Compared to the state-of-the-art FANNet, this enables
our new model checking-based framework to reduce the verification's timing
overhead by a factor of up to 8000, making the framework applicable to NNs even
with approximately $80$ times more network parameters. This in turn allows the
analysis of NN safety properties using the new framework, in addition to all
the NN properties already included with FANNet. The framework is shown to be
efficiently able to analyze properties of NNs trained on healthcare datasets as
well as the well--acknowledged ACAS Xu NNs.
- Abstract（参考訳）: その優れた学習能力と実世界のアプリケーションの性能により、ニューラルネットワーク(nns)に基づく機械学習システムの利用は継続的に増加している。
しかし、文献における様々なケーススタディと経験的知見は、nn入力のわずかな変化が誤動作や望ましくないnn行動につながる可能性を示唆している。
これは、あるNNの行動に関する保証を提供することを目的として、公式な分析にかなりの関心を惹き付けている。
既存のフレームワークは、トレーニングされたNNに対して、満足度解決と線形プログラミングを使用して堅牢性と/または安全性を保証する。
我々は、幅広いNN特性を分析するための最初のモデルチェックベースのフレームワークであるFANNetを提案した。
しかし、モデルチェックに関連する状態空間の爆発はスケーラビリティの問題を引き起こし、FANNetは小さなNNにのみ適用できる。
本研究は,形式的NN解析のスケーラビリティとタイミング効率を向上させるために,状態空間の削減と入力セグメンテーション手法を開発する。
最先端のFANNetと比較して、我々の新しいモデルチェックベースのフレームワークは、検証の時間オーバーヘッドを最大8000倍に減らし、約80ドル以上のネットワークパラメータを持つNNに適用できる。
これにより、FANNetにすでに含まれているすべてのNNプロパティに加えて、新しいフレームワークを使用してNN安全性プロパティの分析が可能になる。
このフレームワークは、医療データセットとよく認識されているACAS Xu NNでトレーニングされたNNの特性を効率的に分析できることが示されている。
関連論文リスト
- Empowering Bayesian Neural Networks with Functional Priors through Anchored Ensembling for Mechanics Surrogate Modeling Applications [0.0]
本稿では,関数空間で利用可能な事前情報を統合するアンカー型アンサンブルに基づく新しいBNNトレーニング手法を提案する。
アンカーリング方式は, NNパラメータ間の低ランク相関を利用して, 事前学習から関数前の実現まで学習する。
また,既存のBNN実装では無視されることが多いNN重み間の相関が,関数空間とパラメータ空間の事前知識を適切に伝達する上で重要であることを示す。
論文 参考訳（メタデータ） (2024-09-08T22:27:50Z) - Neural Network Verification with Branch-and-Bound for General Nonlinearities [63.39918329535165]
ブランチ・アンド・バウンド(BaB)は、ニューラルネットワーク(NN)検証において最も効果的な手法の一つである。
我々は、一般的な非線形性にBaBを実行し、一般的なアーキテクチャでNNを検証する汎用フレームワークGenBaBを開発した。
我々は、Sigmoid、Tanh、Sine、GeLUなどの活性化機能を持つNNを含む幅広いNNの検証におけるGenBaBの有効性を実証する。
論文 参考訳（メタデータ） (2024-05-31T17:51:07Z) - Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation [67.63756749551924]
学習ベースのニューラルネットワーク(NN)制御ポリシは、ロボット工学と制御の幅広いタスクにおいて、印象的な経験的パフォーマンスを示している。
非線形力学系を持つNNコントローラのトラクション領域(ROA)に対するリアプノフ安定性の保証は困難である。
我々は、高速な経験的ファルシフィケーションと戦略的正則化を用いて、Lyapunov証明書とともにNNコントローラを学習するための新しいフレームワークを実証する。
論文 参考訳（メタデータ） (2024-04-11T17:49:15Z) - Provably Safe Neural Network Controllers via Differential Dynamic Logic [2.416907802598482]
NNCS検証のための制御理論の再利用を可能にする最初の一般手法を提案する。
dLの安全な制御エンベロープに基づいて、NN検証によって証明されたNNの仕様を導出する。
本稿では,NNCS の無限時間安全に関する dL 証明によって,仕様に忠実な NNCS の証明が反映されていることを示す。
論文 参考訳（メタデータ） (2024-02-16T16:15:25Z) - Posterior Regularized Bayesian Neural Network Incorporating Soft and
Hard Knowledge Constraints [12.050265348673078]
本稿では,異なる種類の知識制約を組み込んだ後正規化ベイズニューラルネットワーク(PR-BNN)モデルを提案する。
航空機着陸予測と太陽エネルギー出力予測のシミュレーション実験と2つのケーススタディにより,提案モデルの知識制約と性能改善が示された。
論文 参考訳（メタデータ） (2022-10-16T18:58:50Z) - Backward Reachability Analysis of Neural Feedback Loops: Techniques for
Linear and Nonlinear Systems [59.57462129637796]
本稿では,ニューラルネットワークを用いた閉ループシステムの安全性検証のための後方到達性アプローチを提案する。
フィードバックループにおけるNNの存在は、その活性化関数の非線形性や、NNモデルは一般に可逆的ではないため、ユニークな問題セットを示す。
フィードフォワードNNで表される制御ポリシを持つ線形系と非線形系のBP過近似を計算するためのフレームワークを提案する。
論文 参考訳（メタデータ） (2022-09-28T13:17:28Z) - Automated Repair of Neural Networks [0.26651200086513094]
安全でないNNの安全仕様を修復するためのフレームワークを提案する。
提案手法では,重み値のいくつかを修正して,新しい安全なNN表現を探索することができる。
我々は,提案するフレームワークが安全なNNを実現する能力を示す広範な実験を行った。
論文 参考訳（メタデータ） (2022-07-17T12:42:24Z) - On Feature Learning in Neural Networks with Global Convergence
Guarantees [49.870593940818715]
勾配流(GF)を用いた広帯域ニューラルネットワーク(NN)の最適化について検討する。
入力次元がトレーニングセットのサイズ以下である場合、トレーニング損失はGFの下での線形速度で0に収束することを示す。
また、ニューラル・タンジェント・カーネル(NTK)システムとは異なり、我々の多層モデルは特徴学習を示し、NTKモデルよりも優れた一般化性能が得られることを実証的に示す。
論文 参考訳（メタデータ） (2022-04-22T15:56:43Z) - Comparative Analysis of Interval Reachability for Robust Implicit and
Feedforward Neural Networks [64.23331120621118]
我々は、暗黙的ニューラルネットワーク(INN)の堅牢性を保証するために、区間到達可能性分析を用いる。
INNは暗黙の方程式をレイヤとして使用する暗黙の学習モデルのクラスである。
提案手法は, INNに最先端の区間境界伝搬法を適用するよりも, 少なくとも, 一般的には, 有効であることを示す。
論文 参考訳（メタデータ） (2022-04-01T03:31:27Z) - Provably Correct Training of Neural Network Controllers Using
Reachability Analysis [3.04585143845864]
我々は、安全と生活性を満たすことが保証されるサイバー物理システムのためのニューラルネットワーク(NN)コントローラのトレーニングの問題を考える。
我々のアプローチは、動的システムのためのモデルベース設計手法とデータ駆動アプローチを組み合わせることで、この目標を達成することである。
論文 参考訳（メタデータ） (2021-02-22T07:08:11Z) - Modeling from Features: a Mean-field Framework for Over-parameterized
Deep Neural Networks [54.27962244835622]
本稿では、オーバーパラメータ化ディープニューラルネットワーク(DNN)のための新しい平均場フレームワークを提案する。
このフレームワークでは、DNNは連続的な極限におけるその特徴に対する確率測度と関数によって表現される。
本稿では、標準DNNとResidual Network(Res-Net)アーキテクチャを通してフレームワークを説明する。
論文 参考訳（メタデータ） (2020-07-03T01:37:16Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。