CCF软件大会2026|形式化方法与大模型技术论坛

一、论坛介绍

大模型技术为形式化方法的工程化应用正带来前所未有的机遇。近几十年来困扰形式化方法的建模和推理等关键难点导致这个领域技术门槛高、人力成本高等。因此，形式化方法尽管在理论上有很多先进性，却难以大规模的工程化应用。当下，大模型的蓬勃发展为这两个难点问题的根本解决带来了曙光。一方面，大模型强大的文本处理、计算和推理能力能够有效提升形式化建模和验证的效率，推动形式化方法在更多领域的广泛应用，为复杂系统的开发和验证提供有力支持；另一方面，形式化方法通过严格的数理逻辑方法，有望为大模型的安全性、可靠性、可解释性和可信性提供更高级别的安全保障，确保大模型在金融、医疗、自动驾驶、系统开发等高安全要求领域的可靠落地，从而促进大模型技术及产业的健康、安全、可持续发展。同时，大模型技术的普及也为形式化方法带来新的挑战，如何保障智能系统的安全可靠？面向超大规模的数值计算和逻辑推理，如何实现神经网络模型和符号逻辑推理的有效协同，减少大模型的幻觉和统计的不确定性？形式化方法需要快速地丰富自身的理论方法与工具，以应对软硬件系统日益智能化、具身化所带来的安全挑战。

本论坛旨在推动形式化方法与大模型的深度融合：催生新型验证理论，为企业提供更加可落地的验证工具与方法论；推动形式化方法在大模型及其应用可信保障上的系统应用，助力构建社会公众对人工智能的信任，支撑数字经济的可持续发展。

二、论坛组织委员会

• 孙猛（北京大学）
• 张民（华东师范大学）

三、论坛安排

日程安排：

时间：2026年11月7日，15:20-18:20

地点：天津市社会山国际会议中心酒店，四层5号多功能厅

论坛议程：

四、论坛报告嘉宾简介

1. 报告人：王戟 教授

题目：代码/证据协同生成与异构对齐

摘要：大模型将软件开发向智能体式构造推进。当代码和"证明代码正确"的证据都可以由大模型生成时，"构造即正确"具有了智能化实现可能。本报告探讨可信代码智能体的代码/证据协同生成范式，即神经生成与符号验证之间如何交换信息、组织闭环、维持可信边界、以及形成可检验的构造链。进一步，未来软件开发中，自然语言、本体语言、形式规约和编程语言构成了从抽象意图到可执行实现的多层表达链。如何在这些层次之间保持语义对齐，并构建可检验证据，成为大模型时代可信软件构造的挑战。

简介：王戟，国防科技大学教授，复杂关键软件环境全国重点实验室副主任，中国计算机学会会士。从事可信、智能与新兴软件技术研究，在复杂关键软件高可信保证、神经符号融合系统、虚拟计算环境等方面取得了重要进展，在国家和国防重大重点工程发挥了重要作用。获国家和省部级奖励6项，发表论文200余篇。曾获国务院政府特殊津贴、国家杰出青年科学基金、教育部长江学者特聘教授。历任中国计算机学会理事、形式化方法专委主任、软件工程专委副主任。

2. 报告人：李宣东 教授

题目：所解即所证：基于大语言模型的编程和规约与验证一体化

摘要：软件是人类生产的最复杂制品。程序验证是软件可信保障的重要途径，长期以来受制于自动化程度低、人力成本高，无法大规模有效应用。大语言模型及其智能化技术基于概率与统计计算所形成的语言（自然语言、形式规约语言、程序语言以及相关证明语言）理解和生成能力，建立需求、代码、规约之间的语义映射，为提高大规模复杂系统程序验证的自动化程度打开了空间。人工编程基于程序语义和逻辑，编程过程本身形成非形式化的证明。本报告探讨基于大语言模型及其相关智能化技术加速和优化人工编程过程，实现编程和规约与验证一体化，从而支持程序验证途径的大规模有效应用。

简介：李宣东，南京大学教授；教学与科研工作主要涉及软件工程、形式化方法，可信软件，系统软件；曾任南京大学计算机科学与技术系系主任（2006-2018）、软件学院院长（2008-2022），国务院学位委员会软件工程学科评议组成员（2015-2026），国家自然科学基金委员会信息科学部专家咨询委员会委员（2014-2019），中国计算机学会系统软件专业委员会主任（2015-2019），中国计算机学会软件工程专业委员会主任（2020-2023）。

3. 报告人：熊英飞 教授

题目：从数据中挖掘符号规则

摘要：大模型虽然有很强的能力，但在很多场合还是需要符号系统。本报告介绍一种新的数据挖掘方法，通过让大模型分析训练集数据和编写代码，可以形成高效的符号系统。我们已经将该方法用在程序优化和形式化证明上，都取得了良好效果。

简介：熊英飞于2009年从日本东京大学获得博士学位，2009-2011年在加拿大滑铁卢大学工作，2012年加入北京大学，现任新体制长聘教授、软件研究所副所长。研究兴趣是程序设计语言和软件工程，特别是程序合成、修复、分析和验证。工作帮助产生了一系列效果同期最优神经网络代码生成模型，如DeepSeek-Coder模型；大幅提升了缺陷修复的正确率、修复数量和修复效率；提出了最广泛使用的两大双向变换模型之一——基于差别的双向变换；成功自动优化广泛使用的开源软件，如Redis。工作应用到工业界，如字节跳动、华为公司、中兴公司、新一代Linux内核配置项目等。在IEEE TSE担任副主编、OOPSLA担任副主席、ASE担任领域主席，POPL、PLDI、ICSE、FSE等会议定期担任PC，5次在ICSE和FSE会议上获得杰出审稿人奖。承担了优青、青年973、重点研发课题等项目。获得国家技术发明一等奖（排名6）、电子学会自然科学一等奖（排名1）、CCF-IEEE CS青年科学家奖、MODELS十年最有影响力论文奖，5次获得ACM SIGSOFT/IEEE TCSE杰出论文奖，是ACM杰出会员和IFIP WG 2.4唯一来自中国的成员。

4. 报告人：王竟亦 研究员

题目：规约驱动的具身智能：形式化方法在具身大模型中的应用

摘要：以视觉-语言-动作（VLA）模型为代表的具身大模型正快速获得从语言指令到真实操作的端到端能力，但其仍面临泛化能力不足、行为缺乏可信保障等根本挑战。形式化方法有望为解决这些问题在具身大模型训练、评测和部署各阶段提供有力支撑，本报告将梳理形式化方法在具身大模型中的若干应用路径并讨论一些开放问题。

简介：王竟亦，浙江大学控制学院百人计划研究员，新加坡科技设计大学博士，新加坡国立大学博士后。研究兴趣是形式化方法/软件工程基础理论及其在安全攸关控制系统中的应用。在ICSE、ASE、ISSTA、FM、TACAS、S&P、CCS、NDSS等发表论文多篇，并获得ICSE的杰出论文奖两次（2018/2020）、IEEE TDSC最佳论文奖Runner-Up（2024）、ACM SIGSOFT亮点研究、中国指控学会科技进步一等奖（2024）和吴文俊人工智能科技进步二等奖（2025）。受邀担任ACM CCS、USENIX Security、ICSE、FSE、ASE、ISSTA等会议PC，SETTA 2026、ICFEM 2025、Large Model Safety Workshop 2025和SAC-SVT 2026/2027 PC Co-chair。

5. 报告人：曹嘉伦 助理教授

题目：从 AI 辅助到 AI 驱动：形式化程序验证的新探索

摘要：随着大语言模型（LLMs）、推理模型（Reasoning Models）和智能体（Agents）的快速发展，Agent、Harness、Skills 等新型 AI 技术正在不断改变 AI 完成复杂任务的方式，也为形式化程序验证带来了新的可能。本报告将围绕"从 AI 辅助到 AI 驱动"的演进，介绍我们在 AI 赋能形式化程序验证方向上的研究与一些初步探索。报告首先结合近年来的研究工作，介绍如何利用大语言模型自动生成形式化规约，并结合静态分析、测试和验证器反馈不断检查与修正规约；随后进一步分享我们对 Agent 编排、Harness、Skills 以及 Jev 的一些初步尝试，探索如何让 AI 不仅生成验证所需的规约，还能够理解当前验证状态、选择下一步行动，并根据反馈持续迭代。最后，报告将展望面向项目级软件的 Formal Verification Agent，并讨论当 AI 开始参与验证过程中的规划与决策后，形式化程序验证可能出现的新工作方式与研究机会。

简介：曹嘉伦博士是帝国理工计算机系的助理教授。她的研究重点是利用先进的人工智能技术实现软件开发、测试和程序验证的自动化，旨在实现从构建之初就具备可靠性的软件的自动化生产。她在ICSE、ESEC/FSE、CAV、ASE、ACL、AAAI、USENIX Security和TOSEM等顶级会议和期刊上发表了30余篇论文。她担任ICSE、FSE、ISSTA和ASE等顶级会议的程序委员，并担任ESEC/FSE 2025和ASE 2024的分会主席。她获得了2024年杰出论文奖，2025年ACM SIGSOFT杰出博士论文奖、2025年工程科学领域青年科学家奖等。

6. 报告人：李昊坤 技术专家

题目：C 程序形式化验证智能体及工业实践

摘要：大语言模型为程序形式化验证的自动化带来了新的可能，但面向真实 C 程序，仍需解决规约构建、复杂内存建模、长程证明组织以及验证结论可信性等挑战。本报告介绍我们在 c-code-verify 项目中的探索：以大模型智能体为执行主体，结合状态机驱动的流程控制与具有较小可信计算基（TCB）的形式化验证工具链，自主推进程序分析、规约构建与证明，验证范围涵盖内存安全、API 组合安全与功能正确性。报告还将结合该技术在真实工业代码中的应用，分享验证案例、实践经验及面临的挑战。

简介：李昊坤，北京大学博士，现任华为 2012 可信费马实验室形式化方法专家，参与多项形式化验证项目。主要研究方向包括符号计算、自动定理证明与程序验证，近年来重点探索大语言模型智能体在 C 程序形式化验证中的应用。相关成果发表于 CAV、ACL、ISSAC、Journal of Symbolic Computation 等国际会议和期刊。

五、论坛组织委员会简介

1. 论坛组委会：孙猛 教授

简介：北京大学数学科学学院教授，博士生导师，CCF形式化方法专委执行委员，区块链专委执行委员。主要研究领域包括程序理论、软件形式化方法、信息物理系统、可信人工智能、区块链与智能合约，主持国家自然科学基金、重点研发计划课题等多项国家及省部级项目，在TSE、TDSC、ICSE、FSE、FM、NDSS、ICML、NeurIPS、AAAI等期刊及会议发表论文150余篇，获TASE 2026、FSE 2025、ICFEM 2025、SBMF2017、TASE2015、AMAST2004等多个国际会议最佳/杰出论文奖，曾任ICFEM2024、FACS2024、TASE2023、ICFEM2018、TTSS2011、FACS2009等国际会议程序委员会主席及FM、TACAS等多个国际会议程序委员会委员。

2. 论坛组委会：张民 教授

简介：华东师范大学软件工程学院教授，中国计算机学会形式化方法专委会副主任、上海市高可信计算重点实验室主任。主要研究方向高可信智能软件与系统，发表高水平论文100余篇；累计主持国家和产业项目10余项，入选2025年上海市东方英才计划拔尖项目。主持包括国家自然科学基金面上项目、NSFC-ISF联合资助项目、中法"蔡元培"交流合作项目等国家级与国际合作项目，连续6年获华为、蚂蚁等头部企业资助。高安全嵌入式控制软件全生命周期关键开发技术与环境获上海市技术发明一等奖；可证明鲁棒的深度神经网络训练与验证技术获得中国计算机学会自然科学二等奖。