論文の概要: Fully Automatic Neural Network Reduction for Formal Verification

• arxiv url: http://arxiv.org/abs/2305.01932v2
• Date: Tue, 23 Apr 2024 14:45:41 GMT
• ステータス: 処理完了
• システム内更新日: 2024-04-24 20:14:41.051928
• Title: Fully Automatic Neural Network Reduction for Formal Verification
• Title（参考訳）: 形式的検証のための完全自動ニューラルネットワーク削減
• Authors: Tobias Ladner, Matthias Althoff,
• Abstract要約: 到達可能性解析を用いたニューラルネットワークの完全自動・音量低減手法を提案する。 音質は、低減されたネットワークの検証が元のネットワークの検証を必要とすることを保証します。 提案手法は, ニューロンの数を, 小さい外近似で, 元のニューロン数のごく一部に減らすことができることを示す。
• 参考スコア（独自算出の注目度）: 8.017543518311196
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification of neural networks is essential before their deployment in safety-critical applications. However, existing methods for formally verifying neural networks are not yet scalable enough to handle practical problems involving a large number of neurons. We address this challenge by introducing a fully automatic and sound reduction of neural networks using reachability analysis. The soundness ensures that the verification of the reduced network entails the verification of the original network. To the best of our knowledge, we present the first sound reduction approach that is applicable to neural networks with any type of element-wise activation function, such as ReLU, sigmoid, and tanh. The network reduction is computed on the fly while simultaneously verifying the original network and its specifications. All parameters are automatically tuned to minimize the network size without compromising verifiability. We further show the applicability of our approach to convolutional neural networks by explicitly exploiting similar neighboring pixels. Our evaluation shows that our approach can reduce the number of neurons to a fraction of the original number of neurons with minor outer-approximation and thus reduce the verification time to a similar degree.
• Abstract（参考訳）: ニューラルネットワークの形式的検証は、安全クリティカルなアプリケーションにデプロイする前に不可欠である。 しかし、ニューラルネットワークを公式に検証する既存の方法は、多数のニューロンを含む実用的な問題を扱うのに十分なスケーラビリティを持っていない。 我々は、到達可能性分析を用いて、ニューラルネットワークを完全に自動化し、音を下げることによって、この問題に対処する。 音質は、低減されたネットワークの検証が元のネットワークの検証を必要とすることを保証します。 我々の知る限りでは、ReLU、sigmoid、tanhなど、任意の種類の要素活性化関数を持つニューラルネットワークに適用可能な、最初の音量削減手法を提案する。 ネットワークリダクションは、元のネットワークとその仕様を同時に検証しながら、オンザフライで計算される。 すべてのパラメータは自動的に調整され、妥当性を損なうことなくネットワークサイズを最小化する。 さらに、類似の画素を明示的に利用することにより、畳み込みニューラルネットワークへのアプローチの適用性を示す。 評価の結果,本手法は, ニューロンの数を, 外部近似の少ないニューロン数に減らし, 検証時間を同様の程度に短縮できることが示唆された。

関連論文リスト

• Verified Neural Compressed Sensing [58.98637799432153]
  精度の高い計算タスクのために、初めて(私たちの知識を最大限に活用するために)証明可能なニューラルネットワークを開発します。 極小問題次元(最大50)では、線形および双項線形測定からスパースベクトルを確実に回復するニューラルネットワークを訓練できることを示す。 ネットワークの複雑さは問題の難易度に適応できることを示し、従来の圧縮センシング手法が証明不可能な問題を解く。
  論文  参考訳（メタデータ） (2024-05-07T12:20:12Z)
• Graph Neural Networks for Learning Equivariant Representations of Neural Networks [55.04145324152541]
  本稿では,ニューラルネットワークをパラメータの計算グラフとして表現することを提案する。 我々のアプローチは、ニューラルネットワークグラフを多種多様なアーキテクチャでエンコードする単一モデルを可能にする。 本稿では,暗黙的ニューラル表現の分類や編集など,幅広いタスクにおける本手法の有効性を示す。
  論文  参考訳（メタデータ） (2024-03-18T18:01:01Z)
• Expediting Neural Network Verification via Network Reduction [4.8621567234713305]
  本稿では,検証前の事前処理手法として,ネットワーク削減手法を提案する。 提案手法は、安定なReLUニューロンを除去し、それらをシーケンシャルなニューラルネットワークに変換することにより、ニューラルネットワークを削減する。 我々は、最先端の完全および不完全検証ツールの縮小手法をインスタンス化する。
  論文  参考訳（メタデータ） (2023-08-07T06:23:24Z)
• Neural Networks with Sparse Activation Induced by Large Bias: Tighter Analysis with Bias-Generalized NTK [86.45209429863858]
  ニューラル・タンジェント・カーネル(NTK)における一層ReLUネットワークのトレーニングについて検討した。 我々は、ニューラルネットワークが、テクティトビア一般化NTKと呼ばれる異なる制限カーネルを持っていることを示した。 ニューラルネットの様々な特性をこの新しいカーネルで研究する。
  論文  参考訳（メタデータ） (2023-01-01T02:11:39Z)
• Spiking neural network for nonlinear regression [68.8204255655161]
  スパイクニューラルネットワークは、メモリとエネルギー消費を大幅に削減する可能性を持っている。 彼らは、次世代のニューロモルフィックハードウェアによって活用できる時間的および神経的疎結合を導入する。 スパイキングニューラルネットワークを用いた回帰フレームワークを提案する。
  論文  参考訳（メタデータ） (2022-10-06T13:04:45Z)
• Consistency of Neural Networks with Regularization [0.0]
  本稿では,ニューラルネットワークの規則化による一般的な枠組みを提案し,その一貫性を実証する。 双曲関数(Tanh)と整形線形単位(ReLU)の2種類の活性化関数が検討されている。
  論文  参考訳（メタデータ） (2022-06-22T23:33:39Z)
• Why Lottery Ticket Wins? A Theoretical Perspective of Sample Complexity on Pruned Neural Networks [79.74580058178594]
  目的関数の幾何学的構造を解析することにより、刈り取られたニューラルネットワークを訓練する性能を解析する。 本稿では,ニューラルネットワークモデルがプルーニングされるにつれて,一般化が保証された望ましいモデル近傍の凸領域が大きくなることを示す。
  論文  参考訳（メタデータ） (2021-10-12T01:11:07Z)
• Generate and Verify: Semantically Meaningful Formal Analysis of Neural Network Perception Systems [2.2559617939136505]
  ニューラルネットワーク認識システムの精度を評価するためにテストが続けられている。 我々は、モデルが常に基底真理に結びついたある誤差内で推定を生成することを証明するために、ニューラルネットワークの検証を用いる。
  論文  参考訳（メタデータ） (2020-12-16T23:09:53Z)
• Towards Repairing Neural Networks Correctly [6.600380575920419]
  本稿では,ニューラルネットワークの正確性を保証するための実行時検証手法を提案する。 実験結果から,本手法は特性を満たすことが保証されたニューラルネットワークを効果的に生成することが示された。
  論文  参考訳（メタデータ） (2020-12-03T12:31:07Z)
• Compressive sensing with un-trained neural networks: Gradient descent finds the smoothest approximation [60.80172153614544]
  訓練されていない畳み込みニューラルネットワークは、画像の回復と復元に非常に成功したツールとして登場した。 トレーニングされていない畳み込みニューラルネットワークは、ほぼ最小限のランダムな測定値から、十分に構造化された信号や画像を概ね再構成可能であることを示す。
  論文  参考訳（メタデータ） (2020-05-07T15:57:25Z)
• Verifying Recurrent Neural Networks using Invariant Inference [0.0]
  本稿では,リカレントニューラルネットワーク(Recurrent Neural Network)と呼ばれる,ニューラルネットワークの多種多様な特性を検証するための新しいアプローチを提案する。 この手法は不変量の推論に基づいており、再帰的ネットワークを単純かつ非再帰的な問題に検証する際の複雑な問題を軽減できる。
  論文  参考訳（メタデータ） (2020-04-06T08:08:24Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。