論文の概要: Scalable Stochastic Parametric Verification with Stochastic Variational
Smoothed Model Checking
- arxiv url: http://arxiv.org/abs/2205.05398v3
- Date: Thu, 6 Apr 2023 10:53:49 GMT
- ステータス: 処理完了
- システム内更新日: 2023-04-07 18:22:01.327455
- Title: Scalable Stochastic Parametric Verification with Stochastic Variational
Smoothed Model Checking
- Title（参考訳）: 確率変動平滑モデル検査によるスケーラブル確率パラメトリック検証
- Authors: Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, Paolo Pulcini
- Abstract要約: 平滑モデル検査 (smMC) は, パラメータ空間全体の満足度関数を, 限られた観測値から推定することを目的としている。
本稿では,確率論的機械学習の最近の進歩を利用して,この限界を推し進める。
構成された満足度関数のスケーラビリティ,計算効率,精度を調べた結果,smMCとSV-smMCの性能を比較した。
- 参考スコア（独自算出の注目度）: 1.5293427903448025
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Parametric verification of linear temporal properties for stochastic models
can be expressed as computing the satisfaction probability of a certain
property as a function of the parameters of the model. Smoothed model checking
(smMC) aims at inferring the satisfaction function over the entire parameter
space from a limited set of observations obtained via simulation. As
observations are costly and noisy, smMC is framed as a Bayesian inference
problem so that the estimates have an additional quantification of the
uncertainty. In smMC the authors use Gaussian Processes (GP), inferred by means
of the Expectation Propagation algorithm. This approach provides accurate
reconstructions with statistically sound quantification of the uncertainty.
However, it inherits the well-known scalability issues of GP. In this paper, we
exploit recent advances in probabilistic machine learning to push this
limitation forward, making Bayesian inference of smMC scalable to larger
datasets and enabling its application to models with high dimensional parameter
spaces. We propose Stochastic Variational Smoothed Model Checking (SV-smMC), a
solution that exploits stochastic variational inference (SVI) to approximate
the posterior distribution of the smMC problem. The strength and flexibility of
SVI make SV-smMC applicable to two alternative probabilistic models: Gaussian
Processes (GP) and Bayesian Neural Networks (BNN). The core ingredient of SVI
is a stochastic gradient-based optimization that makes inference easily
parallelizable and that enables GPU acceleration. In this paper, we compare the
performances of smMC against those of SV-smMC by looking at the scalability,
the computational efficiency and the accuracy of the reconstructed satisfaction
function.
- Abstract（参考訳）: 確率モデルの線形時間特性のパラメトリック検証は、ある性質の満足度確率をモデルのパラメータの関数として計算するものとして表現することができる。
スムースドモデル検査 (smMC) は, パラメータ空間全体の満足度関数をシミュレーションによって得られた限られた観測値から推定することを目的としている。
観測は高価でノイズが多いため、smMCはベイズ推定問題としてフレーム化され、推定値が不確実性のさらなる定量化を行う。
smmcでは、著者らは期待伝播アルゴリズムによって推定されるガウス過程(gp)を用いる。
このアプローチは、統計的に不確実性の定量化を伴う正確な再構成を提供する。
しかし、GPの有名なスケーラビリティ問題を継承している。
本稿では、確率論的機械学習の最近の進歩を活用し、この制限を推し進め、ベイジアン推定のsmMCを大規模データセットにスケーラブルにし、高次元パラメータ空間を持つモデルに適用できるようにする。
本稿では,SVI(Stochastic Variational Inference)を利用して,smMC問題の後部分布を近似する手法であるStochastic Variational Smoothed Model Checking (SV-smMC)を提案する。
SVIの強度と柔軟性により、SV-smMCはガウス過程(GP)とベイズニューラルネットワーク(BNN)の2つの代替確率モデルに適用できる。
SVIの中核となる要素は確率勾配に基づく最適化であり、推論を容易に並列化し、GPUアクセラレーションを可能にする。
本稿では,SmMCとSV-smMCの性能を比較し,その拡張性,計算効率,再現された満足度関数の精度について検討する。
関連論文リスト
- Variational Bayesian surrogate modelling with application to robust design optimisation [0.9626666671366836]
サロゲートモデルは複雑な計算モデルに対して素早く評価できる近似を提供する。
入力の不確かさと次元減少を伴う統計的代理を構築するためのベイズ推定について考察する。
コスト関数がモデル出力の平均および標準偏差の重み付け和に依存するような本質的で頑健な構造最適化問題を示す。
論文 参考訳（メタデータ） (2024-04-23T09:22:35Z) - Online Variational Sequential Monte Carlo [49.97673761305336]
我々は,計算効率が高く正確なモデルパラメータ推定とベイジアン潜在状態推定を提供する変分連続モンテカルロ法(VSMC)を構築した。
オンラインVSMCは、パラメータ推定と粒子提案適応の両方を効率よく、完全にオンザフライで実行することができる。
論文 参考訳（メタデータ） (2023-12-19T21:45:38Z) - Monte Carlo Neural PDE Solver for Learning PDEs via Probabilistic Representation [59.45669299295436]
教師なしニューラルソルバのトレーニングのためのモンテカルロPDEソルバを提案する。
我々は、マクロ現象をランダム粒子のアンサンブルとみなすPDEの確率的表現を用いる。
対流拡散, アレン・カーン, ナヴィエ・ストークス方程式に関する実験により, 精度と効率が著しく向上した。
論文 参考訳（メタデータ） (2023-02-10T08:05:19Z) - Numerically Stable Sparse Gaussian Processes via Minimum Separation
using Cover Trees [57.67528738886731]
誘導点に基づくスケーラブルスパース近似の数値安定性について検討する。
地理空間モデリングなどの低次元タスクに対しては,これらの条件を満たす点を自動計算する手法を提案する。
論文 参考訳（メタデータ） (2022-10-14T15:20:17Z) - 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) - Information Theoretic Structured Generative Modeling [13.117829542251188]
構造生成モデル (Structured Generative Model, SGM) と呼ばれる新しい生成モデルフレームワークが提案され, 簡単な最適化が可能となった。
この実装では、無限のガウス混合モデルを学習するために適合した単一白色ノイズ源への正則入力によって駆動される1つのニューラルネットワークを採用している。
予備的な結果は、SGMがデータ効率と分散、従来のガウス混合モデルと変分混合モデル、および敵ネットワークのトレーニングにおいてMINE推定を著しく改善することを示している。
論文 参考訳（メタデータ） (2021-10-12T07:44:18Z) - Structured Stochastic Gradient MCMC [20.68905354115655]
近似した後方関数形式を仮定しない新しい非パラメトリック変分近似を提案する。
完全なSGMCMCよりも優れた予測可能性と有効試料サイズが得られる。
論文 参考訳（メタデータ） (2021-07-19T17:18:10Z) - Sinkhorn Natural Gradient for Generative Models [125.89871274202439]
本研究では,シンクホーンの発散による確率空間上の最も急降下法として機能するシンクホーン自然勾配(SiNG)アルゴリズムを提案する。
本稿では,SiNG の主要成分であるシンクホーン情報行列 (SIM) が明示的な表現を持ち,対数的スケールの複雑さを正確に評価できることを示す。
本実験では,SiNGと最先端のSGD型解法を定量的に比較し,その有効性と有効性を示す。
論文 参考訳（メタデータ） (2020-11-09T02:51:17Z) - An adaptive Hessian approximated stochastic gradient MCMC method [12.93317525451798]
後方からのサンプリング中に局所的幾何情報を組み込む適応型ヘッセン近似勾配MCMC法を提案する。
我々は,ネットワークの空間性を高めるために,等級に基づく重み付け法を採用する。
論文 参考訳（メタデータ） (2020-10-03T16:22:15Z) - Improving Sampling Accuracy of Stochastic Gradient MCMC Methods via
Non-uniform Subsampling of Gradients [54.90670513852325]
サンプリング精度を向上させるための一様でないサブサンプリング手法を提案する。
EWSGは、一様勾配MCMC法がバッチ勾配MCMC法の統計的挙動を模倣するように設計されている。
EWSGの実践的な実装では、データインデックス上のMetropolis-Hastingsチェーンを介して、一様でないサブサンプリングを効率的に行う。
論文 参考訳（メタデータ） (2020-02-20T18:56:18Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。