We present a data-driven approach to the quantitative verification of probabilistic programs and stochastic dynamical models. Our approach leverages neural networks to compute tight and sound bounds for the probability that a stochastic process hits a target condition within finite time. This problem subsumes a variety of quantitative verification questions, from the reachability and safety analysis of discrete-time stochastic dynamical models, to the study of assertion-violation and termination analysis of probabilistic programs. We rely on neural networks to represent supermartingale certificates that yield such probability bounds, which we compute using a counterexample-guided inductive synthesis loop: we train the neural certificate while tightening the probability bound over samples of the state space using stochastic optimisation, and then we formally check the certificate's validity over every possible state using satisfiability modulo theories; if we receive a counterexample, we add it to our set of samples and repeat the loop until validity is confirmed. We demonstrate on a diverse set of benchmarks that, thanks to the expressive power of neural networks, our method yields smaller or comparable probability bounds than existing symbolic methods in all cases, and that our approach succeeds on models that are entirely beyond the reach of such alternative techniques.

翻译：我们提出了一种数据驱动的方法，用于概率程序和随机动力学模型的定量验证。该方法利用神经网络计算随机过程在有限时间内达到目标条件的概率的紧致且可靠的上下界。该问题涵盖了多种定量验证任务，从离散时间随机动力学模型的可达性与安全性分析，到概率程序中断言违反与终止分析。我们采用神经网络表示能生成此类概率界限的超鞅证书，并通过反例引导的归纳综合循环进行计算：首先，通过随机优化在状态空间样本上收紧概率界以训练神经证书；随后，使用可满足性模理论对每个可能状态下的证书有效性进行形式化验证；若收到反例，则将其添加至样本集并重复该循环，直至验证通过。我们在多种基准测试上的实验表明，得益于神经网络的表达能力，我们的方法在所有案例中均能产生较现有符号方法更小或相当的概率界限，并且该方法能成功处理完全超出此类技术适用范围的问题模型。