Document Open Access Logo

Quantitative Verification with Neural Networks

Authors Alessandro Abate , Alec Edwards , Mirco Giacobbe , Hashan Punchihewa, Diptarko Roy

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.22.pdf
  • Filesize: 0.8 MB
  • 18 pages

Document Identifiers

Author Details

Alessandro Abate
  • University of Oxford, UK
Alec Edwards
  • University of Oxford, UK
Mirco Giacobbe
  • University of Birmingham, UK
Hashan Punchihewa
  • University of Oxford, UK
Diptarko Roy
  • University of Oxford, UK

Funding

  • Abate, Alessandro: HICLASS project from Innovate UK
  • Edwards, Alec: EPSRC Centre for Doctoral Training in Autonomous Intelligent Machines and Systems (EP/S024050/1)
  • Punchihewa, Hashan: DeepMind Computer Science Scholarship
  • Roy, Diptarko: EPSRC Doctoral Training Partnership, and Department of Computer Science Scholarship, University of Oxford

Cite AsGet BibTex

Alessandro Abate, Alec Edwards, Mirco Giacobbe, Hashan Punchihewa, and Diptarko Roy. Quantitative Verification with Neural Networks. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.22

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Probabilistic computation
  • Computing methodologies → Machine learning
  • Computing methodologies → Neural networks
Keywords
  • Data-driven Verification
  • Quantitative Verification
  • Probabilistic Programs
  • Stochastic Dynamical Models
  • Counterexample-guided Inductive Synthesis
  • Neural Networks

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo. Formal synthesis of Lyapunov neural networks. IEEE Control. Syst. Lett., 5(3):773-778, 2021. Google Scholar
  2. Alessandro Abate, Alec Edwards, Mirco Giacobbe, Hashan Punchihewa, and Diptarko Roy. Quantitative verification with neural networks, 2023. URL: https://arxiv.org/abs/2301.06136.
  3. Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. Learning probabilistic termination proofs. In CAV (2), volume 12760 of Lecture Notes in Computer Science, pages 3-26. Springer, 2021. Google Scholar
  4. Alessandro Abate, Joost-Pieter Katoen, and Alexandru Mereacre. Quantitative automata model checking of autonomous stochastic hybrid systems. In HSCC, pages 83-92. ACM, 2011. Google Scholar
  5. Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proc. ACM Program. Lang., 2(POPL):34:1-34:32, 2018. Google Scholar
  6. Christophe Alias, Alain Darte, Paul Feautrier, and Laure Gonnord. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In SAS, volume 6337 of Lecture Notes in Computer Science, pages 117-133. Springer, 2010. Google Scholar
  7. Christel Baier, Luca de Alfaro, Vojtech Forejt, and Marta Kwiatkowska. Model checking probabilistic systems. In Handbook of Model Checking, pages 963-999. Springer, 2018. Google Scholar
  8. Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Performance evaluation and model checking join forces. Commun. ACM, 53(9):76-85, 2010. Google Scholar
  9. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  10. Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, and Subhajit Roy. Data-driven invariant learning for probabilistic programs. In CAV (1), volume 13371 of Lecture Notes in Computer Science, pages 33-54. Springer, 2022. Google Scholar
  11. Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Probabilistic program verification via inductive synthesis of inductive invariants. In TACAS (2), volume 13994 of Lecture Notes in Computer Science, pages 410-429. Springer, 2023. Google Scholar
  12. D. P. Bertsekas and S. E. Shreve. Stochastic optimal control: The discrete-time case. Athena Scientific, 1996. Google Scholar
  13. Aleksandar Chakarov and Sriram Sankaranarayanan. Probabilistic program analysis with martingales. In CAV, volume 8044 of Lecture Notes in Computer Science, pages 511-526. Springer, 2013. Google Scholar
  14. Ya-Chien Chang, Nima Roohi, and Sicun Gao. Neural Lyapunov control. In NeurIPS, pages 3240-3249, 2019. Google Scholar
  15. Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. Termination analysis of probabilistic programs through positivstellensatz’s. In CAV (1), volume 9779 of Lecture Notes in Computer Science, pages 3-22. Springer, 2016. Google Scholar
  16. Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Trans. Program. Lang. Syst., 40(2):7:1-7:45, 2018. Google Scholar
  17. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Ðorđe Žikelić. Sound and complete certificates for quantitative termination analysis of probabilistic programs. In CAV (1), volume 13371 of Lecture Notes in Computer Science, pages 55-78. Springer, 2022. Google Scholar
  18. Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner, and Ðorđe Žikelić. A learner-verifier framework for neural network controllers and certificates of stochastic systems. In TACAS (1), volume 13993 of Lecture Notes in Computer Science, pages 3-25. Springer, 2023. Google Scholar
  19. Krishnendu Chatterjee, Petr Novotný, and Ðorđe Žikelić. Stochastic invariants for probabilistic termination. In POPL, pages 145-160. ACM, 2017. Google Scholar
  20. Fredrik Dahlqvist and Alexandra Silva. Semantics of probabilistic programming: A gentle introduction. In Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva, editors, Foundations of Probabilistic Programming, pages 1-42. Cambridge University Press, 2020. Google Scholar
  21. Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: an efficient SMT solver. In TACAS, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. Google Scholar
  22. Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Quantitative multi-objective verification for probabilistic systems. In TACAS, volume 6605 of Lecture Notes in Computer Science, pages 112-127. Springer, 2011. Google Scholar
  23. Hongfei Fu and Krishnendu Chatterjee. Termination of nondeterministic probabilistic programs. In VMCAI, volume 11388 of LNCS, pages 468-490. Springer, 2019. Google Scholar
  24. Timon Gehr, Sasa Misailovic, and Martin T. Vechev. PSI: exact symbolic inference for probabilistic programs. In CAV (1), volume 9779 of Lecture Notes in Computer Science, pages 62-83. Springer, 2016. Google Scholar
  25. Timon Gehr, Samuel Steffen, and Martin T. Vechev. λPSI: exact inference for higher-order probabilistic programs. In PLDI, pages 883-897. ACM, 2020. Google Scholar
  26. Mirco Giacobbe, Daniel Kroening, and Julian Parsert. Neural termination analysis. In ESEC/SIGSOFT FSE, pages 633-645. ACM, 2022. Google Scholar
  27. Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. Probabilistic programming. In FOSE, pages 167-181. ACM, 2014. Google Scholar
  28. O. Hernández-Lerma and J. B. Lasserre. Discrete-time Markov control processes, volume 30 of Applications of Mathematics. Springer-Verlag, 1996. Google Scholar
  29. Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. Modular verification for almost-sure termination of probabilistic programs. Proc. ACM Program. Lang., 3(OOPSLA):129:1-129:29, 2019. Google Scholar
  30. O. Kallenberg. Foundations of modern probability. Springer Science & Business Media, 2006. Google Scholar
  31. Dexter Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22(3):328-350, 1981. Google Scholar
  32. Marta Z. Kwiatkowska. Quantitative verification: models techniques and tools. In ESEC/SIGSOFT FSE, pages 449-458. ACM, 2007. Google Scholar
  33. Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Quantitative analysis with the probabilistic model checker PRISM. In QAPL, volume 153 of Electronic Notes in Theoretical Computer Science, pages 5-31. Elsevier, 2005. Google Scholar
  34. Mathias Lechner, Ðorđe Žikelić, Krishnendu Chatterjee, and Thomas A. Henzinger. Stability verification in stochastic control systems via neural network supermartingales. In AAAI, pages 7326-7336. AAAI Press, 2022. Google Scholar
  35. Frederik Baymler Mathiesen, Simeon Craig Calvert, and Luca Laurenti. Safety certification for stochastic systems via neural barrier functions. IEEE Control. Syst. Lett., 7:973-978, 2023. Google Scholar
  36. Annabelle McIver and Carroll Morgan. Games, probability and the quantitative μ-calculus qmμ. In LPAR, volume 2514 of Lecture Notes in Computer Science, pages 292-310. Springer, 2002. Google Scholar
  37. Annabelle McIver and Carroll Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005. Google Scholar
  38. Carroll Morgan, Annabelle McIver, and Karen Seidel. Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst., 18(3):325-353, 1996. Google Scholar
  39. Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. Bounded expectations: resource analysis for probabilistic programs. In PLDI, pages 496-512. ACM, 2018. Google Scholar
  40. Andrea Peruffo, Daniele Ahmed, and Alessandro Abate. Automated and formal synthesis of neural barrier certificates for dynamical models. In TACAS (1), volume 12651 of Lecture Notes in Computer Science, pages 370-388. Springer, 2021. Google Scholar
  41. Armando Solar-Lezama. Program Synthesis by Sketching. PhD thesis, University of California at Berkeley, USA, 2008. Google Scholar
  42. Armando Solar-Lezama, Liviu Tancau, Rastislav Bodík, Sanjit A. Seshia, and Vijay A. Saraswat. Combinatorial sketching for finite programs. In ASPLOS, pages 404-415. ACM, 2006. Google Scholar
  43. Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, and Ichiro Hasuo. Ranking and repulsing supermartingales for reachability in randomized programs. ACM Trans. Program. Lang. Syst., 43(2):5:1-5:46, 2021. Google Scholar
  44. Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, and Alessandro Abate. Quantitative model-checking of controlled discrete-time markov processes. Inf. Comput., 253:1-35, 2017. Google Scholar
  45. Franck van Breugel and James Worrell. Towards quantitative verification of probabilistic transition systems. In ICALP, volume 2076 of Lecture Notes in Computer Science, pages 421-432. Springer, 2001. Google Scholar
  46. Di Wang, Jan Hoffmann, and Thomas W. Reps. Central moment analysis for cost accumulators in probabilistic programs. In PLDI, pages 559-573. ACM, 2021. Google Scholar
  47. Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. Cost analysis of nondeterministic probabilistic programs. In PLDI, pages 204-220. ACM, 2019. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact