一个栗子

比如我们有一袋子卡片，已知里面有一些卡片，而这些卡片中有一些可能被涂成了蓝色的，有一些可能是白色的，具体的数量和比例都不缺定。我们现在可以进行n次抽取，查看后放回袋子里。

贝叶斯统计步骤

设计模型（conjecture）
根据数据，进行条件判断（update）
评估模型（critique）我们的推测Conjecture是什么？

如果蓝色的比例是p，那么白色的一定是1-p
每次抽取都是独立的。

我们假设存在一个p在[0,1]这个区间。这是我们的先验。

再在根据看到的结果（data）进行条件判断，更新我们的p。

具体的步骤：

建立一个联合模型：
- 变量有：
  - data 观测到的数据
  - parameters 待求的变量
- 给data distribution赋值（likelihood）这些值都是先验得到的
- 给parameter distribution赋值（prior）
给定输入，推测联合后验

回到例子中，我们的变量有：

N：一共抽取了N次（data）
b：一共有抽出了多少蓝色的卡片（data）
p：蓝色卡片的占比（parameter）

我们的联合模型：

$b \sim Binomial(N,p)$ data distribution
$p \sim Uniform(0,1)$ prior distribution

所以根据贝叶斯定理，

$posterior = \frac{likelihood \times prior}{average\;likelihood}$

得到后验概率：

$Pr(p|b,N) = \frac{Pr(b|p,N) Pr(p)}{\int Pr(b|p,N)Pr(p)dp}$

什么是概率编程

本质思想是取样所有可能的结果，并得到confidence

就是在普通的编程上添加两个特性：

有从各种分布中随机取值的能力
有根据观察进行条件判断从而决定变量的值的能力

换一种说法就是概率编程能够从正向和反向运行：

正向：计算假设的结果
反向：从观测的数据影响条件（限制可能的解释）

概率编程语言Probabilistic Programming Language

一般来说组成一门语言，需要syntax语法和semantic语义

我们可以看到，基本上概率编程语言的syntax就是在普通编程语言syntax的基础上添加了分布。

那么对应的semantics上我们也添加了概率，

Data Flow

举例来说给变量x赋值一个伯努利分布，如下：

$(x := Bernoulli(p),\sigma) \xrightarrow{p} \sigma[x \leftarrow True]$ $(x:= Bernoulli(p),\sigma) \xrightarrow{1-p} \sigma[x \leftarrow False]$

一个实例：

$({x \rightarrow ?, y \rightarrow ?}, 1.0)$

1	x:=Bernoulli(0.7)

$({x \rightarrow \top, y \rightarrow ?}, 0.7),
({x \rightarrow \perp, y \rightarrow ?}, 0.3)$

1	y:=Bernoulli(0.2)

$({x \rightarrow \top, y \rightarrow \top}, 0.14), ({x \rightarrow \top, y \rightarrow \perp}, 0.56),\\\\ ({x \rightarrow \perp, y \rightarrow \top}, 0.06), ({x \rightarrow \perp, y \rightarrow \perp}, 0.24)$

然后我们需要观测，如：

1	observe x == True

$({x \rightarrow \top, y \rightarrow \top}, 0.14/(0.14+0.56)),\\ ({x \rightarrow \top, y \rightarrow \perp}, 0.56/(0.14+0.56)))$

obeserve 忽略不符合的executions，并正则 $\frac{Pr(non\:stuck\:state)}{\frac{num\:observe\:true}{num\:all\:observation}}$
assume 忽略不符合的execution
assert 让不符合的execution失败

Symbolic Probabilistic Analysis

User Profile

给予我们的输入加一个概率，即我们现在知道某个输入出现的概率是多少。

Symbolic Execution

假设我们有如下函数

public void checkSafety(int pressure,
  int altitude, int spinSpeed){

  int discountedPressure = pressure - altitude/2;
    ...
    if(discountedPressure > 80 && spinSpeed>72){
     abort();
  }
  ...
  return;
}

Path Condition(pc)即到达这个情况的路径，比如上面的函数我们想要安全的达到最后的return，而不在中途abort，那么我们就要从root达到图中两个绿点。每个中间节点就相当于一个条件判断，而我们就象征性Symbolic地走到了想要到达的leaf。

Path Condition有什么用呢？
他使得我们无论怎么分割树的leaf，我们都会获得这些leaves都将是相互独立的。

比方说上面那两个情况，我们就可以直接求

$Pr(PC_1) + Pr(PC_2)$

而不用去计算再减去两者的交集 $Pr(PC_1 \wedge PC_2)$

你可能还想问这有什么用？举个例子，上面那段是1981年失事的哥伦比亚号的一段检查代码，如此判断有几千个之多，我们如何能保证这些代码的可靠性呢？

$\begin{align} Pr(PCs|UP) &= \sum_{i=0}^n Pr(PCs|US_i) p(US_i)\\\\ &= \sum_{i=0}^n \frac{Pr(PCs \wedge US_i)}{Pr(US_i)} p(US_i) \\\\ &= \frac{\frac{num\:(PCs \wedge US_i \wedge D)} {num\:(D)}}{ \frac{num\:(US_i \wedge D)}{num\:(D)} }\\\\ &=\frac{num\:(PCs \wedge US_i \wedge D)}{num\:(US_i \wedge D)} \end{align}$

显然，即使在有限的范围内，通过穷举会消耗polynomial时间，太久。

这时候我们的Symbolic Execution就可以派上用场了，因为他保证了独立性，所以我们可以用分治法。因为独立的clause可以被记录并再利用。这样就比NASA当时的算法快 $10^4$ 倍。

Arbitrary Numerical Constraint

上面的例子都是离散的，但是真实的世界可不是，更多的情况我们需要预估连续的函数。

[Hit-or-Miss Monte Carlo]
[Interval Constraint propagation]
[Stratified sampling]
[Optimal sampling allocation]
[未完待续]

PyMC3

讲了这么多，都是simple ppl或者是用其他语言模拟的概率编程。我们来看一下PyMC3。

Model Variables

Random variables: m.basic_RVs
Free variables: m.free_RVs
Observed variables: m.observed_RVs

[Skipping lots of content]

Spurious Model

Predictor Residual Plot
以A为因，输入B中，我们会得到两个量

一个是Posterior后的 b
另一个是Posterior后的 mu
每一个算粗来线都和

看他们的residual大小