形式化方法基于严格的数学化和机械化方法来规约、设计、构建、验证、演进计算系统，是改善和确保计算系统质量的重要方法，其模型、技术和工具已延伸成为计算思维的重要载体。

形式化方法与应用专刊论坛聚焦形式化方法理论前沿，围绕形式化方法基础理论、技术、支撑工具及领域应用，重点关注形式化方法与理论计算机科学、软件工程、基础软件（操作系统、编译器等）、嵌入式系统、人机物融合系统、概率/量子系统、网络与信息安全、可信人工智能（智能制造、智能交通、智能控制、可信机器学习）等领域的交叉结合，旨在于我国标志性学术刊物上反映形式化方法领域的最新研究成果，深入拓展形式化方法与相关领域的交叉，促进形式化方法、技术和工具在国内的应用和发展。

01

论坛组织委员会

陈明帅（浙江大学）

田聪（西安电子科技大学）

熊英飞（北京大学）

02

论坛议程

03

论坛报告嘉宾简介

孙军

报告题目：鲁棒的神经网络存在吗？

报告摘要：

自从对抗样本被发现以来，已经过去了十多年。然而，鲁棒性问题依然是传统神经网络以及大模型（包括大语言模型和多模态模型）所面临的重大挑战。在本次报告中，我将分享我们团队在应对这一问题时基于形式化方法所开展的一系列研究工作。从理论层面，我们探讨了完美鲁棒性（即不存在对抗样本）的可行性，并进一步研究了概率鲁棒性（即对抗样本有限存在）是否能够成为一个可接受的折中方案。在实践方面，我们提出了一种通过轻量级训练与推理相结合的方法让神经网络实现有理论保证的概率鲁棒性。

报告人简介：

孙军（sun, jun）是新加坡管理大学（smu）的教授。他于2002年和2006年分别获得新加坡国立大学（nus）计算机科学学士和博士学位，自2010年起担任教职。孙军的研究兴趣包括人工智能安全、软件工程、形式化方法、等等。他喜欢设计算法，以解决具有实际应用的难题。也热爱生活。

04

论坛组织委员会简介

论坛主席：陈明帅

个人简介：

陈明帅，浙江大学研究员、博士生导师、启真学者，ccf形式化方法专委通讯委员，杭州市钱江特聘专家，国家优秀青年基金（海外）获得者。主要研究方向包括形式验证、程序理论、概率/量子系统、信息物理融合系统等，与合作者一起，提出新型安全攸关系统形式验证理论，解决了概率程序不动点估计、微分系统可达性判定、时滞系统高效控制生成等若干软件理论难题，研究成果应用于我国探月二期工程“嫦娥”三号等重大工程，在inf. comput.、oopsla、cav、fm、asplos等领域旗舰期刊/会议上发表学术论文30余篇，曾获中科院院长特别奖、atva杰出论文奖、fmac最佳论文奖。

论坛主席：田聪

个人简介：

田聪，西安电子科技大学二级教授，博士生导师，科学研究院常务副院长，陕西省安全攸关智能软件重点科技创新团队负责人。担任中国计算机学会形式化方法专委会副主任、中国自动化学会网络信息服务专委会副主任、全国信息技术标准化技术委员会软件与系统工程分技术委员会委员；软件学报、ieee tr、joco、西电学报等期刊编委。长期从事可信软件、形式化验证理论与方法研究，在tosem、tse、lics、icse、fse、ase、ijcai、issta、软件学报等国内外顶级期刊和会议发表论文100余篇；主持国家自然科学基金重大课题、重点和优青项目、科技部重点研发计划课题、军委装备发展部等项目十余项；获“长江学者”特聘教授、中创软件人才奖、教育部自然科学一等奖1项、陕西省科学技术一等奖2项；相关研究成果应用于航天控制软件开发和芯片设计eda软件验证等安全攸关重要领域。

论坛主席：熊英飞

个人简介：

熊英飞，北京大学长聘副教授，新体制长聘副教授、软件研究所副所长、计算机学院院长助理。2009年从日本东京大学获得博士学位，2009-2011年在加拿大滑铁卢大学工作，2012年加入北京大学。研究兴趣是程序设计语言和软件工程，特别是程序合成、修复和分析。他提出了理论和方法降低程序编写和缺陷修复的代价。比如，基于差别的双向变换框架是最广泛使用的双向变换框架之一，概率和逻辑结合的程序合成框架玲珑框架将程序修复的正确率从此前不到40%提升到80%以上。他的工作也被工业界采用，比如新一代linux内核配置项目、燕云daas系统、华为公司等。他获得电子学会自然科学一等奖（排名1）、ccf-ieee cs青年科学家奖、models十年最有影响力论文奖，5次获得 acm sigsoft/ieee tcse杰出论文奖。他是sate18的程序委员会联合主席，也在pldi、icse、fse等会议担任pc。