2025年CCF形式化方法专委会青年学术论坛——大模型辅助的程序分析与验证专题研讨会

报告摘要: 当前，大语言模型正以各种形式重塑包括形式化方法在内的各种技术领域，为提高软件开发效率、保障软件质量提供了新思路、新方案。然而，大语言模型不是“银弹”，其存在诸如幻觉、符号限制、缺乏领域知识等问题，让软件开发者在很多情况下不能通过简单的问答获得满意的结果。因此，如何在实践中可靠地使用大语言模型，克服上述诸多问题，成为一项亟需解决的难题。该报告将探讨大语言模型应用的一些想法，提出对“可靠使用大语言模型”的两个思路 —— 通过分治算法缓解大语言模型幻觉及符号限制、通过可靠的结果反馈增强大语言模型领域知识 —— 以及这两个思路在网络协议安全分析中的应用。

报告人简介: 时清凯，南京大学计算机学院副教授，博士生导师，国家级青年人才。2020年于香港科技大学获得博士学位，曾任源伞科技联合创始人、蚂蚁集团技术专家、美国普渡大学博士后研究员，目前主要从事编译技术及基于编译的软件安全技术研究，其研究成果广泛发表于诸如PLDI、OOPSLA、ICSE、FSE、SP、CCS等程序设计语言、软件工程、网络安全领域的CCF A类会议或期刊，其中一作论文10篇，并受邀担任相关会议审稿人，曾获ACM SIGPLAN或SIGSOFT杰出论文奖4次、Google论文奖、Hong Kong PhD Fellowship，曾三次参加全国软件大会原型竞赛均获一等奖。

报告摘要: 形式化证明与其相关的程序分析，测试用例生成等各种软件工程技术在实践中被广泛用以提升软件质量。然而这些技术带来的使用代价也常常被开发者所诟病。而大模型的出现为我们带来了一种新的可能性，即低代价（由AI代劳）高可靠的形式化与软件工程手段。本次报告会介绍我们在操作系统领域的实践与思考，如何将大模型与静态分析，自动化测试，形式化证明等相结合，通过更低的成本寻找代码中的缺陷，提升软件质量。

报告人简介: 李屹，现为华为操作系统部OS内核实验室技术专家，负责鸿蒙内核形式化和程序分析工作。主要研究兴趣包括，软件的形式化证明、程序分析与安全漏洞挖掘等泛形式化领域工作，大模型与软件工程的结合以及操作系统的智能化探索。

报告摘要: 相比于以自然语言形式表达的程序注释，由形式化语言写就的程序规约能够准确、全面、无歧义地描述程序的语义与行为，因此在软件生命周期的不同阶段均可发挥重要作用。然而传统的规约生成技术受限于程序的高度复杂性，难以生成有用的规约对程序的语义进行准确的描述。大语言模型打开了解决问题的新空间，基于大语言模型的程序规约生成技术吸引了业界的广泛关注。本次汇报，报告人围绕基于大语言模型的程序规约理解与生成展开，重点介绍如何利用程序规约度量大语言模型对于程序的语义理解能力（SpecEval）和利用大语言模型生成高质量的程序规约（SpecGen）。

报告人简介: 刘尚清，南京大学软件学院副教授，主要研究领域是智能化软件工程包括基于人工智能的程序漏洞检测与修复技术、代码自动化生成技术以及代码模型的可解释性研究等，在软件工程和人工智能领域发表高水平学术论文30余篇，包括ICSE、ASE、ICLR、NeurIPS等。报告人于2022年在南洋理工大学获取博士学位，从2023至2024年在南洋理工大学从事博士后研究，入选国家级青年人才项目。

报告摘要: The research in AI-based formal mathematical reasoning has shown an unstoppable growth trend. These studies have excelled in mathematical competitions like IMO and have made significant progress. This paper focuses on formal verification, an immediate application scenario of formal reasoning, and breaks it down into sub-tasks. We constructed 18k high-quality instruction-response pairs across five formal specification languages (Coq, Lean4, Dafny, ACSL, and TLA+) by distilling gpt-4o and evaluated against ten open-sourced LLMs, including recent popular DeepSeek-R1. We also fine-tuned several 7~8B small models to achieve comparable performance with Deepseek-R1-671B. Interestingly, we observed that fine-tuning with formal data also enhances mathematics, reasoning, and coding capabilities.

报告人简介: Dr. Jialun Cao is a Research Assistant Professor at the Hong Kong University of Science and Technology. Her main research areas include AI testing, AI4SE, and AI4formal verification, etc. She received her Ph.D. from the Hong Kong University of Science and Technology under the supervision of Professor Shing-Chi Cheung. She has published more than 20 papers in ICSE, ESEC/FSE, CAV, ASE, USENIX Security, TOSEM. She serves as a program committee member of top-tier conferences including ICSE, FSE and ASE. She received the 2025 ACM SIGSOFT Outstanding Dissertation Award.

报告摘要: 本报告围绕非线性实数算术的可满足性问题（SMT-NRA），介绍我们在多项式公式求解与局部搜索方法方面的最新研究进展。我们首先提出了一种面向仅包含严格不等式的 SMT-NRA 子类的局部搜索算法。该算法基于实根隔离，设计了一种名为 Cell-Jump 的新型跳跃操作，可沿指定方向跨越由多项式集合在实数空间中划分的胞腔（cell），从而实现原生支持非线性实数算术的局部搜索策略。 在此基础上，我们进一步提出了 二维 Cell-Jump（2D Cell-Jump） 操作，增强搜索的空间跳跃能力，并据此构建了局部搜索框架 2d-LS。为提升求解效率，我们将该框架与模型构造型可满足性演算（MCSAT）相结合，并引入 Sample-Cell 投影算子，用于在实数域中引导搜索避开冲突状态。最终，我们设计了一个融合 2d-LS、MCSAT 与 OpenCAD 的混合求解框架，通过信息交互进一步提升整体性能。实验结果表明，该方法在搜索效率和求解能力方面均取得了显著提升。

报告人简介: 李昊坤，2022年获北京大学博士学位，现于华为2012可信费马实验室形式化方法专家，参与多个重要的形式化验证项目。主要研究方向为符号计算，定理证明及程序验证，相关工作发表在CAV，ACL, ISSAC，JSC等国际知名期刊和会议上。