用于建模认知与偶然不确定性的概率统一关系：语义与基于定理证明的自动化推理
计算机科学中的逻辑
2024-09-30 v3 机器学习
编程语言
摘要
概率编程将通用计算机编程、统计推断与形式语义相结合，以帮助系统在面临不确定性时做出决策。概率程序无处不在，并对机器智能产生了重大影响。尽管许多概率算法已在不同领域得到实际应用，但基于形式语义的自动化验证仍是一个相对新颖的研究领域。在过去二十年中，它吸引了大量关注。然而，许多挑战依然存在。本文提出的概率统一关系（ProbURel）向我们应对这些挑战的愿景迈出了一步。我们的工作基于 Hehner 的预测式概率编程，但其工作的更广泛应用存在若干障碍。我们的贡献包括：（1）通过引入 Iverson 括号记号以分离关系与算术，形式化其语法与语义；（2）使用统一编程理论（UTP）形式化关系，并在括号外通过对实数拓扑空间求和来处理概率；（3）使用 Kleene 不动点定理给出概率循环的构造性语义；（4）将其语义从分布丰富到子分布与超分布，以处理构造性语义；（5）使用唯一不动点定理简化概率循环的推理；（6）在 Isabelle/UTP（Isabelle/HOL 中 UTP 的实现）中机械化我们的理论，以使用定理证明进行自动化推理。我们用六个示例展示了我们的工作，包括机器人定位、机器学习中的分类以及概率循环的终止问题。
引用
@article{arxiv.2303.09692,
title = {Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving},
author = {Kangfeng Ye and Jim Woodcock and Simon Foster},
journal= {arXiv preprint arXiv:2303.09692},
year = {2024}
}
备注
The final version before publication. The published version is available at https://doi.org/10.1016/j.tcs.2024.114876