非确定性概率规划的尾界代价分析

doi:10.1007/s12204-022-2456-z

摘要/Abstract

摘要： 对于概率程序，已有一些关于期望或均值的定性和定量分析工作，例如期望终止时间和预期消耗分析。然而，另一个非常重要的问题是尾部界限（即尾部概率的上界），可以为极端事件提供高概率保证。在这项工作中，我们关注的问题是对于非确定性概率程序消耗的尾部界限分析，旨在自动获取这些程序的资源使用的尾部界限。为了实现这一目标，提出了一种新颖的方法，结合适当的集中不等式，来推导程序终止之前累积消耗的尾部界限。提出的方法可以处理正、负消耗。此外，这个方法实现了基于模板的排序上鞅的自动合成，并产生了一个高效的多项式时间算法。为了展示提出的方法的有效性，提供了对不同程序的实验结果，并与最先进的工具进行了比较。

关键词: 程序消耗分析，概率程序，尾部界限，鞅

Abstract: For probabilistic programs, there is some work for qualitative and quantitative analysis about expectation or mean, such as expected termination time, and expected cost analysis. However, another non-trivial issue is about tail bounds (i.e., upper bounds of tail probabilities), which can provide high-probability guarantees to extreme events. In this work, we focus on the problem of tail-bound cost analysis over nondeterministic probabilistic programs, which aims to automatically obtain the tail bound of resource usages over such programs. To achieve this goal, we present a novel approach, combined with a suitable concentration inequality, to derive the tail bound of accumulated cost until program termination. Our approach can handle both positive and negative costs. Moreover, our approach enables an automated template-based synthesis of supermartingales and leads to an efficient polynomial-time algorithm. To show the effectiveness of our approach, we present experimental results on various programs and make a comparison with state-of-the-art tools.

Key words: program cost analysis, probabilistic programs, tail bound, martingales

中图分类号:

TP31

王培新. 非确定性概率规划的尾界代价分析[J]. J Shanghai Jiaotong Univ Sci, 2023, 28(6): 772-782.

WANG Peeixin(王培新). Tail-Bound Cost Analysis over Nondeterministic Probabilistic Programs[J]. J Shanghai Jiaotong Univ Sci, 2023, 28(6): 772-782.

参考文献 44

[7]	′ SCIBIOR A, GHAHRAMANI Z, GORDON A D. Practical probabilistic programming with monads [C]//2015 ACM SIGPLAN Symposium on Haskell. Vancouver: ACM, 2015: 165-176.
[1]	GORDON A D, HENZINGER T A, NORI A V, et al. Probabilistic programming [C]// Future of Software Engineering Proceedings. New York: ACM, 2014: 167- 181.
[8]	CLARET G, RAJAMANI S K, NORI A V, et al. Bayesian inference using data flow analysis [C]//9th Joint Meeting on Foundations of Software Engineering. Saint Petersburg: ACM, 2013: 92-102.
[2]	FOSTER N, KOZEN D, MAMOURSA K, et al. Probabilistic NetKAT [M]// Programming languages and systems. Berlin, Heidelberg: Springer, 2016: 282-309.
[9]	THRUN S. Probabilistic algorithms in robotics [J]. AI Magazine, 2000, 21(4): 93-109.
[3]	SMOLKA S, KUMAR P, FOSTER N et al. Cantor meets Scott: Semantic foundations for probabilistic networks [C]//44th ACM SIGPLAN Symposium on Principles of Programming Languages. Paris: ACM, 2017: 557-571.
[10]	THRUN S. Probabilistic robotics [J]. Communications of the ACM, 2002, 45(3): 52-57.
[4]	KAHN D M. Undecidable problems for probabilistic network programming [C]//42nd International Symposium on Mathematical Foundations of Computer Science. Aalborg: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017: 68.
[11]	JIANG X, COOPER G F. A Bayesian spatio-temporal method for disease outbreak detection [J]. Journal of the American Medical Informatics Association, 2010, 17(4): 462-471.
[12]	BARTHE G, K?PF B, OLMEDO F, et al. Probabilistic relational reasoning for differential privacy [J]. ACM Transactions on Programming Languages and Systems, 2013, 35(3): 9.
[13]	MANFREDI G, JESTIN Y. An introduction to ACAS Xu and the challenges ahead [C]//2016 IEEE/AIAA 35th Digital Avionics Systems Conference. Sacramento: IEEE, 2016: 1-9.
[14]	CHAKAROV A, SANKARANARAYANAN S. Probabilistic program analysis with martingales [M]// Computer aided verification. Berlin, Heidelberg: Springer, 2013: 511-526.
[15]	WANG D, HOFFMANN J, REPS T. PMAF: An algebraic framework for static analysis of probabilistic programs [C]//39th ACM SIGPLAN Conference on Programming Language Design and Implementation. Philadelphia: ACM, 2018: 513-528.
[5]	ROY D, MANSINGHKA V, GOODMAN N, et al. A stochastic programming perspective on nonparametric Bayes [C]//25th International Conference on Machine Learning. Helsinki: ACM, 2008: 1-3.
[16]	NGO V C, CARBONNEAUX Q, HOFFMANN J. Bounded expectations: Resource analysis for probabilistic programs [C]//39th ACM SIGPLAN Conference on Programming Language Design and Implementation. Philadelphia: ACM, 2018: 496-512.
[6]	GORDON A D, AIZATULIN M, BORGSTROM J, et al. A model-learner pattern for Bayesian reasoning [C]//40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Rome: ACM, 2013: 403-416.
[17]	AGRAWAL S, CHATTERJEE K, NOVOTN′ Y P. Lexicographic ranking supermartingales: An efficient approach to termination of probabilistic programs [J]. Proceedings of the ACM on Programming Languages, 2018, 2(POPL): 1-32.
[7]	′ SCIBIOR A, GHAHRAMANI Z, GORDON A D. Practical probabilistic programming with monads [C]//2015 ACM SIGPLAN Symposium on Haskell. Vancouver: ACM, 2015: 165-176.
[18]	CHATTERJEE K, FU H, NOVOTN′ Y P, et al. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs [C]//43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. St. Petersburg, FL: ACM, 2016: 327–342.
[8]	CLARET G, RAJAMANI S K, NORI A V, et al. Bayesian inference using data flow analysis [C]//9th Joint Meeting on Foundations of Software Engineering. Saint Petersburg: ACM, 2013: 92-102.
[19]	CHATTERJEE K, FU H, GOHARSHADY A K. Termination analysis of probabilistic programs through positivstellensatz’s [M]//Computer aided verification. Cham: Springer, 2016: 3-22.
[9]	THRUN S. Probabilistic algorithms in robotics [J]. AI Magazine, 2000, 21(4): 93-109.
[20]	ESPARZA J, GAISER A, KIEFER S. Proving termination of probabilistic programs using patterns [M]//Computer aided verification. Cham: Springer, 2012: 123-138.
[10]	THRUN S. Probabilistic robotics [J]. Communications of the ACM, 2002, 45(3): 52-57.
[21]	KAMINSKI B L, KATOEN J-P, MATHEJA C, et al. Weakest precondition reasoning for expected runtimes of probabilistic programs [M]//Programming languages and systems. Berlin, Heidelberg: Springer, 2016: 364-389.
[11]	JIANG X, COOPER G F. A Bayesian spatio-temporal method for disease outbreak detection [J]. Journal of the American Medical Informatics Association, 2010, 17(4): 462-471.
[22]	KAMINSKI B L, KATOEN J-P, MATHEJA C. On the hardness of analyzing probabilistic programs [J]. Acta Informatica, 2019, 56(3): 255-285.
[12]	BARTHE G, K?PF B, OLMEDO F, et al. Probabilistic relational reasoning for differential privacy [J]. ACM Transactions on Programming Languages and Systems, 2013, 35(3): 9.
[23]	COUSOT P, COUSOT R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints [C]//4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. Los Angeles: ACM, 1977: 238-252.[24] RUBINSTEIN R Y, KROESE D P. Simulation and the Monte Carlo method [M]. Hoboken: John Wiley & Sons, 2016.
[13]	MANFREDI G, JESTIN Y. An introduction to ACAS Xu and the challenges ahead [C]//2016 IEEE/AIAA 35th Digital Avionics Systems Conference. Sacramento: IEEE, 2016: 1-9.
[25]	BATZ K, KAMINSKI B L, KATOEN J, et al. How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times [M]//Programming languages and systems. Cham: Springer, 2018: 186-213.
[14]	CHAKAROV A, SANKARANARAYANAN S. Probabilistic program analysis with martingales [M]// Computer aided verification. Berlin, Heidelberg: Springer, 2013: 511-526.
[26]	WANG P, FU H, GOHARSHADY A K, et al. Cost analysis of nondeterministic probabilistic programs [C]//40th ACM SIGPLAN Conference on Programming Language Design and Implementation. Phoenix, AZ: ACM,2019: 204-220.
[15]	WANG D, HOFFMANN J, REPS T. PMAF: An algebraic framework for static analysis of probabilistic programs [C]//39th ACM SIGPLAN Conference on Programming Language Design and Implementation. Philadelphia: ACM, 2018: 513-528.
[27]	KURA S, URABE N, HASUO I. Tail probabilities for randomized program runtimes via martingales for higher moments [M]//Tools and algorithms for the construction and analysis of systems. Cham: Springer, 2019: 135-153.
[16]	NGO V C, CARBONNEAUX Q, HOFFMANN J. Bounded expectations: Resource analysis for probabilistic programs [C]//39th ACM SIGPLAN Conference on Programming Language Design and Implementation. Philadelphia: ACM, 2018: 496-512.
[28]	WANG D, HOFFMANN J, REPS T. Tail bound analysis for probabilistic programs via central moments [J/OL]. (2020-01-28). https://arxiv.org/abs/2001.10150.
[17]	AGRAWAL S, CHATTERJEE K, NOVOTN′ Y P. Lexicographic ranking supermartingales: An efficient approach to termination of probabilistic programs [J]. Proceedings of the ACM on Programming Languages, 2018, 2(POPL): 1-32.
[29]	WILLIAMS D. Probability with martingales [M]. Cambridge: Cambridge University Press, 1991.
[18]	CHATTERJEE K, FU H, NOVOTN′ Y P, et al. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs [C]//43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. St. Petersburg, FL: ACM, 2016: 327–342.
[30]	CHATTERJEE K, FU H, NOVOTN′ Y P, et al. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs [J]. ACM Transactions on Programming Languages and Systems, 2018, 40(2): 7.
[31]	CHATTERJEE K, FU H, GOHARSHADY A K. Termination analysis of probabilistic programs through positivstellensatz’s [EB/OL]. (2016-04-25). http://arxiv.org/abs/1604.07169.
[19]	CHATTERJEE K, FU H, GOHARSHADY A K. Termination analysis of probabilistic programs through positivstellensatz’s [M]//Computer aided verification. Cham: Springer, 2016: 3-22.
[20]	ESPARZA J, GAISER A, KIEFER S. Proving termination of probabilistic programs using patterns [M]//Computer aided verification. Cham: Springer, 2012: 123-138.
[32]	MEYN S, TWEEDIE R. Markov chains and stochastic stability [M]. London: Springer, 1993.
[21]	KAMINSKI B L, KATOEN J-P, MATHEJA C, et al. Weakest precondition reasoning for expected runtimes of probabilistic programs [M]//Programming languages and systems. Berlin, Heidelberg: Springer, 2016: 364-389.
[33]	FIORITI L M F, HERMANNS H. Probabilistic termination: Soundness, completeness, and compositionality [C]//42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Mumbai: ACM, 2015: 489-501.
[22]	KAMINSKI B L, KATOEN J-P, MATHEJA C. On the hardness of analyzing probabilistic programs [J]. Acta Informatica, 2019, 56(3): 255-285.
[34]	WANG P, FU H, CHATTERJEE K, et al. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time [J]. Proceedings of the ACM on Programming Languages, 2020, 4(POPL): 25.
[23]	COUSOT P, COUSOT R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints [C]//4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. Los Angeles: ACM, 1977: 238-252.[24] RUBINSTEIN R Y, KROESE D P. Simulation and the Monte Carlo method [M]. Hoboken: John Wiley & Sons, 2016.
[35]	NAKAMOTO S. Bitcoin: A peer-to-peer electronic cash system [EB/OL].
[25]	BATZ K, KAMINSKI B L, KATOEN J, et al. How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times [M]//Programming languages and systems. Cham: Springer, 2018: 186-213.
	[2020-09-24]. https://bitcoin.org/bitcoin.pdf.
[26]	WANG P, FU H, GOHARSHADY A K, et al. Cost analysis of nondeterministic probabilistic programs [C]//40th ACM SIGPLAN Conference on Programming Language Design and Implementation. Phoenix, AZ: ACM,2019: 204-220.
[36]	DE VRIES A. Bitcoin’s growing energy problem [J]. Joule, 2018, 2(5): 801-805.
[37]	ABATE A, KATOEN J, LYGEROS J, et al. Approximate model checking of stochastic hybrid systems [J]. European Journal of Control, 2010, 16(6): 624-641.
[27]	KURA S, URABE N, HASUO I. Tail probabilities for randomized program runtimes via martingales for higher moments [M]//Tools and algorithms for the construction and analysis of systems. Cham: Springer, 2019: 135-153.
[38]	FU H, CHATTERJEE K. Termination of nondeterministic probabilistic programs [M]//Verification, model checking, and abstract interpretation. Cham: Springer, 2019: 468-490.
[28]	WANG D, HOFFMANN J, REPS T. Tail bound analysis for probabilistic programs via central moments [J/OL]. (2020-01-28). https://arxiv.org/abs/2001.10150.
[29]	WILLIAMS D. Probability with martingales [M]. Cambridge: Cambridge University Press, 1991.
[39]	HOEFFDING W. Probability inequalities for sums of bounded random variables [M]//The collected works of Wassily Hoeffding. New York: Springer, 1994: 409- 426.
[40]	CHATTERJEE K, FU H, GOHARSHADY A K, et al. Computational approaches for stochastic shortest path on succinct MDPs [C]//Proceedings of the 27th International Joint Conference on Artificial Intelligence. Stockholm: AAAI Press, 2018: 4700-4707.
[30]	CHATTERJEE K, FU H, NOVOTN′ Y P, et al. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs [J]. ACM Transactions on Programming Languages and Systems, 2018, 40(2): 7.
[31]	CHATTERJEE K, FU H, GOHARSHADY A K. Termination analysis of probabilistic programs through positivstellensatz’s [EB/OL]. (2016-04-25). http://arxiv.org/abs/1604.07169.
[41]	FENG Y, ZHANG L, JANSEN D N, et al. Finding polynomial loop invariants for probabilistic programs [M]//Automated technology for verification and analysis. Cham: Springer, 2017: 400-416.
[32]	MEYN S, TWEEDIE R. Markov chains and stochastic stability [M]. London: Springer, 1993.
[33]	FIORITI L M F, HERMANNS H. Probabilistic termination: Soundness, completeness, and compositionality [C]//42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Mumbai: ACM, 2015: 489-501.
[42]	FARKAS J. A fourier-f′ele mechanikai elv alkalmaz′asai [J]. Mathematikai′es Term′eszettudom′anyi ′ Ertesit¨o, 1894, 12: 457-472 (in Hungarian).
[34]	WANG P, FU H, CHATTERJEE K, et al. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time [J]. Proceedings of the ACM on Programming Languages, 2020, 4(POPL): 25.
[43]	BARTHE G, ESPITAU T, GR′ EGOIRE B, et al. Proving expected sensitivity of probabilistic programs [J]. Proceedings of the ACM on Programming Languages, 2018, 2(POPL): 57.
[35]	NAKAMOTO S. Bitcoin: A peer-to-peer electronic cash system [EB/OL].
[44]	LETAN T, R′ EGIS-GIANAS Y, CHIFFLIER P, et al. Modular verification of programs with effects and effect handlers in Coq [M]//Formal methods. Cham: Springer, 2018: 338-354.
	[2020-09-24]. https://bitcoin.org/bitcoin.pdf.
[36]	DE VRIES A. Bitcoin’s growing energy problem [J]. Joule, 2018, 2(5): 801-805.
[37]	ABATE A, KATOEN J, LYGEROS J, et al. Approximate model checking of stochastic hybrid systems [J]. European Journal of Control, 2010, 16(6): 624-641.
[38]	FU H, CHATTERJEE K. Termination of nondeterministic probabilistic programs [M]//Verification, model checking, and abstract interpretation. Cham: Springer, 2019: 468-490.
[39]	HOEFFDING W. Probability inequalities for sums of bounded random variables [M]//The collected works of Wassily Hoeffding. New York: Springer, 1994: 409- 426.
[40]	CHATTERJEE K, FU H, GOHARSHADY A K, et al. Computational approaches for stochastic shortest path on succinct MDPs [C]//Proceedings of the 27th International Joint Conference on Artificial Intelligence. Stockholm: AAAI Press, 2018: 4700-4707.
[41]	FENG Y, ZHANG L, JANSEN D N, et al. Finding polynomial loop invariants for probabilistic programs [M]//Automated technology for verification and analysis. Cham: Springer, 2017: 400-416.
[42]	FARKAS J. A fourier-f′ele mechanikai elv alkalmaz′asai [J]. Mathematikai′es Term′eszettudom′anyi ′ Ertesit¨o, 1894, 12: 457-472 (in Hungarian).
[43]	BARTHE G, ESPITAU T, GR′ EGOIRE B, et al. Proving expected sensitivity of probabilistic programs [J]. Proceedings of the ACM on Programming Languages, 2018, 2(POPL): 57.
[44]	LETAN T, R′ EGIS-GIANAS Y, CHIFFLIER P, et al. Modular verification of programs with effects and effect handlers in Coq [M]//Formal methods. Cham: Springer, 2018: 338-354.