夜雨聆风目录
智能体软件工程与开发基础设施
• : A Typed Lambda Calculus for LLM Agent Composition • CodeTracer: Towards Traceable Agent States • Context Kubernetes: Declarative Orchestration of Enterprise Knowledge for Agentic AI Systems • From Translation to Superset: Benchmark-Driven Evolution of a Production AI Agent from Rust to Python • OOM-RL: Out-of-Money Reinforcement Learning Market-Driven Alignment for LLM-Based Multi-Agent Systems • Evaluating LLM Agents on Automated Software Analysis Tasks • Sema Code: Decoupling AI Coding Agents into Programmable, Embeddable Infrastructure
程序分析、修复与形式化验证
• Enhancing Program Repair with Specification Guidance and Intermediate Behavioral Signals • FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning • DuET: Dual Execution for Test Output Prediction with Generated Code and Pseudocode • AnomalyGen: Enhancing Log-Based Anomaly Detection with Code-Guided Data Augmentation • Ambiguity Detection and Elimination in Automated Executable Process Modeling • Fast Atomicity Monitoring • A Categorical Basis for Robust Program Analysis
软件系统、运维与运行时工程
• ACT: Automated CPS Testing for Open-Source Robotic Platforms • AutonomyLens: A Self-Evolving Simulation-Based Testing Loop for Autonomous Systems • Nanvix: A Multikernel OS Design for High-Density Serverless Deployments • Nix: A Solution With Problems • Using Budgets to Reduce Application Emissions • E2E-REME: Towards End-to-End Microservices Auto-Remediation via Experience-Simulation Reinforcement Fine-Tuning
编程语言、形式语言与编译基础
• Foundations of the GraphAlg Language • Parameterized Algorithms and Complexity for Function Merging with Branch Reordering • Emulation-Completeness of Programming Languages • Minimizing Streaming String Transducers: An algebraic approach
软件工程实践、治理与数字社会
• The Unified Field Theory of Phygital Space • Participation and Power: A Case Study of Using Ecological Momentary Assessment to Engage Adolescents in Academic Research • Beyond the Golden Record: Toward a Design Theory for Trustworthy Master Data Management with Self-Sovereign Identity • Designing Adaptive Digital Nudging Systems with LLM-Driven Reasoning • Taking a Pulse on How Generative AI is Reshaping the Software Engineering Research Landscape • Compliant But Unsatisfactory: The Gap Between Auditing Standards and Practices for Probabilistic Genotyping Software
智能体软件工程与开发基础设施
: A Typed Lambda Calculus for LLM Agent Composition
• 作者：Qin Liu • arXiv URL：https://arxiv.org/abs/2604.11767v1
Abstract
现有 LLM 智能体框架缺乏形式语义：目前没有一种有原则的方法来判断某个智能体配置是否良构，或者其执行是否会终止。我们提出 ，一种用于智能体组合的有类型 lambda 演算，它在简单类型 lambda 演算的基础上扩展了 oracle 调用、有界不动点（即 ReAct 循环）、概率选择以及可变环境。我们证明了类型安全性、有界不动点的终止性，以及由此导出的 lint 规则的健全性，并完成了部分 Coq 机制化（共 1,567 行、43 个已完成证明）。作为实际应用，我们导出了一种 lint 工具，可直接从操作语义中检测结构性配置错误。在 835 个来自 GitHub 的真实智能体配置上的评估表明，按 的标准，其中 94.1% 在结构上并不完整；仅基于 YAML 的 lint 精度为 54%，而在 175 个样本上联合使用 YAML 与 Python AST 分析时，精度提升至 96% 至 100%。这一差距首次量化了智能体生态系统中声明式配置与命令式代码之间语义纠缠的程度。我们进一步表明，五种主流范式（LangGraph、CrewAI、AutoGen、OpenAI SDK、Dify）都可嵌入为带类型的 子片段，从而确立了 作为 LLM 智能体组合统一演算的地位。
CodeTracer: Towards Traceable Agent States
• 作者：Han Li, Yifan Yao, Letian Zhu, Rili Feng, Hongyi Ye, Jiaming Wang, Yancheng He, Pengyu Zou, Lehan Zhang, Xinping Lei, Haoyang Huang, Ken Deng, Ming Sun, Zhaoxiang Zhang, He Ye, Jiaheng Liu • arXiv URL：https://arxiv.org/abs/2604.11641v1
Abstract
代码智能体正在迅速发展，但对其进行调试也正变得越来越困难。随着框架在复杂任务上编排并行工具调用和多阶段工作流，智能体的状态转移与错误传播变得难以观测。在这类运行过程中，早期一步误操作就可能使智能体陷入无效循环，甚至级联为根本性错误，形成隐蔽的错误链，使人难以判断智能体何时偏离轨道以及原因何在。现有智能体追踪分析要么仅关注简单交互，要么依赖小规模人工检查，因而限制了其在真实编码工作流中的可扩展性和实用性。我们提出 CodeTracer，一种追踪架构，能够通过不断演化的提取器解析异构运行产物，将完整的状态转移历史重建为带持久记忆的层次化追踪树，并执行失败起点定位，以精确指出失败源头及其下游链条。为支持系统评估，我们构建了 CodeTraceBench，它来源于四种广泛使用的代码智能体框架在多样化代码任务（如缺陷修复、重构与终端交互）上生成的大规模已执行轨迹集合，并在阶段级和步骤级都提供失败定位监督。实验表明，CodeTracer 明显优于直接提示和轻量级基线；在相同预算下回放其诊断信号，还能持续恢复原本失败的运行。我们的代码和数据已公开。
Context Kubernetes: Declarative Orchestration of Enterprise Knowledge for Agentic AI Systems
• 作者：Charafeddine Mouzouni • arXiv URL：https://arxiv.org/abs/2604.11623v1
Abstract
我们提出 Context Kubernetes，这是一种面向智能体 AI 系统的企业知识编排架构，并给出了原型实现和八项实验。其核心观察是：在整个组织范围内，以正确的权限和正确的新鲜度，将正确的知识送达正确的智能体，这一问题在结构上与 Kubernetes 十年前解决的容器编排问题高度类似。我们形式化定义了六个核心抽象、一个基于 YAML 的声明式“知识架构即代码”清单、一个协调循环，以及一个三层的智能体权限模型，其中智能体权限始终是人类权限的严格子集。三项价值实验表明：（1）在缺乏治理时，智能体会在 26.5% 的查询中引用已删除来源的幽灵内容并发生跨域数据泄露；（2）在缺乏新鲜度监控时，过时内容会被静默提供，而引入协调机制后，可在 1 毫秒内检测到陈旧性；（3）在五种攻击场景中，平坦权限模型拦截 0/5，基础 RBAC 拦截 4/5，而三层模型拦截 5/5。另有五项正确性实验确认：不存在未授权投递，不存在不变量违反，并且实现了当前调研中的企业平台均未提供的、对带外审批通道的架构级隔离。我们对微软、Salesforce、AWS 与 Google 四大平台的调研显示，没有任何一家在架构层面隔离智能体审批通道。我们进一步识别出四项使上下文编排比容器编排更困难的性质，并论证这些性质也让该问题的解决更具价值。
From Translation to Superset: Benchmark-Driven Evolution of a Production AI Agent from Rust to Python
• 作者：Jinhua Wang, Biswa Sengupta • arXiv URL：https://arxiv.org/abs/2604.11518v1
Abstract
大型软件系统的跨语言迁移是一项长期存在的工程挑战，尤其当源代码库快速演化时更是如此。我们提出一种基于 LLM 的持续代码翻译方法：由大语言模型将一个生产级 Rust 代码库（64.8 万行代码，65 个 crate）翻译为 Python（4.1 万行代码，28 个模块），并以公开智能体基准作为目标函数驱动迭代改进。研究对象为生产级 AI 编码智能体 Codex CLI。我们表明：（1）Python 版本在 SWE-bench Verified 上解决了 80 个任务中的 59 个（73.8%），而 Rust 版本为 56/80（70.0%）；在 Terminal-Bench 上取得 42.5%，而 Rust 版本为 47.5%，说明其在真实智能体任务上达到近似等价；（2）以基准驱动的调试比仅依赖静态测试更有效，它暴露了 API 协议不匹配、环境污染、静默 WebSocket 失效模式以及 API 400 崩溃等问题；（3）该架构支持通过 LLM 辅助的“差异-翻译-测试”循环，持续与上游保持同步；（4）Python 版本已经演化为一个能力超集，包含 Rust 中不存在的 30 个特性开关扩展（如多智能体编排、语义记忆、guardian 安全与成本跟踪），同时保留了严格对齐模式用于比较。评估表明，对于 API 延迟占主导的 LLM 智能体而言，Python 的表达能力以几乎可忽略的性能代价实现了 15.9 倍的代码压缩；而“以基准为目标函数”的方法为跨语言移植从等价实现走向扩展平台提供了一个有原则的框架。
OOM-RL: Out-of-Money Reinforcement Learning Market-Driven Alignment for LLM-Based Multi-Agent Systems
• 作者：Kun Liu, Liqun Chen • arXiv URL：https://arxiv.org/abs/2604.11477v1
Abstract
面向自主软件工程的多智能体系统（MAS）对齐，受到评估器认知不确定性的限制。当前范式，如基于人类反馈的强化学习（RLHF）和基于 AI 反馈的强化学习（RLAIF），往往会诱导模型谄媚行为；而基于执行的环境又会遭受不受约束智能体实施的“测试规避”攻击。本文提出一种客观的对齐范式：Out-of-Money Reinforcement Learning（OOM-RL）。通过将智能体部署到实时金融市场这一非平稳、高摩擦的现实环境中，我们把资本耗尽这一不可规避的后果作为不可被作弊的负梯度。在一项持续 20 个月（2024 年 7 月至 2026 年 2 月）的纵向实证研究中，我们记录了系统如何从高换手、带有谄媚倾向的基线，演化为稳健且具备流动性感知能力的架构。我们表明，金融亏损这一不可否认的本体性后果，迫使 MAS 放弃过拟合式幻觉，转而采用严格测试驱动的智能体工作流（STDAW）；该工作流施加了一种受拜占庭思想启发的单向状态锁（RO-Lock），并锚定在一个经确定性验证、代码覆盖率不低于 95% 的约束矩阵上。结果显示，尽管早期迭代经历了严重的执行退化，最终经 OOM-RL 对齐的系统在成熟阶段实现了年化 Sharpe 比率 2.06 的稳定平衡。我们据此认为，以严格的经济惩罚替代主观人类偏好，可以为高风险真实环境中的自主智能体对齐提供一种稳健方法，并为更一般的范式奠定基础，在这些范式中，计算计费也可作为客观的物理约束。
Evaluating LLM Agents on Automated Software Analysis Tasks
• 作者：Michael Pradel, Cristian Cadar, Islem Bouzenia • arXiv URL：https://arxiv.org/abs/2604.11270v1
Abstract
如今已经存在大量软件分析工具，但将其应用到多样化开源项目上仍然困难重重，原因包括环境搭建、依赖解析和工具配置等。基于 LLM 的智能体提供了一种潜在解决方案，但此前尚无工作系统研究其在自动化软件分析这一特定任务上的有效性。与问题修复或一般环境配置不同，这一任务要求同时安装和配置独立的分析工具及目标项目，生成工具特定的先决条件，并验证工具是否产生有意义的分析输出。我们提出 AnalysisBench，这是一项包含 35 个“工具-项目”对的基准，覆盖 7 种分析工具和 10 个多样化的 C/C 与 Java 项目，并为每个任务手工构建了参考配置。基于 AnalysisBench，我们在 4 种 LLM 后端上评估了 4 种智能体架构。我们定制的 AnalysisAgent 在人工验证下达到 94% 的成功率（Gemini-3-Flash，35 个任务中成功 33 个），而最佳基线 ExecutionAgent 为 77%。除定量结果外，我们还识别出当前智能体的关键局限，包括阶段混淆、错误定位能力差以及过早终止，并表明智能体架构的重要性高于 LLM 能力本身。我们进一步发现，整程序分析和符号执行是最困难的任务，Java 工具链比 C/C 更具挑战，而由 LLM 自行验证的成功率会持续高估人工验证的真实成功率。
Sema Code: Decoupling AI Coding Agents into Programmable, Embeddable Infrastructure
• 作者：Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Feiyu Chen, Jiarou Wu, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, Yi Xu • arXiv URL：https://arxiv.org/abs/2604.11045v1
Abstract
AI 编码智能体已经成为开发者工作流的核心组成部分，但现有每一种方案都将其推理能力锁定在某种特定交付形态中，例如 CLI、IDE 插件或 Web 应用。这种限制在企业尝试跨异构工程环境复用这些能力时形成了系统性障碍。为解决这一问题，我们提出 Sema Code，这是一种开放的 AI 编码框架，其设计原则是可嵌入、可插拔，并以框架优先为核心。Sema Code 将核心智能体引擎与所有客户端层彻底解耦，并将其发布为一个独立的 npm 库，使任何运行时都可以通过编程方式驱动它。围绕这一架构，我们设计了八项关键机制：多租户引擎隔离、带安全会话重建的 FIFO 输入队列、自适应上下文压缩、多智能体协作调度、基于 Todo 的智能流程管理、四层异步权限控制、涵盖 MCP、Skills 与 Plugins 的三层生态集成，以及一种将执行权限与观测权限分离的后台任务框架。这些机制共同应对了将复杂智能体引擎转化为共享可编程核心时所面临的工程挑战。为了展示其架构通用性，同一个 Sema Core 引擎同时驱动了一个 VSCode 扩展和一个多通道消息网关 SemaClaw，用以统一 Telegram 和 Feishu 等平台上的智能体交互。这代表了两种根本不同的产品形态共享同一推理内核，仅在客户端层有所区别。
程序分析、修复与形式化验证
Enhancing Program Repair with Specification Guidance and Intermediate Behavioral Signals
• 作者：Minh Le-Anh, Cuong Chi Le, Tien N. Nguyen • arXiv URL：https://arxiv.org/abs/2604.11770v1
Abstract
自动程序修复（APR）近年来已从大语言模型（LLM）中显著受益。然而，大多数基于 LLM 的 APR 方法仍主要依赖测试套件结果这类粗粒度的端到端信号来指导修复，因此难以揭示程序内部逻辑究竟在何处偏离了预期行为。相比之下，人类调试通常会借助局部正确性条件或断言，对程序状态进行中间层次的推理。受此启发，我们提出 SpecTune，这是一种由规格引导的调试框架，可将中间行为推理纳入 APR 过程。SpecTune 将修复任务分解为由执行检查点连接的可疑区域，并在这些位置推导表示期望程序行为的局部后置条件。通过执行缺陷程序并评估这些后置条件，SpecTune 产生微观层面的调试信号，用以指示观测行为与预期行为之间的不匹配，从而实现更精确的故障定位和更有针对性的补丁生成。为应对 LLM 生成后置条件可能不可靠的问题，我们引入两种互补信号：规格验证信号 alpha，用于借助部分通过的测试用例估计所生成后置条件的一致性；以及判别信号 beta，用于在执行过程中检测经验证后置条件的违反情况。借助这两类信号，SpecTune 能够在 APR 中安全地利用自动生成的规格。实验结果表明，SpecTune 在故障定位和 APR 效果上均优于基线方法。
FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning
• 作者：Haoran Ding, Zhaoguo Wang, Haibo Chen • arXiv URL：https://arxiv.org/abs/2604.11556v1
Abstract
LLM 辅助的软件开发日益普及，甚至能够生成编译器等大规模系统，因此增强生成代码的正确性变得至关重要。然而，由于代码复杂，大规模系统的自动推理仍极具挑战。Hoare 逻辑提供了一种将大系统分解为较小组件并分别推理的方法，即组合式推理。但现有工作仍难以扩展，因为 Hoare 逻辑要求为每个函数编写形式规格，给人类带来了沉重负担。对于由 LLM 生成的代码，这一问题更为严重，因为开发者通常并不深入理解每个函数的预期行为。本文提出 FM-Agent，这是首个实现面向大规模系统自动组合式推理的框架。借助 LLM，FM-Agent 引入一种自顶向下范式，自动生成函数级规格。具体而言，FM-Agent 从调用者对某函数行为的期望中推导该函数的规格，因此即使实现存在缺陷，生成的规格仍能反映开发者意图。开发者意图通常以自然语言表达，而现有验证器只支持公式，因此 FM-Agent 将 Hoare 风格推理推广到可针对自然语言规格进行推理。最后，为了确认缺陷存在并解释其成因，FM-Agent 还能自动生成测试用例以触发潜在缺陷。在评估中，FM-Agent 能在 2 天内完成对大规模系统的推理，每个系统规模最高达 14.3 万行代码。尽管这些系统已经由开发者测试过，FM-Agent 仍新发现了 522 个缺陷，这些缺陷可能导致系统崩溃和错误执行结果等严重后果。
DuET: Dual Execution for Test Output Prediction with Generated Code and Pseudocode
• 作者：Hojae Han, Jaejin Kim, Seung-won Hwang, Yu Jin Kim, Moontae Lee • arXiv URL：https://arxiv.org/abs/2604.11514v1
Abstract
本文研究测试输出预测这一测试用例生成中的关键挑战。为了提高 LLM 所预测输出的可靠性，已有方法通常先生成代码，再以此作为预测依据。其中一种依据方式是直接执行生成的代码，但即便是轻微错误也可能导致执行失败。为此，我们引入基于 LLM 的伪代码执行方法，它通过更具容错性的伪代码来提供支撑，并借助 LLM 推理模拟执行过程。在此基础上，我们进一步提出 DuET，一种双执行框架，将直接代码执行与伪代码执行结合，并通过功能层面的多数投票作出预测。我们的分析表明，这两种方法具有互补性：前者易受代码错误影响，后者则容易受到幻觉干扰，而双执行能够同时缓解这两类局限。在 LiveCodeBench 上，DuET 取得了当前最优性能，使 Pass@1 提升了 13.6 个百分点。
AnomalyGen: Enhancing Log-Based Anomaly Detection with Code-Guided Data Augmentation
• 作者：Xinyu Li, Yintong Huo, Chenxi Mao, Shiwen Shan, Yuxin Su, Yanlin Wang, Zibin Zheng • arXiv URL：https://arxiv.org/abs/2604.11107v1
Abstract
基于日志的异常检测从根本上受限于训练数据稀疏性。我们的实证研究表明，公共基准数据集覆盖的源代码日志模板不到 10%。因此，模型常常把未见过但实际上有效的执行路径误判为异常，导致大量误报。为解决这一问题，我们提出 AnomalyGen，这是一种通过源代码合成带标签日志序列来增强训练数据的新框架。AnomalyGen 将面向日志的静态分析与大语言模型推理结合起来，分为三个阶段：（1）构建面向日志的控制流图（LCFG），枚举结构上有效的执行路径；（2）利用 LLM 的链式思维（CoT）推理验证逻辑一致性，并生成真实的运行时参数，如块编号和 IP 地址；（3）用领域启发式规则为生成序列打标签。在 HDFS 和 Zookeeper 上对 12 种不同异常检测模型的评估表明，AnomalyGen 能稳定提升性能。深度学习模型的平均 F1 分数分别提高了 2.18%（HDFS）和 1.69%（Zookeeper）；其中 HDFS 上的一个无监督 Transformer 从 0.818 提升到 0.970。消融实验表明，静态分析与基于 LLM 的验证二者都不可或缺：去掉它们会分别使 F1 最多下降 8.7 和 10.7 个百分点。我们的框架和数据集已公开，以促进后续研究。
Ambiguity Detection and Elimination in Automated Executable Process Modeling
• 作者：Ion Matei, Praveen Kumar Menaka Sekar, Maksym Zhenirovskyy, Hon Yung Wong, Sayuri Kohmura, Shinji Hotta, Akihiro Inomata • arXiv URL：https://arxiv.org/abs/2604.10884v1
Abstract
大语言模型正越来越多地被用于从自然语言规格自动生成可执行的 BPMN（业务流程模型与标注）模型。然而，含糊或规格不足的文本可能生成结构上有效但仿真行为不同的模型。我们的目标并非证明某个生成的 BPMN 模型在语义上正确，而是检测某段自然语言规格在多次生成与仿真下，是否无法支持稳定的可执行解释。我们提出一种由诊断驱动的框架：通过关键性能指标（KPI）的经验分布检测行为不一致；借助基于模型的诊断将分歧定位到网关逻辑；再将该逻辑映射回原始叙述中的逐字片段；最后通过基于证据的细化修复源文本。针对糖尿病肾病健康指导政策的实验表明，该方法能够降低重新生成模型行为的波动性。结果表明，在缺乏真实 BPMN 金标准模型的情况下，这是一种用于验证和修复可执行流程规格的闭环方法。
Fast Atomicity Monitoring
• 作者：Hünkar Can Tun, Yifan Dong, Andreas Pavlogiannis • arXiv URL：https://arxiv.org/abs/2604.11369v1
Abstract
原子性是并发中的一个基本抽象，它要求程序行为可以通过将特定代码块视为原子执行来理解。然而，在优化代码效率的同时维持原子性不变量并不容易，原子性违例也是许多并发缺陷的常见根源。为了解决这一问题，已经出现了多种动态技术，用于测试程序执行是否满足某种原子性规格，通常实例化为冲突可串行化。分析效率一直是该方向的重点，当前最先进的算法 RegionTrack 和 Aerodrome 在包含 n 个事件、k 个线程、v 个位置和 ℓ 个锁的执行轨迹 σ 上，时间复杂度分别达到 O(nk^3) 和 O(nk(k + v + ℓ))。本文提出 AtomSanitizer，这是一种新的冲突可串行化测试算法，时间复杂度为 O(nk^2)。AtomSanitizer 以高效的流式方式运行，在理论上比所有现有算法更快，且内存占用也更小。此外，AtomSanitizer 还是首个在并发监控场景中以最小锁开销为目标设计的算法。标准基准上的实验表明，AtomSanitizer 在实践中始终快于所有现有冲突可串行化测试器。最后，我们还将 AtomSanitizer 集成到 TSAN 框架中，以实时监控原子性。实验显示，与 TSAN 的数据竞争检测引擎相比，AtomSanitizer 仅带来极小的时间和空间开销，因此是首个被证明适用于运行时监控场景的冲突可串行化算法。
A Categorical Basis for Robust Program Analysis
• 作者：Zachary Kincaid, Shaowei Zhu • arXiv URL：https://arxiv.org/abs/2604.11029v1
Abstract
程序分析的用户通常期望：当程序发生变化时，分析结果也应以可预测的方式变化，但许多分析方法并不具备这种鲁棒性。本文提出一个理论框架，为表述鲁棒性属性提供统一语言。通过将程序及其性质建模为某个范畴中的对象，诸如变量重命名、语义精化和结构变换等不同形式的鲁棒性，都可以被刻画为保持结构的函子。除阐明鲁棒性的含义之外，本文还给出了实现鲁棒性的两种方法。第一种是一条通用设计路线：将一个在受限（次图灵）计算模型上既健全又鲁棒的分析，提升为面向一般程序的健全且鲁棒的分析。该路线揭示了若干现有循环摘要与终止性分析实际上都是这一通用方案的实例，并进一步澄清了它们的鲁棒性性质。第二种方法则刻画了代数程序分析在何种意义上是鲁棒的：只要其由鲁棒算子构成，整个分析便是鲁棒的。特别地，我们证明，这类分析在常见重构模式（如变量重命名和循环展开）下会呈现可预测行为。
软件系统、运维与运行时工程
ACT: Automated CPS Testing for Open-Source Robotic Platforms
• 作者：Aditya A. Krishnan, Donghoon Kim, Hokeun Kim • arXiv URL：https://arxiv.org/abs/2604.11708v1
Abstract
面向信息物理系统（CPS）的开源软件往往缺乏结合真实机器人平台的稳健测试，导致关键错误长期无法被发现。当 CPS 软件的多个模块由不同开源贡献者共同开发时，这一问题尤为突出。为弥补这一缺口，我们提出 Automated CPS Testing（ACT），它能够结合机器人平台，对开源软件执行自动化、持续化测试，并与 GitHub 等开源基础设施集成。我们实现了 ACT 原型，并在一个使用教学机器人平台的开源 CPS 上开展案例研究，以展示其能力。
AutonomyLens: A Self-Evolving Simulation-Based Testing Loop for Autonomous Systems
• 作者：Ankit Agrawal, Jithin Garapati, Bohan Zhang • arXiv URL：https://arxiv.org/abs/2604.11672v1
Abstract
用于验证自主信息物理系统（例如无人机）的软件工程实践，当前仍分散在场景设计、仿真执行和遥测分析等环节之间，限制了需求、测试与证据之间的可追溯性。这种碎片化削弱了可复现性，拖慢了调试与迭代过程，并阻碍了在复杂且不断变化的环境条件下开展系统性保障。我们提出 AutonomyLens，这是一个由 LLM 驱动的框架，可将场景规格、仿真执行和遥测分析整合为统一的验证工作流。AutonomyLens 使开发者能够将高层验证意图转化为可执行、随时间演化的场景，自动运行仿真，并对产生的系统行为执行具备上下文感知能力的分析。该框架引入了：（1）面向任务级场景的结构化表示；（2）自动化执行流水线；（3）将遥测数据与场景上下文对齐以生成可操作洞见的分析机制；以及（4）反事实场景生成，通过根据观测到的失败来细化并合成新测试用例，从而闭合整个循环。我们描述了 AutonomyLens 的早期设计，讨论了构建自主系统集成验证工作流的关键挑战，并概述了此类方法如何提升自主性验证中的可追溯性、可复现性和可扩展性。
Nanvix: A Multikernel OS Design for High-Density Serverless Deployments
• 作者：Carlos Segarra, Pedro Henrique Penna, Enrique Saurez, Íñigo Goiri, Peter Pietzuch, Shan Lu, Rodrigo Fonseca • arXiv URL：https://arxiv.org/abs/2604.11669v1
Abstract
无服务器计算提供商致力于通过优化部署密度来提高资源利用率，即在每台宿主服务器上部署尽可能多的应用。然而，如何在不损害应用性能和隔离性的前提下实现高部署密度，仍是一个开放挑战。通过跨应用共享组件可以提高密度，但由于侧信道攻击风险，不同租户的应用必须被强隔离。对于同一租户的应用，如果共享做法过于直接，又可能在宿主资源上引入争用，从而损害应用性能。我们介绍 Nanvix，这是一种新的多内核操作系统，它将每次应用调用独有的短暂执行状态，与同一租户不同调用之间共享的长期持久状态进行解耦。在 Nanvix 中，应用运行于轻量级用户虚拟机内，其中的微内核实现线程和内存管理，并将所有 I/O 请求转发给系统虚拟机；系统虚拟机运行具备丰富设备驱动的宏内核，并由同一租户的所有调用共享。Nanvix 的拆分式设计在不牺牲应用性能的情况下，实现了跨租户的强 hypervisor 级隔离，并通过将所有 I/O 请求复用到系统虚拟机来减少同租户争用。得益于全系统协同设计，Nanvix 在仅付出适度 I/O 开销的前提下，将应用启动时间降低了一个数量级。当回放生产环境轨迹时，与现有最先进系统相比，Nanvix 需要的宿主服务器数量减少了 20 至 100 倍，从而显著提升了部署密度。
Nix: A Solution With Problems
• 作者：Matias Zwinger • arXiv URL：https://arxiv.org/abs/2604.11398v1
Abstract
软件部署长期面临诸多问题，例如可复现性和依赖解析。Nix 项目中实现的纯函数式包管理方法已经成功解决了其中不少难题。然而，Nix 并未解决所有问题，而且它本身也引入了一些新的问题。因此，本文旨在通过文献综述梳理当前关于 Nix 的研究现状，并确定未来研究方向。论文第一部分回顾了软件部署不同领域中历史上面临的问题，例如不可复现性和依赖解析困难，并以构建系统、包管理器、配置管理和开发环境这四类软件部署工具为主线，结合各类代表性软件作为案例进行说明。第二部分介绍了 Nix，并解释其用于解决前述部分问题的方法。由于 Nix 是首个大规模采用纯函数式方法的项目，它远非完美解决方案。因此，第三部分专门分析 Nix 引入的新问题，以及其尚未解决的旧问题，例如信任问题和细粒度增量构建问题。此外，论文还讨论了 Nix 社区提出的一些当前最先进的解决思路。
Using Budgets to Reduce Application Emissions
• 作者：Leo Wilhelm Lierse, Mahyar Tourchi Moghaddam, Sebastian Werner • arXiv URL：https://arxiv.org/abs/2604.11341v1
Abstract
随着欧盟排放交易体系等碳定价机制逐步推高能源消耗成本，软件架构师面临越来越大的压力，需要设计能够在财务上可预测的排放约束内运行的应用。现有方法通常采用刚性的单位时间排放率约束，但在碳强度高度动态变化的电网中，这种方式并不适用，而这在可再生能源占比持续提升的电网中相当常见。我们提出“排放预算”的概念，用在时间范围内约束累计预算来替代固定排放率，使应用能够在低碳强度时段保存未使用的排放额度，并在高碳强度时段加以使用。我们采用 MAPE-K 反馈回路描述排放感知型应用：持续监测应用功耗与电网碳强度，并通过垂直扩缩容或迁移来调整资源分配，以在维持长期排放上限的同时最大化性能。基于德国、法国和波兰六周真实碳强度数据的仿真表明，与固定排放率相比，基于预算的管理在波动性电网中可将任务完成率提高最多 36%。关键的是，在稳定电网中，预算方法与固定排放率表现持平，因此可作为一种安全替代方案。我们表明，当排放会直接转化为财务惩罚时，排放预算是平衡环境约束、运营成本和服务质量的实用机制。
E2E-REME: Towards End-to-End Microservices Auto-Remediation via Experience-Simulation Reinforcement Fine-Tuning
• 作者：Lingzhe Zhang, Yunpeng Zhai, Tong Jia, Minghua He, Chiming Duan, Zhaoyang Liu, Bolin Ding, Ying Li • arXiv URL：https://arxiv.org/abs/2604.11094v1
Abstract
当代微服务系统持续在规模和复杂性上增长，导致故障发生得更频繁、代价也更高。尽管近期出现了基于 LLM 的自动修复方法，但这些方法主要是把文本指令翻译为可执行的 Ansible playbook，并依赖专家手工设计的提示，既缺乏运行时知识引导，又依赖大规模通用 LLM，从而限制了准确性和效率。我们提出 End-to-End Microservice Remediation（E2E-MR）这一新任务：要求系统能够直接根据诊断报告生成可执行 playbook，以自主恢复故障系统。为实现严格评估，我们构建了 MicroRemed 基准，它自动完成微服务部署、故障注入、playbook 执行以及修复后的验证。进一步地，我们提出 E2E-REME，这是一种通过“经验-仿真”强化微调训练的端到端自动修复模型。在公共和工业微服务平台上的实验，并与 9 个代表性 LLM 对比后表明，E2E-REME 在准确性和效率上都具有优势。
编程语言、形式语言与编译基础
Foundations of the GraphAlg Language
• 作者：Daan de Graaf, Robert Brijder, Nikolay Yakovets • arXiv URL：https://arxiv.org/abs/2604.11454v1
Abstract
面向图算法的领域特定语言 GraphAlg 使用户能够在图数据库中定义自定义算法。本文展示了 GraphAlg 如何建立在用于矩阵操作的形式语言 MATLANG 之上。我们从 MATLANG 出发，说明为导出 GraphAlg Core 所需的扩展；GraphAlg Core 是 GraphAlg 的一个简化版本，并作为 GraphAlg 编译器中的内部表示。此外，我们证明任意 GraphAlg Core 表达式都可以在支持同步归纳的 for-MATLANG 扩展中得到模拟。
Parameterized Algorithms and Complexity for Function Merging with Branch Reordering
• 作者：Amir K. Goharshady, Kerim Kochekov, Tian Shu, Ahmed Khaled Zaher • arXiv URL：https://arxiv.org/abs/2604.11027v1
Abstract
缩减二进制大小正成为编译器越来越重要的优化目标。一项新兴技术是函数合并：将多个相似函数合并为一个，从而消除冗余。当前最先进的方法基于序列对齐，将函数视为线性的指令序列，并寻找使对齐程度最大的匹配方式。本文考虑该问题的一个显著推广版本：允许在每个函数内部对分支进行重排，从而实现更灵活的匹配与更优的合并。我们证明，这一推广会使问题变为 NP-难，因此转而从参数化算法与复杂性角度研究它，识别出支配其复杂性的若干输入参数。我们重点考察两个自然参数：输入函数的分支因子和嵌套深度。具体来说，输入由两个函数 F1 与 F2 组成，其中每个 Fi 的规模为 ni、分支因子为 bi、嵌套深度为 di。任务是对 F1 和 F2 的分支进行重排，使所得线性化达到最大序列对齐。令 n=max(n1,n2)，并类似定义 b 与 d。我们的结果如下：第一，存在一个时间复杂度为 2^{O(bd)} n^2 的简单算法，表明该问题关于全部四个参数 b1、d1、b2、d2 是固定参数可解的；第二，存在一个时间复杂度为 2^{O(bd2)} n^7 的算法，说明即使其中一个函数的嵌套深度无界，该问题仍属于 FPT；第三，我们给出一个硬性结果，表明即便将 d1、b2、d2 限制为常数，该问题仍然是 NP-难的。据我们所知，这是首次从算法或复杂性理论角度，对带分支重排的函数合并进行系统研究。
Emulation-Completeness of Programming Languages
• 作者：Gregory Morse, Tamás Kozsik • arXiv URL：https://arxiv.org/abs/2604.11021v1
Abstract
我们研究一种编程语言是否能够在不把被模拟程序重新委托给宿主求值器或编译器的情况下，模拟用该语言本身编写的程序。我们将这一性质称为“模拟完备性”（emulation-completeness）。核心观察是，仅具备图灵完备性并不足够：一个自模拟器不仅要计算出宾客程序的结果，还必须处理现实程序所依赖的、对宾客可见的状态，包括控制流、异常、回调、时序、内存使用以及栈轨迹或行号等运行时元数据。本文是一篇系统化论文，其贡献不在于提出新的模拟器实现，而在于建立一套精确术语与结构化分类体系，以便推理自模拟问题。我们区分源代码级求值与编译代码级模拟，定义语法层面和编译代码层面的模拟完备性，并根据需要保留多少可观测运行时行为，将其划分为弱模拟完备性与强模拟完备性。随后，我们将要求整理为两类：语言侧要求，用于决定宾客语义能否在该语言内部被显式表示；以及模拟器侧要求，用于决定所得模拟器能否忠实地屏蔽或再现相关观测。讨论通过具体实例加以支撑，包括 Erlang 的公开文档细节，其中参数上限、位串模式匹配与消息接收等机制揭示了直接执行与自模拟之间的微妙不一致。我们希望该框架能为语言设计者、求值器与模拟器实现者，以及研究安全沙箱、反编译和反射执行的研究者提供指导。
Minimizing Streaming String Transducers: An algebraic approach
• 作者：Yahia Idriss Benalioua, Nathan Lhote, Pierre-Alain Reynier • arXiv URL：https://arxiv.org/abs/2604.11567v1
Abstract
本文研究如何对以追加式流字符串转换器（aSST）表示的有理函数进行最小化。我们借助这些函数的一种代数表示，即 bimachine，来同时处理 aSST 的状态最小化与寄存器最小化。首先，我们证明了某个 aSST 子类与 bimachines 之间存在一个双射，该双射将 aSST 的状态数和寄存器数映射到 bimachine 的两个自然参数上。利用已有的 bimachine 最小化结果，我们由此得到：对该 aSST 子类而言，关于寄存器最小化存在一个多项式时间过程，而关于状态与寄存器同时最小化则存在一个 NP 过程。其次，我们引入一种新的 bimachine 模型，称为异步 bimachine，它使得上述双射可以推广到整个 aSST 类。基于此，我们证明：在底层自动机固定的情况下，寄存器最小化问题是 NP-完全的。
软件工程实践、治理与数字社会
The Unified Field Theory of Phygital Space
• 作者：Silvio Meira • arXiv URL：https://arxiv.org/abs/2604.11619v1
Abstract
本文提出“物理-数字融合空间”（Phygital Space）的统一场论，认为当代现实并非“线上”与“线下”的二分，而是由若干不可约但相互耦合的维度组成的统一存在流形。我们将物理维度（U）、网络化数字维度（D）和网络化社会维度（S）构成的拓扑站点上的层定义为物理-数字融合空间，并以“信息性”（即可计算、可通信、可控制三位一体的能力）为基础，通过平台将其具体化。我们进一步构建了一个严格框架，引入 Finsler 几何以刻画跨维交互中天然存在的非对称成本；定义“本体质量” μ 为一个张量量，用于编码跨耦合维度的变化阻力；并引入自创生动力学，以解释个体、算法和社会形态的内生能动性。我们提出一种非平衡热力学模型，将经济价值视为平台作为耗散结构所生成的负熵，并通过李导数形式化“时间剪切”理论，以解释现代时间的病理现象。该理论通过对中国电商生态系统（1999 至 2025）的纵向分析获得经验验证，建模了淘宝、京东、拼多多和抖音在二十五年演化过程中的维度轨迹。我们还将该框架扩展到包含合成智能体的后人类生态，并阐述其对平台治理与人类福祉的规范性含义。
Participation and Power: A Case Study of Using Ecological Momentary Assessment to Engage Adolescents in Academic Research
• 作者：Ozioma C. Oguine, Elmira Rashidi, Pamela J. Wisniewski, Karla Badillo-Urquiola • arXiv URL：https://arxiv.org/abs/2604.11551v1
Abstract
生态瞬时评估（EMA）被广泛用于研究青少年的经历，但 EMA 平台的设计如何塑造青年研究中的参与方式、研究实践和权力关系，仍缺乏充分考察。我们开发了一个以青年为中心的 EMA 平台，优先支持青年参与和研究者工作，并通过一个关于青少年双胞胎、聚焦心理健康与睡眠行为的纵向研究案例对其进行了评估。我们对研究团队进行了访谈，以考察平台设计选择如何影响参与者入组、持续参与、风险监测和数据解释。应用面向青少年的设计与游戏化功能有助于维持青少年参与度，而 Web 门户则通过集中式仪表板简化了行政监督。然而，技术不稳定性和僵化的数据结构带来了显著障碍，既引发了家长的隐私担忧，也使研究者难以分析原始使用元数据。基于此，我们提出了可操作的交互设计指南，用于开发兼顾青年能动性、伦理实践和研究目标的 EMA 平台。
Beyond the Golden Record: Toward a Design Theory for Trustworthy Master Data Management with Self-Sovereign Identity
• 作者：Niklas Schulte, Isaac Henderson Johnson Jeyakumar, Michael Kubach, Christian Janiesch • arXiv URL：https://arxiv.org/abs/2604.11537v1
Abstract
确保主数据的时效性与可靠性，长期以来一直是许多组织面临的持续挑战。为缓解这些质量缺陷，组织往往依赖商业数据经纪商。然而，这种做法会形成战略依赖，并带来显著商业风险，尤其是在供应方通常不对所提供数据的准确性承担责任的情况下。与此相对，现代数据生态系统能够在强数据主权的前提下实现可信的数据资产共享。本文针对这一范式转变，提出了一种基于自主主权身份（SSI）的可信主数据管理初步设计理论。该理论通过解释学文献综述与行业专家访谈获得基础支撑，并被实例化为一种数据空间参考架构中的集成方案。经由进一步的行业专家访谈评估后，我们的工作为数据生态系统中的可信主数据管理提供了一个兼具可靠性、主权性与可追责性的框架。
Designing Adaptive Digital Nudging Systems with LLM-Driven Reasoning
• 作者：Tiziano Santilli, Mina Alipour, Mahyar Tourchi Moghaddam • arXiv URL：https://arxiv.org/abs/2604.11206v1
Abstract
数字助推系统在将行为科学转化为软件设计方面缺乏体系化的架构指导。尽管已有研究识别了助推策略和质量属性，但现有体系结构未能把多维用户建模与伦理合规视为架构层面的核心关注点。我们提出一种架构，通过显式的架构决策将行为理论融入系统设计，并将伦理与公平作为结构性护栏，而不是实现细节。通过文献综述，我们综合得到 68 种助推策略、11 个质量属性和 3 个用户画像维度，并将其转化为架构需求。该架构实现了串行处理层，并通过横切的评估模块来强制执行监管合规。13 位软件架构师的验证表明，该方案满足需求，且可迁移到不同领域。一个面向住宅能源可持续性的、由 LLM 驱动的概念验证系统在 15 位用户中的评估显示，该架构具有可行性，能够获得较高的干预质量感知，并带来可测量的积极情绪影响。该工作通过提供可复用的架构模式，弥合了行为科学与软件架构之间的鸿沟，使自适应系统能够在有效性与伦理约束之间取得平衡。
Taking a Pulse on How Generative AI is Reshaping the Software Engineering Research Landscape
• 作者：Bianca Trinkenreich, Fabio Calefato, Kelly Blincoe, Viggo Tellefsen Wivestad, Antonio Pedro Santos Alves, Júlia Condé Araújo, Marina Condé Araújo, Paolo Tell, Marcos Kalinowski, Thomas Zimmermann, Margaret-Anne Storey • arXiv URL：https://arxiv.org/abs/2604.11184v1
Abstract
背景：软件工程（SE）研究者越来越多地研究生成式 AI（GenAI），同时也将其纳入自身研究实践。尽管采用速度很快，但关于 GenAI 如何被用于 SE 研究以及它对研究实践与治理有何影响的实证证据仍然有限。目标：我们对 2023 至 2025 年间在顶级 venue 发表论文的 457 名 SE 研究者开展了大规模调查。方法：通过定量与定性分析，我们考察了谁在使用 GenAI、为何使用、它被用于哪些研究活动，以及研究者如何看待其收益、机会、挑战、风险与治理问题。结果：GenAI 的使用非常普遍，许多研究者表示感受到采用和使研究与其对齐的压力。其应用主要集中在写作和早期研究阶段，而方法设计与分析任务在很大程度上仍由人类主导。尽管生产率提升被广泛感知，但关于可信性、正确性和监管不确定性的担忧依然存在。研究者强调不准确性与偏见等风险，主张通过人工监督与验证加以缓解，并呼吁建立更明确的治理机制，包括负责任使用指南和同行评审指引。结论：我们对 GenAI 在研究活动中的使用给出了细粒度、面向 SE 的刻画，并提出了 GenAI 在研究和同行评审中的用例、机会、风险、缓解策略与治理需求分类体系。这些发现为将 GenAI 负责任地整合进学术实践提供了一个经验基线。
Compliant But Unsatisfactory: The Gap Between Auditing Standards and Practices for Probabilistic Genotyping Software
• 作者：Angela Jin, Alexander Asemota, Dan E. Krane, Nathaniel D. Adams, Rediet Abebe • arXiv URL：https://arxiv.org/abs/2604.10875v1
Abstract
AI 治理工作日益依赖审计标准，即关于如何开展审计的约定性实践。但如果标准设计不良，它反而会掩盖并赋予不充分系统以表面可信度。我们以 ASB 018 为案例，研究审计标准的设计如何影响其有效性。ASB 018 是一个用于审计概率基因分型软件的标准，而这类软件正日益被美国刑事司法系统用于分析 DNA 样本。通过对 ASB 018 与 5 份审计报告的定性分析，我们识别出该标准期望达成的目标与其实际允许的审计实践之间存在诸多缺口。例如，ASB 018 设想合规审计应根据观察到的失败为软件使用设定边界，但实际上审计即使不建立此类边界也能被判定为合规。我们进一步将这些缺口追溯到标准要求本身的设计问题，如措辞模糊和术语未定义。最后，我们提出了关于如何设计审计标准并评估其有效性的建议。
