人机物融合系统是一种集成人类社会、信息空间和物理世界的软件密集型系统。人工智能技术的快速发展正使得系统从人机无互联向人机物智联阶段跨越式发展。然而，ai算法和系统自身存在安全隐患，如何确保系统的安全可信是实现大规模智能互联与协作的重要前提。

高可信人机物融合智能系统论坛面向人机物融合系统的安全可信问题，聚焦系统的安全可信理论、技术与方法和案例分析，具体内容包括神经网络模型的形式化验证、智能控制系统建模与验证、大语言模型的安全可信保障技术、神经网络模型的攻击与防御方法等内容，为国内外学者提供交流和学习当前人机物智能系统安全可信技术与方法最新学术成果的平台。

01

论坛组织委员会

张民（华东师范大学）

刘关俊（同济大学）

董威（国防科技大学）

02

论坛议程

03

论坛报告嘉宾简介

孙猛

报告题目：基于统计模型检查的深度神经网络鲁棒性估计

报告摘要：

以深度神经网络为代表的深度学习系统已在自动驾驶、医疗诊断等安全攸关领域得到了广泛应用。与传统软件系统不同，其数据驱动的特点使得该类系统拥有与传统系统完全不同的决策逻辑，并且深度学习系统的高维输入、庞大参数规模和状态空间使得其复杂程度远远超过传统的软件系统，从而使得目前应用于传统软件系统的形式化技术难以直接应用于大规模深度学习系统的安全性、鲁棒性保障之中。本次报告中将介绍我们近期关于统计模型检查算法改进和深度神经网络鲁棒性估计的部分工作结果。我们对主流统计模型检查工具中使用的okamoto bound估计方法进行了改进，设计了新的统计模型检查算法，大幅减少了采样次数，可比现有统计模型检查算法节省40%-60%的时间。从统计模型检查的角度，我们给出了深度神经网络鲁棒性的估计算法，仅用少量图片即可获得与传统方法使用大量图片计算得到的全局鲁棒性值强相关的结果。

报告人简介：

孙猛，北京大学数学科学学院信息与计算科学系教授，博士生导师， ccf形式化方法专委执行委员，ccf区块链专委执行委员，csiam区块链专委常务委员，csiam金融科技与算法专委常务委员，caai人工智能逻辑专委委员。主要研究领域包括程序理论、软件形式化方法、信息物理系统、深度学习、区块链与智能合约，主持及作为主要成员参与国家自然科学基金、重点研发计划等国家及省部级项目十余项，在ieee tse、icse、fse、aaai、fm等期刊及会议发表论文百余篇，获amast2004、tase2015、sbmf2017等国际会议最佳论文奖，曾任facs2009、ttss2011、icfem2018、tase2023、facs2024、icfem2024等国际会议程序委员会主席及fm、tacas等多个国际会议程序委员会委员。

张立军

报告题目：智能算法安全建模与验证

报告摘要：

智能算法广泛应用于自动驾驶、医疗等安全攸关的国家重点领域。这对智能算法的可信性提出了更高的要求。自动驾驶系统中的智能算法规模庞大、结构复杂、运行环境开放，其可信性很难保障。通过对自动驾驶系统安全分析，我们探讨智能算法安全保障框架，通过形式建模和形式规约，讨论如何形式化描述系统的运行场景，对系统建立包含概率选择、不确定性选择等抽象模型，以及形式规约及验证方法。我们通过开源自动驾驶平台iss介绍课题组在自动驾驶系统的安全性的测试与验证方面取得的系列进展。

报告人简介：

张立军，中国科学院软件研究所研究员，主要从事形式化方法、智能算法可靠性研究，在学术会议及期刊发表了一百余篇论文。2013年加入中科院软件所，现为可信智能系统研究室主任。回国前曾任丹麦科技大学长聘副教授。致力于概率与混成模型量化分析、可信智能软件等前沿技术的研究。担任国际逻辑大会 lics 2020（ccf a类会议）共同主席，及tacas 2019、concur 2018（ccf b类会议）程序委员会主席。获国家自然科学基金委员会“重点项目”、科技部重点研发课题、中德国际合作等多项项目资助。2022年获中科院稳定支持基础研究团队项目资助，作为负责人带领研究开放环境下的可信智能算法。

杨争峰

报告题目：polynomial neural barrier certificate synthesis of hybrid systems via counterexample guidance

报告摘要：

in this talk, we present a novel approach to safety verification by synthesizing barrier certificates (bcs) for hybrid systems, which integrates counterexample-guided learning with efficient sos-based verification. we develop an inductive loop for generating easily verifiable barrier certificates by training polynomial neural networks guided by a high-quality counter-example set. by leveraging the polynomial candidates obtained from the learning phase, the identification of valid barrier certificate can be converted into linear matrix inequality (lmi) feasibility testing problems, instead of directly solving the non-convex bilinear matrix inequality (bmi) problems inherent in barrier certificate generation. furthermore, we decompose the large sos programming into several manageable sub-programming ones. benefiting from the efficiency and scalability advantages, our proposed approach can synthesize barrier certificates not amenable to existing methods.

报告人简介：

杨争峰，华东师范大学软件工程学院，教授，于 2006 年获得中国科学院数学与系统科学研究院博士学位。博士毕业后年赴美国北卡州立大学从事博士后研究工作。主要研究方向包括数学机械化、ai for math、混成系统验证等。迄今为止在cav、fm、emsoft、issac、cvpr等国际会议和acm tecs、ieee tcad、jsc等国际期刊上发表了80余篇论文。近年来主持国家重点研发计划“数学和应用研究”专项课题、国防科工委创新项目、国家自然科学基金等多个科研课题的研究。

马帅

报告题目：高效大图数据近似计算

报告摘要：

图数据表达能力较强，成为工业界和学术界共同的重点关注之一。本报告将介绍高效大图数据计算的一种主要方法，近似计算（包括查询近似和数据近似），通过案例来介绍相关方法的思想。最后，讨论近似计算的潜在研究方向。

报告人简介：

马帅, 北京航空航天大学计算机学院教授，主要从事大数据理论与系统的研究，其成果持续发表在数据库领域、数据挖掘、人工智能和系统等顶级会议和期刊。曾任多个国际顶级期刊编委及国际顶级领域主席、程序委员。获国家杰出青年科学基金，获vldb最佳论文奖、中国电子学会科技进步特等奖和自然科学一等奖等。

李晓锋

报告题目：控制算法代码智能生成技术研究与应用

报告摘要：

控制软件以控制算法为核心，以空间飞行器为例，算法功能通常占比不少于50%，部分型号算法功能占比达到75%。实现控制算法代码智能生成能大幅提升控制软件开发效率和质量。报告首先概述空间飞行器控制软件研制现状和存在的问题;在此基础上,提出了融合自然语言理解与形式化转换的代码生成方法,并重点阐述智能化代码生成、代码高质量保证、定制功能可扩展等方面的研究进展与成果；最后,对控制软件代码智能生成技术未来的发展方向进行展望。

报告人简介：

李晓锋，研究员，中国空间技术研究院软件技术专业学术技术带头人，北京控制工程研究所软件中心副主任。长期从事嵌入式软件设计、验证与智能化软件技术及在航天器的应用研究，负责完成了嫦娥系列以及星网星座等10余个国家航天重大工程型号的嵌入式控制软件研制，主持或参与国家核高基、国防基础预研、国家自然科学基金等20余项。获得北京市科技进步一等奖，军队科技进步二等奖，国际发明展金奖，发表论文50余篇，获授权发明专利40余项。

王海峰

报告题目：轨道交通运行控制系统智能化的挑战与趋势

报告摘要：

轨道交通列车运行控制是一个典型的安全攸关系统，智能技术的发展在优化系统性能、提升服务品质，以及变革业务模式等方面带来新的机遇。介绍轨道交通列车运行控制原理和国内发展现状，从自动驾驶、优化调度、数据运维等角度探讨ai技术应用面临的问题和挑战，分析轨道交通列车运行控制的智能化发展趋势。

报告人简介：

王海峰，北京交通大学自动化与智能学院、轨道交通运行控制系统国家工程研究中心，教授、博士生导师。长期从事轨道交通运行控制系统的科研与技术开发，曾参与多项核心技术装备的研发，获国家科技进步奖二等奖1项，北京市科技进步一等奖1项，发表论文40余篇。

研究方向包括:轨道交通安全系统建模与分析、形式化方法与人工智能技术在轨道交通领域的应用。

04

论坛组织委员会简介

论坛主席：张民

个人简介：

张民，博士，华东师范大学软件工程学院教授，博士生导师，ccf高级会员，形式化方法专委会副主任。主要研究方向为可信软件，利用数学的方法实现智能系统、物联网、嵌入式系统的可靠性，目前聚焦人工智能系统的安全可信问题研究。研究受到国家自然基金委国际合作项目（中以）、面上项目与青年项目、华为全球创新研究计划(hirp)、国家留学基金委以及法国高等教育署等国家级和国际合作项目的资助。相关成果发表在cav、neurips、aaai、cvpr、ase等国际旗舰会议。

论坛主席：刘关俊

个人简介：

同济大学计算机科学系教授、博士生导师。中国计算机学会高级会员（形式化方法专委会常委与软件工程专委会执行委员），中国人工智能学会会员，ieee高级会员，ieee transactions on computational social systems编委（associate editor,2023.1-2025.12）。曾先后于新加坡科技设计大学、柏林洪堡大学（德国洪堡基金资助）开展博士后研究工作。主要从事模型检测、petri网理论、基于强化学习与软件定义的无人机协同系统、以及基于深度学习的网络交易欺诈检测等方面的研究。发表学术论文150余篇，出版学术专著4本。

论坛主席：董威

个人简介：

董威，国防科技大学计算机学院教授、博士生导师，中国计算机学会形式化方法专委会副主任、软件工程专委会执行委员，主要研究方向为高可信软件技术、智能化软件开发方法。入选教育部新世纪优秀人才支持计划，曾获中国计算机学会首届nasac青年软件创新奖、霍英东基金会高校青年教师奖等。先后主持国家和国防课题20余项，发表学术论文80余篇，出版国家级规划教材两部，相关成果应用于航空航天、装备控制、自主基础软件等关键领域。