License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2023.22
URN: urn:nbn:de:0030-drops-190162
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19016/
Abate, Alessandro ;
Edwards, Alec ;
Giacobbe, Mirco ;
Punchihewa, Hashan ;
Roy, Diptarko
Quantitative Verification with Neural Networks
Abstract
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.
BibTeX - Entry
@InProceedings{abate_et_al:LIPIcs.CONCUR.2023.22,
author = {Abate, Alessandro and Edwards, Alec and Giacobbe, Mirco and Punchihewa, Hashan and Roy, Diptarko},
title = {{Quantitative Verification with Neural Networks}},
booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)},
pages = {22:1--22:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-299-0},
ISSN = {1868-8969},
year = {2023},
volume = {279},
editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/19016},
URN = {urn:nbn:de:0030-drops-190162},
doi = {10.4230/LIPIcs.CONCUR.2023.22},
annote = {Keywords: Data-driven Verification, Quantitative Verification, Probabilistic Programs, Stochastic Dynamical Models, Counterexample-guided Inductive Synthesis, Neural Networks}
}
|
Keywords: |
|
Data-driven Verification, Quantitative Verification, Probabilistic Programs, Stochastic Dynamical Models, Counterexample-guided Inductive Synthesis, Neural Networks |
|
Collection: |
|
34th International Conference on Concurrency Theory (CONCUR 2023) |
|
Issue Date: |
|
2023 |
|
Date of publication: |
|
07.09.2023 |
