基于随机变分平滑模型检验的可扩展随机参数验证
机器学习
2023-04-07 v3 机器学习
摘要
随机模型线性时序性质的参数验证可表述为计算某一性质满足概率作为模型参数的函数。平滑模型检验（smMC）旨在从通过模拟获得的有限观测集中推断整个参数空间上的满足函数。由于观测成本高且含噪声，smMC 被构建为贝叶斯推断问题，从而使估计值附带额外的不确定性量化。在 smMC 中，作者使用高斯过程（GP），通过期望传播（Expectation Propagation）算法推断。该方法提供准确的重建及统计上可靠的不确定性量化。然而，它继承了 GP 众所周知的可扩展性问题。在本文中，我们利用概率机器学习的最新进展来推进这一限制，使 smMC 的贝叶斯推断可扩展到更大数据集，并使其能够应用于高维参数空间的模型。我们提出随机变分平滑模型检验（SV-smMC），一种利用随机变分推断（SVI）来近似 smMC 问题后验分布的解决方案。SVI 的强度和灵活性使 SV-smMC 可应用于两种替代概率模型：高斯过程（GP）和贝叶斯神经网络（BNN）。SVI 的核心要素是基于随机梯度的优化，使推断易于并行化并支持 GPU 加速。在本文中，我们通过考察可扩展性、计算效率和重建满足函数的准确性，比较 smMC 与 SV-smMC 的性能。
引用
@article{arxiv.2205.05398,
title = {Scalable Stochastic Parametric Verification with Stochastic Variational Smoothed Model Checking},
author = {Luca Bortolussi and Francesca Cairoli and Ginevra Carbone and Paolo Pulcini},
journal= {arXiv preprint arXiv:2205.05398},
year = {2023}
}