Probabilistic programming combines general computer programming, statistical inference, and formal semantics to help systems make decisions when facing uncertainty. Probabilistic programs are ubiquitous, including having a significant impact on machine intelligence. While many probabilistic algorithms have been used in practice in different domains, their automated verification based on formal semantics is still a relatively new research area. In the last two decades, it has attracted much interest. Many challenges, however, remain. The work presented in this paper, probabilistic unifying relations (ProbURel), takes a step towards our vision to tackle these challenges. Our work is based on Hehner's predicative probabilistic programming, but there are several obstacles to the broader adoption of his work. Our contributions here include (1) the formalisation of its syntax and semantics by introducing an Iverson bracket notation to separate relations from arithmetic; (2) the formalisation of relations using Unifying Theories of Programming (UTP) and probabilities outside the brackets using summation over the topological space of the real numbers; (3) the constructive semantics for probabilistic loops using Kleene's fixed-point theorem; (4) the enrichment of its semantics from distributions to subdistributions and superdistributions to deal with the constructive semantics; (5) the unique fixed-point theorem to simplify the reasoning about probabilistic loops; and (6) the mechanisation of our theory in Isabelle/UTP, an implementation of UTP in Isabelle/HOL, for automated reasoning using theorem proving. We demonstrate our work with six examples, including problems in robot localisation, classification in machine learning, and the termination of probabilistic loops.

翻译：概率编程融合通用计算机编程、统计推断与形式语义学，以帮助系统在面临不确定性时做出决策。概率程序无处不在，对机器智能产生了重要影响。尽管许多概率算法已在不同领域得到实际应用，但基于形式语义的自动验证仍是一个相对新兴的研究领域。过去二十年间，该领域已引起广泛关注，但仍存在诸多挑战。本文提出的概率统一关系（ProbURel）为实现应对这些挑战的愿景迈出了一步。我们的工作基于Hehner的谓词概率编程，但其更广泛采用仍存在若干障碍。本文的贡献包括：（1）通过引入Iverson括号标记分离关系与算术运算，形式化其语法与语义；（2）利用统一编程理论（UTP）形式化关系，并通过实数拓扑空间上的求和运算形式化括号外的概率；（3）基于Kleene不动点定理构建概率循环的构造性语义；（4）将语义从分布扩展至子分布与超分布以处理构造性语义；（5）提出唯一不动点定理以简化概率循环的推理；（6）在Isabelle/UTP（UTP在Isabelle/HOL中的实现）中对理论进行机械化，以支持基于定理证明的自动推理。我们通过六个案例展示工作成果，涵盖机器人定位、机器学习分类及概率循环终止等问题。