厦门大学系统与网络课题组的一项研究成果被IWQoS’2023录用。第31届国际服务质量研讨会(The IEEE/ACM International Symposium on Quality of Service, IWQoS 2023, CCF B类会议)是网络服务质量领域的顶级会议，将于2023年 6月19日-21日在美国佛罗里达州奥兰多召开，本次会议共录取62篇论文，录取率为23.5%。

具体论文信息如下

Yangfan Huang (厦门大学SNG二年级硕士生), Yuling Lin (厦门大学SNG一年级硕士生), Haizhou Du (上海电力大学), Yijian Chen (上海电力大学二年级硕士生), Haohao Song (厦门大学SNG二年级博士生), Linghe Kong (上海交通大学), Qiao Xiang（厦门大学SNG）, Qiang Li （阿里巴巴）, Franck Le（IBM Research）, Jiwu Shu（厦门大学，闽江学院）

Toward a Unified Framework for Verifying and Interpreting Learning-Based Networking Systems

【论文简介】

机器学习系统具有黑盒特性，模型接受输入并产生相应输出，但不提供任何关于为什么选择该输出的见解。这使得应用机器学习的网络系统不便于调试和进行临时性调整，也难以完成大规模部署。为了理解网络机器学习系统的决策原理和实际能力，我们需要关注：

（1）如何自动验证和解释网络系统的行为；

（2）理解模型预测背后的原因；

现有的工作通常将这二者作为两个独立的、正交的课题来处理。在本文中我们表明机器学习模型的验证和可解释性是紧密相关的，并且可以通过可满足性模数理论（SMT）来统一，并提出“不仅机器学习模型的各种属性可以被规约成SMT问题完成验证，而且许多通常研究的可解释性问题也可以通过迭代检查多个SMT问题的可满足性和相关属性来求解”这一新观点。基于此本文设计了UINT,一个针对网络机器学习系统的通用验证和可解释性框架,能够实现：

（1）允许操作者将验证和可解释性问题规约为SMT公式；

（2）将目标机器学习模型编码为多组SMT约束；

（3）使用SMT求解器自动解决相应的验证和可解释性问题。

模型验证:

验证问题研究的是给定一个网络机器学习系统，验证该系统的训练模型的（输入，输出）映射是否总是满足某些属性。用N来表示训练模型，P是表示模型输入约束的一组谓词逻辑，Q表示模型输出约束的一组谓词逻辑。这样一个系统的验证问题可以定义为：检查SMT公式P∧N→Q是否是一个永真式，这等价于检查P∧N∧¬Q是否是不可满足的。

UINT将广泛的属性统一归纳成SMT公式的形式进而完成验证。我们把网络机器学习系统的常见属性总结为健壮性属性：验证系统对干扰的韧性。我们为健壮性属性提供一个通用的SMT表述，（x^,y^）为已知的输入输出映射，F表示所有输入特征的集合，L表示被扰动的输入特征集合。用P_l表示对可扰动输入特征的谓词逻辑，P_r表示对其他输入特征的谓词逻辑。输出约束的谓词逻辑Q为N（x）=y∗。健壮性属性的统一表述为：

模型可解释性：

可解释性问题旨在为操作者提供一套简单的、确定的规则以解释训练过的模型的行为或分析特征以提供解释。这类问题可以抽象成给定一个网络机器学习系统和其输出上的一组谓词逻辑，在其输入上找到一组满足某些标准的谓词，使输出上的谓词总是成立。

UINT关注（1）rule explanation（规则解释），旨在找到一组规则来解释模型会做出某种预测的原因；（2）feature attribution（特征归因），旨在探究特征对于模型输出的贡献。这两类可解释性问题代表了网络机器学习系统中最重要和最常见的可解释性问题。我们也将这些可解释性问题规约成一个通用的SMT公式。P_l表示所研究输入特征L上的谓词，而P_r表示其他输入特征上的谓词。在N (x)上设置输出谓词Q。统一的公式为：

通过不同谓词的设置，该公式可以表示anchor（锚点），decision boundary（决策边界），feature importance（特征重要性），sensitivity analysis（敏感性分析）等多种常见的可解释性问题，如下图。UINT完成设计具体算法，通过迭代验证相关SMT问题和属性的可满足性完成具体可解释性问题的求解。

本文设置多组实验进行验证与解释，与现有可解释技术相比，UINT模型解释覆盖范围提升4倍，单个模型解释问题计算时间最快可达秒级。下图显示了单个模型解释问题计算的执行用时分布，结果证明了UINT在统一验证和解释网络机器学习系统关键问题方面的有效性。

本工作是厦门大学系统与网络课题组在智能网络系统方面的进一步探索，之前的研究工作包括BoxOpt (TON’21, AAAI’19)。

本工作已开源所有核心代码(链接为https://github.com/sngroup-xmu/UINT)。

厦门大学系统与网络课题组主页:

http://sngroup.org.cn/