约束求解公开课
约束求解简介
约束模型介绍
符号主义：问题可以描述清楚
整体过程：
约束数学语言：
一阶谓词逻辑特别复杂，比如费马大定理，是不可判定的，
于是只支持一些smt的背景理论：
问题分类：
约束模型：
SAT问题：
布尔可满足性问题：给定一个命题逻辑公式，判断是否存在使其为真的赋值
其中的离散数学基础：
Tseitin编码：
应用：
电路等价性验证、密码分析
SMT：
应用：软件验证、符号执行
线性规划：
可以引入新变量表达以转换为标准型：
CSP
特点是全局约束，CSP求解器对全局约束有专门的处理方法，之前的方法不是特别支持：
求解器
完备算法
算法框架：
基本采用回溯：
决策启发式
即认为一个变量经常产生冲突，那它接下来也可能会引起冲突。我们求解希望尽早产生冲突，这样我们就可以尽早把这个分支裁掉
推理技术
propagate，比如进行一个x1的赋值后，可以对其他子句进行化简
同理还有域传播：
sat里的冲突分析
不完备算法，局部搜索
基本算子
如何处理局部最优是一个重要问题，比如一些随机扰动、惩罚
初始化
评分函数
搜索启发式
神经网络验证——SMT方法
神经网络鲁棒性：
加入微小噪声就有错误判定。
在正常样本上做一个小扰动，认为神经网络仍不影响对这个输入样本的判断（即后面的e.g）
什么是神经网络？
函数，是由简单函数复合构成的
affine放射函数（线性）： y = Wx + b
ReLU激活函数（非线性）：max(0, x)
如果是做一个分类任务，输出是一个Rn(n 维向量)，代表n个分类得到的分数或概率
期望给定一个输入的范围，所有的输出都不会有坏的行为
即f比如为分类任务，X为输入，P为理想输出，期望所有f(x)都落在P中
面临的挑战：
可扩展性、输入空间大、非线性
难以通过验证结果推断真实鲁棒性、目前只关注安全性而没关注隐私性等什么的
方法：
以一个简单的神经网络为例：
先是一个，比如第一层x1x2，第二层x3x4，全连接层：前一层和后一层的任意两点之间都有边连接。按照权值做仿射变换
上图编码将RELU转换为了线性实数范围内的约束
但上述这样编码是比较慢的，于是我们可以考虑不要析取了，而单独将Relu编码成一种约束，构造成一个新theory叫ReLu pairs（一个二元关系） 如何依据relu对做一些推理规则
线性等式约束+只有合取，其实就是线性规划问题
分为basic变量和非基变量，即基变量（红）必须是非基变量（蓝）的线性组合，我们只能自由变换非基变量。如果想变基变量 ，使用Pivot 把想变的基变量与一个非基变量交换
B
T：储存线性等式的表，因为将变量排好序了，表中只需要储存系数即可
l,u：每个变量的上下界
a：每个变量的当前赋值
右边的z1,z2,z3初始的基变量直接把原先左边的0换掉就行了
规则：
update：如果非基变量不在下界与上界之间，就需要update换值
success：一个值处于在上界与下界之间，那就是sat的
Pivot1：如果一个基变量比下界还小，就需要找一个非基变量与它做交换，希望这个非基变量的赋值改变能使这个基变量变大（线性等式，比如如果这个非基变量前面的系数是正的，它变大，基变量就会变大；系数为负，它变小，基变量也会变大）。所以能选择的变量：前面系数是正的，并且该变量还没有到达它的upper bound；前面系数是负的，并且该变量还没有到达它的lower bound.
交换之后把新的交换后的基变量的系数除成1，然后把其他线性等式使用到xj的也用这条当前等式换掉，保证右侧没有基变量
加上Reluplex
Update：a(xj) = Relu(a(xi))，第一个是调整xi的，第二个是调整xj的
PivotForRelu：只要选取一个能使它变化的系数不为0的变量就可以了，没有做太多限制，因为Relu的变化不像线性的那么直观
ReluSplit：由于是分段函数，经过一定次数的pivot可能还是不满足，并且sat,unsat都证明不出来。如果它的下界<0，上界大于0，说明它确实是分段非线性的，可能是激活的，也可能是非激活的。于是将它分成2段，一段是上界为0，另一段是下界为0
还是优先做线性的pivot
举例：
初始数值界：抽象解释算的。然后随机做一组赋值，y和x7的赋值不在Bound中
x7需要变大，挑了正系数的x5（x1变小也行，但是x1现在已经是-1不能再往下走了；x2也可以，但我们首选了x5，因为x5前面的系数比x2前面的系数更大）。由于x7是基变量，需要对x7做pivot
同理调整y
右上图时所有变量的赋值已经满足上下界要求，但是还要检查relu对是否满足，比如x6=Relu(x4)，但是不满足，假设这里就split，启发式选择x4做split（x4,x6发生的冲突次数更多，而x3,x5还没有发生过冲突）。然后就分成上下界两部分，线性等式不用变，只用变界表
NP-Complete
modulo：满足某些固定范式的约束问题
混合整数线性规划：
MLIP for uncertain ReLu，其实都是分支限界
ReLu分类：每个变量 Relu输入都会有一个可靠的界，可分为一定激活activated(恒正>0)，一定不激活deactivated（恒负）和uncertain（我们根据界可能判断是uncertain，但我们的界通常范围更大，但它本身可能不是Uncertain的，后续界限变化，它也可能就不再uncertain）。非uncertain的其实就是线性函数
上图如果ti+1为0或者1，代表激活与非激活，取0时结合式子1，就是激活的情况，取1时间看式子2，4就是非激活的情况
LP encoding：线性规划，只能sound而不complete，于是用三角形包住
上界是虚线，下界是两条实线
generic framework
基于分支限界：
做一定pivot（也算局部搜索）之后，要做split，分成激活与非激活两个分支。走着走着，如果得到结果，可以将约束求解的结果合取进去，别的变量有的范围也会顺势缩进
还用了局部搜索，就快速得到反例，不用再做额外的分支
三个核心：计算边界（通过不断assertion将范围缩得更紧，更有助于得到unsat（界越窄越容易不符合即unsat））、分支选择、约束求解
整体框架其实就是：
split就分分支走，并行走入两个分支，走进分支之后先根据这条分支的要求计算一个新的bound，如果是满足属性unsat的，就回溯到分出这个分支的上一步结点；如果直接是sat就有反例了，就直接return；如果还有子问题，就推进队列里慢慢看 backtrack是什么意思呢，要做什么？
在分支环节进行优化：
并行实现
uncertain Relu的选择应该可以有优先级：CDCL冲突子句
CDCL弹性滤波
在一群assertion中推出冲突了，在这一群冲突中找最关键的断言 =>给断言一些弹性，比如引入了si放松。每次就把其他约束设为紧的，当前变松弛，如果一个assertion需要松弛的量越大，它对这个冲突产生的影响越大；如果一个断言稍稍松弛一下就能让冲突消去了，说明它对这个冲突产生的贡献小
Node dependency
相当于提供了一些额外冲突，某些Node激活，能推出另外的node非激活这样...
将所有神经元的激活依赖关系画成一张依赖图，如果结点a激活能推出结点b激活，依赖图就存在a到b的一条有向边
Sum of Infeasibilities
如果这个东西不可满足，那么激活前与激活后会有差。
zi hat指激活后，fsoi就是指激活前和激活后的值造成的误差，min的两项分别对应max取zi和max取0两种情况，对误差做累和，这个值越小，说明不可行性越小，就更容易找出一个正确的解（return sat）
先split靠前层的神经元，做到后面的层的时候，这个split一定是有效的（如果先做后面，可能上近似范围太大了，先算了第0层，给了准确的界，那第一层的界也一定更准确了，相当于利用了神经网络的结构化信息）
神经网络增量验证：
当神经网络只发生微小改动的时候，如果复用旧的验证，继续做新的经过微小扰动的神经元验证