論文の概要: Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers

• arxiv url: http://arxiv.org/abs/2202.05207v1
• Date: Thu, 10 Feb 2022 18:09:23 GMT
• ステータス: 処理完了
• システム内更新日: 2022-02-11 18:15:33.621581
• Title: Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers
• Title（参考訳）: vehicle: 対話型定理プロバーを用いたニューラルネットワーク検証器
• Authors: Matthew L. Daggitt, Wen Kokke, Robert Atkey, Luca Arnaboldi, Ekaterina Komendantskya
• Abstract要約: 車両には、ニューラルネットワーク仕様を記述するための表現力のあるドメイン固有言語が備わっている。 同様のITPの形式化において、保守性とスケーラビリティに関する過去の問題を克服しています。 ニューラルネットワーク検証器であるMarabouをAgdaに接続し、ニューラルネットワークで操縦された車が道路を離れないことを正式に検証することで、その実用性を実証する。
• 参考スコア（独自算出の注目度）: 1.5749416770494706
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Verification of neural networks is currently a hot topic in automated theorem proving. Progress has been rapid and there are now a wide range of tools available that can verify properties of networks with hundreds of thousands of nodes. In theory this opens the door to the verification of larger control systems that make use of neural network components. However, although work has managed to incorporate the results of these verifiers to prove larger properties of individual systems, there is currently no general methodology for bridging the gap between verifiers and interactive theorem provers (ITPs). In this paper we present Vehicle, our solution to this problem. Vehicle is equipped with an expressive domain specific language for stating neural network specifications which can be compiled to both verifiers and ITPs. It overcomes previous issues with maintainability and scalability in similar ITP formalisations by using a standard ONNX file as the single canonical representation of the network. We demonstrate its utility by using it to connect the neural network verifier Marabou to Agda and then formally verifying that a car steered by a neural network never leaves the road, even in the face of an unpredictable cross wind and imperfect sensors. The network has over 20,000 nodes, and therefore this proof represents an improvement of 3 orders of magnitude over prior proofs about neural network enhanced systems in ITPs.
• Abstract（参考訳）: ニューラルネットワークの検証は現在、自動定理証明のホットトピックである。 進歩は急速に進み、数十万のノードを持つネットワークの特性を検証できる幅広いツールが利用可能になった。 理論的には、これはニューラルネットワークコンポーネントを使用するより大きな制御システムの検証への扉を開く。 しかしながら、これらの検証器の結果を個々のシステムのより大きな性質を証明するためにうまく組み入れてきたが、現在では検証器と対話的定理証明器(ITP)のギャップを埋めるための一般的な方法論はない。 本稿では,この問題に対する我々の解決策である車両について述べる。 車両は、検証者およびIPPの両方にコンパイル可能なニューラルネットワーク仕様を記述するための表現力豊かなドメイン固有言語を備えている。 ネットワークの単一標準表現として標準のNNXファイルを使用することで、同様のIPP形式における保守性とスケーラビリティに関する過去の問題を克服する。 ニューラルネットワーク検証器であるmarabouをagdaに接続し、予測不能なクロスウインドと不完全なセンサーに直面しても、ニューラルネットワークが操縦する車が道路を離れないことを正式に検証することで、その有用性を実証する。 ネットワークには20,000以上のノードがあり、この証明はIPPのニューラルネットワーク強化システムに関する以前の証明よりも3桁の精度向上を示している。

関連論文リスト

• Verified Neural Compressed Sensing [58.98637799432153]
  精度の高い計算タスクのために、初めて(私たちの知識を最大限に活用するために)証明可能なニューラルネットワークを開発します。 極小問題次元(最大50)では、線形および双項線形測定からスパースベクトルを確実に回復するニューラルネットワークを訓練できることを示す。 ネットワークの複雑さは問題の難易度に適応できることを示し、従来の圧縮センシング手法が証明不可能な問題を解く。
  論文  参考訳（メタデータ） (2024-05-07T12:20:12Z)
• Deep Neural Networks Tend To Extrapolate Predictably [51.303814412294514]
  ニューラルネットワークの予測は、アウト・オブ・ディストリビューション(OOD)入力に直面した場合、予測不可能で過信される傾向がある。 我々は、入力データがOODになるにつれて、ニューラルネットワークの予測が一定値に向かう傾向があることを観察する。 我々は、OOD入力の存在下でリスクに敏感な意思決定を可能にするために、私たちの洞察を実際に活用する方法を示します。
  論文  参考訳（メタデータ） (2023-10-02T03:25:32Z)
• How neural networks learn to classify chaotic time series [77.34726150561087]
  本研究では,通常の逆カオス時系列を分類するために訓練されたニューラルネットワークの内部動作について検討する。 入力周期性とアクティベーション周期の関係は,LKCNNモデルの性能向上の鍵となる。
  論文  参考訳（メタデータ） (2023-06-04T08:53:27Z)
• Fully Automatic Neural Network Reduction for Formal Verification [8.017543518311196]
  到達可能性解析を用いたニューラルネットワークの完全自動・音量低減手法を提案する。 音質は、低減されたネットワークの検証が元のネットワークの検証を必要とすることを保証します。 提案手法は, ニューロンの数を, 小さい外近似で, 元のニューロン数のごく一部に減らすことができることを示す。
  論文  参考訳（メタデータ） (2023-05-03T07:13:47Z)
• 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)
• Consistency of Neural Networks with Regularization [0.0]
  本稿では,ニューラルネットワークの規則化による一般的な枠組みを提案し,その一貫性を実証する。 双曲関数(Tanh)と整形線形単位(ReLU)の2種類の活性化関数が検討されている。
  論文  参考訳（メタデータ） (2022-06-22T23:33:39Z)
• Neuro-Symbolic Verification of Deep Neural Networks [20.973078277539276]
  本稿ではニューラルシンボリック検証という,ニューラルネットワークの検証のための新しいフレームワークを提案する。 重要なアイデアは、論理的な仕様の一部としてニューラルネットワークを使用することだ。 本稿では,ニューラルネットワークの既存の検証基盤上に,ニューロシンボリック検証をどのように実装できるかを示す。
  論文  参考訳（メタデータ） (2022-03-02T08:40:01Z)
• Why Lottery Ticket Wins? A Theoretical Perspective of Sample Complexity on Pruned Neural Networks [79.74580058178594]
  目的関数の幾何学的構造を解析することにより、刈り取られたニューラルネットワークを訓練する性能を解析する。 本稿では,ニューラルネットワークモデルがプルーニングされるにつれて,一般化が保証された望ましいモデル近傍の凸領域が大きくなることを示す。
  論文  参考訳（メタデータ） (2021-10-12T01:11:07Z)
• Scalable Verification of Quantized Neural Networks (Technical Report) [14.04927063847749]
  ビットベクトル仕様を持つ量子化ニューラルネットワークのビットエクササイズ実装はPSPACEハードであることを示す。 量子化されたニューラルネットワークのSMTに基づく検証をよりスケーラブルにするための3つの手法を提案する。
  論文  参考訳（メタデータ） (2020-12-15T10:05:37Z)
• Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming [97.40955121478716]
  本稿では,ネットワークアクティベーションの総数にのみ線形なメモリを必要とする一階二重SDPアルゴリズムを提案する。 L-inf の精度は 1% から 88% ,6% から 40% に改善した。 また,変分オートエンコーダの復号器に対する2次安定性仕様の厳密な検証を行った。
  論文  参考訳（メタデータ） (2020-10-22T12:32:29Z)
• Firearm Detection and Segmentation Using an Ensemble of Semantic Neural Networks [62.997667081978825]
  本稿では,意味的畳み込みニューラルネットワークのアンサンブルに基づく兵器検出システムを提案する。 特定のタスクに特化した単純なニューラルネットワークのセットは、計算リソースを少なくし、並列にトレーニングすることができる。 個々のネットワークの出力の集約によって与えられるシステムの全体的な出力は、ユーザが偽陽性と偽陰性とをトレードオフするように調整することができる。
  論文  参考訳（メタデータ） (2020-02-11T13:58:16Z)

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

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