首届国际理论计算机联合大会（International Joint Conference on Theoretical Computer Science，IJTCS）于2020年8月17日-22日在线上举行，主题为“理论计算机科学领域的最新进展与焦点问题”，由北京大学与中国工业与应用数学学会（CSIAM）、中国计算机学会（CCF）、国际计算机学会中国委员会（ACM China Council）联合主办，北京大学前沿计算研究中心承办。

　　8月19日，大会“机器学习与形式化方法”分论坛如期举行，由中国科学院软件研究所张立军研究员主持。小编为大家带来论坛精彩回顾。

Neural Networks: Fairness and Interpretability
孙军，Singapore Management University

　　讲者首先从现有的 AI 算法所存在的一些问题（如识别错误）引入，类比现有的非 AI 程序中存在的 bug，来解释 AI 程序中的 bug——不公平问题是如何产生的，继而给出了 AI 算法（尤指神经网络）中“公平”的定义。报告介绍的论文提出了一种检测神经网络不公平因素的模型（ADF）和验证神经网络算法有效性的方法（PFA）。在检测方面，其巧妙地利用神经网络中回传的梯度，对输入特征进行干扰，从而高效、准确地测试出干扰项。在验证方面，则将训练后的神经网络的隐藏层中蕴含的信息进行提取、聚类，从而对原神经网络进行抽象，更方便最终的验证。在与几种已有的检测、验证神经网络算法的方法比较之后，实验结果显示作者提出的方法获得了较好的效果。

PAC Model Checking of Block-Box Continuous-Time Dynamical Systems
薛白，中国科学院

　　现在科技对自动化的追求，推动了许多人工智能黑盒子的出现。这些系统相对理想安全的模拟运行环境下保证了它们的稳定。但是，在现实环境中如何确保这些系统仍能稳定运行至关重要。这便涉及到了对 AI 模型进行验证的方法。

　　论文提出了一种对连续时间的动态黑盒子系统进行验证的方法——PAC 方法。它首先给出了详细的黑盒子系统和验证问题的数学模型和定义，并在此基础上引出了 PAC 方法中的相关数学定理。

　　该模型首先从数据中获取独立同分布的时间序列集合 t_j、独立同分布的输入数据集合 x_i，以及根据时间 t_j、输入 x_i，使用黑盒模型计算出的 y_i,j。这样的一组 (x, t, y) 被当作 PAC 的一个输入轨迹。PAC 模型利用了简单的线性规划思想。将无限时间的优化问题，转化为一定的时间间隔内，每个场景的单独优化。同时优化过程中加入了鲁棒性约束，考虑了误差概率和置信度指数，从而达到对整个系统进行验证的作用。作者详细介绍了针对单组数据和多组数据的情况下，算法运行的详细情况。并且，该方法在很好的解决相关黑盒子问题的同时，对大规模系统同样适用。

Safety Certification of Deep Learning
黄小炜，University of Liverpool

　　讲者首先介绍了深度学习算法的安全性检测问题。他首先大致讲解了深度学习算法的几种风险，包括 robust risk，generalize risk，security risk，fairness risk，data privacy risk，understanding risk 等，然后讲解了关于 AI 安全近些年的发展。

　　接下来，讲者介绍了有关模型验证的定义。模型验证主要是通过验证算法来提取模型中成功的案例和失败的案例，其中失败的案例可以用来对模型进行进一步的加深优化。在此定义基础上，讲者讲解了一些 SOTA 的方法和他们的常规想法。这些 SOTA 主要可以分为 constraint solving based method，approximation method，anytime method。这些方法主要用于避免鲁棒性风险（robust risk）。

　　最后，整个报告对深度学习中安全验证所面临的挑战进行了总结。主要包括：Scalability，Adaptive Machine Learning，Interaction of Interpretability with Certification，Correct by Construction。

Spectral Analysis of Convolutional Neural Networks
易新平，University of Liverpool

　　卷积神经网络（CNN）在深度学习领域应用广泛，许多更复杂的卷积神经网络被不断提出。为什么卷积神经网络这么成功？论文试图用谱方法来分析卷积神经网络。

　　为了了解卷积神经网络中卷积层的行为，作者通过谱密度矩阵（spectral density matrix）来表示卷积层的线性变换，发现谱密度矩阵的奇异值分布和卷积层线性变换矩阵的奇异值分布渐进一致（asymmetrically identical），因此对于线性卷积层的谱分析可以在相应的谱密度矩阵上进行。

　　这样的谱分析方法可用于奇异值估计（singular value approximation）和谱范数界限（spectral norm bounding），进而用于正则化增强模型的泛化性能。