Scalable Stochastic Parametric Verification with Stochastic Variational Smoothed Model Checking

要約

タイトル：Scalable Stochastic Parametric Verification with Stochastic Variational Smoothed Model Checking

要約：

– 確率的モデルの線形時間的な性質のパラメーター検証は、モデルのパラメーターの関数として特定の性質の満足確率を計算することで表すことができる。
– Smoothed model checking (smMC)は、シミュレーションによって得られた限られた観測値から、パラメーター空間全体にわたる満足関数を推定することを目的としています。
– 観測値が高価でノイズがあるため、smMCはベイズ推論問題としてフレーム化されます。このアプローチでは、期待伝搬アルゴリズムによって推定されたガウス過程（GP）が使用されます。このアプローチは、統計的に正確な不確実性の定量化を持つ正確な再構築を提供しますが、GPのスケーラビリティの問題を継承します。
– この論文では、確率的機械学習の最近の進歩を利用して、この制限を押し広げ、大規模なデータセットにスケーラブルなベイジアン推論のsmMCを可能にし、高次元パラメーター空間を持つモデルに適用することができるStochastic Variational Smoothed Model Checking（SV-smMC）を提案します。
– SVIの強度と柔軟性により、SV-smMCは2つの代替確率モデルに応用できます：ガウス過程（GP）およびベイズニューラルネットワーク（BNN）。
– SVIの核心要素は、推論を容易に並列化し、GPUアクセラレーションを可能にする確率的勾配ベースの最適化です。
– この論文では、スケーラビリティ、計算効率、再構築された満足関数の精度を比較することにより、smMCとSV-smMCのパフォーマンスを比較します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, OpenAI