目录

代码生成、智能代理与开发工具

• • Leveraging LLMs for Grammar Adaptation: A Study on Metamodel-Grammar Co-Evolution
• • Stdlib or Third-Party? Empirical Performance and Correctness of LLM-Assisted Zero-Dependency Python Libraries
• • SpecBench: Measuring Reward Hacking in Long-Horizon Coding Agents
• • Insights Generator: Systematic Corpus-Level Trace Diagnostics for LLM Agents
• • Domain-Adaptable Reinforcement Learning for Code Generation with Dense Rewards
• • ACL-Verbatim: hallucination-free question answering for research
• • Governance by Construction for Generalist Agents

程序验证、测试与质量安全

• • Quality and Security Signals in AI-Generated Python Refactoring Pull Requests
• • Agentic Model Checking
• • Validating Navmesh using Geometry: Voxel-Based Analysis with Prioritized Exploration
• • Beyond the Tip of the Iceberg: Understanding SATD in Dockerfiles through the Lens of Co-evolution
• • Detecting Trojaned DNNs via Spectral Regression Analysis
• • BioDefect: The First Dataset for Defect Detection in Bioinformatics Software
• • An Event-Driven Tool for Context-Aware Code Smell Detection Using SmellDSL

编程语言、语义与编译

• • Multicategorical Semantics for Untyped Effects
• • Combinatorial manifolds and Kleene's theorem, homotopically
• • Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
• • Sutra: Tensor-Op RNNs as a Compilation Target for Vector Symbolic Architectures

系统软件与软件工程实践

• • Software Product Line Engineering: Adoption, Tooling and AI Era Challenges
• • RSE of a Quantum Transport Code and its Effects
• • Transforming Privacy Artifacts into Accessible Reports for Non-Technical Stakeholders
• • ParaCell: Paravirtualized Secure Containers with Lightweight Intra-Container Isolation and Intent-Driven Memory Management

代码生成、智能代理与开发工具

Leveraging LLMs for Grammar Adaptation: A Study on Metamodel-Grammar Co-Evolution

• • 作者：Weixing Zhang, Bowen Jiang, Rahul Sharma, Regina Hebig, Daniel Strüber
• • arXiv URL：https://arxiv.org/abs/2605.21465v1

Abstract

在模型驱动工程中，元模型演化会带来相应语法的适配需求，以维持一致性，这通常需要繁琐的人工工作。现有基于规则的方法虽然能实现部分自动化，但在处理复杂语法场景时存在局限。本文提出一种基于大语言模型的方法，通过学习先前版本中的语法适配方式，自动将这些适配应用到演化后的新语法上。我们在六个真实世界的 Xtext 领域特定语言上评估了该方法，其中四个 DSL 用于训练提示策略，两个 DSL 用于测试验证，并对 QVTo 开展了纵向案例研究。评估使用了三种大语言模型（Claude Sonnet 4.5、ChatGPT 5.1、Gemini 3），并从三个维度衡量语法适配质量：语法规则级适配一致性、输出相似度以及元模型符合性。结果表明，在测试集上，三种 LLM 都实现了 100% 的适配一致性和输出相似度，而基于规则的方法在 DOT 上仅为 84.21%，在 Xcore 上仅为 62.50%。在 QVTo 纵向研究中，基于 LLM 的方法在三次演化步骤中都成功复用了已学习到的适配，无需人工编辑语法，而基于规则的方法在三次迁移中的两次都需要人工调整。不过，在大规模语法（EAST-ADL，297 条规则）上，LLM 的适配一致性远低于 90%。该研究表明，基于 LLM 的方法在处理复杂语法场景时具有优势，同时也揭示了其在大规模语法适配中的局限。

Stdlib or Third-Party? Empirical Performance and Correctness of LLM-Assisted Zero-Dependency Python Libraries

• • 作者：Peng Ding, Rick Stevens
• • arXiv URL：https://arxiv.org/abs/2605.21405v1

Abstract

第三方 Python 库会带来依赖管理开销、供应链风险以及在受限环境中的部署摩擦。一个自然的问题是：仅使用 Python 标准库能够在多大程度上复现这一生态系统，以及会以怎样的正确性和性能代价来实现。我们通过 zerodep 对这一问题进行了实证研究。zerodep 是一个不断扩展的单文件 Python 模块集合，每个模块都是对一个流行第三方库的仅依赖标准库的重实现，并在严格约束下由 LLM 辅助开发：不得使用外部导入、必须是单文件、需保持可直接替换的 API 兼容性，并且必须通过与参考库对照的正确性验证。zerodep 覆盖 12 个类别中的 40 多个模块，包括序列化、网络、密码学、代理协议和文本处理，为两个相互关联的问题提供了受控测试床：(1) 标准库在哪些场景下足够？(2) 在紧约束的符号条件下，LLM 是否能够有效生成正确且高性能的代码？系统性基准测试表明，纯标准库实现中的大多数都能达到与参考实现相当的性能（在 2 倍以内）。性能下降的主要来源是依赖 C 扩展的计算（图像处理、二进制序列化、底层密码学），而不是纯 Python 第三方库本身的固有开销。相反，许多广泛使用的库带有架构性开销，而 LLM 生成的标准库重实现可以避免这些开销，在若干类别中带来 5 到 115 倍的加速。我们刻画了标准库能力边界在不同复杂度层级和库类别上的分布，讨论了 LLM 辅助开发在何处成功、在何处需要迭代式人工修正，并分析了其对大规模无依赖软件工程的启示。zerodep 已开源于 https://github.com/Oaklight/zerodep。

SpecBench: Measuring Reward Hacking in Long-Horizon Coding Agents

• • 作者：Bingchen Zhao, Dhruv Srikanth, Yuxiang Wu, Zhengyao Jiang
• • arXiv URL：https://arxiv.org/abs/2605.21384v1

Abstract

随着长时程编码智能体生成的代码量超过任何开发者可审阅的范围，监督最终会收缩到单一表面：自动化测试套件。在这种设置下，奖励黑客自然出现，因为智能体会优化“通过测试”，却偏离用户的真实目标。我们通过将软件工程任务分解为三个部分来研究这一奖励黑客现象：(i) 规范的自然语言描述；(ii) 覆盖规范功能子集的可见验证测试；(iii) 用于模拟真实使用场景的留出测试。基于规范和可见验证测试套件，一个真正遵循目标的智能体应当也能生成可通过全部留出测试的解。因此，我们使用这两套测试的通过率差距来量化奖励黑客。基于该方法，我们提出 SpecBench，一个包含 30 个系统级编程任务的基准，任务长度从构建 JSON 解析器这样的短程任务，到从零构建整个操作系统内核这样的超长程任务不等。大规模实验揭示出一种一致模式：尽管所有前沿智能体都能将可见测试套件跑满，奖励黑客仍然存在，而且更小的模型在留出测试上的差距更大。该差距也会随着任务长度急剧扩大：代码规模每增加十倍，差距便增长 28 个百分点。失败形态既包括微妙的功能隔离，也包括蓄意利用，例如一个 2,900 行的哈希表“编译器”会记忆测试输入。SpecBench 为衡量编码智能体是在构建真正可用的系统，还是只是在利用开发者提供的测试套件，提供了一个原则性测试床。

Insights Generator: Systematic Corpus-Level Trace Diagnostics for LLM Agents

• • 作者：Akshay Manglik, Apaar Shanker, Kaustubh Deshpande, Jason Qin, Yash Maurya, Veronica Chatrath, Vijay S. Kalmath, Levi Lentz, Yuan, Xue
• • arXiv URL：https://arxiv.org/abs/2605.21347v1

Abstract

LLM 智能体的故障诊断在很大程度上仍是人工完成的。实践者通常只检查少量执行轨迹，提出临时假设，然后反复迭代。这个过程会遗漏只有在轨迹群体层面才会显现的模式，并且无法扩展到个别轨迹就长达数万 token 的生产级语料库。我们将“语料级轨迹诊断”这一问题形式化：给定一个执行轨迹语料库，目标是生成有据可依的自然语言洞见，用以刻画轨迹分组中的系统性行为模式，并为每条洞见提供支撑证据。我们提出 Insights Generator（IG），这是一个多智能体系统，通过在轨迹语料库上提出并检验假设，来回答诊断问题并生成一份有证据支撑的洞见报告。我们从定性和客观两个维度对 IG 进行评估，覆盖基于量表的报告质量评审以及由实施 IG 洞见所带来的下游性能提升。使用 IG 报告的人类专家在 scaffold 性能上相较未修改基线提高了 30.4 个百分点，利用 IG 洞见的编码智能体也表现出持续且稳定的收益。在各项基准上，IG 的 scout-investigator 架构在检测覆盖率上与竞争方法相当，而领域专家将 IG 报告评为深度和证据质量最佳之一。

Domain-Adaptable Reinforcement Learning for Code Generation with Dense Rewards

• • 作者：Erfan Aghadavoodi Jolfaei, Daniel Maninger, Abhinav Anand, Mert Tiftikci, Mira Mezini
• • arXiv URL：https://arxiv.org/abs/2605.21180v1

Abstract

大语言模型在自动代码生成方面展现出强大潜力，但在正确性、质量、安全性以及领域特定约束方面缺乏保障。例如在机器人领域，代码生成越来越多地用于动作规划与执行，而对环境和物理约束的感知至关重要。为促进代码生成型 LLM 适应多样化需求，包括领域特定需求，我们提出一个强化学习框架，使用近端策略优化对预训练 LLM 进行微调。我们可定制的执行感知奖励公式同时捕获并优化语法、功能正确性、代码风格、安全性以及模拟器可执行性。一个 token 级奖励映射机制使得执行结果能够有效归因到生成 token。我们在通用代码生成（MBPP/MBPP+）和机器人程序合成（RoboEval）上评估了该框架。结果表明，功能正确性和模拟器可执行性均有显著提升，其中 MBPP 的 pass@1 绝对提升了 19%，RoboEval 的执行失败减少了 51%。这些结果表明，结构化强化学习能够有效地将语言模型对齐到正确程序生成和领域特定需求上。

ACL-Verbatim: hallucination-free question answering for research

• • 作者：Gábor Recski, Szilveszter Tóth, Nadia Verdha, István Boros, Ádám Kovács
• • arXiv URL：https://arxiv.org/abs/2605.21102v1

Abstract

学术研究者需要高效且可靠的方法，从可信来源收集高质量信息，但现代 AI 辅助研究工具仍受到大语言模型倾向于生成事实错误或无意义输出的影响，这通常被称为“幻觉”。我们将抽取式问答系统 VerbatimRAG 应用于 ACL Anthology 中的研究论文，直接把用户查询映射到检索文档中的逐字文本片段。我们贡献了一个新的真值数据集，用于将用户查询映射到研究论文中的相关文本片段，并以此训练和评估多种抽取式模型。人工标注由 NLP 研究者完成，基于使用定制流水线并结合 ScIRGen 方法生成的合成用户查询，以及由 VerbatimRAG 检索到的论文切块。在该基准上，一个 1.5 亿参数的 ModernBERT token 分类器，在我们的流水线生成的银标监督上训练后，取得了最佳词级 F1（53.6），超过了表现最强的 LLM 抽取器（48.7）。

Governance by Construction for Generalist Agents

• • 作者：Segev Shlomov, Iftach Shoham, Alon Oved, Ido Levy, Sami Marreed, Harold Ship, Offer Akrabi, Sergey Zeltyn, Avi Yaeli, Nir Mashkif
• • arXiv URL：https://arxiv.org/abs/2605.20874v1

Abstract

企业级智能体越来越需要在工具和界面之间自主运行，但生产部署要求“按构建即治理”（governance by construction）。系统必须规定哪些动作是允许的、何时需要人工监督，以及可以暴露哪些信息，同时又不能为每个领域重新构建智能体。本文演示了 CUGA 的策略系统，这是一个模块化的 policy-as-code 层，可与通用 LLM 智能体组合，在不进行模型微调的情况下，为复合工作流提供可预测、可审计且符合合规要求的行为。我们展示了一种运行时治理架构，它在执行的每个关键阶段都强制实施策略干预。策略并不是被动地约束行为，而是通过五个结构性检查点拦截智能体：在规划之前的上游（Intent Guard）、在系统提示内部以引导推理（Playbook）、在工具调用边界以强制正确使用（Tool Guide）、在推理环之外作为高风险操作的人在回路门控（Tool Approvals），以及在输出阶段对最终响应进行过滤和结构化（Output Formatter）。这五个阶段共同将治理持续嵌入智能体的执行流水线，而不是把它当作事后补丁。借助一个医疗场景和多层级执行干预，该演示展示了用于结构化工具序列约束的动态 playbook 注入、用于拦截恶意或意外有害请求的 intent guards，以及针对潜在破坏性操作的人在回路工具审批检查点。该工件说明，类型化的治理原语能够帮助更快、更安全地部署企业级 agentic 系统，同时提升策略遵循度和执行一致性。

程序验证、测试与质量安全

Quality and Security Signals in AI-Generated Python Refactoring Pull Requests

• • 作者：Mohamed Almukhtar, Anwar Ghammam, Hua Ming
• • arXiv URL：https://arxiv.org/abs/2605.21453v1

Abstract

随着 AI 智能体越来越多地参与代码开发与维护，我们对于它们在真实项目中所做更改的质量与风险特征仍缺乏充分的实证证据，尤其是针对重构类贡献。代理生成的重构编辑在合并到 GitHub 仓库后，会如何影响可维护性、代码质量与安全性，仍不清楚。为弥补这一空白，我们基于 AIDev 数据集中的 Python 重构拉取请求（PR）开展了一项实证研究。我们使用基于机器学习的 Python 质量评估工具 PyQu 来分析代理生成的重构 PR，以量化五个质量属性上的变化，并结合与领域无关的静态分析工具 Pylint 和 Bandit，在每次变更前后衡量代码质量和安全问题。结果显示，平均而言，代理提交仅在 22.5% 的被研究变更中改善了某项质量属性，其中可用性改善最频繁（36.5%）。与此同时，24.17% 的被修改文件引入了新的 Pylint 问题，主要是长行等惯例层面的违规，而 4.7% 引入了新的 Bandit 发现。根据观察到的差异，我们归纳出 24 类重复出现的变更操作，并将其映射到它们最常影响的 lint 和安全发现。尽管结果喜忧参半，开发者接受度很高：被分析的 PR 中有 73.5% 被合并，其中包括引入新的 lint 或安全问题的案例，且这些问题常常与对既有问题的移除同时出现。总体来看，这些发现既凸显了代理式重构的潜力，也表明其当前仍存在局限，并说明需要在 AI 驱动开发流程中引入更强的工具在环质量与安全门控。

Agentic Model Checking

• • 作者：Youcheng Sun, Jiawen Liu, Daniel Kroening, Jason Xue
• • arXiv URL：https://arxiv.org/abs/2605.21434v1

Abstract

在验证 LLM 生成的系统代码时，困难来自多个方面：漏洞普遍存在，形式化规格缺失，而且安全约束往往编码在调用点的隐式上下文中，而不是被函数边界显式强制。我们提出智能体式模型检查，这是一种将 LLM 智能体与有界模型检查后端结合的范式，其原则是“智能体提出，求解器验证”：智能体负责需要语义判断的任务（规格推断、检查选择、反例分类、细化建议），而有界模型检查器负责完成所有与正确性相关的判定。该范式建立在三项承诺之上。首先，规格从调用者上下文自顶向下推断，并使用受限 DSL 表达，然后确定性地转换为后端的 assume/assert 原语；可选的函数正确性条款则将验证从“无崩溃”提升到“行为忠实性”。其次，验证是组合式的：每个函数都在其规格下独立检查，调用者则由带后置条件约束的 stub 替代，因此每次查询的成本随单个函数的状态空间而变化，且细化会自动传播到调用者。再次，反例并不直接等同于缺陷报告：它们会经过一个验证流水线（可达性、被调用者可行性、动态回放、真实性审计），以区分正在运行的仓内崩溃与潜在的公共 API 失败，同时将建模工件用于细化循环而不是简单屏蔽。我们在 BMC-Agent 中实现了该方法，并将其评估于 LLM 生成的内核和编译器 C/Rust 代码以及成熟、经过 OSS-Fuzz 加固的库上，结果确认了真实缺陷，在经受大量 fuzz 的表面上产生了有界的洁净验证，并在部分算法函数上建立了功能等价性。

Validating Navmesh using Geometry: Voxel-Based Analysis with Prioritized Exploration

• • 作者：Ramesh Raghavan, Ojas Sharma, Sebastien Larrue, Alan Isaac Kunder, Aakash Sai, Rishi Mathur
• • arXiv URL：https://arxiv.org/abs/2605.21397v1

Abstract

导航网格（Navmesh）中的不一致会直接影响游戏环境中非玩家角色（NPC）所使用的导航系统，从而破坏玩家体验。虽然 navmesh 通常由世界几何通过成熟算法生成，但在开发过程中，地形会被调整，资产会被移动或替换，导致 navmesh 与实际环境之间出现不匹配。现有自动化方法通常尝试借助探索智能体和强化学习技术检测导航问题。然而，由于这些方法依赖导航数据本身，或者仅间接评估导航行为，它们并不能明确验证导航表示是否真实反映了底层几何所定义的可通行空间。本文提出一个通过独立的、由几何驱动的分析来验证导航网格正确性的框架。该方法首先以体素表示直接从环境几何中重建可通行空间，随后进行约束感知的遍历与连通性评估。验证被形式化为体素空间上的优先级搜索问题，其中强化学习用于引导采样，聚焦更可能暴露不一致的区域。在每个采样位置，基于体素表示推导出的可达性会与通过引擎级查询从 navmesh 获得的可达性进行比较。针对多个大规模开放世界游戏环境的实验表明，该方法在保持相近缺陷检测覆盖率的同时，持续降低了探索开销。该框架可在游戏引擎内部离线运行，并可集成到自动化质量保障流水线中。由于该方法依赖几何信息，它可以较少修改地适配不同游戏引擎，因此适合生产环境部署。

Beyond the Tip of the Iceberg: Understanding SATD in Dockerfiles through the Lens of Co-evolution

• • 作者：Wei Minn, Yan Naing Tun, Biniam Fesseha Demissie, Rui'ang Hu, Jiakun Liu, Mariano Ceccato, Lwin Khin Shar, David Lo
• • arXiv URL：https://arxiv.org/abs/2605.21238v1

Abstract

Dockerfile 用于创建应用代码可移植的基于容器的执行环境，已成为现代软件开发流程的重要组成部分。作为一种基础设施即代码（IaC）形式，Dockerfile 中可能包含临时性权宜之计和其他次优实现，从而在未来积累影响可靠性、安全性和可维护性的技术债务。已有工作从 Dockerfile 注释及其周边文件块的角度刻画了自陈式技术债务（SATD）。然而，这种单文件视角并不完整，因为源代码演化涉及生产、测试、构建以及其他配置文件等不同类型的软件工件的变更。因此，我们通过同时研究 Dockerfile 中的 SATD 事件及其关联源代码，来弥补这一空白。我们发现，约 27% 的认领事件和 40% 的偿还事件与非 Dockerfile 工件相关联，而且这种耦合来源具有子类型特征。我们还观察到，耦合 SATD 总体上偿还得显著更快（p = 0.0201），但与缺失功能相关的耦合 SATD 比其孤立对应项持续时间更长。最后，我们对耦合 SATD 事件进行了开放式编码和轴心编码，观察到外部依赖问题，尤其是尚未发布的上游包和 bug 修复，是源代码中最常见的认领触发原因；同时，我们也观察到，架构重构是 Dockerfile 中 SATD 偿还的最常见前置条件。这些发现表明，实践者（如开发者和项目经理）与 SATD 研究者都应将源代码侧的共演化，而非单文件视图，作为分析的主要单位。

Detecting Trojaned DNNs via Spectral Regression Analysis

• • 作者：Samuele Pasini, Jinhan Kim, Paolo Tonella
• • arXiv URL：https://arxiv.org/abs/2605.21146v1

Abstract

现代 DNN 会反复进行微调，以纳入新的数据与功能。这一演化式工作流带来了安全风险，因为当更新数据无法被完全信任时，攻击者可能在微调过程中植入木马。我们提出 MIST，一种通过分析模型在微调过程中内部表示如何变化来检测木马的办法。MIST 并不试图重建触发条件，而是利用预激活谱来刻画良性模型演化，并将与这一参考不一致的谱偏移的更新标记出来。这一表述将木马检测视为对模型更新的回归问题。跨四个数据集和八种木马攻击的实证评估表明，谱距离能够可靠地区分含木马的更新与干净微调。MIST 在单次更新后即以高于现有方法的检测精度工作，而无需了解任何关于中毒数据或触发器的信息；在多步良性演化下仍然有效，只出现平稳且有限的性能退化。这些结果表明，谱演化为检测恶意模型更新提供了稳定且假设较少的信号。

BioDefect: The First Dataset for Defect Detection in Bioinformatics Software

• • 作者：Tianxiang Xu, Xiaoyan Zhu, Xin Lai, Xin Lian, Hangyu Cheng, Jiayin Wang
• • arXiv URL：https://arxiv.org/abs/2605.20788v1

Abstract

软件缺陷检测是软件工程中的关键任务。然而，尚无先前研究专门针对生物信息学软件中的缺陷检测。鉴于缺陷检测任务的性能主要受模型和数据集双重影响，我们的实验控制了模型相关因素，并确认了现有数据集在生物信息学软件场景中的局限性。为解决这一问题，我们引入 BioDefect，这是首个专门为生物信息学软件缺陷检测设计的数据集，旨在克服该领域现有数据集的局限。与以往数据集不同，BioDefect 包含完整的源代码仓库，保留了有缺陷代码的真实上下文信息，从而更准确地反映生物信息学软件中的真实缺陷场景。此外，BioDefect 缓解了标签不一致和数据泄漏问题，确保了较高的数据质量和实验可靠性。为评估 BioDefect 的有效性，我们在九种语言模型上进行了系统评估，包括 DeepSeek-R1。结果表明，BioDefect 显著提升了生物信息学软件的缺陷检测性能。与现有数据集相比，BioDefect 在所有模型上的平均 F1 提升为 29.61% 到 38.04%，凸显其显著优势。该研究填补了生物信息学软件缺陷检测中的一个关键研究空白，为未来研究奠定了基础，并为提升生物信息学软件质量保障提供了新的思路。

An Event-Driven Tool for Context-Aware Code Smell Detection Using SmellDSL

• • 作者：Matheus dos Santos Viegas, Adrian Gabriel Keller dos Santos, Kleinner Farias, Robson Keemps da Silva
• • arXiv URL：https://arxiv.org/abs/2605.20675v1

Abstract

代码异味表明设计原则遭到破坏，会降低演化中软件系统的内部质量。尽管许多工具使用静态指标检测此类异常，但它们往往忽视异味产生和被消除时的开发情境。这一局限会导致误导性的告警，并削弱对重构决策的支持。为了解决这一问题，我们提出 SmellHunter，一个上下文感知工具，它解释用 SmellDSL 领域特定语言编写的脚本，以检测并情境化代码异味。SmellHunter 将静态代码指标与上下文信息（如团队特征、项目阶段和地理元数据）结合起来，生成更丰富、更可操作的分析。该工具采用事件驱动架构，由服务总线通过异步事件协调验证、解释和持久化服务。这种架构能够在尽量减少对开发者工作流干扰的同时，实现可扩展分析。SmellHunter 通过专用插件集成到 Eclipse 开发环境中，并通过移动应用提供聚合洞见，使开发者能够按类型、严重程度和位置探索异味发生情况。通过将异味检测与上下文数据和协作可视化相结合，SmellHunter 支持开发者像“异味猎人”一样工作，帮助团队识别来自特定位置的重复质量问题，并把重构任务分配给具有相关专长的开发者。我们描述了 SmellHunter 的架构、SmellDSL 脚本的解释过程，以及上下文数据的集成方式，以支持现代软件开发环境中更明智的重构决策。

编程语言、语义与编译

Multicategorical Semantics for Untyped Effects

• • 作者：Ariel Grunfeld, Liron Cohen
• • arXiv URL：https://arxiv.org/abs/2605.21337v1

Abstract

在范畴语义中的完备性证明，通常通过构造一个由代换给出复合的句法范畴来进行。对于未类型化、带效应的按值调用语言而言，这会遇到一个根本障碍：由于求值顺序在语义上是有意义的，因此不存在计算的同时代换的规范概念。我们通过将单个计算代换，也就是绑定步骤，作为原语来解决这一问题，并用串接来表示由有限顺序列表构成的计算代换。我们在一个单对象的 Freyd-多范畴设定中将这一思想形式化。我们引入 Freyd operad，将值的笛卡尔 operad 与计算的对称 Ren-笛卡尔 preoperad 分离开来，并通过一个 Freyd 函子将二者连接；并且从任意 Freyd operad 出发，我们构造出一个对应的 Freyd PROP，用于表示代换。我们证明了这一构造是可表征的，并且在严格的一对象设定下，它是限制到余域 1 的左伴随。借助由此导出的项模型，我们在弱闭 Freyd operad 中解释带过程和高阶函数的未类型化计算 λ 演算，并证明了其可靠性、初始性与完备性。这为未类型化效应计算提供了一种专门的范畴语义，同时也足够广泛，能够包含基于可实现性的模型，例如单子组合代数。

Combinatorial manifolds and Kleene's theorem, homotopically

• • 作者：Yorgo Chamoun
• • arXiv URL：https://arxiv.org/abs/2605.21142v1

Abstract

我们给出一种通用方法，用于构造组合流形的类别，即由满足每个“点”处局部性质的组合对象构成的类别，并将其作为关系预层范畴中的余反射子范畴来构造。为此，我们关键地依赖唯一分解系统，并且可以把这一技术理解为一种构造模型范畴的方法，其中的 cofibrant 对象恰好是组合流形。随后我们通过两个应用展示这一观点的有效性。首先，我们构造欧几里得 precubical sets 的范畴，即在局部上看起来像某个固定维度网格的 precubical sets，并证明它在关系 precubical sets 范畴中是余反射的。这是欧几里得局部有序空间和有向拓扑中的 blowup 构造的组合对应。其次，我们通过定义行为良好的“流形自动机”来给出自动机理论中 Kleene 定理的一个抽象证明，并说明其与串接相容。

Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows

• • 作者：Benedikt Bollig
• • arXiv URL：https://arxiv.org/abs/2605.20923v1

Abstract

分布式 LLM 智能体工作流不应被当作一个单一的顺序日志来监控。在异步执行中，一个决策只能依赖于对作出该决策的那条生命线而言“因果可见”的事件：某个在某些日志中更早出现的事件，在本地可能仍不可见。我们将 ZipperGen 智能体工作流框架扩展为 Causal Past Logic（CPL），这是一种用于条件分支和 while 循环守卫的简单过去时态逻辑。除了标准的过去时模态（如 previous 和 since）外，守卫还可以检查另一条生命线最近因果可见的事件，以及存储在那里的选定变量。该公式是源级守卫：它由拥有者生命线在线求值，并可在运行时影响控制流。我们给出一个带最新值视图的向量时钟监视器，并证明本地计算的监视器值与当前事件处守卫的指称语义一致。因此，运行时验证成为协调语言本身的一部分，而不是对执行日志进行事后检查。

Sutra: Tensor-Op RNNs as a Compilation Target for Vector Symbolic Architectures

• • 作者：Emma Leonhart
• • arXiv URL：https://arxiv.org/abs/2605.20919v1

Abstract

Sutra 是一种带类型的纯函数式编程语言，其编译后的前向传播就是一个 PyTorch 神经网络。编译器将整个程序——原语、控制流、字符串 I/O——β 归约为一个基于冻结嵌入基底的、融合为单一张量算子图的结构。旋转绑定、解绑、捆绑、多项式 Kleene 三值逻辑以及尾递归循环都被下推为张量运算；其中 Kleene 连接词被表示为拉格朗日插值得到的多项式，并在 {-1, 0, +1} 真值网格上精确成立。验证有两个方面。(1) 同一程序在四种冻结嵌入上运行，这四种嵌入覆盖两种模态——三个文本编码器（nomic-embed-text、all-minilm、mxbai-embed-large）和一个蛋白质语言模型（ESM-2）——并在所有基底上、宽度 k=8 的条件下，以 100% 的准确率解码 bundle，而教科书式 Hadamard 积在这些基底上已经崩溃（mxbai-embed-large 上 2.5%，all-minilm 上 7.5%）。(2) PyTorch autograd 能够穿过实际编译出来的图：一个写在 .su 中的模糊规则分类器可以从随机初始化（18.7±9.5%；chance = 20%，5 类）训练到 100.0±0.0%（3 个随机种子），而无需修改符号源，只需对发射出的图进行反向传播。一个加权变体还会训练一个标量余弦增益，并将其写回 .su 源代码中的数值字面量；重新编译后可将训练后的行为复现到每个 logit 约 2e-7 的精度，因此训练得到的模型本身就是可读、可重新编译的代码。由此，同一工件既是逻辑程序，也是可训练的神经网络。

系统软件与软件工程实践

Software Product Line Engineering: Adoption, Tooling and AI Era Challenges

• • 作者：Najam Nazar
• • arXiv URL：https://arxiv.org/abs/2605.21353v1

Abstract

软件产品线工程（SPLE）使得在一组相关软件密集型系统中能够系统化复用。本文综述了 SPLE 的核心基础、生命周期概念、采纳模型、工具支持以及 AI 时代的挑战。基于结构化文献回顾，我们比较了主要的采纳与评估模型，包括 BAPO、FEF、PuLSE、SIMPLE、COPLIMO、PROMOTE-PL 和 APPLIES。我们还梳理了 SPLE 研究从领域工程基础到 AI 辅助变异性管理的历史演进。本文进一步考察了工具互操作性、基于 UVL 的标准化、SME 采纳、从 clone-and-own 开发向迁移、面向变异性的 DevOps、实证证据缺口以及 AI 辅助 SPLE 的保障挑战。本文通过整合当代 SPLE 中的开放问题和未来研究方向，为软件工程与 ICT 研究者提供了一份紧凑的研究议程。

RSE of a Quantum Transport Code and its Effects

• • 作者：Christoph Conrads, Edoardo Di Napoli
• • arXiv URL：https://arxiv.org/abs/2605.21334v1

Abstract

本文报告了我们在过去两年中围绕量子输运代码 libNEGF 的研究软件工程（RSE）经验。我们描述了代码质量保障的实践方法，包括持续集成、自动化测试与编译器警告修正，以及通过持续基准测试进行的性能工程。我们系统性地应用这些实践后，暴露出若干关键缺陷：未初始化内存读取、越界写入，以及一个尤其重要的、对边界条件处理中的数学模型理解错误。我们还记录了持续基准测试如何揭示由于 HPC 系统配置变化而导致的性能回退。我们的结果提供了证据，说明一种危险的缺陷类别，即在 C/C++ 中等同于未定义行为、在 Fortran 中等同于依赖处理器行为的缺陷，其在 Fortran 科学代码中的普遍性与其他语言并无二致。尽管 libNEGF 以 Fortran 实现，大多数建议都适用于任何实现语言的科学软件，并且可以按需选择性地、或完整地应用于新项目与现有项目。

Transforming Privacy Artifacts into Accessible Reports for Non-Technical Stakeholders

• • 作者：Zoe Pfister, Clemens Sauerwein, Benedikt Dornauer, Tina Mersch, Christian Wolf, Ruth Breu, Michael Vierhauser
• • arXiv URL：https://arxiv.org/abs/2605.21269v1

Abstract

向工业 5.0 的过渡正在重塑工业工作环境，强调以人为中心，促进人机协作以提升生产率与灵活性。然而，这类系统通常需要监测人类工人和操作员，往往涉及敏感数据，从而引发严重的隐私担忧。因此，受影响的工人和工会经常因缺乏对隐私威胁及其缓解策略的透明认识，而拒绝人机协作功能。为尽早让利益相关方参与、建立信任并支持知情决策，隐私影响必须以非技术利益相关方也能理解的方式进行沟通。然而，现有需求工程（RE）实践对如何使隐私威胁和缓解措施对非技术利益相关方（例如单个工人或其代表工会）可理解，提供的方法支持十分有限。在这篇 RE@Next 论文中，我们提出一个概念框架，用于指导软件设计从与人类监测相关的用例和需求出发，生成面向非技术利益相关方的知情决策指导。该框架以隐私保护设计等原则为基础，利用大语言模型将技术工件转化为易于理解的隐私报告。我们分享了来自两个工业用例的初步见解，评估了生成报告的质量，并展望了将隐私透明性整合进面向人本工业系统的需求工程过程的未来研究方向。

ParaCell: Paravirtualized Secure Containers with Lightweight Intra-Container Isolation and Intent-Driven Memory Management

• • 作者：Yiyang Wu, Xunjie Wang, Jinyu Gu, Haibo Chen
• • arXiv URL：https://arxiv.org/abs/2605.20906v1

Abstract

安全容器通过为每个容器配备独立内核来隔离容器，从而缓解传统容器系统中普遍存在的共享内核攻击。然而，现有设计仍然面临根本性的隔离-性能权衡。嵌套云部署会放大 VM 退出和页表管理的开销，而新兴的智能体工作负载则表现出突发性的内存需求，需要更细粒度的弹性。我们将这一权衡归因于两个根本原因。首先，现有设计缺乏用于频繁容器用户-内核转换的轻量级容器内隔离原语。其次，宿主机将容器内存管理视为黑盒，迫使系统采用反应式的次级缺页异常和粗粒度的大页映射来摊销其成本。本文基于两个洞察提出 ParaCell，这是一种半虚拟化安全容器运行时。首先，地址空间内的硬件保护原语可以提供轻量级的容器内隔离。ParaCell 使用基于 MPK 的 XGates，在单一地址空间内隔离容器用户态和容器内核态，把频繁的用户-内核转换变成直接的域切换。其次，容器内核分配器本身已经编码了内存管理意图。ParaCell 引入 Pager，在分配和释放事件上进行拦截，批量主动建立和解除 GPA 到 HPA 的绑定，避免反应式的影子页表缺页，同时保持细粒度内存弹性。ParaCell 以 RunV 的直接替代品形式实现。我们的实验表明，在传统云工作负载和新兴智能体应用上，ParaCell 相比 PVM 在裸机和嵌套环境中分别将延迟最多降低 57% 和 79%，相比 RunV 分别降低 33% 和 88%。在智能体工作负载上，ParaCell 相比最先进的 VM 内存回收技术 HyperAlloc 最多节省 35.6% 的内存。