J Shanghai Jiaotong Univ Sci ›› 2023, Vol. 28 ›› Issue (6): 772-782.doi: 10.1007/s12204-022-2456-z
王培新
接受日期:
2021-01-12
出版日期:
2023-11-28
发布日期:
2023-12-04
WANG Peeixin(王培新)
Accepted:
2021-01-12
Online:
2023-11-28
Published:
2023-12-04
摘要: 对于概率程序,已有一些关于期望或均值的定性和定量分析工作,例如期望终止时间和预期消耗分析。然而,另一个非常重要的问题是尾部界限(即尾部概率的上界),可以为极端事件提供高概率保证。在这项工作中,我们关注的问题是对于非确定性概率程序消耗的尾部界限分析,旨在自动获取这些程序的资源使用的尾部界限。为了实现这一目标,提出了一种新颖的方法,结合适当的集中不等式,来推导程序终止之前累积消耗的尾部界限。提出的方法可以处理正、负消耗。此外,这个方法实现了基于模板的排序上鞅的自动合成,并产生了一个高效的多项式时间算法。为了展示提出的方法的有效性,提供了对不同程序的实验结果,并与最先进的工具进行了比较。
中图分类号:
王培新. 非确定性概率规划的尾界代价分析[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.
[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. |
[1] | 曾志贤,曹建军,翁年凤,袁震,余旭. 基于细粒度联合注意力机制的图像-文本跨模态实体分辨[J]. J Shanghai Jiaotong Univ Sci, 2023, 28(6): 728-737. |
[2] | 曹鹤玲a,b,刘方正a,石建树a,楚永贺a,邓淼磊a. 基于随机搜索和代码相似性的程序自动修复[J]. J Shanghai Jiaotong Univ Sci, 2023, 28(6): 738-752. |
[3] | 胡铭轩, 乔钧, 张执南. 连续康复训练动作分割与评估(网络首发)[J]. J Shanghai Jiaotong Univ Sci, 0, (): 0-. |
阅读次数 | ||||||
全文 |
|
|||||
摘要 |
|
|||||