論文の概要: Neural Abstractions

• arxiv url: http://arxiv.org/abs/2301.11683v1
• Date: Fri, 27 Jan 2023 12:38:09 GMT
• ステータス: 処理完了
• システム内更新日: 2023-01-30 15:46:26.606139
• Title: Neural Abstractions
• Title（参考訳）: 神経抽象化
• Authors: Alessandro Abate, Alec Edwards, Mirco Giacobbe
• Abstract要約: 本稿では,ニューラルネットワークを用いた非線形力学モデルの安全性検証手法を提案する。 提案手法は,既存のベンチマーク非線形モデルにおいて,成熟度の高いFlow*と同等に動作することを示す。
• 参考スコア（独自算出の注目度）: 72.42530499990028
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present a novel method for the safety verification of nonlinear dynamical models that uses neural networks to represent abstractions of their dynamics. Neural networks have extensively been used before as approximators; in this work, we make a step further and use them for the first time as abstractions. For a given dynamical model, our method synthesises a neural network that overapproximates its dynamics by ensuring an arbitrarily tight, formally certified bound on the approximation error. For this purpose, we employ a counterexample-guided inductive synthesis procedure. We show that this produces a neural ODE with non-deterministic disturbances that constitutes a formal abstraction of the concrete model under analysis. This guarantees a fundamental property: if the abstract model is safe, i.e., free from any initialised trajectory that reaches an undesirable state, then the concrete model is also safe. By using neural ODEs with ReLU activation functions as abstractions, we cast the safety verification problem for nonlinear dynamical models into that of hybrid automata with affine dynamics, which we verify using SpaceEx. We demonstrate that our approach performs comparably to the mature tool Flow* on existing benchmark nonlinear models. We additionally demonstrate and that it is effective on models that do not exhibit local Lipschitz continuity, which are out of reach to the existing technologies.
• Abstract（参考訳）: 本稿では,ニューラルネットワークを用いた非線形力学モデルの安全性検証手法を提案する。 ニューラルネットワークは従来,近似器として広く用いられてきた。この研究では,さらに一歩進めて,初めて抽象化として使用する。 与えられた力学モデルに対して,本手法は,近似誤差に対して任意にタイトかつ正式に認定された境界を保証することによって,そのダイナミクスを近似するニューラルネットワークを合成する。 本研究では,逆例誘導型誘導合成法を用いる。 解析対象の具体的なモデルの形式的抽象化を構成する非決定論的乱れを持つニューラルODEが生成されることを示す。 これは基本的な特性を保証する: 抽象モデルが安全である、すなわち、望ましくない状態に達する初期化軌道から解放された場合、具体的なモデルもまた安全である。 reluアクティベーション関数を持つニューラルodeを抽象化として使用することにより,非線形力学モデルの安全性検証問題をアフィンダイナミクスを用いたハイブリッドオートマトンにキャストし,spaceexを用いて検証した。 提案手法は,既存のベンチマーク非線形モデルにおいて,成熟度の高いFlow*と同等に動作することを示す。 さらに,既存の技術には届かない局所的なリプシッツ連続性を発現しないモデルに対して有効であることを示す。

関連論文リスト

• The Edge-of-Reach Problem in Offline Model-Based Reinforcement Learning [37.387280102209274]
  オフライン強化学習は、事前に収集されたデータセットからエージェントをトレーニング可能にすることを目的としている。 モデルベースの手法は、エージェントが学習されたダイナミックスモデルでロールアウトを介して追加の合成データを収集できるようにすることで、ソリューションを提供する。 しかし、学習したダイナミックスモデルを真のエラーフリーなダイナミックスに置き換えると、既存のモデルベースのメソッドは完全に失敗する。 本稿では, エッジ・オブ・リーチ問題に直接対処する単純で堅牢な手法であるReach-Aware Value Learning (RAVL)を提案する。
  論文  参考訳（メタデータ） (2024-02-19T20:38:00Z)
• Symmetry-regularized neural ordinary differential equations [0.0]
  本稿では,隠れ状態のダイナミクスとバック伝播のダイナミクスの両方において,Lie対称性を用いたニューラルODEの新たな保存関係を提案する。 これらの保存法則は、損失関数にさらなる正規化項として組み込まれ、モデルの物理的解釈可能性や一般化可能性を高める可能性がある。 これらの保存関係から新たな損失関数を構築し、典型的なモデリングタスクにおける対称性規則化ニューラル・オードの適用性を示す。
  論文  参考訳（メタデータ） (2023-11-28T09:27:44Z)
• On the Trade-off Between Efficiency and Precision of Neural Abstraction [62.046646433536104]
  ニューラル抽象化は、最近、複雑な非線形力学モデルの形式近似として導入されている。 我々は形式的帰納的合成法を用いて、これらのセマンティクスを用いた動的モデルをもたらすニューラル抽象化を生成する。
  論文  参考訳（メタデータ） (2023-07-28T13:22:32Z)
• Learning solution of nonlinear constitutive material models using physics-informed neural networks: COMM-PINN [0.0]
  非線形, 経路依存的な物質挙動の関係を解くために, 物理インフォームドニューラルネットワークを適用した。 この研究の利点の1つは、複雑な物質モデルにおける非線形方程式を解くのに必要な反復ニュートン反復をバイパスすることである。
  論文  参考訳（メタデータ） (2023-04-10T19:58:49Z)
• Capturing dynamical correlations using implicit neural representations [85.66456606776552]
  実験データから未知のパラメータを復元するために、モデルハミルトンのシミュレーションデータを模倣するために訓練されたニューラルネットワークと自動微分を組み合わせた人工知能フレームワークを開発する。 そこで本研究では, 実時間から多次元散乱データに適用可能な微分可能なモデルを1回だけ構築し, 訓練する能力について述べる。
  論文  参考訳（メタデータ） (2023-04-08T07:55:36Z)
• Bridging the Model-Reality Gap with Lipschitz Network Adaptation [22.499090318313662]
  ロボットが現実世界に進出するにつれ、ロボットは非モデル化された力学と乱れにさらされる。 従来のモデルベースの制御アプローチは、比較的静的で既知の運用環境で成功している。 本稿では,モデルと現実のギャップを埋め,動的不確実性が存在する場合でもモデルに基づくアプローチの適用を可能にする手法を提案する。
  論文  参考訳（メタデータ） (2021-12-07T15:12:49Z)
• Closed-form Continuous-Depth Models [99.40335716948101]
  連続深度ニューラルモデルは高度な数値微分方程式解法に依存している。 我々は,CfCネットワークと呼ばれる,記述が簡単で,少なくとも1桁高速な新しいモデル群を提示する。
  論文  参考訳（メタデータ） (2021-06-25T22:08:51Z)
• Sparse Flows: Pruning Continuous-depth Models [107.98191032466544]
  生成モデルにおいて,プルーニングによりニューラルネットワークの一般化が向上することを示す。 また、プルーニングは、元のネットワークに比べて最大98%少ないパラメータで、精度を損なうことなく、最小かつ効率的なニューラルODE表現を見出すことを示した。
  論文  参考訳（メタデータ） (2021-06-24T01:40:17Z)
• Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models [70.70479436076238]
  バリア証明書(BC)の自動的,形式的,反例に基づく合成手法を提案する。 このアプローチは、ニューラルネットワークとして構造化されたBCの候補を操作する誘導的フレームワークと、その候補の有効性を認証するか、反例を生成する音検証器によって支えられている。 その結果,音のBCsを最大2桁の速度で合成できることがわかった。
  論文  参考訳（メタデータ） (2020-07-07T07:39:42Z)

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

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