This is a summary of the group meeting on 20 January 2021

First-Order Quantified Separators

这篇文章定义了 separator 的概念以及 quantified separation 问题，并给出用 separator 来推断量词 alternating 不变量的方法。

具体来说，本文首先定义 k-SEP 问题是确定一个带有 positive 和 negative 两种标记的 structure 集合能否被一个 k 个 prefix 的 前束范式分开。文章一方面对给定的一个 3-SAT 公式构造它所 separate 的 structures，另一方面把一些 structures 能否被 separate 的问题转化为一个 SAT 公式是否可满足的问题，来说明 separation 问题是 NP-complete 的。这种对应本身蕴含了找到一个 separator 的方法，如果得到的 SAT 公式是可满足的，那么通过满足性赋值可以构造一个 syntactic 的 separator。文章给出了一些必要的优化方案。这种 separation 的方法能够用于解 IC3/PDR 所产生的 inductive generation queries，以配合 IC3/PDR 找到量词 alternating 的不变量。这是本文的创新之处。

讨论和思考：

1. 这种 separation 方法它的输入是什么，是这些图吗？ 输入是 transition system，更具体地，文中的测试用例都是 first-order and many-sorted logic 所表达的 transition system。演示文稿中的无向图只是为了演示方便。

2. 它和 synthesis 的关系是什么？ Separator 与 synthesis 的联系不太大，不过 separator 的概念和 interpolant 有些相似，interpolant 也可以看作 separate 一些 states 的 separator。

---

ReluDiff: Differential Verification of Deep Neural Networks

论文的主要Motivation是对相同输入、相同结构的两个神经网络做输出差异的量化验证。由于传统的对于神经网络验证的方法只关注单独一个网络，对于上述问题，只能将两网络的结果在输出层进行相减。

本文就在Reluval的符号区间分析的基础上加入了差异的区间分析，并提出了差异在仿射变换和ReLU变换的方式，在同样保证结果是过近似以外，对于对应节点的激活状态（inactive，active，non-linear），提出了三种优化差异界限的方法。并在最后提出了Refinement的做法来提升验证的精度。

讨论和思考：

1. 网络是否必须结构相同？ 是的。
2. Reludiff的精度是否比Deeppoly高？ 不确定。