2026年CCF形式化方法专委会青年学术论坛——形式化方法与AI的双向赋能专题研讨会

报告摘要: 随着深度学习模型的广泛应用，如何保护训练数据免遭未经授权的学习，已成为 AI 安全领域的核心问题之一。本次报告围绕“数据能否保护自己”这一主线，介绍我们在 Unlearnable Data 方向上的系列工作。我们首先从理论出发，证明贝叶斯误差是神经网络鲁棒性的内在上界，揭示学习的根本极限；进而将这一理论工具反转为设计目标，构造出首个具有可证明保证的 Unlearnable Examples 方法，并证明其在混合数据场景下依然有效。然而，上述方法在大语言模型面前遭遇根本性挑战：LLM的强泛化能力使其对传统扰动高度不敏感，令既有的形式化保证失去前提。对此，我们转换思路，不再对抗 LLM 的鲁棒性，而是利用其自身的 alignment 机制：通过 Disclaimer Injection，使模型在微调时持续触发对齐约束，从而无法习得有效的任务知识，在大语言模型时代实现数据主权保护。

报告人简介: 张睿涵（ZHANG Ruihan），新加坡管理大学博士后研究员，于2026年获得新加坡管理大学博士学位，博士导师为孙军教授。她的研究方向为可信 AI，聚焦于深度学习系统的鲁棒性、公平性与隐私性认证，结合形式化方法与实证分析开展研究。相关成果发表于 ACL、AAAI、OOPSLA、CAV 等顶级学术会议。她致力于弥合理论保证与实际 AI 部署之间的鸿沟，推动 AI 系统走向安全、公平与可信。

报告摘要: 保证大规模软件的绝对正确性，是信息化社会可靠运行的基石，也是软件工程的“圣杯”级梦想。形式化证明凭借其数学意义上的严密性，是通向这一梦想的有效途径。然而，其极高的人力成本却成为横亘在理想与现实之间一道难以逾越的鸿沟。本报告将介绍基于神经符号融合的定理证明自动化技术相关进展，包括数学领域的不等式证明与软件领域的seL4定理证明，并探讨大模型时代AI在软件开发领域的应用与潜力。

报告人简介: 姚远，南京大学计算机学院副教授、博士生导师。长期从事软件智能化技术研究，近年来尤其关注软件形式验证技术。在中国科学：信息科学、OSDI、ICSE、FSE、ISSTA、ASE、CCS、S&P、ICLR、NeurIPS、AAAI、IJCAI等软件智能化相关领域的国内外重要期刊与会议上发表论文百余篇，工作曾获ACM 杰出论文奖等奖励，并受到了业内权威媒体MIT Technology Review报道。

报告摘要: 交互式定理证明技术是验证程序复杂性质的重要手段，其主要思想是在现有自动化验证工具无力完成验证工作的情况下，由人提供额外信息从而辅助验证工具『理解』程序并验证其功能以及安全性。本报告将介绍 Verified Software Toolchain（VST）工具，该工具以交互式定理证明技术为基础，集成了学术界在程序逻辑等诸多方面的理论研究前沿成果，可用于验证复杂 C 语言程序的功能正确性与安全性，排查空指针引用漏洞、缓冲区溢出错误、并发数据访问竞争等各种问题。

报告人简介: 曹钦翔本科毕业于北京大学，博士毕业于美国普林斯顿大学，2018年回国任教。现为上海交通大学约翰霍普克洛夫特计算机科学中心副教授、博导，CCF形式化专委会委员。曹钦翔长期从事基于交互式定理证明的程序验证研究，著有Software Foundations系列教材第五卷Verifiable C。

报告摘要: 从大语言模型（LLM）提出以来，软件工程领域迎来了重要变革，在软件开发过程中引入大模型和大模型智能体生成软件制品已逐渐成为主流开发模式。然而，围绕大模型安全与可信方面的挑战一直存在，如模型幻觉、逻辑推理能力薄弱、数据与模型隐私安全与公平等问题日益突出，数据质量保障、模型决策正确性验证、数据驱动的软件制品与传统逻辑驱动的软件制品融合与协同等系统性挑战，也制约了智能化技术在软件工程领域的深度应用。在此背景下，本报告聚焦神经模型与符号模型的交叉协同，探讨形式化方法在其中的作用和可能的结合点，为推动智能技术在软件工程领域从 “可用” 走向 “可信”提供一些洞察和思考，并介绍课题组近期在该研究领域的一些进展。

报告人简介: 李钦，华东师范大学软件工程学院教授，院长助理，博士生导师，主要研究方向为安全可信智能系统建模与构造方法、形式化方法赋能的大模型智能体可信评测与优化、神经符号协同的新一代软件工程等。已在IEEE TC、IEEE TIP、CVPR、FSE、FAC、SCP等国际期刊和会议上发表学术论文50余篇。承担国家重点研发计划课题《多源城市数据全生命周期可信保障技术体系》，基金委面上项目《面向智能网联车的时空认知多粒度分解与协同机制的建模与验证》，作为骨干参与新一代人工智能国家科技重大专项《人工智能安全可信理论及验证平台》。“高安全嵌入式控制软件全生命周期关键开发技术与环境”获得上海市技术发明奖一等奖，“可证明鲁棒的深度神经网络训练与验证技术”获得中国计算机学会自然科学奖二等奖。担任中国工业软件协同创新平台副秘书长，上海市人工智能学会可信智能系统专委会秘书长，中国计算机学会形式化方法专委会执行委员。担任可信软件方向重要国际会议TASE2020、ICFEM2026程序委员会主席，是可信软件领域多个国际期刊审稿人和国际会议程序委员会委员。

报告摘要: 本文提出 Preguss，一个结合静态分析、演绎验证与大语言模型的规约自动生成框架。其采用分而治之策略，首先根据证明目标（即潜在运行时错误断言）构建并排序验证单元，然后合成并精化单元级过程间规约，并保证可靠性与终止性。实验表明，Preguss优于现有先进方法，可对千行以上工业程序实现高自动化内存安全验证，将人工验证工作量减少 80.6%–88.9%，并发现了某航天器控制软件中的6个真实运行时错误。

报告人简介: 王钟逸，浙江大学计算机科学与技术学院博士生，导师是陈明帅研究员。主要研究方向是程序自动化验证与静态分析。相关研究成果发表于OOPSLA、ASE、J. Comput. Sci. Technol.等领域重要国际会议/期刊。

报告摘要: 大语言模型与 AI 智能体正以前所未有的速度发展，在推理、规划以及自主决策等方面展现出日益复杂的能力。然而，这些进展也伴随着不断增长的安全与可靠性风险，尤其是在此类系统逐渐被部署到高风险与安全关键场景中的背景下。确保其可靠性因此已不再是可选项，而是一项基础性要求。在本次报告中，我将探讨构建系统化 AI 安全方法所面临的挑战，并介绍三类互补的技术路线，以提升大规模 AI 系统的安全性与可信赖性。针对每一类方法，我将重点讨论其中若干关键的开放性理论问题，并介绍一些正在兴起的研究工作，这些工作开始为解决上述问题提供新的思路与方向。

报告人简介: 孙军(SUN Jun)是新加坡管理大学的教授。他于2002年和2006年分别获得新加坡国立大学(NUS)计算机科学学士和博士学位，自2010年起担任教职。孙军的研究兴趣包括人工智能安全、软件工程、形式化方法等等。他喜欢设计算法，以解决具有实际应用的难题，也热爱生活。更多信息请见:https://sunjun.site

报告摘要: 随着大语言模型在代码理解与生成任务中的快速发展，程序规约合成正成为提升软件正确性、可靠性的重要技术路径。然而，现有研究多依赖简化后的小型基准测试集，难以充分反映真实软件项目中的上下文依赖、语义约束与修复复杂性。本报告围绕大模型程序规约合成的初步实践与案例分析，讨论其从基准测试走向更真实代码场景时面临的挑战，并展望面向实际软件系统的智能程序规约合成方法。

报告人简介: 文成，西安电子科技大学准聘副教授。他于2022年于深圳大学获得计算机科学与技术博士学位，研究兴趣包括人工智能使能软件测试与验证、可信软件的基础理论与方法等。目前已经在包括ICSE、ASE、FSE、CAV、FM、ACL、TPDS、TKDD等国内外重要会议和期刊上发表三十余篇论文。发现Linux内核等开源软件数百缺陷（获80+CVE编号），研究成果应用于航天、华为。

报告摘要: 确保复杂并发系统从抽象模型到实现代码的精化过程中始终保持信息流安全性质，是构建高等级可信系统的核心挑战之一。本报告将分享发表于 CCS ‘25 的研究成果：一种通用的并发系统信息流安全精化验证框架。该框架通过依赖-保证组合验证技术有效处理了线程间的复杂交互，支持包括受控信息泄漏在内的多种安全策略，并已在 ARINC 653 航空操作系统等工业级案例中通过 Isabelle/HOL 进行形式化验证。报告最后将探讨信息流安全理论在 AI 智能体安全领域的新机遇。针对智能体在自主调用工具时面临的间接提示词注入等新兴风险，讨论如何借鉴污点追踪与非干扰性原则，为下一代智能体构建具备逻辑透明度与强鲁棒性的安全监控机制。

报告人简介: 孙欢，上海人工智能实验室青年研究员，2025年获浙江大学控制科学与工程博士学位，师从王竟亦研究员与王文海教授。研究方向涵盖程序逻辑、定理证明、并发程序验证与信息流安全等，相关成果发表于CCS、ICFEM软件学报等国际国内会议期刊，并已申请多项发明专利。