論文の概要: Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models

• arxiv url: http://arxiv.org/abs/2007.03251v2
• Date: Mon, 19 Oct 2020 13:27:10 GMT
• ステータス: 処理完了
• システム内更新日: 2022-11-12 20:44:33.205827
• Title: Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models
• Title（参考訳）: 動的モデルのためのニューラルバリア証明書の自動および形式的合成
• Authors: Andrea Peruffo, Daniele Ahmed, Alessandro Abate
• Abstract要約: バリア証明書(BC)の自動的,形式的,反例に基づく合成手法を提案する。 このアプローチは、ニューラルネットワークとして構造化されたBCの候補を操作する誘導的フレームワークと、その候補の有効性を認証するか、反例を生成する音検証器によって支えられている。 その結果,音のBCsを最大2桁の速度で合成できることがわかった。
• 参考スコア（独自算出の注目度）: 70.70479436076238
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) for the safety verification of continuous and hybrid dynamical models. The approach is underpinned by an inductive framework: this is structured as a sequential loop between a learner, which manipulates a candidate BC structured as a neural network, and a sound verifier, which either certifies the candidate's validity or generates counter-examples to further guide the learner. We compare the approach against state-of-the-art techniques, over polynomial and non-polynomial dynamical models: the outcomes show that we can synthesise sound BCs up to two orders of magnitude faster, with in particular a stark speedup on the verification engine (up to five orders less), whilst needing a far smaller data set (up to three orders less) for the learning part. Beyond improvements over the state of the art, we further challenge the new approach on a hybrid dynamical model and on larger-dimensional models, and showcase the numerical robustness of our algorithms and codebase.
• Abstract（参考訳）: 連続およびハイブリッド力学モデルの安全性検証のために, 自動的, 形式的, 反例ベースでバリア証明書(bc)を合成する手法を提案する。 この手法は、ニューラルネットワークとして構造化されたBCの候補を操作する学習者と、その候補の有効性を証明するか、さらに学習者を導くために反例を生成する音響検証者との間で、逐次ループとして構成される。 結果、より小さなデータセット(最大3桁以下)を必要とする一方で、特に検証エンジンの大幅な高速化(最大5桁以下)によって、音のbcsを最大2桁速く合成できることが示されています。 技術状況の改善以外にも、ハイブリッドな動的モデルと大規模モデルの新たなアプローチに挑戦し、我々のアルゴリズムとコードベースの数値的堅牢性を示す。

関連論文リスト

• On the Trade-off Between Efficiency and Precision of Neural Abstraction [62.046646433536104]
  ニューラル抽象化は、最近、複雑な非線形力学モデルの形式近似として導入されている。 我々は形式的帰納的合成法を用いて、これらのセマンティクスを用いた動的モデルをもたらすニューラル抽象化を生成する。
  論文  参考訳（メタデータ） (2023-07-28T13:22:32Z)
• Dynamic Mixed Membership Stochastic Block Model for Weighted Labeled Networks [3.5450828190071655]
  混合メンバシップブロックモデル(MMSBM)の新たなファミリーは、混合メンバシップクラスタリングを前提として静的ラベル付きネットワークをモデル化することができる。 提案手法は既存手法とは大きく異なり,より複雑なシステム - 動的ラベル付きネットワークをモデル化できることを示す。
  論文  参考訳（メタデータ） (2023-04-12T15:01:03Z)
• ConCerNet: A Contrastive Learning Based Framework for Automated Conservation Law Discovery and Trustworthy Dynamical System Prediction [82.81767856234956]
  本稿では,DNNに基づく動的モデリングの信頼性を向上させるために,ConCerNetという新しい学習フレームワークを提案する。 本手法は, 座標誤差と保存量の両方において, ベースラインニューラルネットワークよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-02-11T21:07:30Z)
• Neural Abstractions [72.42530499990028]
  本稿では,ニューラルネットワークを用いた非線形力学モデルの安全性検証手法を提案する。 提案手法は,既存のベンチマーク非線形モデルにおいて,成熟度の高いFlow*と同等に動作することを示す。
  論文  参考訳（メタデータ） (2023-01-27T12:38:09Z)
• Evolve Smoothly, Fit Consistently: Learning Smooth Latent Dynamics For Advection-Dominated Systems [14.553972457854517]
  複雑な物理系のサロゲートモデルを学ぶための,データ駆動・時空連続フレームワークを提案する。 ネットワークの表現力と特別に設計された整合性誘導正規化を利用して,低次元かつ滑らかな潜在軌道を得る。
  論文  参考訳（メタデータ） (2023-01-25T03:06:03Z)
• Dynamically-Scaled Deep Canonical Correlation Analysis [77.34726150561087]
  カノニカル相関解析 (CCA) は, 2つのビューの特徴抽出手法である。 本稿では,入力依存の正準相関モデルをトレーニングするための新しい動的スケーリング手法を提案する。
  論文  参考訳（メタデータ） (2022-03-23T12:52:49Z)
• Contrastively Disentangled Sequential Variational Autoencoder [20.75922928324671]
  本稿では,C-DSVAE(Contrastively Disentangled Sequential Variational Autoencoder)という新しいシーケンス表現学習手法を提案する。 我々は,静的因子と動的因子の相互情報をペナルティ化しながら,入力と潜伏因子の相互情報を最大化する新しいエビデンスローバウンドを用いる。 実験の結果、C-DSVAEは従来の最先端の手法よりも優れていたことが判明した。
  論文  参考訳（メタデータ） (2021-10-22T23:00:32Z)
• The Role of Isomorphism Classes in Multi-Relational Datasets [6.419762264544509]
  アイソモーフィックリークは,マルチリレーショナル推論の性能を過大評価することを示す。 モデル評価のためのアイソモーフィック・アウェア・シンセサイティング・ベンチマークを提案する。 また、同型類は単純な優先順位付けスキームによって利用することができることを示した。
  論文  参考訳（メタデータ） (2020-09-30T12:15:24Z)
• Forecasting Sequential Data using Consistent Koopman Autoencoders [52.209416711500005]
  クープマン理論に関連する新しい物理学に基づく手法が導入された。 本稿では,既存の作業の多くと異なり,前方・後方のダイナミクスを生かした新しいコンシスタント・クープマン・オートエンコーダモデルを提案する。 このアプローチの鍵となるのは、一貫性のある力学と関連するクープマン作用素との相互作用を探索する新しい解析である。
  論文  参考訳（メタデータ） (2020-03-04T18:24:30Z)

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

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