知行融创论坛第二期活动成功举办

基础软件与系统重点实验室党支部于 2025 年 5月 28日成功举办了知行融创论坛第二期活动。本次活动有四位同志进行了精彩的汇报交流，以下是报告的主要内容。

孟泊宁：针对典型 #EO 问题的多项式时间算法 研究了加权欧拉定向计数问题（记作 #EO）的计算复杂性，这是在计数框架 Holant 中的一个关键问题。主要贡献有三点：给出由二元和四元签名定义的 #EO 的复杂性二分类定理，推广了六顶点模型的结果；对所谓“纯签名”定义的 #EO 问题也建立了复杂性二分类，该类签名在构造组合模块时具有封闭性；提出一种多项式时间算法，解决由特定“重平衡签名”定义的 #EO 问题，并扩展到了非纯签名（如 $f_{40}$）的情形。此外还构造了一个非重平衡签名 $f_{56}$，其对应的 #EO 问题是否可多项式时间求解仍是一个公开问题。

迟智名：用于深度神经网络属性修复的补丁合成 深度神经网络（DNN）容易受到对抗攻击等可靠性问题的影响，限制了其在安全关键领域的应用。为此，近年来出现了一些神经网络修复技术，但多数方法仅适用于特定数据集，且缺乏理论保证。本文提出一种新的基于补丁的修复方法 PATCHPRO，专注于局部鲁棒性属性的修复。PATCHPRO 的核心思想是构造补丁模块，将其与原网络集成后，可针对鲁棒性邻域内的所有样本进行专门修复，同时保持原有性能。该方法结合形式化验证与启发式模块分配机制，不仅能抵御对抗攻击，还具有良好的泛化能力。实验证明，PATCHPRO 在效率、可扩展性和修复成功率方面均优于现有方法，在多个高维数据集上实现了100%的属性级修复。

高敏博：从最优传输对偶性出发的完备量子关系 Hoare 逻辑 提出了一种面向量子程序的定量关系 Hoare 逻辑，其断言形式是一种正半定算子的无限扩展。我们证明了该逻辑在有界后条件和几乎确定终止的程序下是完备的。完备性证明依赖于一种量子版本的最优传输对偶性定理。此外，我们还将带有投影断言的关系 Hoare 逻辑完整嵌入到本文逻辑中。

李勰：面向大语言模型引导的内核直接模糊测试探索 内核直接模糊测试是一种聚焦操作系统内核特定区域的技术，能有效应对频繁更新和系统复杂性带来的挑战。本文提出 SyzAgent 框架，将大语言模型（LLMs）与先进内核模糊器 Syzkaller 相结合，利用 LLM 实时引导测试用例的生成与变异。初步实验表明，该方法在基准测试中约 67% 的案例上有效。

本期“知行融创”论坛成功举办，为党员打造了学习交流、开拓视野的平台。论坛紧扣基础软件与系统领域，促进了学术进步，生动实践了党建与业务深度融合，党员先锋模范作用在科研一线得到充分激发，切实赋能科技创新。