AI 赋能的自动化程序验证

演讲者:    曹嘉伦，香港科技大学

时间:        2026年7月21日，10:00

邀请人:    陈宇奇

地点:        信息学院1A-200

摘要:

随着大语言模型（LLMs）的快速发展，AI 正在深刻改变形式化方法的研究与应用方式。本报告将介绍 AI 赋能自动化程序验证的最新进展，首先回顾程序测试与形式化验证的区别，以及契约式编程和程序规约在软件可信性中的核心作用；随后结合近年来的研究成果，分享如何利用大语言模型自动生成形式化规约、结合静态分析与验证器反馈提升验证成功率，并探讨推理模型（Reasoning Models）与 Agent 技术在形式化程序验证中的能力边界与发展趋势。最后，报告将展望 Harness 驱动的形式化验证智能体（FM Agent）以及面向项目级软件验证的新范式，讨论 AI 与形式化方法双向赋能的发展方向，以及构建可信 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年工程科学领域青年科学家奖等。