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 relations, 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.

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