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

Beyond the Single Neuron Convex Barrier for Neural Network Certification

这篇文章提出了k-relu的神经网络验证框架，可以同时计算k个relu节点的最优凸松弛，相比于每次计算单个神经元的上下界，在保证神经网络验证规模的情况下提高了验证效率，还可以和现有一些主流的验证器相结合。

对于比较大的k，本篇文章还提出了一种计算k-relu的方法，降低计算复杂度，同时提高了只计算l-relu的精确性。

然后文章将k-relu和现有的验证器deeppoly相结合，得到新的验证工具k-poly，这个工具相比于deeppoly和refinezono能验证更多的性质并且所花时间要低于refinezono。

Comments：

这篇文章思路比较简单，非常有趣，可以考虑一下和TACAS的一篇文章的方法用进来可以提高k-poly的精确性。然后可以将这个框架用到我们的工具上复现一下。

Questions：

实验结果的第二列的那些数据是什么意思？

这是用神经网络对1000张图片进行识别，前面的这些九百多的数字分别表示这个神经网络能正确分类的图片个数，这里就是对神经网络正确分类图片的例子做鲁棒性验证，这里添加了无穷范数球上的一个小扰动，ε就是扰动半径。

---

Proving Termination Through Conditional Termination

这篇文章提出了一种分析程序终止性的方法，作者定义了有条件终止(conditional termination)，即如果存在 程序位置 l 和条件φ，使得所有在 l 处满足 φ 的程序路径都一定终止，则说该程序是(l , φ) – 有条件终止的。基于这一思想，作者提出了（1）使用Max-SMT求解器，结合Ranking Function和模版约束求解的寻找有条件终止的(l , φ)的方法；（2）利用求出的有条件终止的条件来对程序做简化，以优化程序终止性和非终止性的分析。

同时该作者也开发了针对C++的程序分析工具VeryMax，该工具对比当时的其它工具在耗时和验证成功率上均有较好的表现，但其不足为不支持递归，以及指针操作的分析。此外，该方法求解时使用的约束模版和Ranking Function均为线性模版，且我个人认为求解过程比较依赖于求解器的效率。

Questions&Comments：

• 该文章的前半部分说的算法是一次生成一个终止条件么？

  不是这样的，文章中的算法一 CondTerm 可以使用Max-SMT求解器通过多次迭代，求出一个SCC（强连通分量）上所有程序位置的一个终止条件（针对该SCC的，即保证该SCC一定终止）（当然求解器也可能求不出解）。

• 这篇文章前面都在说终止性分析，为什么实验部分有非终止性分析？

  这里工具实现时是使用了一个后端的非终止性分析工具来分析非终止性，此外Table 3中的实验数据也是为了展现利用条件终止的条件对程序做简化也有可以提高非终止性分析的效率。

• 该工具使用的是非线性的Max-SMT求解器，那么他支持非线性的模板么？为什么？

  我个人认为这里使用的非线性的Max-SMT求解器是因为其可以提高求解效率。这篇文章中没有提到其支持非线性的模板，我个人认为问题还是在求解上（求解器或者求解方法），我在看相关的文献时，总看到求解时用到Farkas’ Lemma，但这个定理我只看到线性的表述，所以也可能是求解方法上限制了模版只能是线性的。

  建议：slides在Ranking Function部分有问题

  这是我的疏忽，已经改正，多谢指出，后面一定注意在这些基础知识上的掌握和理解。