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.

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