Formal verification of probabilistic algorithms
Formal verification of probabilistic algorithms
复制标题
概率算法的形式验证
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Joe Hurd
中科院分区：
文献类型：
--
作者：
Joe Hurd
本论文展示了如何使用机械定理证明器来正式验证概率算法。我们从概率的广泛基础发展开始，创建数学测度论的高阶逻辑形式化。这允许定义我们用来建模随机位生成器的概率空间，它非正式地是硬币翻转流，或者技术上是 IID Bernoulli( 2 ) 随机变量的无限序列。概率程序使用函数式编程中熟悉的状态转换器单子进行建模，其中随机位生成器在计算中传递。函数从生成器中删除随机位以执行计算，然后将更改后的随机位生成器与结果一起传回。我们对随机位生成器进行概率空间建模，使我们能够给出此类程序的精确概率规范，然后在定理证明器中验证它们。我们还开发旨在加快验证的技术支持：概率量词；包含可测量性和独立性的组合属性；概率 while 循环以及概率为 1 的终止的正式概念。我们还引入了一种技术，用于将概率 while 循环的属性简化为保证终止的程序属性：然后可以使用程序正确性的归纳和标准方法来建立这些属性。我们通过一些示例概率程序演示了正式框架：四种概率分布的采样算法；一些通过抛硬币生成骰子的最佳程序；对称简单随机游走。此外，我们还验证了 Miller-Rabin 素性测试，这是一种众所周知的商业使用的概率算法。我们的基本观点使我们能够定义具有强大属性的版本，我们可以在逻辑中执行该版本以证明数字的复合性。
This thesis shows how probabilistic algorithms can be formally verified using a mechanical theorem prover. We begin with an extensive foundational development of probability, creating a higherorder logic formalization of mathematical measure theory. This allows the definition of the probability space we use to model a random bit generator, which informally is a stream of coin-flips, or technically an infinite sequence of IID Bernoulli( 2 ) random variables. Probabilistic programs are modelled using the state-transformer monad familiar from functional programming, where the random bit generator is passed around in the computation. Functions remove random bits from the generator to perform their calculation, and then pass back the changed random bit generator with the result. Our probability space modelling the random bit generator allows us to give precise probabilistic specifications of such programs, and then verify them in the theorem prover. We also develop technical support designed to expedite verification: probabilistic quantifiers; a compositional property subsuming measurability and independence; a probabilistic while loop together with a formal concept of termination with probability 1. We also introduce a technique for reducing properties of a probabilistic while loop to properties of programs that are guaranteed to terminate: these can then be established using induction and standard methods of program correctness. We demonstrate the formal framework with some example probabilistic programs: sampling algorithms for four probability distributions; some optimal procedures for generating dice rolls from coin flips; the symmetric simple random walk. In addition, we verify the Miller-Rabin primality test, a well-known and commercially used probabilistic algorithm. Our fundamental perspective allows us to define a version with strong properties, which we can execute in the logic to prove compositeness of numbers.