形式化方法赋能的AI生成软件制品可信评测与优化

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

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