人工智能系统已被广泛应用于航空航天、自动驾驶等安全攸关领域。研究确保智能系统的安全可靠的验证与构造方法，已成为急需解决的关键技术需求。最近，软件工程学院赵韩蕊博士研究生在智能系统的安全验证和控制策略构造等方面取得了一些研究进展。

针对系统安全验证问题，赵韩蕊与其合作者提出了一种基于反例制导的DNN型障碍证书生成方法。相关论文”Formal Synthesis of Neural Barrier Certificates for Continuous Systems via Counterexample Guided Learning”被嵌入式系统领域国际顶级会议International Conference on Embedded Software（EMSOFT 2023）接收发表。 

SynNBC可验证障碍证书综合框架

该工作设计了基于反例制导循环的迭代框架，其中Learner模块使用通过多项式优化求解生成的反例来更新网络，将具有特殊结构的神经网络训练为障碍证书候选者，并利用边界增强采样和空间划分技术提升其学习性能；Verifier模块通过线性矩阵不等式求解来进一步验证生成的障碍证书候选者，不仅高效且在形式上更加可靠。基于该方法开发的技术工具SynNBC能成功解决高达19维的系统形式化安全验证问题。

针对安全控制策略生成问题，赵韩蕊与其合作者提出了一种基于Meta-RL的非线性系统DNN型安全控制器综合方法，极大地提升了控制器合成的效率与成功率，不仅在高维示例上有着出色表现同时还成功应用于没有固定系统维度的控制器生成任务。相关成果“Safe DNN-type Controller Synthesis for Nonlinear Systems via Meta Reinforcement Learning” 已发表于电子设计自动化（EDA）和嵌入式系统设计与验证领域国际顶级会议Design Automation Conference（DAC 2023）。

赵韩蕊目前为软件工程学院博士二年级研究生，导师杨争峰教授，研究方向为安全强化学习，目前在DAC 2023（第一作者）、EMSOFT 2023（第一作者）国际会议和Journal of System Sciences and Complexity(学生一作)国际期刊上发表学术论文三篇。

图文由论文作者提供

编辑丨陈励

审核丨曹桂涛