摘要：

神经网络在诸如机载空中防撞系统(Traffic Collision Avoidance System, TCAS)、自动驾驶和无人系统等信息物理系统中有着巨大的潜力。然而，神经网络在该类安全关键系统部署前必须经过严格的测试和验证，以确保在所有情况下都能提供可靠的决策。进一步地，当神经网络无法满足部署需求时有必要对神经网络进行有效的修复来满足要求。本报告将介绍一种基于形式化验证的神经网络修复技术，对无法满足给定安全性质（如safety property、backdoor-freeness等）的神经网络进行形式化验证引导下的定向修复。

报告人简介：

王竟亦，浙江大学“百人计划”研究员。新加坡科技设计大学（与MIT联合建校）博士，新加坡国立大学博士后。主要研究兴趣是SE4AI，形式化方法与安全，及控制系统软件安全。在S&P、CCS、FM、TACAS、ICSE、WWW等国际顶级会议或期刊发表论文多篇。曾两次获得ICSE的杰出论文奖，并入选ACM SIGSOFT亮点研究。目前担任CCS、ICSE、ASE、 ISSTA、WWW等国际顶级会议程序委员会委员和ICFEM 2025程序委员会主席。