2024年月5月5日（星期日），在江苏苏州CCF业务总部&学术交流中心105会议室召开了“2024 CCF形式化方法专委会战略研讨会”，此次研讨会主题为“形式化方法与人工智能的交叉融合：机遇与挑战”，关注“AI for FM
”
与“FM for AI
”
两方面的机遇与挑战。此次研讨会吸引了来自高校、研究所、工业界共60余名专家参加。
此次研讨会由CCF主办，CCF形式化方法专委会承办，华东师范大学软件工程学院与中国科学院软件研究所协办。另外，研讨会得到了华为费马实验室、华为可信领域科学家委员会、黄大年茶思屋科技网站的大力支持。研讨会共同主席为国防科技大学的王戟教授、北京大学的詹乃军教授、华为费马实验室秦胜潮主任，程序委员会成员包括西安电子科技大学计算机学院田聪教授，华东师范大学软件工程学院张民教授，中国科学院软件研究所张立军研究员，组织委员会成员包括中国科学院软件研究所研究员吴志林研究员，国防科技大学陈振邦教授，北京航空航天大学葛宁副教授，上海海洋大学张文博讲师，西北工业大学沈博副教授，湖南大学张羽丰副教授。
此次研讨会包括
“AI for FM”和“FM for AI”两个Session和Panel
，共9个报告。研讨会上午9:00开幕，形式化方法专委秘书长吴志林研究员主持了开幕式。开幕式邀请了形式化方法专委前任主任王戟教授、现任主任詹乃军教授、华为费马实验室秦胜潮主任进行致辞。
上午举行了
“AI for FM”的Session和Panel，由
来自上海交通大学的曹钦翔副教授主持。该Session包括5个报告：首先来自南京大学的李宣东老师做了“神经符号融合软件的可信理论与方法”的报告，然后来自华为费马实验室的秦胜潮老师做
了“Enchanting Program Specification Synthesis by LLMs using Static Analysis and Program Verification”的报告，
来自中国科学院软件研究所的蔡少伟老师做了
“SAT Solvers meet AI”
的报告，来自华为诺亚方舟 AI 基础理论实验室的李震国老师做了“LEGO-Prover: 基于大语言模型的自动定理证明”的报告，最后来自香港科技大学的曹嘉伦老师做了“基于大语言模型的需求描述到形式化规约生成初探”的报告。5位报告人从不同的角度分享了在
“AI for FM”
方面的一些思考和探索，并在Panel环节与听众进行了充分的互动和交流。
下午举行了
“FM for AI”的Session和Panel，由
来自华东师范大学的张民教授主持。该Session包括4个报告：首先来自北京大学的孙猛教授做了“深度神经网络的语义鲁棒性”的报告，然后来自英国利物浦大学的黄小炜教授做了
“Safeguarding Large Language Models”的报告
，来自新加坡管理大学的孙军教授做
了“Causality Analysis for AI”
的报告。来自英国南安普顿大学的黄超教授做了
“Safe Reinforcement Learning for Cyber Physical Systems”的报
告。Panel环节除了报告人之外，还邀请了浙江大学的王竟亦研究员参加。Panel嘉宾对于“FM for AI”的相关问题进行了充分讨论与交流。
此次研讨会通过深入探讨形式化方法与人工智能技术的双向赋能，有望推动两者的协同发展和加强产学研各界的交流与合作。
