Probabilistic programming is a programming paradigm that combines general computer programming, statistical inference, and formal semantics to help systems to made decisions when facing uncertainty. Probabilistic programs are ubiquitous and believed to have a major 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 been attracting a lot of interest. Many challenges, however, still remain. Our work presented in this paper, probabilistic relations, takes a step into our vision to tackle these challenges. Our work in essence is based on Hehner's predicative probabilistic programming, but there are several obstacles to the wider 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 the Kleene's fixed point theorem; (4) the enrichment of its semantics from distributions to subdistributions and superdistributions in order to deal with the constructive semantics; (5) the unique fixed point theorem to largely 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 six interesting examples, and among them, one is about robot localisation, two are classification problems in machine learning, and two contain probabilistic loops.

翻译：概率编程是一种融合通用计算机编程、统计推断和形式语义的编程范式，旨在帮助系统在面临不确定性时做出决策。概率程序无处不在，并被认为将对机器智能产生重大影响。尽管许多概率算法已在不同领域的实践中得到应用，但基于形式语义的自动化验证仍是一个相对较新的研究领域。在过去二十年中，该领域已引发大量关注，但仍面临众多挑战。本文提出的概率关系研究，正是朝着解决这些挑战迈出的一步。我们的工作本质上基于Hehner的谓词式概率编程，但其成果的广泛推广仍面临若干障碍。本文的主要贡献包括：(1) 通过引入艾弗森括号表示法将关系与算术分离，形式化其语法与语义；(2) 使用统一程序设计理论建立关系的形式化，并通过实数拓扑空间上的求和实现括号外概率的形式化；(3) 基于Kleene不动点定理构造概率循环的构造性语义；(4) 将语义从分布扩展至子分布与超分布以适配构造性语义；(5) 提出唯一不动点定理以大幅简化概率循环的推理；(6) 在Isabelle/UTP（即Isabelle/HOL中的UTP实现）中机械化我们的理论，实现基于定理证明的自动推理。我们通过六个典型示例进行验证，其中涉及机器人定位、两个机器学习分类问题及两个包含概率循环的案例。