近日，由CCF形式化方法专委会主办、我院承办的CCF形式化方法专委会青年学术论坛——面向AI安全的形式化方法前沿研讨会在滴水湖国际软件学院顺利举办。本次论坛以AI系统安全、可靠性与可信保障为核心主题，围绕形式化方法赋能人工智能安全的前沿挑战、技术路径与产业应用开展交流研讨，旨在搭建青年学者交流协作平台，凝练领域关键科学问题，推动形式化方法在可信AI领域落地创新。论坛共邀请九位来自高校、科研院所的领域专家进行最新研究成果分享，通过线上线下相结合的方式汇聚国内多所高校、科研院所青年学者共同参与。

张  民    华东师范大学教授

王培新   华东师范大学青年研究员

首先，CCF形式化方法专委会副主任、华东师范大学张民教授为本次论坛致辞。随后，会议由华东师范大学王培新青年研究员、浙江理工大学林望教授共同主持。九位报告专家分别从理论方法、算法创新、行业落地层面展示形式化方法与人工智能交叉领域最新研究成果，覆盖程序规约、法律 AI、强化学习、神经网络、金融可信软件等多元场景。参会师生、科研人员针对形式化工具开发、大模型形式验证、工业系统安全落地等热点问题展开讨论。

冯胜华   中国科学院软件所副研究员

CCF形式化方法专委会执行委员

Certified Test-Case Checking for Dafny Specifications

中科院软件所冯胜华围绕Dafny形式规约可验证测试用例校验框架展开分享，提出 SpecCheck 工具解决规约行为对齐偏差问题。

黄中昱  上海人工智能实验室神经-符号团队负责人

法律形式推理约束的人工智能安全模型

上海人工智能实验室黄中昱介绍法律形式推理约束下的AI安全模型，实现自然语言法律条文向可执行形式化规范转化。

杨  敏   同济大学在读博士生

深度强化学习的运行时监控方法研究

同济大学杨敏针对深度强化学习黑盒安全缺陷，讲解动态运行时监控系列方法。

孙泽宇   中国科学院软件所副研究员

LLM自动化测试与修复

中科院软件所孙泽宇聚焦大模型质量管控，分享 LLM 自动化测试与缺陷修复技术。

陈立前    国防科技大学教授

视觉神经网络控制系统的可证概率安全控制器合成

国防科技大学陈立前带来视觉神经网络可证概率安全控制器合成方案，为安全关键智能控制系统提供形式化保障思路。

林 云    上海交通大学副教授

需求编译与驾驭工程

上海交通大学林云围绕需求编译与智能体软件工程，结合生成式 AI 时代软件研发转型趋势，介绍可执行需求建模、测试左移与全链路可追溯工程流水线。

刘尚清    南京大学副教授

从规约理解到验证：形式化规约作为大语言模型与可信软件之间的桥梁

南京大学刘尚清以形式化规约为纽带，提出连接大模型代码生成与可信软件验证的完整技术体系。

王竟亦    浙江大学控制学院安全所百人计划研究员

Provable Repair of Deep Neural Network Defects through Pre-image Synthesis and Property Refinement

浙江大学王竟亦分享神经网络缺陷可证修复统一框架，借助原像合成与属性精化实现具备完备证明的模型修复。

陈小红    华东师范大学教授

大语言模型赋能的金融科技软件合规测试用例自动生成