Model-checking for parametric stochastic models can be expressed as checking
the satisfaction probability of a certain property as a function of the
parameters of the model. Smoothed model checking (smMC) leverages Gaussian
Processes (GP) to infer the satisfaction function over the entire parameter
space from a limited set of observations obtained via simulation. This approach
provides accurate reconstructions with statistically sound quantification of
the uncertainty. However, it inherits the 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, enabling its application to larger models in terms of the dimension
of the parameter set. 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). Moreover,
SVI makes inference easily parallelizable and it 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 at the accuracy of
the reconstructed satisfaction function.
Luca Bortolussi1, Francesca Cairoli1, Ginevra Carbone1, and Paolo Pulcini1
Luca Bortolussi1, Francesca Cairoli1, Ginevra Carbone1, Paolo Pulcini1
0.47
DMG, University of Trieste, Italy
イタリア・トリエステ大学 dmg
0.49
Abstract. Model-checking for parametric stochastic models can be expressed as checking the satisfaction probability of a certain property as a function of the parameters of the model.
Smoothed model checking (smMC) [4] leverages Gaussian Processes (GP) to infer the satisfaction function over the entire parameter space from a limited set of observations obtained via simulation.
smoothed model checking (smmc) [4] はガウス過程 (gp) を利用して、シミュレーションによって得られた限られた観測集合からパラメータ空間全体の満足度関数を推定する。
0.84
This approach provides accurate reconstructions with statistically sound quantification of the uncertainty.
このアプローチは、統計的に不確実性の定量化を伴う正確な再構成を提供する。
0.53
However, it inherits the scalability issues of GP.
しかし、GPのスケーラビリティの問題を継承している。
0.59
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, enabling its application to larger models in terms of the dimension of the parameter set.
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.
本稿では,SVI(Stochastic Variational Inference)を利用して,smMC問題の後部分布を近似する手法であるStochastic Variational Smoothed Model Checking (SV-smMC)を提案する。
0.80
The strength and flexibility of SVI make SV-smMC applicable to two alternative probabilistic models: Gaussian Processes (GP) and Bayesian Neural Networks (BNN).
Moreover, SVI makes inference easily parallelizable and it enables GPU acceleration.
さらに、SVIは推論を簡単に並列化し、GPUアクセラレーションを可能にする。
0.63
In this paper, we compare the performances of smMC [4] against those of SV-smMC by looking at the scalability, the computational efficiency and at the accuracy of the reconstructed satisfaction function.
1 Introduction Parametric verification of logical properties aims at providing meaningful insights into the behaviour of a system, checking whether its evolution satisfies or not a certain requirement, expressed as a temporal logic formula, varying some parameters of the system’s model.
1 はじめに 論理特性のパラメトリック検証(parametric verification of logical properties)は、システムの振る舞いに関する有意義な洞察を提供することを目標とし、その進化が特定の要求を満たすかどうかをチェックする。
0.56
Stochastic systems, however, require the use of probabilistic model checking techniques as the satisfaction of a property is itself a stochastic quantity.
しかし確率系は、性質の満足度自体が確率量であるので確率的モデル検査技術を使う必要がある。
0.70
In this direction, statistical model checking (SMC) uses statistical tools to estimate the satisfaction probability of logical properties from trajectories sampled from the stochastic model and it enriches these estimates with probabilistic bounds of the estimation errors.
For instance, if the number of sampled trajectories is sufficiently large, the satisfaction probability, estimated as the average of satisfaction on individual runs, will converge to the true probability.
However, if the parameters of the stochastic model vary, the dynamics of the system will also vary.
しかし、確率モデルのパラメータが変化すると、システムのダイナミクスも変化する。
0.58
Therefore, SMC has to be performed from
したがって、SMCは実行されなければならない。
0.59
英語（論文から抽出）
日本語訳
スコア
2 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, and Paolo Pulcini
2 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, Paolo Pulcini
0.40
scratch for each set of parameter values, making SMC computationally unfeasible for parametric stochastic models.
パラメータの集合のスクラッチは、SMC計算がパラメトリック確率モデルでは不可能である。
0.76
In this regard, the satisfaction probability of a signal temporal logic (STL) requirement over a parametric stochastic model has been proved to be a smooth function of the parameters of the model [4].
The authors thus resort to the Expectation Propagation (EP) algorithm to approximate the posterior inference.
したがって、著者らは後方推定を近似するために期待伝播(ep)アルゴリズムを用いる。
0.69
Unfortunately, the cost of EP is cubic in the number of observations used to train the GP, making smMC applicable only to models with a low dimensional parameter space that require a limited number of training observations.
On the other hand, variational inference is used to perform approximate inference of a GP classification (GPC) problem.
一方、変分推論はgp分類(gpc)問題の近似推論を行うために用いられる。
0.58
The variational approach for GPC used in [15] builds on [18], in which the objective function used for optimization does not depend explicitly on the inducing variables, forcing them to be fixed a priori.
Moreover, in [15] the smMC problem is framed as a GPC problem, meaning that observations come from the satisfaction of a single trajectory.
さらに, [15]では, smMC問題はGPC問題であり, 単一の軌道の満足度から観測される。
0.70
If for a certain parameter we simulate M trajectories, this would result in M different observations.
あるパラメータに対して M 軌道をシミュレートすると、これは M の異なる観測をもたらす。
0.80
On the contrary, in [4] the observation process was modeled by a Binomial so that the satisfaction of the M simulations is condensed into a single observation.
In this paper, we propose a novel approach for scalable smMC, called Stochastic Variational Smoothed Model Checking (SVsmMC) that leverages Stochastic Variational Inference (SVI), a popular solution for making Bayesian inference scalable to large datasets.
The main advantage of SVI, compared to the VI used for example in [15], is that the gradient-based optimization can be stochastically approximated using mini-batches of data, resulting in the well-known stochastic gradient descent (SGD) algorithms.
2 Background 2.1 Population Continuous Time Markov Chain
背景 2.1連続時間マルコフ連鎖
0.48
A population model of interacting agents can be modeled as a stochastic system evolving continuously in time over a finite or countable state space X .
相互作用するエージェントの集団モデルは、有限あるいは可算状態空間 x 上で連続的に進化する確率的システムとしてモデル化することができる。
0.76
If the system is Markovian, meaning if the memory-less property holds, the population model can be modeled as a population Continuous Time Markov Chain (CTMC) M. Given a population with n different species {S1, . . . , Sn} and m possible reactions {R1, . . . , Rm}, the respective CTMC can be described by: – a state vector, X(t) = (X1(t), . . . , Xn(t)), taking values in X ⊆ Nn and
A general reaction Ri is identified by the tuple (τi, νi), where: - τi : S × Θi → R≥0 is the rate function of reaction Ri that associates to each reaction the rate of an exponential distribution, depending on the global state of the model and on a parameter θi, and
一般反応 Ri は、次のタプル (τi, νi) によって同定される: - τi : S × シュイ → R≥0 は、モデルのグローバル状態とパラメータ θi に依存する指数分布の速度を各反応に関連付ける反応 Ri の速度関数である。
0.84
- νi is the update vector, giving the net change of agents due to the reaction, so that the firing of reaction Ri results in a transition of the system from state X(t) to state X(t) + νi.
νi は更新ベクトルであり、反応によるエージェントの純変化を与えるので、反応 Ri の燃焼は系を状態 X(t) から状態 X(t) + νi へ遷移させる。
0.67
Reaction rules are easily visualised in the chemical reaction style, as
反応規則は化学反応様式で容易に可視化される。
0.86
(cid:88) Ri :
(cid:88) 理
0.25
αijSj j∈{1,...,n}
αijSj j∂{1, ...,n}
0.38
τi(X,θi)−→ (cid:88)
τi(X,θi)−→ (cid:88)
0.40
βijSj. j∈{1,...,n}
βijSj。 j∂{1, ...,n}
0.58
The stoichiometric coefficients αi = [αi1, . . . , αin], βi = [βi1, . . . , βin] can be arranged so that they form the update vector νi = βi − αi for reaction Ri.
STL allows the specification of properties of dense-time, real-valued signals, and
STLは、高密度時間、実値信号の特性の指定を可能にし、
0.67
英語（論文から抽出）
日本語訳
スコア
4 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, and Paolo Pulcini
4 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, Paolo Pulcini
0.40
the automatic generation of monitors for testing properties on individual trajectories.
個々の軌道上の特性をテストするためのモニタの自動生成。
0.78
The rationale of STL is to transform real-valued signals into Boolean ones, using formulae build on the following STL syntax : ϕ := true | µ | ¬ϕ | ϕ ∧ ϕ | ϕ UI ϕ,
(1) where I ⊆ T is a temporal interval, either bounded, I = [a, b], or unbounded, I = [a, +∞), for any 0 ≤ a < b. Atomic propositions µ are (non-linear) inequalities on population variables. From this essential syntax it is easy to define other operators, used to abbreviate the syntax in a STL formula: f alse := ¬true, ϕ ∨ ψ := ¬(¬ϕ ∧ ¬ψ), FI := true UI ϕ and GI := ¬FI¬ϕ. Monitoring the satisfaction of a formula is done recursively leveraging the tree structure of the STL formula. See [12] for the details on the STL Boolean semantics and on Boolean STL monitors.
(1) where I ⊆ T is a temporal interval, either bounded, I = [a, b], or unbounded, I = [a, +∞), for any 0 ≤ a < b. Atomic propositions µ are (non-linear) inequalities on population variables. From this essential syntax it is easy to define other operators, used to abbreviate the syntax in a STL formula: f alse := ¬true, ϕ ∨ ψ := ¬(¬ϕ ∧ ¬ψ), FI := true UI ϕ and GI := ¬FI¬ϕ. Monitoring the satisfaction of a formula is done recursively leveraging the tree structure of the STL formula. See [12] for the details on the STL Boolean semantics and on Boolean STL monitors. 訳抜け防止モード: ( 1 ) ここで i は t は時間間隔である。 有界、i = [ a, b ], 非有界の場合、i = [ a, + ∞ ) 任意の 0 ≤ a < b に対して、原子命題 μ は人口変数 上の(非-線型)不等式である。 この本質的な構文から、他の演算子を簡単に定義できます。 stl式における構文を略すのに使用される : f alse : = \true である。 φ ~ ψ : = ; ( φ ) ; fi : = 真の ui φ である。 公式の満足度をモニタリングする stl公式のツリー構造を再帰的に活用する。 stl boolean の意味論の詳細は 12 を参照してください。 そして、boolean stlモニター。
0.83
2.3 Smoothed Model Checking
2.3 平滑化モデルチェック
0.67
Smoothed Model Checking (smMC), presented in [4], uses Gaussian processes to infer the satisfaction function of pCTMC from a set of observations obtained via statistical model checking.
4] で示される smoothed model checking (smmc) は、統計モデルチェックによって得られた一連の観測から pctmc の満足度関数を推測するためにガウス過程を用いる。
0.87
Statistical Model Checking (SMC).
統計モデル検査(SMC)。
0.71
Given a CTMC Mθ with fixed parameters θ, time-bounded CTMC trajectories are sampled by standard simulation algorithms, like SSA [8], and monitoring algorithms for STL [12] are used to assess if the formula ϕ is satisfied for each sampled trajectory.
SMC [20,21] then uses standard statistical tools, either frequentist [20] or Bayesian [21], to estimate from these samples the satisfaction probability P r(ϕ|Mθ) or to test if P r(ϕ|Mθ) > q with a given confidence level.
SMC[20,21] は、これらのサンプルから満足度確率 P r(φ|Mθ) を推定するために、または与えられた信頼度レベルを持つ P r(φ|Mθ) > q を検定するために、標準統計ツールを使用する。
0.78
Satisfaction Function for pCTMCs.
pCTMCの満足度関数
0.67
Building on [4], our interest is to quantify how the satisfaction of STL formulae depends on the unknown parameters of the pCTMC.
We define the satisfaction function fϕ : Θ → [0, 1] associated to ϕ as
φ に付随する満足度関数 fφ : > → [0, 1] を定義する。
0.85
fϕ(θ) = P r(ϕ = true|Mθ).
fφ(θ) = p r(θ = true|mθ) である。
0.77
(2) In order to have an accurate estimation, the satisfaction function fϕ over the entire parameter space Θ by means of SMC would require a prohibitively large number of evaluations.
In [4], Theorem 1, it has been shown that fϕ(θ) is a smooth function of the model parameters and thus machine learning techniques can be used to infer this function from a limited set of observations.
Problem statement. Given a pCTMC Mθ and an STL formula ϕ, the goal of smMC is to find a statistical estimate of the satisfaction function of (2) from a set of noisy observations of fϕ obtained at few parameter values θ1, θ2, . . . .
The task is then to construct a statistical model that, for any value θ∗ ∈ Θ, computes efficiently an estimate of fϕ(θ∗) together with a credible interval for such a
そのタスクは、任意の値 θ∗ ∈ θ に対して、その a に対する信頼できる間隔と共に fφ(θ∗) の推定を効率的に計算する統計モデルを構築することである。
0.75
英語（論文から抽出）
日本語訳
スコア
Stochastic Variational Smoothed Model Checking
確率的変分平滑化モデルチェック
0.69
5 prediction. More precisely, given an input point θ, our observations are obtained by evaluating a property ϕ on a single trajectory sampled from the stochastic model Mθ via SSA.
Thus, given a set of Nt parameter values, Θt = {θ1, . . . , θNt}, we simulate, for each parameter θi, Mt trajectories, obtaining Mt Boolean values i ∈ {0, 1} for j = 1, . . . , Mt. We condense these Boolean values in a vector (cid:96)j Li = [(cid:96)1 ] .
The noisy observations can be summarized as a training set
雑音の観測はトレーニングセットとして要約できる
0.77
i , . . . , (cid:96)Mt
I , . , (cid:96)Mt
0.40
i Dt = {(θi, Li) | i = 1, . . . , Nt} .
私は Dt = {(θi, Li) | i = 1, . , Nt} である。
0.67
(3) SmMC uses GP to solve the above inference problem.
(3) smmcはgpを用いて上記の推論問題を解決する。
0.51
Since the observation process is non-Gaussian, exact inference is unfeasible and thus Expectation Propagation is used to approximate the posterior distribution.
This solution scales as O(N 3 t ), it is thus unfeasible for large datasets.
この解は o(n 3 t ) とスケールするので、大規模なデータセットでは実現不可能である。 訳抜け防止モード: この解は O(N 3 t ) としてスケールする。 大規模なデータセットでは不可能です
0.75
Notice that, if the observation process is modeled by a Bernoulli, as in [15], meaning if Boolean values (cid:96)j i are considered as individual observations instead of condensing them in a
観察過程が[15]のようにベルヌーイによってモデル化された場合、ブール値 (cid:96)j i が a に凝縮するのではなく個々の観測と見なされる。
0.79
vector Li, inference scales as O(cid:0)(NtMt)3(cid: 1).
ベクトル Li, inference scales as O(cid:0)(NtMt)3(cid: 1)。
0.90
In order to mitigate such scalability
このようなスケーラビリティを緩和するために
0.63
issue, in [15] the authors use variational inference together with sparsification techniques to make inference feasible for slightly larger datasets.
問題 著者らは[15]において、ばらつき推論とスパーシフィケーション技法を併用して、わずかに大きなデータセットに対して推論を可能にする。 訳抜け防止モード: issue, in [ 15 ] the author using variational inference with sparsification techniques わずかに大きなデータセットに対して 推論を可能にするためです
0.87
Nonetheless, stochastic variational inference is not applicable and sparsification strongly reduces the reconstruction accuracy, thus scalability remains an open issue.
The goal of Stochastic Variational Smoothed Model Checking (SV-smMC) is to efficiently infer an accurate probabilistic estimate of the unknown satisfaction function fϕ : Θ → [0, 1].
Stochastic Variational Smoothed Model Checking (SV-smMC) の目標は、未知の満足度関数 fφ の正確な確率的推定を効率的に推測することである。
0.83
In order to do so, we define a function f : Θ → [0, 1] that should behave as similarly as possible to fϕ.
そのために f : θ → [0, 1] を f φ にできる限り同じように振る舞う関数 f : θ → [0, 1] を定義する。
0.78
The main ingredients of a Bayesian approach to the problem stated above are the following:
上記の問題に対するベイズ的アプローチの主成分は以下のとおりである。
0.78
1. Choose a prior distribution, p(f ), over a suitable function space encapsulat-
1. 適切な関数空間をカプセル化する前置分布 p(f ) を選択する-
0.87
ing the beliefs about function f prior to any observations being taken.
観測される前に関数 f についての信念を記入する。
0.77
2. Determine the functional form of the observation process by defining a suitable likelihood function that effectively models how the observations depend on the uncertain parameter θ.
. tractable for non-conjugate prior-likelihood distributions.
. 非共役事前相似分布を選べる。
0.47
Therefore, we need algorithms to accurately approximate such posterior distribution.
したがって,このような後方分布を正確に近似するアルゴリズムが必要である。
0.66
p(Dt|f )p(f )
p(Dt|f )p(f )
0.48
英語（論文から抽出）
日本語訳
スコア
6 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, and Paolo Pulcini
6 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, Paolo Pulcini
0.40
4. Evaluate such posterior at points θ∗, resulting in a predictive distribution p(f∗|θ∗, Dt), whose statistics are used to obtain the desired estimate of the satisfaction probability together with the respective credible interval.
SV-smMC leverages stochastic variational inference to efficiently compute the approximate posterior distribution p(f|Dt) so that smMC inference scales well to large dataset Dt.
3.1 Gaussian Processes Gaussian Processes (GP) define a distribution over real-valued functions of the form g : Θ → R and such distribution is uniquely identified by its mean and covariance functions, respectively denoted by µ(θ) = E[g(θ)] and kγ(θ, θ(cid:48)).
Let gt, µt and KNtNt denote respectively the latent, the mean and the covariance functions evaluated over the training inputs Θt.
gt, μt と KNtNt はそれぞれ、トレーニング入力 t に対して評価された潜在関数、平均関数、共分散関数を表す。
0.65
The outputs of the latent functions g : Θ → R are mapped into the [0, 1] interval by means of a so-called link function Φ, typically the logit or the probit function, so that f = g ◦ Φ.
潜在関数 g : θ → r の出力は、いわゆるリンク関数 φ によって [0, 1] 間隔にマッピングされる。 訳抜け防止モード: 潜在関数 g : θ → r の出力は、リンク関数 φ と呼ばれる so によって [0, 1 ] 間隔にマッピングされる。 通常、ロジット(logit)またはプロビット関数(probit function)は、f = g {\displaystyle g} となる。
0.76
The GP prior over latent functions g is defined as p(g|Θt) = N (g | µt, KNtNt).
潜在関数 g 上の gp は p(g|θt) = n (g | μt, kntnt) と定義される。
0.82
For simplicity, we assume µt = 0.
単純さのため、μt = 0 と仮定する。
0.67
In order to do inference over a test input θ∗, with latent variable g∗, we have to compute
テスト入力 θ∗ 上で推論を行うには、潜在変数 g∗ で計算しなければならない。
0.72
p(f∗|θ∗, Θt, Lt) =
p(f∗|θ∗, st, Lt) =
0.48
Φ(g∗)p(g∗|θ∗, Θt, Lt)dg∗,
t(g∗)p(g∗|θ∗, t, Lt)dg∗。
0.81
(4) (cid:90)
(4) (cid:90)
0.41
(cid:90) where Lt, denotes the set of Boolean tuples corresponding to points in Θt.
(cid:90) ここで Lt は t の点に対応するブールタプルの集合を表す。
0.52
To compute equation (4), we have to marginalize the posterior over the latent Gaussian variables:
方程式 (4) を計算するには、後続のガウス変数を余剰化しなければならない。
0.60
p(g∗|θ∗, Θt, Lt) =
p(g∗|θ∗, st, Lt) =
0.48
p(g∗|θ∗, Θt, gt)p(gt|Θt, Lt)dgt,
p(g∗|θ∗, st, gt)p(gt|\t, Lt)dgt,
0.46
(5) where the posterior p(gt|Θt, Lt) is not available in closed form since it is the convolution of a Gaussian and a binomial distribution.
Computing the KL divergence in (8) requires only O(m3) computations.
8)でのKL分散の計算はO(m3)計算のみを必要とする。
0.72
Most of the work will thus be in computing the expected likelihood terms.
したがって、ほとんどの作業は期待された確率条件の計算に費やされる。
0.56
Given the ease of parallelizing the simple sum over Nt, we can optimize LGP in a distributed or in a stochastic fashion by selecting mini-batches of the data at random.
From the mean and the variance of q(g∗), we obtain the respective credible interval and use the link function Φ to map it to a subset of the interval [0, 1], so that we have mean and credible interval of the posterior predictive distribution p(f∗|θ∗, Dt).
The core idea of Bayesian neural networks (BNNs) is to place a probability distribution over the weights w of a neural network fw : Θ → [0, 1], transforming the latter into a probabilistic model.
The Bayesian learning process starts by defining a prior distribution for w that expresses our initial belief about the weights values.
ベイズ学習プロセスは、重み値に関する最初の信念を表現するwの事前分布を定義することから始まります。
0.78
A common choice is to choose a zero-mean Gaussian prior.
一般的な選択は、ゼロ平均ガウス事前を選択することである。
0.60
As we observe data Dt, we update this prior to a posterior distribution using Bayes’ rule:
データDtを観察しながら、ベイズのルールを使って後続分布に先立ってこれを更新する。
0.75
p(w | Dt) =
p(w | Dt) =
0.42
p(Dt | w)p(w)
p(Dt | w)p(w)
0.42
p(Dt) . (9)
p(Dt) . (9)
0.42
英語（論文から抽出）
日本語訳
スコア
8 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, and Paolo Pulcini
8 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, Paolo Pulcini
0.40
Because of the non-linearity introduced by the neural network function fw(θ) and since the likelihood is binomial, the posterior p(w|Dt) is non-Gaussian and it cannot be computed analytically.
In order to predict the satisfaction function over an unobserved input θ∗, we marginalize the predictions with respect to the posterior distribution of the parameters, obtaining
(10) The latter is called posterior predictive distribution and it can be used to retrieve information about the uncertainty of a specific prediction f∗.
Unfortunately, the integration is analytically intractable due to the non-linearity of the neural network function [3,11].
残念ながら、ニューラルネットワーク関数[3,11]の非線形性のため、統合は分析的に難解である。
0.71
Stochastic Variational Inference. Given the unknown posterior distribution p(w|Dt), the rationale of SVI is to choose a family of parametric distributions qψ(w), over the same latent variables and minimize the KL divergence between these two distributions, KL[qψ(w)||p(w|Dt)].
(11) The first term is the expected log-likelihood of our data with respect to values of fw sampled from qψ(w|Dt), whereas the second term is the KL divergence between the proposal distribution and the prior.
Let [w1 , . . . , wC ] denote a vector of C realizations of the random variable w ∼ qψ(w).
w1 , . . . , wC ] を確率変数 w の C 実化のベクトルとする。
0.54
Each realization wi induces a deterministic function fwi that can be evaluated at θ∗, the unobserved input, providing an empirical approximation of p(f∗|θ∗, Dt).
各実現 wi は θ∗ で評価できる決定論的関数 fwi を誘導し、p(f∗|θ∗, Dt) の経験的近似を与える。
0.74
By the strong law of large numbers, the empirical approximation converges to the true distribution as C → ∞ [19].
大数の強い法則により、経験的近似は c → ∞ [19] として真の分布に収束する。
0.80
The sample size C can be chosen, for instance, to ensure a given width of the confidence interval for a statistic of interest [16] or to bound the probability that the empirical distribution differs from the true one by at most some given constant [13].
This formula monitors rapid increases in LacZ counts, followed by long periods of lack of protein production.
この式はlacz数の増加をモニターし、その後長期にわたってタンパク質生産の欠如を追跡する。
0.62
– Three-layer Phosphorelay (PhosRelay): network of three proteins L1, L2, L3 involved in a cascade of phosphorylation reactions (changing the state of the protein), in which protein Lj, in its phosphorylated form Ljp, acts as a catalyser of phosporylation of protein L(j + 1).
Dataset generation. The training set Dt is built as per Eq (3).
データセット生成。 トレーニングセットDtはEq (3)に従って構築される。
0.77
The test set, )) |
test set (複数形 test sets)
0.61
j (cid:9), where Mv is chosen very large, Mv (cid:29) Mt, so that we have a
j (cid:9) Mv が非常に大きく、Mv (cid:29) が山なので、
0.58
j = 1, . . . , Nv good estimate of the true satisfaction probability over each test input.
j = 1 , . . , Nv の各テスト入力に対する真の満足度確率を推定する。
0.83
Input data, i.e. the parameter values, are scaled to the interval [−1, 1] to enhance the performances of the inferred models and to avoid sensitivity to different scales
10 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, and Paolo Pulcini
10 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, Paolo Pulcini
0.40
in the parameter space. In order to deal with scenarios with gradually increasing parametric complexity, we choose, for each case study, different subsets of varying parameters and train a separate model on each of these choices.
In other words, we fix some of the parameters and let only the remaining parameters vary.
言い換えると、いくつかのパラメータを修正し、残りのパラメータだけを変更させます。
0.75
The parameter space considered is thus a subspace of the original one.
したがって、考慮されるパラメータ空間は元の部分空間である。
0.74
This allows us to analyze the scalability of the inferred smMC models across the different case studies and with respect to parameter spaces with different dimensions.
The experiments were conducted on a shared virtual machine with 32 cores, Intel(R) Xeon(R) Gold 6140 CPU @ 2.30GHz processors and 264GB of RAM and a NVidia V100 GPU with 16Gb of RAM.
実験は32コアの共有仮想マシン、Intel(R) Xeon(R) Gold 6140 CPU @ 2.30GHz、RAMは264GB、RAMは16GbのNVidia V100 GPUで実施された。
0.83
The results are fully reproducible.
結果は再現可能である。
0.70
Code is available at: https://github.com/g inevracoal/ smoothed-model-check ing.
Training and evaluation. We apply Stochastic Variational Inference on both Gaussian Processes (SVI-GPs) and Bayesian Neural Networks (SVI-BNNs) and compare them to the baseline smMC approach, where Gaussian Processes were inferred using Expectation Propagation (EP-GPs).
For simplicity, we call the latter SMC satisfaction probability.
単純性については、後者をSMC満足度確率と呼ぶ。
0.62
We stress that SMC estimates provably converge to the true satisfaction probabilities, meaning that the width of confidence intervals converges to zero in the limit of infinite samples, while Bayesian inference quantifies the predictive uncertainty.
Consequently, regardless of the number of samples, SMC and Bayesian estimates have different statistical meanings.
したがって、サンプルの数に関係なく、SMCとベイズ推定は異なる統計的意味を持つ。
0.78
j , . . . , (cid:96)Mv
j , . , (cid:96)Mv
0.41
j Evaluation metrics. To define meaningful measures of performance, let’s clarify the notation.
j 評価指標。 パフォーマンスの有意義な尺度を定義するために、記法を明確にしましょう。
0.57
For each point in the test set, j ∈ {1, . . . , Nv}, let fϕ(θj) and σj denote respectively the average and the standard deviation over the Mv Bernoulli trials ((cid:96)1 ).
The inferred models, on the other hand, provide a posterior predictive distribution p(fj|θj, Dt), let qj α denote the α-th quantile of such distribution.
j (i) the mean squared error (MSE) between SMC and the expected satisfaction
j (i)SMCと期待満足度の間の平均二乗誤差(MSE)
0.65
probabilities, i.e. the average of the squared residuals
確率、すなわち2乗残差の平均は
0.60
MSE = 1 Nv Nv(cid:88)
MSE = 1Nv Nv(cid:88)
0.41
j=1 (cid:0)fϕ(θj) − Ep(f|θj ,Dt)[f (θj)](cid:1)2
j=1 (cid:0)fφ(θj) − Ep(f|θj ,Dt)[f(θj)](cid:1)2
0.38
. This measure evaluates the quality of reconstruction provided by the mean of the posterior predictive distribution; (ii) the accuracy over the test set, i.e. the fraction of non empty intersections between SMC confidence intervals and estimated (1 − α) credible intervals:
(iii) the average width of the estimated credible intervals
(iii)推定信頼区間の平均幅
0.62
(cid:1), Unc =
(cid:1) unc =
0.34
1 Nv 1−α/2 − qj
1Nv 1−α/2−qj
0.34
α/2 (cid:0)qj
α/2 (cid:0)qj
0.36
Nv(cid:88)
Nv(cid:88)
0.42
j=1 which quantifies how informative the predictive uncertainty is and allows us to detect overconservative predictors.
j=1 予測の不確実性がいかに情報であるかを定量化し 過保守な予測を検出できます
0.48
A good predictor should be balanced in terms of low MSE, high test accuracy, i.e. high values for Acc, and narrow credible intervals, i.e. low values for Unc.
They are trained for 5k epochs with mini-batches of size 100 and a learning rate of 0.001.
訓練は5kエポックで、サイズ100のミニバッチと0.001の学習率を持つ。
0.69
The prior distribution over the weights of the BNNs is a Gaussian N (0, 1/m) on each weight, where m is the layer width, i.e. the number of neurons per layer.
BNNの重みに対する以前の分布は、各重みのガウス N (0, 1/m) であり、m は層幅、すなわち層毎のニューロンの数である。
0.73
In the most challenging setting, PhosRelay with 6 parameters (l), we set the number of epochs to 100 and the batch size to 5k for both SVI-GPs and SVI-BNNs.
The cost of SVI-GP inference is cubic in the number of inducing points, which is chosen to be sufficiently small, and linear in the number of training instances.
Variational models are trained by means of SGD, which is a stochastic inference approach.
変分モデルは確率的推論手法であるSGDを用いて訓練される。
0.61
Thus, at least on simple configurations, it is likely to take longer than EP in reaching convergence.
したがって、少なくとも単純な構成では、収束に達するのにEPよりも長くかかる可能性が高い。
0.64
The computational advantage becomes significant as the complexity of the case study increases, i.e., when the training set is sufficiently large, moving towards the memory-bound problem of EP, which is typically unfeasible on configurations with a parameter space with dimensions larger than four (like our last testing configuration).
Moreover, SVI-GP has an important collateral advantage in that of optimizing the kernel hyperparameters on the fly during the training phase, whereas in EP-GP the hyperparameters search is performed beforehand and it is rather expensive.
Table 1 reports training times for EP-GP, SVI-GP and SVI-BNN.
表1はEP-GP、SVI-GP、SVI-BNNのトレーニング時間を報告する。
0.54
We can observe how SVI-GP, trained leveraging GPU
GPUを活用したSVI-GPのトレーニングを観察できる
0.71
英語（論文から抽出）
日本語訳
スコア
Stochastic Variational Smoothed Model Checking
確率的変分平滑化モデルチェック
0.69
13 Fig. 1: Satisfaction probability estimated by EP-GPs, SVI-GPs and SVI-BNNs and true satisfaction probability on 30 equispaced points from the test set on configuration (a), with 95% confidence intervals around the mean.
acceleration, is, in general, the most efficient model as its convergence times are comparable to EP’s on simple configurations and they outperform EP on more complex ones.
Moreover, we noticed how it seems more convenient to train SVI-BNN on the CPU alone for small datasets, since using the GPU introduces a significant overhead due to memory transfer.
In particular, we compare the SMC satisfaction probability fϕ(θj) to the average satisfaction probability E[f (θj)] estimated by EP-GPs, SVI-GPs and SVI-BNNs over each input θj of the test set.
15 Fig. 2: True satisfaction probability is compared to the satisfaction probability estimated by EP-GPs, SVI-GPs and SVI-BNNs on the test set for configuration (c).
(b) (right). SVI-BNNs are evaluated using 1k posterior samples.
b) (右)。 SVI-BNNは1k後方サンプルを用いて評価した。
0.53
About the informativeness of uncertainty estimations, we notice how SVIBNN tends to produce credible intervals that are always larger than the one of SVI-GP, which, in turn, tends to underestimate the underlying uncertainty.
This phenomenon appears in all the different configurations and it is easily observable in Fig 3-12.
この現象は様々な構成に現れ、図3-12で容易に観測できる。
0.75
On the other hand, the baseline smMC tends to have tight uncertainty estimates on low-dimensional configurations, but it becomes excessively over-conservative in high-dimensional configurations, making the predicted credible intervals almost uninformative.
Discussion. To summarize, we can see how, in general, SV-smMC solutions scale a lot better to high-dimensional problems compared to smMC, both in terms of
16 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, and Paolo Pulcini
16 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, Paolo Pulcini
0.40
Fig. 4: Distribution of uncertainty for test parameters’ tuples of true (test) and predicted (EP-GP, SVI-GP, SVI-BNN) satisfaction probabilities for configurations (c) and (i).
SVI-GP, on the other, is the most efficient with respect to training times in low dimensions, reaches low MSEs and tends to provide overconfident predictions.
5 Conclusions This paper presents SV-smMC, an extension of Smoothed Model Checking, based on stochastic variational inference, that scales well to high dimensional parameter spaces and that enables GPU acceleration.
結論5 本稿では,sv-smmc(sv-smmc)を提案する。sv-smmcは,確率的変分推論に基づいて,高次元パラメータ空間によく拡張し,gpuアクセラレーションを実現する。 訳抜け防止モード: 結論5 本稿では,Smoothed Model Checkingの拡張であるSV-smMCについて述べる。 確率的変分推論に基づいて 高次元パラメータ空間にうまくスケールし、GPUアクセラレーションを可能にする。
0.64
In addition, this paper offers a comparison of the performances of stochastic variational inference over two different Bayesian approaches - namely Gaussian processes (SVI-GP) and Bayesian neural networks (SVI-BNN) - against those of the baseline smMC, based on the expectation propagation technique.
さらに,本論文では,gaussian process (svi-gp) と bayesian neural networks (svi-bnn) の2つのベイズ法における確率的変分推論の性能を期待伝播法に基づいて比較した。
0.70
In particular, our experiments show that the posterior predictive distribution provided by SVI-BNN provides the best overall results in terms of the estimated satisfaction probabilities.
3. Bishop, C.M.: Pattern recognition and machine learning.
3. c.m.ビショップ:パターン認識と機械学習。
0.73
Springer (2006)
Springer (複数形 Springers)
0.30
4. Bortolussi, L., Milios, D., Sanguinetti, G.
4) Bortolussi, L., Milios, D., Sanguinetti, G。
0.38
: Smoothed model checking for uncertain continuous-time markov chains.
: 不確定な連続時間マルコフ連鎖に対するモデルチェックの平滑化
0.67
Information and Computation 247, 235–253 (2016)
情報計算247,235-253 (2016)
0.76
5. Bortolussi, L., Silvetti, S.
5) Bortolussi, L., Silvetti, S。
0.75
: Bayesian statistical parameter synthesis for linear temporal properties of stochastic models.
: 確率モデルの線形時間的性質に対するベイズ統計パラメータ合成
0.81
In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018.
in: beyer, d., huisman, m. (eds.) tools and algorithms for the construction and analysis of systems - 24th international conference, tacas 2018(英語) 訳抜け防止モード: Beyer, D., Huisman, M. (eds )。 )システムの構築と分析のためのツールとアルゴリズム -第24回国際会議- 2018年。
Mass-action reactions: R1 : P Lac + RN AP → P LacRN AP with rate k1, R2 : P LacRN AP → P Lac + RN AP with rate k2, R3 : P LacRN AP → T rLacZ1 with rate k3, R4 : T rLacZ1 → RbsLacZ + P Lac + T rLacZ2 with rate k4, R5 : T rLacZ2 → RN AP with rate k5, R6 : Ribosome + RbsLacZ → RbsRibosome with rate k6, R7 : RbsRibosome → Ribosome + RbsLacZ with rate k7, R8 : RbsRibosome → T rRbsLacZ + RbsLacZ with rate k8, R9 : T rRbsLacZ → LacZ with rate k9, R10 : P LacZ → dgrLacZ with rate k10, R11 : RbsLacZ → dgrRbsLacZ with rate k11.
質量反応 r1 : p lac + rn ap → p lacrn ap レートk1, r2 : p lacrn ap → p lac + rn ap レートk2, r3 : p lacrn ap → t rlacz1 レートk3, r4 : t rlacz1 → rbslacz + p lac + t rlacz2 レートk4, r5 : t rlacz2 → rn ap レートk5, r6 : リボソーム + rbsribosome レートk6, r7 : rbsribosome → ribosome + rbslacz レートk7, r8 : rbsribosome → trbslacz レートrbslacz + rbslacz レートr10: rbslacz + rbslacz レートr10 → rbslacz レートr10 → rbslacz レートk10 : r10 → rbs10 → krbs10 → krbs11 → krbz10 → krbs11 レートr10 レートk6, r6 : r6 : rbsribosome + rbslacz → rbsribosome レートk6, r7, r7: rbsribosome + rbslacz レートrrbslacz レートk10。 訳抜け防止モード: 質量反応 r1 : p lac + rn ap → p lacrn ap 率 k1, r2 : p lacrn ap → p lac + rn ap レート k2, r3 : p lacrn ap → t rlacz1 速度k3, r4 : t rlacz1 → rbslacz + p lac + t rlacz2 レートk4。 r5 : t rlacz2 → rn ap レートk5, r6 : ribosome + rbslacz → rbsribosome レートk6, r7 : rbsribosome → ribosome + rbslacz レートk7, r8 : rbsribosome → t rrbslacz + rbslacz レートk8, r9 : t rrbslacz → lacz レート k9, r10 : p lacz → dgrlacz レート k10, r11 : rbslacz → dgrrbslacz レート k11 である。
0.60
Initial state: P Lac = 1, RN AP = 35, Ribosome = 350, P LacRN AP = T rLacZ1 = RbsLacZ = T rLacZ2 = RbsRibosome = T rRbsLacZ = LacZ = dgrLacZ = dgrRbsLacZ = 0.
初期状態: P Lac = 1, RN AP = 35, Ribosome = 350, P LacRN AP = T rLacZ1 = RbsLacZ = T rLacZ2 = RbsRibosome = T rRbsLacZ = LacZ = dgrRbsLacZ = 0 訳抜け防止モード: 初期状態 : p lac = 1, rn ap = 35 リボソーム = 350, p lacrn ap = t rlacz1 = rbslacz = t rlacz2 = rbsribosome = t rrbslacz = lacz = dgrlacz = dgrrbslacz = 0 である。
In configuration (d), k2 varies in [10, 100000], whereas in configuration
構成 (d),k2は[10,100000]で異なるが,構成は異なる
0.62
(e), k2 varies in [10, 10000] and k7 varies in [0.45, 4500].
(e),k2は[10,10000]で,k7は[0.45,4500]で変化する。
0.73
– Three-layer Phosphorelay: network of three layers L1, L2, L3.
– 3層蛍光体:3層L1,L2,L3のネットワーク。
0.76
Each layer can be found also in phosphorylate form L1p, L2p, L3p and there is a ligand B. Initial state: L1p = L2p = L3p = L4p = B = 0, L1 = L2 = L3 = 32 and N = 5000.
Reactions: R1 : ∅ → B with rate function kp R2 : L1 + B → L1p + B with rate function k1 · L1 · B/N R3 : L1p + L2 → L1 + L2p with rate function k2 · L1p · L2/N R4 : L2p + L3 → L2 + L3p with rate function k3 · L2p · L3/N R5 : L3p → L3 with rate function k4 · L2p/N R6 : B → ∅ with rate function kd · B
反応: レート関数 kp r2 : l1 + b → l1p + b レート関数 k1 · l1 · b/n r3 : l1p + l2 → l1 + l2p レート関数 k2 · l1p · l2/n r4 : l2p + l3 → l2 + l3p レート関数 k3 · l2p · l3/n r5 : l3p → l3 とレート関数 k4 · l2p/n r6 : b → でレート関数 kd · b 訳抜け防止モード: 反応: レート関数 kp R2 : L1 を持つ R1 : s → B + B → L1p + B with rate function k1 · L1 · B / N R3 : L1p + L2 → L1 + L2p with rate function k2 · L1p · L2 / N R4 : L2p + L3 → L2 + L3p with rate function k3 · L2p · L3 / N R5 : L3p → L3 with rate function k4 · L2p / N R6 : B → B
0.77
The default parametric values are kp = 0, 1, kd = 0.05, k1 = k2 = k3 = 1 and k4 = 2.
20 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, and Paolo Pulcini
20 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, Paolo Pulcini
0.40
B Additional Plots Fig. 5: Satisfaction probability estimated by EP-GPs, SVI-GPs and SVI-BNNs and true satisfaction probability on 30 equispaced points from the test set on configuration (b), with 95% confidence intervals around the mean.
b 追加プロット 図5: EP-GPs, SVI-GPs, SVI-BNNsで推定される満足度確率と, 設定(b)で設定した試験から得られた30点の真満足度確率は平均95%の信頼区間を有する。
0.77
SVI-BNNs are evaluated on 1k posterior samples.
SVI-BNNを1k後方試料で評価した。
0.52
Fig. 6: Satisfaction probability estimated by EP-GPs, SVI-GPs and SVI-BNNs and true satisfaction probability on 30 equispaced points from the test set on configuration (d), with 95% confidence intervals around the mean.
図6: EP-GPs, SVI-GPs, SVI-BNNsで推定される満足度確率と、設定(d)に設定した試験から30の等間隔点に対する真の満足度確率は平均95%の信頼区間を有する。 訳抜け防止モード: 図 6 : EP-GPsで推定される満足度確率 SVI - GPs and SVI - BNNs and true satisfaction probability on 30 equispaced points from the test set on configuration (d) 平均で95%の信頼区間を 確保しています
0.88
SVI-BNNs are evaluated on 1k posterior samples.
SVI-BNNを1k後方試料で評価した。
0.52
英語（論文から抽出）
日本語訳
スコア
Stochastic Variational Smoothed Model Checking
確率的変分平滑化モデルチェック
0.69
21 Fig. 7: Satisfaction probability estimated by EP-GPs, SVI-GPs and SVI-BNNs and true satisfaction probability on 30 equispaced points from the test set on configuration (f), with 95% confidence intervals around the mean.
21 図7: EP-GPs, SVI-GPs, SVI-BNNsで推定される満足度確率と、設定(f)に設定した試験から30の等間隔点に対する真の満足度確率は平均95%の信頼区間を有する。 訳抜け防止モード: 21 図 7 : EP-GPsで推定される満足度確率 SVI - GPs and SVI - BNNs and true satisfaction probability on 30 equispaced points from the test set on configuration (f) 平均で95%の信頼区間を 確保しています
0.66
SVI-BNNs are evaluated on 1k posterior samples.
SVI-BNNを1k後方試料で評価した。
0.52
Fig. 8: True satisfaction probability is compared to the satisfaction probability estimated by EP-GPs, SVI-GPs and SVI-BNNs on the test set for configuration (e).
Fig. 9: True satisfaction probability is compared to the satisfaction probability estimated by EP-GPs, SVI-GPs and SVI-BNNs on the test set for configuration (g).
22 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, and Paolo Pulcini
22 Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, Paolo Pulcini
0.40
Fig. 10: Uncertainty of true (test) and predicted (EP-GP, SVI-GP, SVI-BNN) satisfaction probabilities for models trained on configuration (d) (left) and on configuration (f ) (right).
第10図:構成(d)および構成(f)に基づいて訓練されたモデルに対する真(テスト)及び予測(EP-GP、SVI-GP、SVI-BNN)満足度確率。 訳抜け防止モード: 図10: true(テスト)の不確かさと予測(EP-GP) SVI - GP, SVI - BNN ) 構成 (d ) (左) で訓練されたモデルに対する満足度 and on configuration ( f ) ( right )
0.87
SVI-BNNs are evaluated using 1k posterior samples.
SVI-BNNは1k後方サンプルを用いて評価した。
0.49
Fig. 11: Distribution of uncertainty for test parameters’ tuples of true (test) and predicted (EP-GP, SVI-GP, SVI-BNN) satisfaction probabilities.