10月12日上午，学院成功举办CCF形式化方法专业委员会走进高校—银河电子游戏1331站活动。此次活动邀请到CCF高级会员、形式化方法专委会副主任、华东师范大学教授张民，CCF高级会员、形式化方法专委会执行委员、北京大学教授孙猛，CCF会员、形式化方法专委会执行委员、北京理工大学研究员张艳，CCF高级会员、形式化方法专委会常务委员、同济大学教授刘关俊开展主题报告。活动由学院院长助理陈程立诏教授主持，学院院长庞善臣教授出席活动，学院教师代表、学生代表参与此次活动。

张民教授首先对中国计算机学会作简要介绍，并作《Towards the Formal Methods for DNN-Controlled Systems with Safety Guarantee》主题报告。张教授讲述了将形式化方法与机器学习相结合方面的进展，通过抽象来促进，以开发经过认证的安全DNN控制的智能系统。张教授从设计CEGAR方法时使用抽象来在精炼的状态空间上训练DNN、提高复杂DNN控制系统可达状态计算的效率和精度、建模混合自动机等方面进行了详细介绍。

孙猛教授作《深度学习系统的可信性保障》主题报告。孙教授从深度学习系统和传统软件系统完全不同的决策逻辑出发，详细介绍了由于深度学习系统的高维输入、庞大参数规模和状态空间使得其复杂程度远远超过传统的软件系统，目前传统软件系统的形式化建模和验证技术在大规模深度学习系统中的局限性。

张艳老师作《基于类型lambda演算的自动证明技术研究与工具设计》主题报告。当前大部分交互式定理证明工具的语义设计大多数符合数学逻辑，要求用户具有较高的数学专业领域知识，表达复杂算法与程序语义需要做更多的转换；同时作为交互式工具，它们的自动化程度与证明策略存在局限。张老师通过介绍实验室近期在类型 Lambda演算的理论体系、自动证明技术与大语言模型结合方面，对类型Lambda演算证明解释器自动证明器框架的设计、类型Lambda演算的形式语言Tigrazul以及它的证明解释器的设计并实现、以及该工具的形式验证能力与辅助定理证明能力实验验证等方面详细介绍了自动证明技术在数学命题证明领域以及软件形式化验证领域的重要意义。

刘关俊教授作《鲁棒的多智能体深度强化学习》主题报告。刘教授从多智能体深度强化学习的重要性出发，分析了由于运行环境的复杂与不确定性、甚或恶意的攻击等因素，导致训练的控制模块鲁棒性存在的挑战。接着从多智能体强化学习扰动的生成、鲁棒性提升、以及相应方法在双无人机协同搬运真实场景下的实验等研究方面介绍了相关工作及成果。

每个报告结束后，老师们与现场师生进行交流讨论，通过解决了师生在人工智能方面的部分科研问题。

此次报告会聚焦人工智能的神经网络、机器学习、大语言模型可靠性、可信性的验证研究等领域，对学院师生在人工智能方面的探索学习提供了新的思路，有助于提升专业知识水平和实践能力。

【作者：毕浩冉 摄影：段栩瑶 王东勤 审核：张玮】