論文の概要: Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification
- arxiv url: http://arxiv.org/abs/2407.21029v1
- Date: Mon, 15 Jul 2024 11:49:44 GMT
- ステータス: 処理完了
- システム内更新日: 2024-08-05 00:46:38.892546
- Title: Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification
- Title（参考訳）: 形式検証のためのバイナリ・トレー・ガウスプロセスによるデータ駆動抽象化
- Authors: Oliver Schön, Shammakh Naseer, Ben Wooding, Sadegh Soudjani,
- Abstract要約: ガウス過程(GP)回帰に基づく抽象的解は、量子化された誤差を持つデータから潜在システムの表現を学習する能力で人気を博している。
二分木ガウス過程(BTGP)により未知系のマルコフ連鎖モデルを構築することができることを示す。
BTGPの関数空間に真の力学が存在しない場合でも、統一公式による非局在誤差量子化を提供する。
- 参考スコア（独自算出の注目度）: 0.22499166814992438
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: To advance formal verification of stochastic systems against temporal logic requirements for handling unknown dynamics, researchers have been designing data-driven approaches inspired by breakthroughs in the underlying machine learning techniques. As one promising research direction, abstraction-based solutions based on Gaussian process (GP) regression have become popular for their ability to learn a representation of the latent system from data with a quantified error. Results obtained based on this model are then translated to the true system via various methods. In a recent publication, GPs using a so-called binary-tree kernel have demonstrated a polynomial speedup w.r.t. the size of the data compared to their vanilla version, outcompeting all existing sparse GP approximations. Incidentally, the resulting binary-tree Gaussian process (BTGP) is characteristic for its piecewise-constant posterior mean and covariance functions, naturally abstracting the input space into discrete partitions. In this paper, we leverage this natural abstraction of the BTGP for formal verification, eliminating the need for cumbersome abstraction and error quantification procedures. We show that the BTGP allows us to construct an interval Markov chain model of the unknown system with a speedup that is polynomial w.r.t. the size of the abstraction compared to alternative approaches. We provide a delocalized error quantification via a unified formula even when the true dynamics do not live in the function space of the BTGP. This allows us to compute upper and lower bounds on the probability of satisfying reachability specifications that are robust to both aleatoric and epistemic uncertainties.
- Abstract（参考訳）: 未知のダイナミクスを扱うための時間論理的要求に対する確率システムの形式的検証を進めるために、研究者たちは、基礎となる機械学習技術のブレークスルーにインスパイアされたデータ駆動アプローチを設計してきた。
1つの有望な研究方向として、ガウス過程(GP)回帰に基づく抽象化ベースのソリューションは、量子化された誤差を持つデータから潜在システムの表現を学習する能力で人気を博している。
このモデルに基づいて得られた結果は、様々な方法で実際のシステムに変換される。
最近の出版物では、いわゆるバイナリツリーカーネルを用いたGPは、バニラバージョンと比較してデータのサイズが多項式スピードアップすることを示した。
ちなみに、結果として生じる二分木ガウス過程(BTGP)は、その断片的に一貫した後続平均と共分散関数の特徴であり、入力空間を離散分割に自然に抽象化する。
本稿では,BTGPのこの自然な抽象化を形式的検証に活用し,煩雑な抽象化や誤り量化処理の不要さを解消する。
BTGPは未知系のインターバルマルコフ連鎖モデルを構築することができることを示す。
BTGPの関数空間に真の力学が存在しない場合でも、統一公式による非局在誤差量子化を提供する。
これにより、アレタリックおよびエピステマティックな不確実性の両方に対して堅牢な到達可能性仕様を満たす確率の上限と下限を計算することができる。
関連論文リスト
- Conditionally-Conjugate Gaussian Process Factor Analysis for Spike Count Data via Data Augmentation [8.114880112033644]
近年、GPFAはスパイクカウントデータをモデル化するために拡張されている。
本稿では,解析的および計算的抽出可能な推論が可能な条件共役型ガウス過程因子解析(ccGPFA)を提案する。
論文 参考訳（メタデータ） (2024-05-19T21:53:36Z) - Data-driven Modeling and Inference for Bayesian Gaussian Process ODEs
via Double Normalizing Flows [28.62579476863723]
本稿では,ODEベクトル場を再パラメータ化するために正規化フローを導入し,データ駆動の事前分布を導出する。
また, GP ODE の後部推定に正規化フローを適用し, 強平均場仮定の問題を解く。
シミュレーション力学系と実世界の人間の動作データに対するアプローチの有効性を検証した。
論文 参考訳（メタデータ） (2023-09-17T09:28:47Z) - Score-based Diffusion Models in Function Space [140.792362459734]
拡散モデルは、最近、生成モデリングの強力なフレームワークとして登場した。
本稿では,関数空間における拡散モデルをトレーニングするためのDDO(Denoising Diffusion Operators)という,数学的に厳密なフレームワークを提案する。
データ解像度に依存しない固定コストで、対応する離散化アルゴリズムが正確なサンプルを生成することを示す。
論文 参考訳（メタデータ） (2023-02-14T23:50:53Z) - FaDIn: Fast Discretized Inference for Hawkes Processes with General
Parametric Kernels [82.53569355337586]
この研究は、有限なサポートを持つ一般パラメトリックカーネルを用いた時間点プロセス推論の効率的な解を提供する。
脳磁図(MEG)により記録された脳信号からの刺激誘発パターンの発生をモデル化し,その有効性を評価する。
その結果,提案手法により,最先端技術よりもパターン遅延の推定精度が向上することが示唆された。
論文 参考訳（メタデータ） (2022-10-10T12:35:02Z) - Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression [11.729744197698718]
安全クリティカルなシナリオにおける自律システムの活用には、不確実性の存在下での行動を検証する必要がある。
本研究では,非モデル化された力学と雑音測定を用いた離散時間力学システムの検証フレームワークを開発した。
論文 参考訳（メタデータ） (2021-12-31T05:10:05Z) - Inverting brain grey matter models with likelihood-free inference: a
tool for trustable cytoarchitecture measurements [62.997667081978825]
脳の灰白質細胞構造の特徴は、体密度と体積に定量的に敏感であり、dMRIでは未解決の課題である。
我々は新しいフォワードモデル、特に新しい方程式系を提案し、比較的スパースなb殻を必要とする。
次に,提案手法を逆転させるため,確率自由推論 (LFI) として知られるベイズ解析から最新のツールを適用した。
論文 参考訳（メタデータ） (2021-11-15T09:08:27Z) - Non-Gaussian Gaussian Processes for Few-Shot Regression [71.33730039795921]
乱変数ベクトルの各成分上で動作し,パラメータを全て共有する可逆なODEベースのマッピングを提案する。
NGGPは、様々なベンチマークとアプリケーションに対する競合する最先端のアプローチよりも優れています。
論文 参考訳（メタデータ） (2021-10-26T10:45:25Z) - Bayesian inference of ODEs with Gaussian processes [17.138448665454373]
本稿では、ガウス過程を用いて未知のODEシステムの後部をデータから直接推測する新しいベイズ非パラメトリックモデルを提案する。
ベクトル場後部を表すために,分離された関数型サンプリングを用いてスパース変分推論を導出する。
この手法はベクトル場後部演算の利点を示し、予測不確実性スコアは複数のODE学習タスクにおける代替手法よりも優れている。
論文 参考訳（メタデータ） (2021-06-21T08:09:17Z) - Probabilistic Numeric Convolutional Neural Networks [80.42120128330411]
画像や時系列などの連続的な入力信号は、不規則にサンプリングされたり、値が欠けていたりすることは、既存のディープラーニング手法では困難である。
ガウス過程(GP)として特徴を表す確率的畳み込みニューラルネットワークを提案する。
次に、畳み込み層を、このGP上で定義されたPDEの進化として定義し、次いで非線形性とする。
実験では,SuperPixel-MNISTデータセットの先行技術と医療時間2012データセットの競合性能から,提案手法の誤差を3倍に削減できることが示されている。
論文 参考訳（メタデータ） (2020-10-21T10:08:21Z) - Weak SINDy For Partial Differential Equations [0.0]
我々はWeak SINDy(WSINDy)フレームワークを偏微分方程式(PDE)の設定にまで拡張する。
弱い形状による点微分近似の除去は、ノイズフリーデータからモデル係数の効率的な機械的精度回復を可能にする。
我々は、いくつかの挑戦的なPDEに対して、WSINDyの堅牢性、速度、精度を実証する。
論文 参考訳（メタデータ） (2020-07-06T16:03:51Z) - The data-driven physical-based equations discovery using evolutionary
approach [77.34726150561087]
与えられた観測データから数学的方程式を発見するアルゴリズムについて述べる。
このアルゴリズムは遺伝的プログラミングとスパース回帰を組み合わせたものである。
解析方程式の発見や偏微分方程式(PDE)の発見にも用いられる。
論文 参考訳（メタデータ） (2020-04-03T17:21:57Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。