概率程序验证的理论研究

In recent years, due to the increasing complexity of computer systems, the traditional approach of testing becomes less reliable on detecting critical bugs in systems as it cannot cover all execution paths. Program verification is the study of proving program correctness through rigorous approaches such as logic and mathematics. Compared with testing, program verification can cover all execution paths, thus is receiving increasing attention. We consider program verification for probabilistic programs. Probabilistic programs are programs with stochastic sampling, thus can be applied to stochastic systems such as randomized algorithms, distributed systems, cyberphysical systems, systems with artificial intelligence, etc. We study new approaches for proving correctness over probabilistic programs, including theory, algorithm and computational complexity for proving termination, running time, accumulated cost, probabilistic logical specifications for probabilistic programs, etc. Currently, the verification theory for probabilistic programs is largely immature. In this project, we aim to establish a series of new fundamental results for verification of probabilistic programs. We expect that our results will lay a solid foundation for both applications in stochastic systems and implementation of verification tools.

近年来，由于计算机系统的复杂性逐年上升，通过传统测试方法越来越难以保证关键系统不出现重大漏洞，而通过程序验证确保关键系统正确性的方法正得到越来越广泛的关注。程序验证是理论计算机科学以及形式化方法的一个重要分支，其目的在于通过严格的方法以证明程序的正确性。概率程序是带有概率赋值语句的程序，在随机算法、分布式系统、信息物理系统、人工智能系统等具有随机性特征的系统中扮演着重要的角色。本项目关注如何从理论上通过逻辑和数学方法以证明概率程序的正确性，具体将着重探讨如何对概率程序的各种正确性性质（包括终止性、运行时间、资源消耗以及概率逻辑规范等）进行验证，并研究相关验证理论、算法和计算复杂性。目前，概率程序的验证理论尚处于起步阶段，理论框架尚不成熟。本项目预期建立起针对概率程序形式化验证的一系列基础性、原创性理论成果，为之后的验证工具实现以及具体场景的应用研究打下坚实的基础。

项目背景：.. 本项目以概率编程为背景，考察概率程序的形式化方法理论，即如何通过数学方法严格保障概率程序的正确性。概率程序是带有概率语句的程序，在概率建模、人工智能、随机算法等方面具有潜在的应用价值。在一些安全关键场合，一些重要的概率性质（如终止性、灵敏性、资源消耗、断言等）必须被满足。因此，针对这些性质的形式化方法理论在这些场合中具有重要的意义。..主要研究内容：.. 本项目主要研究概率程序终止性、资源消耗、灵敏性以及断言方面的形式化方法理论。终止性考察如何通过数学方法证明给定概率程序是否在概率意义下是终止的。资源消耗考察如何通过数学方法以及算法自动输出概率程序执行过程中所消耗资源的期望值上下界。灵敏性主要考察如何证明概率程序在输入有轻微扰动的情况下其输出在期望意义下是否也是微小的。断言主要考察如何分析概率程序中预设的断言逻辑条件被违反的概率紧致上下界。..重要结果：.. 本项目在概率程序终止性、资源消耗、灵敏性以及断言的形式化方法理论方面均取得理论突破。在终止性方面，给出了概率程序几乎处处终止性的鞅理论方法框架以及相关验证算法。在灵敏性方面，给出了一般情况下概率程序灵敏性验证的数学理论以及验证算法。在资源消耗分析方面，给出了一般情况下的鞅理论方法。在断言分析方面，给出了基于不动点理论的断言概率上下界分析。以上结果均发表在程序语言理论国际著名学术会议POPL、PLDI、OOPSLA（CCF A类）等上。其中部分成果发表于剑桥大学出版社出版的专著章节中。..科学意义：..本项目所作成果考察概率程序形式化方法的基础理论，在终止性、灵敏性、资源消耗以及断言等概率程序的基本性质层面均作出了理论突破，为概率程序形式化方法理论的发展打下坚实的基础。