Piecewise Analysis of Probabilistic Programs via $k$-Induction
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912800816758784 |
|---|---|
| author | Yang, Tengshun Feng, Shenghua Fu, Hongfei Zhan, Naijun Ke, Jingyu Wu, Shiyang |
| author_facet | Yang, Tengshun Feng, Shenghua Fu, Hongfei Zhan, Naijun Ke, Jingyu Wu, Shiyang |
| contents | In probabilistic program analysis, quantitative analysis aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability. Most previous works consider numerical bounds over the whole program state space monolithically and do not consider piecewise bounds. Not surprisingly, monolithic bounds are either conservative, or not expressive and succinct enough in general. To derive better bounds, we propose a novel approach for synthesizing piecewise bounds over probabilistic programs. First, we show how to extract useful piecewise information from latticed $k$-induction operators, and combine the piecewise information with Optional Stopping Theorem to obtain a general approach to derive piecewise bounds over probabilistic programs. Second, we develop algorithms to synthesize piecewise polynomial bounds, and show that the synthesis can be reduced to bilinear programming in the linear case, and soundly relaxed to semidefinite programming in the polynomial case. Experimental results show that our approach generates tight piecewise bounds for a wide range of benchmarks when compared with the state of the art. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_17567 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Piecewise Analysis of Probabilistic Programs via $k$-Induction Yang, Tengshun Feng, Shenghua Fu, Hongfei Zhan, Naijun Ke, Jingyu Wu, Shiyang Programming Languages D.3.1; G.3 In probabilistic program analysis, quantitative analysis aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability. Most previous works consider numerical bounds over the whole program state space monolithically and do not consider piecewise bounds. Not surprisingly, monolithic bounds are either conservative, or not expressive and succinct enough in general. To derive better bounds, we propose a novel approach for synthesizing piecewise bounds over probabilistic programs. First, we show how to extract useful piecewise information from latticed $k$-induction operators, and combine the piecewise information with Optional Stopping Theorem to obtain a general approach to derive piecewise bounds over probabilistic programs. Second, we develop algorithms to synthesize piecewise polynomial bounds, and show that the synthesis can be reduced to bilinear programming in the linear case, and soundly relaxed to semidefinite programming in the polynomial case. Experimental results show that our approach generates tight piecewise bounds for a wide range of benchmarks when compared with the state of the art. |
| title | Piecewise Analysis of Probabilistic Programs via $k$-Induction |
| topic | Programming Languages D.3.1; G.3 |
| url | https://arxiv.org/abs/2403.17567 |