一句话：用神经网络表示上鞅证书，通过反例引导的归纳合成循环，为概率程序与随机模型计算紧致且可靠的概率界。
本文提出一种数据驱动的定量验证方法，用于概率程序与随机动力模型的验证。目标问题是计算随机过程在有限时间内命中目标条件的概率的紧致且可靠的上下界，该问题涵盖离散时间随机动力模型的可达性与安全性分析，以及概率程序的断言违反与终止性分析。方法上，作者用神经网络表示能导出此类概率界上鞅证书，并采用反例引导的归纳合成循环：先用随机优化在状态空间样本上训练神经证书并同时收紧概率界，再用可满足性模理论（SMT）形式化地检查证书在全部状态上的有效性；若得到反例，则将其加入样本集并重复该循环，直至确认有效性。在一组多样化的基准测试上，得益于神经网络的表达能力，该方法给出的概率界在所有情形下都不劣于现有符号方法，并且能处理后者完全无法企及的模型。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{AbateEGPR26,
title = {Quantitative Verification with Neural Networks},
author = {Alessandro Abate and Alec Edwards and Mirco Giacobbe and Hashan Punchihewa and Diptarko Roy},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 2},
year = {2026},
doi = {10.46298/lmcs-22(2:4)2026}
}