近年来人工智能领域在深度神经网络和以大语言模型为代表的基础模型技术方面产生的重大突破，推动信息世界、物理世界和人类社会日趋交叉融合，进一步打开了开放、动态和不确定场景下的复杂应用需求空间。有效解决开放、动态和不确定场景下的复杂应用问题，需要采用基于逻辑设计的符号计算和基于概率统计的神经计算相融合的智能化方案，这样的凯发k8登录的解决方案对应于一种新的软件形态：神经符号融合软件。神经符号融合软件有机结合基于逻辑设计的符号算法和数据使能的神经网络模型解决开放、动态和不确定场景下的复杂应用问题，在国防和经济建设的智能化应用领域存在广泛需求，是关键软件技术前沿领域战略性竞争的重要制高点。
神经符号融合软件作为新的软件形态，承载着数据知识双驱动的复杂系统构造和运行，目前缺乏针对性和系统性的软件理论和方法，亟需发展基础性的可信理论与方法以支撑新一代软件的可信构造与保障。本论坛拟就神经符号软件的模型与语言、设计与构造、可信与演化等内容开展前沿分析，探讨研发路线。欢迎软件工程、人工智能、可信软件等领域的专家和学者前来参加。
01
论坛组织委员会
王戟（国防科技大学）
李宣东（南京大学）
02
论坛议程
03
论坛报告嘉宾简介
马晓星
报告题目：神经符号系统-非确定管理视角的分析与展望
报告摘要：
作为一种智能化软件形态，融合了神经网络和符号规则的神经符号系统正受到越来越多的关注。然而，现有技术仍然难以有效支持较大规模神经符号系统“端到端”的自动构建。神经网络训练和符号规则学习过程中对非确定性的不兼容的处理方式是造成神经符号学习效果欠佳的一个关键因素。本报告旨在以非确定性管理的新视角，讨论分析“端到端”神经符号系统构建的技术挑战，评述相关工作思路、进展和当前仍然存在的问题，并在此基础上，展望下一步的发展方向。
报告人简介：
马晓星， ccf理事、软件工程专委主任，南京大学教授、计算机学院副院长。主要研究方向包括智能软件工程、软件自适应技术、软件体系结构与中间件等。研究工作得到国家杰出青年科学基金、国家973/863项目课题、国家自然科学基金重大项目课题等项目资助；发表学术论文百余篇，曾获中创软件人才奖、两次国家科技进步二等奖（分别为第2、第4完成人）等。
陈立前
报告题目：神经网络控制系统的验证
报告摘要：
在神经网络控制系统部署到安全关键场景之前，对其开展可达性分析和安全性验证至关重要。最近，泰勒模型和数值抽象域在验证神经网络控制系统方面各自显示出了优势。然而，仅使用泰勒模型在处理神经网络时可能会遇到可扩展性问题，而仅使用抽象域则无法精确地刻画控制系统受控体中常见的非线性状态。报告将探讨一种结合泰勒模型和数值抽象域的验证方法，以发挥两者的优势，在精度和可扩展性之间取得较好权衡。
报告人简介：
陈立前，国防科技大学计算机学院副教授。主要研究领域为可信软件，包括软件分析验证、软件自动修复等方向。在acm/ieee transactions、popl、fse等期刊会议上发表论文多篇，获acm sigsoft杰出论文奖，出版教材译著4部。研究成果获省部级科技进步一等奖1项、二等奖1项。部分成果已在航天、国防等领域重大工程中应用。
蒲戈光
报告题目：深度神经网络公平性测试的应用与挑战
报告摘要：
神经网络技术正快速融入人类社会，并被逐渐应用于包括招聘审核、贷款风控等敏感领域中。但由于算法可能存在对不同群体的歧视与偏见，人们正越来越关心这项技术在公平性上的表现。为了改善或解决深度神经网络中不公平的问题，已有大量致力于提供有效的公平性度量、测试挖掘模型中的公平性缺陷以及为模型提供公平性修复。然而，在模型性能与公平性的权衡、算法的效率、缺陷挖掘的有效性等方面仍然存在诸多挑战。为了应对这些挑战，我们提出了cfp、eidig、fipser等相关技术。其中，cfp基于同时考虑多种公平性指标和模型性能的综合测量方法，构建了能够有效改善机器学习分类器的强化学习框架，在不牺牲性能的前提下，显著提升了多个公平性指标。eidig和fipser则分别从个体歧视实例挖掘的梯度计算和种子选取阶段入手，通过引入动量机制、减少梯度计算和种子优先选取的方法，改善了个体歧视实例缺陷挖掘。
报告人简介：
蒲戈光，华东师范大学软件工程学院教授、执行院长，上海工业控制安全创新科技有限公司总经理，研究聚焦形式化方法与软件工程领域，特别是在软件验证理论与算法，工业级验证工具研发等方面做出了贡献。目前担任科技部重点研发计划专项“人工智能安全可信理论及验证平台“首席科学家。研究成果曾获acm 杰出论文奖，上海市科技进步特等奖，北京市科技进步一等奖等奖项。近五年在icse、ase、fse、cav等国际权威会议发表学术论文30余篇。研发的多款创新验证与测试算法对发现真实软件缺陷非常有效，如研发的自动化测试工具stoat发现了5000多个app的8000多个缺陷，包括微信、抖音等商业app的严重缺陷。近期一直致力于产学研的转化研究，主导研发的测试与验证工具平台服务了100多家家企业，有效提升了企业软件开发的质量与效率。
张立军
报告题目：基于替代模型构造的神经网络鲁棒性保障方法
报告摘要：
由于深度神经网络等智能算法模型规模庞大、结构复杂，其可信性很难保障。我们讨论智能算法的鲁棒性、安全性分析，通过基于pac（probably approximately correct）模型学习等方法对神经网络模型验证分析，讨论智能算法鲁棒性等可信性质的白盒及黑盒验证方法。我们通过开源自动驾驶平台iss介绍课题组在可信智能算法安全验证取得的系列进展。
报告人简介：
张立军，中国科学院软件研究所研究员，主要从事形式化方法、智能算法可靠性研究，在学术会议及期刊发表了一百余篇论文。2013年加入中科院软件所，回国前曾任丹麦科技大学长聘副教授。致力于概率与混成模型量化分析、可信智能软件等前沿技术的研究。担任国际逻辑大会 lics 2020（ccf a类会议）共同主席，及tacas 2019、concur 2018（ccf b类会议）程序委员会主席。获国家自然科学基金委员会“重点项目”、科技部重点研发课题、中德国际合作等多项项目资助。2022年获中科院稳定支持基础研究团队项目资助，作为负责人带领研究开放环境下的可信智能算法。
熊英飞
报告人简介：
熊英飞于2009年从日本东京大学获得博士学位，2009-2011年在加拿大滑铁卢大学工作，2012年加入北京大学，现任新体制长聘副教授、软件研究所副所长、计算机学院院长助理。熊英飞的研究兴趣是程序设计语言和软件工程，特别是程序合成、修复和分析。他的工作产生了一系列不同规模的效果同期最优代码生成神经网络模型；大幅提升了缺陷修复的正确率、修复数量和修复效率；提出了最广泛使用的两大双向变换模型之一——基于差别的双向变换；成功自动求解大量算法问题，包括世界顶级算法竞赛中的问题。他的工作也被工业界采用，比如新一代linux内核配置项目、燕云daas系统、华为公司、中兴公司等。他获得电子学会自然科学一等奖（排名1）、ccf-ieee cs青年科学家奖、models十年最有影响力论文奖，5次获得acm sigsoft/ieee tcse杰出论文奖。他是sate18的程序委员会联合主席，也在pldi、icse、fse等会议担任pc
万成城
报告人简介：
万成城，华东师范大学软件工程学院研究员，博导。博士毕业于芝加哥大学计算机系。主要研究方向为智能软件系统优化和智能化软件工程。多项研究成果发表于icse、fse、tosem、dac、atc、vldb、icml等国际顶级会议和期刊。曾获siebel 学者、eecs rising star、icse的杰出论文奖等荣誉与奖项。
04
论坛组织委员会简介
论坛主席：王戟
个人简介：
王戟，国防科技大学教授，主要研究方向是可信、智能与新兴软件技术和系统。
论坛主席：李宣东
个人简介：
李宣东，南京大学教授，教学与科研工作主要涉及软件工程、可信软件、形式化方法、系统软件。
