近日，软件工程学院师生在可信人工智能和模型检测两个课题组的多项成果被计算机理论领域顶级国际会议CAV 2024录用，标志着学院在可信人工智能和模型验证领域再次取得关键性进展。

在可信人工智能领域，由于人工智能模型的黑盒特性，如何从系统和深度神经网络模型层面研究系统的安全可信是当前国际学术领域面临的关键难题。 在系统验证层面，可信人工智能课题组在张民教授的指导下，提出了一种基于神经障碍证书（Neural Barrier Certificate）的神经网络控制系统定性和定量统一验证框架，可在无限和有限时间步内定性和定量地证明系统的安全性。该成果证明通过定义适当的NBC可以从不同的维度严格地证明类如智能控制系统等随机复杂系统的安全性，为研究大型智能系统的安全性提供了理论支撑。

图：深度神经网络控制系统定性与定量统一验证框架

在深度神经网络验证层面，课题组联合希伯来大学参与深度神经网络验证工具Marabou 2.0的研制，新的版本支持多种神经网络架构和多类激活函数的验证，验证效率比早期版本有了大幅提升，为工具在实际场景中的应用奠定了基础。

在模型检测方面，博士生夏晔川在李建文青年研究员的指导下，和意大利FBK的NuSmv/NuXmv模型检测工具课题组展开深入合作，提出了一种新的针对活性性质的模型检测算法rlive。传统的活性检测算法通过寻找套索形状的反例路径是否存在来证明性质是否成立，但该方式实践证明效率较低。rlive则通过寻找归纳不变式并进行状态剪枝的办法，间接但高效地寻找套索形状的反例路径。文章通过大量实验结果表明rlive的性能优于其他SOTA的活性性质的模型检测算法。

图：rlive算法的搜索示意

近年来，学院组织优秀骨干教师重点攻关可信人工智能领域关键难题，依托科技部科技创新2030——新一代人工智能重大项目《人工智能安全可信理论及验证平台》、国家自然科学基金委国际合作项目（中国-以色列）、华东师范大学-华为联合创新实验室等资助，在深度学习系统鲁棒性验证、深度强化学习系统的可信构造、混成系统的分析与验证等方面取得了一系列进展，相关成果发表在CAV、NeurIPS、ICSE、ASE等计算机理论领域、人工智能领域以及软件工程领域的顶级会议上。

CAV（Computer-Aided Verification）是计算机科学理论领域的顶级会议之一，也是中国计算机协会（CCF）推荐A类会议，截至2024年已举办35届，每年录用的文章仅有60篇左右。学院在可信软件领域的研究成果已经连续四年在该会议上发表，本年度多篇论文同时被录用尚属首次。

内容由课题组提供

编辑丨陈励

审核丨曹桂涛 邓玉欣