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.

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