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.

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