CCF形式化方法专业委员会走进高校-银河电子游戏1331站活动，将于2024年10月12日（星期六）上午8:30点举行，会议地点为银河电子游戏1331工科E座1716会议室，学术报告相关内容如下：

报告主题：Towards the Formal Methods for DNN-Controlled Systems with Safety Guarantee

报 告 人：张民，CCF高级会员，形式化方法专委会副主任，华东师范大学教授

时    间：2024年10月12日 8:30-9:10

地    点：工科E座1716会议室

报告摘要：

Abstraction plays a crucial role in formal methods, simplifying target systems by filtering out extraneous details in models, thereby facilitating scalable verification. In this presentation, we outline our recent advancements in merging formal methods with machine learning, facilitated by abstraction, to develop certified safe DNN-controlled intelligent systems. We demonstrate the critical role of abstraction in this integration by showcasing: (i) the use of abstraction in devising a CEGAR approach to train DNNs on refined state spaces until verification against predefined properties is achieved; (ii) the enhanced efficiency and precision in computing reachable states for complex DNN-controlled systems; and (iii) training verification-friendly piece-wise linear controllers which can be faithfully modeled as hybrid automata and verified by off-the-shelf tools. More details can be found in our CAV 2022, 2024 and NeurIPS 2023 papers.

报告人简介：

张民，华东师范大学软件工程学院（滴水湖国际软件学院）教授，博士生导师，副院长，形式化方法专委会副主任。2011年于日本北陆先端科技大学信息学科获得博士学位。主要研究方向为可信软件与形式化方法，通过数学建模、自动化验证与分析等方法确保神经网络与智能系统的可靠性，目前聚焦人工智能系统的安全可信问题研究。研究受到国家自然基金委国际合作项目（中以）、面上项目与青年项目、华为全球创新研究计划(HIRP)、国家留学基金委以及法国高等教育署等国家级基金资助。相关成果发表在CAV、NeurIPS、AAAI、CVPR、ASE等国际旗舰会议上。

报告主题：深度学习系统的可信性保障

报 告 人：孙猛，CCF 高级会员，形式化方法专委会执行委员，北京大学教授

时    间：2024年10月12日9:10-9:50

地    点：工科E座1716会议室

报告摘要：

深度学习系统已在诸多安全攸关领域中得到了广泛应用，与传统软件系统不同，深度学习系统数据驱动的特点使得该类系统拥有与传统系统完全不同的决策逻辑，并且深度学习系统的高维输入、庞大参数规模和状态空间使得其复杂程度远远超过传统的软件系统，从而使得目前应用于传统软件系统的形式化建模和验证技术难以直接应用于大规模深度学习系统的可信性保障之中。本次报告中将对相关问题以及我们近期我校深度神经网络的语义鲁棒性验证和估计的部分工作结果进行介绍。

报告人简介：

孙猛，北京大学数学科学学院信息与计算科学系副主任，教授，博士生导师， CCF形式化方法专委执行委员，CCF区块链专委执行委员，CSIAM区块链专委常务委员，CSIAM金融科技与算法专委常务委员，CAAI人工智能逻辑专委委员。主要研究领域包括程序理论、软件形式化方法、信息物理系统、可信人工智能、区块链与智能合约，主持及作为主要成员参与国家自然科学基金、重点研发计划等国家及省部级项目十余项，在IEEE TSE、ICSE、FSE、NeuIPS、AAAI、FM等期刊及会议发表论文百余篇，获TASE2015、SBMF2017等国际会议最佳论文奖，任FACS2009、TTSS2011、ICFEM2018、TASE2023、FACS2024、ICFEM2024等国际会议程序委员会主席，FM、TACAS、ICECCS等多个国际会议程序委员会委员。

报告主题：基于类型lambda演算的自动证明技术研究与工具设计

报 告 人：张艳，CCF 会员，形式化方法专委会执行委员，北京理工大学研究员

时    间：2024年10月12日10:10-10:50

地    点：工科E座1716会议室

报告摘要：

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

报告人简介：

张艳，2018年毕业于北京理工大学，获得计算机科学与技术专业工学博士。同年受聘于北京理工大学计算机学院助理研究员，硕士生导师。2019-2024CCF专业会员。主要科研方向是行为语义形式化方法及知识表示。近年来在ASE、QRS、MIS、KDD等知名国际会议和期刊发表学术论文10余篇。2022年获得科技部科学技术学术专著基金项目，2023-2024年完成出版《信息化总体学-网络主体系统论与网络行为学》。2019-至今承担计算理论与算法分析、计算机系统导论、编译原理与技术和形式语义学等本科课程，2022、2023年全国系统能力大赛华为毕昇杯编译大赛获得优秀指导老师奖，指导学生分获二等奖、优胜奖。2019-至今参加多项国家自然基金和国家重点研发计划等相关课题。

报告主题：鲁棒的多智能体深度强化学习

报 告 人：刘关俊，CCF 高级会员，形式化方法专委会常务委员，同济大学教授

时    间：2024年10月12日10:50-11:30

地    点：工科E座1716会议室

报告摘要：

多智能体深度强化学习是解决复杂的协同并发系统控制的重要途径之一,然而由于运行环境的复杂与不确定性、甚或恶意的攻击等因素，导致训练的控制模块鲁棒性受到挑战。该汇报将介绍本课题组在多智能体强化学习扰动的生成、鲁棒性提升、以及相应方法在双无人机协同搬运真实场景下的实验等研究。

报告人简介：

刘关俊，教授，博士生导师，2011年获得同济大学计算机软件与理论专业博士学位，曾于新加坡科技设计大学、德国柏林洪堡大学（德国洪堡基金资助）从事博士后研究工作。是中国计算机学会高级会员，计算机学会形式化方法专委会常务委员、软件工程专委会执行委员、中国人工智能学会会员、上海市人工智能学会可信智能系统专委副主任委员、IEEE Senior Member、IEEE Transactions on Computational Social Systems编委（2023.1-2025.12）。已出版学术著作4本，发表学术论文160余篇（含40余篇ACM/IEEE Trans论文），主持国家自然科学基金、上海市曙光人才项目、上海市科技创新行动计划（人工智能专项）等项目10余项。主要研究兴趣：并发理论、Petri网与模型检测、多智能体深度强化学习与无人机协同、实时嵌入式系统分析、网络支付欺诈检测等。