概率可解循环的基于矩的不变量的自动生成
摘要：概率编程分析中的主要挑战之一是计算总结循环行为的不变属性。不变性生成的自动化仍处于初级阶段，大多数情况下仅针对程序变量的期望值，这不足以恢复完整的概率编程行为。我们提出了一种方法，用于自动生成一类概率编程的基于矩的不变性，称为Prob-Solvable循环，其中包含了对随机变量和参数化分布进行多项式赋值。我们结合了符号求和和统计方法，以导出作为高阶矩的有效属性的不变性，例如程序变量的期望值或方差。我们成功地在几个例子上评估了我们的工作，在这些例子中，计算高阶矩和程序变量不变性的完全自动化尚不可能。
作者：Ezio Bartocci and Laura Kov''acs and Miroslav Stankoviv{c}
论文ID：1905.02835
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2019-05-30