2023年11月11日下午，由中国计算机学会（CCF）主办，CCF YOCSEF苏州学术委员会承办，中国科学技术大学协办的中国计算机学会青年计算机科技论坛的YOCSEF技术论坛“大模型背景下基础软件及工具链的形式化验证方法 【论坛编号：CCF-Yo-23-135】”在中国科学技术大学苏州高等研究院唯真楼4楼第一会议室举行。

本次论坛执行主席是YOCSEF苏州AC委员王超和薛吟兴，参会专家包括YOCSEF总部联系AC鄢兴雨，现任CCF苏州YOCSEF主席史国良，副主席许佳捷，学术秘书叶雅梅，AC委员徐峰磊、孙高飞，中国航天五院502所研究员乔磊，浙江大学研究员姚培森，华为苏州研究所高级工程师钱忆等20余人线下参加本次会议。

论坛的引导发言环节由王超主持，他介绍了论坛的背景和参会的嘉宾，作了开场致辞。

图1：王超介绍YOCSEF

引导发言环节，来自中国航天五院502所研究员乔磊做了题为“航天器操作系统的研究与实践”的精彩报告。该发言从航天器计算机特征出发，介绍了研究所研制的SpaceOS I、SpaceOS II和SpaceOS III等航天操作系统及其相关典型应用，如载人航天、深空探测和通信等。乔磊研究员还分享了航天器操作系统的设计，如操作系统研制流程和不同的功能组成等，介绍了操作系统的任务调度策略，并在最后给出了研究所相关研究的总结。

图2：乔磊作为引导嘉宾获得感谢牌

浙江大学研究员姚培森则从软件质量保障的角度作了主题为“基于符号抽象的程序分析”的报告。报告点出程序分析是保障软件质量的重要手段，而抽象解释理论是静态程序分析的核心理论，介绍了基于抽象解释的程序分析和验证工具，符号抽象框架等。报告还分享了姚培森研究员近期关于计算最佳多面体抽象的研究工作，提出尝试采样更极端的高质量解、借助最佳区间抽象寻找“极端解”的想法。最后，报告还探讨了符号抽象与大模型的结合。

图3：姚培森作为引导嘉宾获得感谢牌

华为苏州研究所高级工程师钱忆从智能驾驶供应链出发，报告主题为“智能驾驶大规模仿真”。报告首先介绍了测试评价工具链，包括智能驾驶实车测试、智能驾驶仿真测试，并指出两者的优缺点。报告接着介绍了智能大规模仿真的组成：场景库、仿真平台、评价体系、安全、能力范围和体验。最后，报告分享了华为团队近些年的研究进度和未来研究目标：构建全球领先的大规模仿真数据集，评测准确性进一步提升，最终实现完全自动化。

图4：钱忆作为引导嘉宾获得感谢牌

引导发言结束后，参会嘉宾到唯真楼一楼进行合影留念。

图5：本次会议全体参与人员合影

论坛的思辨环节由薛吟兴主持。第一个议题是：国产基础软件的验证，包括航天操作系统软件等，最大的困境是卡脖子技术问题还是生态问题?

航天五院502研究所研究员乔磊首先发言，他认为脖子和生态都有，可能更为突出的是生态问题，如开发测试验证等，经统计目前使用的软硬件70-80%都是欧美的，操作系统、芯片问题更严重。AC委员徐峰磊从学校角度出发，他认为国家芯片公司这种都是体制优势，集中力量办事。对于学生学习、使用的软件或标准等，能不能也归统起来统一制定相关准则？ 主席史国良认为生态问题涉及到三个方面：第一，涉密之后怎么形成生态？第二，商业竞争不利于生态发展该怎么解决？第三，学生就业与生态相关，该如何既保证就业又构建自主可控的生态？华为苏州研究所高级工程师钱忆认为生态问题应奉行政府主导推行，企业优先使用，学生再学习的原则，政府主导效率更高，能防止企业自己竞争相互掣肘。

图6：思辨环节乔磊发言

第二个议题是：国产基础软件，在LLM蓬勃发展的趋势下，在Langchain等技术背景下，开发和维护过程中有哪些新的挑战？

乔磊首先提出大模型目前处于研究阶段，还没有真正使用，存在泛化性和可解释性等问题。大模型产生代码的过程非完全可控，不知该如何保证它的可靠性？且没有有效的泛化性验证方法。华为苏州研究所工程师赵剑认为大语言模型传统的协议、标准等可以一键生成，这对通信等行业来说是一大挑战。目前显卡如A100等对中国禁售，可获得性低，如何用二流的硬件实现一流的效果也是一个挑战。此外，如何很好的聚集大量的人才并协同工作也是一方面的挑战。会议执行主席薛吟兴提出大语言模型泛化性需要微调，很难在多模型、多领域中实现一般通用。大语言模型可解释性很难，这一块目前很难从科学上解决。大语言模型的公平性问题也较难解决。YOCSEF总部联系AC鄢兴雨提出两点挑战，一是如何让工程师和大模型形成紧密的合作，更好的一起工作；二是大模型生成的代码可能存在问题，是否有一个更好的方法能够对它进行直接验证。

图7：思辨环节鄢兴雨发言

第三个议题是：基础软件的形式化验证方面，大语言模型的出现是可以帮助形式化验证的效率和准确性，还是更多会带来一些新的安全挑战（例如prompt injection攻击）？

华为苏州研究所工程师庄航表示，模型生成可能会优先考虑某个方法，注入风险会一直存在，可通过恶意注入素材来保证未来能持续注入攻击。该种攻击可通过实现训练集的安全可控来解决，但是这会造成训练集体量的指数增长。薛吟兴认为，大模型通过强化学习到错误的信息就会一直存在风险，训练集安全可控很难实现。比如操作系统验证使用NLP技术生成简单的形式化脚本，但是AI生成的脚本可能会存在问题，漏掉样例，脚本的完备性等与高昂的成本费用挂钩。姚培森认为，有些步骤比如说验证，用求解器进行求解、用评测方法判断在某些特定场景可以做到，需要根据特定场景进行设计。鄢兴雨表示，可以先生成更容易验证的代码，再根据每个模块生成更有效率但是逻辑相同的代码。对于开源大模型可以找一个基座，再拿出绝对安全的部分代码对它进行相应的规划和训练，这样能有利于解决大模型存在的安全问题。

图8：思辨环节庄航发言

最后薛吟兴对思辨环节的议题做了相关的总结发言，论坛在轻松愉快的知识分享与交流中结束。感谢参会嘉宾的大力支持。