Learning Probabilistic Termination Proofs

Alessandro Abate*, M. Giacobbe*, Diptarko Roy*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

23 Downloads (Pure)

Abstract

We present the first machine learning approach to the termination analysis of probabilistic programs. Ranking supermartingales (RSMs) prove that probabilistic programs halt, in expectation, within a finite number of steps. While previously RSMs were directly synthesised from source code, our method learns them from sampled execution traces. We introduce the neural ranking supermartingale: we let a neural network fit an RSM over execution traces and then we verify it over the source code using satisfiability modulo theories (SMT); if the latter step produces a counterexample, we generate from it new sample traces and repeat learning in a counterexample-guided inductive synthesis loop, until the SMT solver confirms the validity of the RSM. The result is thus a sound witness of probabilistic termination. Our learning strategy is agnostic to the source code and its verification counterpart supports the widest range of probabilistic single-loop programs that any existing tool can handle to date. We demonstrate the efficacy of our method over a range of benchmarks that include linear and polynomial programs with discrete, continuous, state-dependent, multi-variate, hierarchical distributions, and distributions with undefined moments.
Original languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publication3rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part II
EditorsAlexandra Silva, K. Rustan M. Leino
Place of PublicationCham
PublisherSpringer
Pages3–26
Number of pages24
Edition1
ISBN (Electronic)9783030816889
ISBN (Print)9783030816872
DOIs
Publication statusPublished - 17 Jul 2021
Event33rd International Conference on Computer-Aided Verification - Virtual
Duration: 18 Jul 202124 Jul 2021

Publication series

NameTheoretical Computer Science and General Issues
PublisherSpringer
Volume12760
ISSN (Print)2512-2010
ISSN (Electronic)2512-2029

Conference

Conference33rd International Conference on Computer-Aided Verification
Abbreviated titleCAV 2021
Period18/07/2124/07/21

Fingerprint

Dive into the research topics of 'Learning Probabilistic Termination Proofs'. Together they form a unique fingerprint.

Cite this