夜雨聆风目录
AI 代理、开发工作流与语义控制
• Language-Based Agent Control • AgentLens: Revealing The Lucky Pass Problem in SWE-Agent Evaluation • Protocol-Driven Development: Governing Generated Software Through Invariants and Evidence • TruncProof: A Guardrail for LLM-based JSON Generation under Token-Length Constraints • SWE-Cycle: Benchmarking Code Agents across the Complete Issue Resolution Cycle • Improving Code Translation with Syntax-Guided and Semantic-aware Preference Optimization • SkillOps: Managing LLM Agent Skill Libraries as Self-Maintaining Software Ecosystems • (How) Do Large Language Models Understand High-Level Message Sequence Charts? • Neurosymbolic Auditing of Natural-Language Software Requirements
代码质量、安全与缺陷检测
• Security Incentivization: An Empirical Study of how Micropayments Impact Code Security • Code-Centric Detection of Vulnerability-Fixing Commits: A Unified Benchmark and Empirical Study • Automatic Detection of Reference Counting Bugs in Linux Kernel Drivers • Robust Mutation Analysis of Quantum Programs Under Noise • The Readability Spectrum: Patterns, Issues, and Prompt Effects in LLM-Generated Code • SieveFL: Hierarchical Runtime-Aware Pruning for Scalable LLM-Based Fault Localization
测试、评测与可复现性基础设施
• UIBenchKit: A unified toolkit for design-to-code model evaluation • ReproScore: Separating Readiness from Outcome in Research Software Reproducibility Assessment • AI Harness Engineering: A Runtime Substrate for Foundation-Model Software Agents • Integration of an Agent Model into an Open Simulation Architecture for Scenario-Based Testing of Automated Vehicles • Learning Responsibility-Attributed Adversarial Scenarios for Testing Autonomous Vehicles
形式化验证与程序逻辑
• LFPL: Revisited and Mechanized • Scalable Deductive Verification of Data-Level Parallel Programs • First Steps Towards Probabilistic Iris: Harmonizing Independence, Conditioning, and Dynamic Heap Allocation • On the Complexity of Checking Soundness of Natural Reductions (Extended Version)
自动机与计算理论
• Decoupled Planning for Multiple Omega-Regular Objectives • Universal Design and Physical Applications of Non-Uniform Cellular Automata on Translationally Invariant Lattices • Exact Accepting-State Spectrum for Reversal of Permutation Automata • Liquid Tree Automata
AI 代理、开发工作流与语义控制
Language-Based Agent Control
• 作者：Timothy Zhou, Loris D'Antoni, Nadia Polikarpova • arXiv URL：https://arxiv.org/abs/2605.12863v1
Abstract
本文提出基于语言的代理控制（language-based agent control，LBAC），这是一种面向代理式应用的新编程模型，它将编程语言与基于语言的安全技术引入代理控制问题。在传统编程中，静态类型与运行时强制执行的组合长期以来被用于保证类型正确的程序满足用户指定的策略，包括访问控制、信息流、数据溯源等策略。LBAC 的核心思想，是通过要求代理生成的程序本身在外围支撑代码的上下文中保持类型正确，把这些保证扩展到代理式应用中。任何不安全的程序都会在执行前被类型检查器拒绝，从而使策略能够统一作用于整个应用，包括代理生成的行为以及开发者编写的支撑代码。同时，LBAC 仍保留了相当的表达能力：代理可以执行任意无副作用计算，并递归调用子代理，而子代理在相同的、或潜在更严格的策略约束下，仍保留对工具的完整访问权限。我们通过三个案例研究展示了 LBAC：利用文件系统能力进行 I/O 沙箱化、数据溯源，以及信息流控制。
AgentLens: Revealing The Lucky Pass Problem in SWE-Agent Evaluation
• 作者：Priyam Sahoo, Gaurav Mittal, Xiaomin Li, Shengjie Ma, Benjamin Steenhoek, Pingping Lin, Yu Hu • arXiv URL：https://arxiv.org/abs/2605.12925v1
Abstract
软件工程（SWE）代理的评测主要依赖一个二元信号：最终补丁是否通过测试。这样的结果导向视角，把一个遵循原则的解决方案与一种混乱的试错过程视为等价。我们证明这种等价在经验上并不成立。我们评估了来自八种模型后端的 2,614 条 OpenHands 轨迹，这些轨迹对应 60 个 SWE-bench Verified 任务。其中 47 个任务拥有足够多的通过轨迹，可用于构造任务级过程参考，因此形成了一个 1,815 条轨迹的评测子集。在该子集中，通过轨迹里有 10.7% 表现出我们称为“Lucky Pass（幸运通过）”的行为，包括回归循环、盲目重试、缺少验证，或在时间顺序上混乱的探索、实现与验证。我们提出 AgentLens，这是一个用于对 SWE 代理轨迹进行过程级评估的框架，并发布了 AgentLens-Bench，这是一个包含 1,815 条轨迹的数据集，其中标注了质量分数、浪费信号、分歧点，以及 47 个任务级前缀树接受器（Prefix Tree Acceptor，PTA）参考。AgentLens 通过合并同一任务的多个通过解来构造 PTA 参考，并使用上下文敏感的意图标注器，依据轨迹历史而非仅凭工具身份，将动作标注为探索、实现、验证或编排。在 AgentLens-Bench 上，质量分数能够把通过轨迹区分为 Lucky、Solid 和 Ideal 三个层级，并进一步把 Lucky Pass 细分为五种反复出现的机制。在八种模型后端中，Lucky 比例从 0.5% 到 23.2% 不等，而且按质量分数而不是按通过率排序时，某些模型的名次会变化多达五位。我们在 https://github.com/microsoft/code-agent-state-trajectories/ 发布了匿名化项目仓库，其中包含 AgentLens-Bench 数据集和 AgentLens SDK。
Protocol-Driven Development: Governing Generated Software Through Invariants and Evidence
• 作者：Jun He, Deying Yu • arXiv URL：https://arxiv.org/abs/2605.12981v1
Abstract
自动程序合成降低了产生候选实现的成本，但也带来了一个更困难的治理问题：如何判定哪些生成产物可以被纳入软件系统。自然语言规格仍然存在语义歧义，而基于示例的测试只能抽样覆盖部分行为空间。单独使用这两者，都不足以为自动化软件构建提供充分的控制边界。我们提出 Protocol-Driven Development（PDD，协议驱动开发），这是一种开发模型，其中主要的软件工件不是实现代码，而是一个可由机器强制执行的协议。我们将协议定义为三元组 P = (S, B, O)，其中 S 指定结构不变量，B 指定行为不变量，O 指定运行不变量。三者的合取共同定义了某个软件组件的可接受实现空间。在 PDD 下，实现被视为通过受限搜索发现的可替换实现。如果且仅如果某个实现满足所治理的协议并产生一条可验证的合规证据链（Evidence Chain），它才会被接受。因此，接受依据不是对生成器的信任，而是对协议满足性及其记录在案的证据的信任。PDD 将形式化方法、基于性质的测试、policy-as-code 与软件溯源等思想结合起来，为自动化软件工程定义了一层治理机制。其组织原则很简单：代码是暂时的，协议至上。
TruncProof: A Guardrail for LLM-based JSON Generation under Token-Length Constraints
• 作者：Yoshio Kato, Shuhei Tarashima • arXiv URL：https://arxiv.org/abs/2605.13076v1
Abstract
基于 LLM 的机器可读输出生成，例如 JSON，已经因其可与外部系统集成而受到广泛关注。然而，现有方法无法严格约束生成的最大 token 数量，从而导致无限生成，或者生成被截断后引发系统故障。为了解决这一限制，我们提出 TruncProof，这是一种新的受语法约束生成方法，使 LLM 能够生成语法有效的 JSON，同时遵守预定义的 token 上限。TruncProof 利用 LL(1) 解析器的性质，在每个解码步骤高效近似完成一个语法有效输出所需的最少 token 数量。针对 Text-to-JSON 指令任务的实验表明，即使在严格的 token 约束下，TruncProof 也能成功生成语法正确的输出。此外，我们还表明，TruncProof 可以与高级解码策略有效结合，从而生成不仅语法有效、而且语义准确的输出。
SWE-Cycle: Benchmarking Code Agents across the Complete Issue Resolution Cycle
• 作者：Hao Guan, Lingyue Fu, Shao Zhang, Yaoming Zhu, Kangning Zhang, Lin Qiu, Xunliang Cai, Xuezhi Cao, Weiwen Liu, Weinan Zhang, Yong Yu • arXiv URL：https://arxiv.org/abs/2605.13139v1
Abstract
随着自主代码代理逐步迈向端到端软件开发，评估其实际自治能力变得至关重要。现有基准通过预配置环境来掩盖摩擦，而且其静态评测流水线在解析完全自治的轨迹时经常失效。我们通过 SWE-Cycle 解决这些局限，这是一个经过严格筛选、包含 489 个实例的基准。SWE-Cycle 将代理置于四类任务上进行评估：三项彼此独立的任务，包括环境重建、代码实现和验证测试生成，以及一个整合前三者的端到端 FullCycle 任务。FullCycle 要求代理在一个没有人工支撑的空仓库中自主工作。为了可靠评估这些复杂执行路径，我们开发了 SWE-Judge。该评测代理结合静态代码审查与动态测试，能够准确验证功能正确性，并消除传统静态解析器带来的系统性测量误差。我们使用六个最先进 LLM 驱动的代码代理，在这四类任务上进行评测。结果显示，从独立任务切换到 FullCycle 执行时，解决率出现显著下降，暴露出处理跨阶段依赖和维持代码质量方面的关键瓶颈。SWE-Cycle 与 SWE-Judge 共同提供了一个用于准确衡量自主软件代理端到端能力的完整框架。
Improving Code Translation with Syntax-Guided and Semantic-aware Preference Optimization
• 作者：Yuhan Wu, Huan Zhang, Wei Cheng, Chen Shen, Jingyue Yang, Wei Hu • arXiv URL：https://arxiv.org/abs/2605.13229v1
Abstract
LLM 已展示出在代码翻译上的巨大潜力，但它们往往难以同时保证语法正确性与语义一致性。尽管基于偏好的学习提供了一条有前景的对齐路径，但它受到不可靠的语义奖励所限制，因为这类奖励通常来自稀疏测试用例或过于受限的参考翻译。我们认为，面向代码翻译的稳健语义奖励必须直接从源代码中导出。本文提出 CTO，用语法引导与语义感知的偏好优化来改进代码翻译。我们通过对比学习训练一个跨语言语义模型，使其能够直接评估源代码与翻译后代码之间的功能等价性。我们将代码翻译形式化为一个多目标优化问题，把这一稳健的语义信号与基于编译器的语法反馈在直接偏好优化框架中无缝统一起来。在 C++、Java 和 Python 翻译上的大量实验表明，CTO 明显优于现有基线和其他偏好优化策略。
SkillOps: Managing LLM Agent Skill Libraries as Self-Maintaining Software Ecosystems
• 作者：Hongji Pu, Xinyuan Song, Liang Zhao • arXiv URL：https://arxiv.org/abs/2605.13716v1
Abstract
大语言模型代理越来越依赖技能库来完成多步骤任务，但当技能被添加、复用、补丁修复并与不断变化的依赖关系连接起来时，这些库会积累持续性的缺陷。我们把这种失效模式称为技能技术债（skill technical debt）：它是库层面的缺陷，未必会在局部把某个技能直接弄坏，却会损害未来的检索、组合与执行。现有的基于技能的代理主要关注任务时刻的检索、规划与修复，而库级维护仍然缺乏研究。我们提出 SkillOps，这是一种与方法无关的插件式框架，用于维护技能库。SkillOps 将每个技能表示为带类型的 Skill Contract（P、O、A、V、F），用层级技能生态图（Hierarchical Skill Ecosystem Graph）组织技能，并从效用、兼容性、风险和验证四个维度诊断库健康状况。给定一个原始技能库后，SkillOps 能产出一个经过维护的技能库，且无需更改现有检索或规划代理的内部代码即可使用。在 ALFWorld 上，作为一个独立代理，SkillOps 取得了 79.5% 的任务成功率，比最强基线高出 8.8 个百分点，且没有增加任务时刻的大语言模型调用。作为一个插件层，它把检索密集型基线的表现提升了 0.68 到 2.90 个百分点。当前基于规则的维护实现几乎不需要库时刻的大语言模型调用或 token，说明技能库维护可以作为一种低开销的架构层加入系统。
(How) Do Large Language Models Understand High-Level Message Sequence Charts?
• 作者：Mohammad Reza Mousavi • arXiv URL：https://arxiv.org/abs/2605.13773v1
Abstract
大语言模型（LLM）已被广泛用于自动化软件开发生命周期中的各种任务。然而，这些任务是否始终与所处理工件的语义保持一致仍不清楚。对于架构设计规格而言，这一问题尤其缺乏研究。本文针对高层消息序列图（High-Level Message Sequence Charts，HMSCs）回答这一问题。HMSCs 是一种具有严格形式语义的可视化模型，曾被用于多种用途，包括作为统一建模语言（UML）中序列图的基础。我们通过考察三种 LLM（Gemini-3、GPT-5.4 和 Qwen-3.6）在 129 项语义任务上的表现，来检验 LLM 是否“理解”HMSCs 的语义；这些任务从查询 HMSC 中基本语义构件（即事件及其顺序）开始，一直到语义保持的抽象与组合，以及计算迹集和迹等价标记迁移系统。结果表明，LLM 仅对 HMSC 的形式语义有中等程度的理解（总体准确率约 52%），且不同语义概念之间差异很大：它们似乎能理解 MSC 的基本语义概念（约 88% 准确率），但在涉及抽象与组合的语义推理任务上表现吃力（约 36% 准确率），在处理迹和 LTS 的任务上也同样困难（约 42% 准确率）。特别地，这三种 LLM 都难以理解 co-region 和显式因果依赖的概念，并且在语义保持变换中从未使用过它们。
Neurosymbolic Auditing of Natural-Language Software Requirements
• 作者：Bethel Hall, William Eiers • arXiv URL：https://arxiv.org/abs/2605.13817v1
Abstract
自然语言软件需求往往含糊、不一致且规定不充分；在安全关键领域，这些缺陷会传播到形式模型中，导致验证的是错误的规格，并使实现最终交付不安全的行为。我们表明，配合 SMT 求解器的大语言模型可以审计这类需求：将其翻译为形式逻辑，通过生成形式化结果时的随机变化检测歧义，并在由此得到的规格上通过求解器查询暴露不一致、空洞性以及安全违规。我们提出 VERIMED，这是一个用于医疗器械软件需求的神经符号流水线，用来把这一想法落地，并报告两项发现。第一，独立形式化之间的随机变化可以作为歧义信号：允许多种合理解释的需求会产生 SMT 不等价的形式化结果，而双向 SMT 等价性检查可以把这种分歧转化为可由求解器检查的测试。第二，符号反馈的有效性取决于其粒度：在针对血液透析问答基准的 counterexample-guided 修复中，具体的 SMT 反例把经验证的准确率从 55.4% 提升到 98.5%。在对开源血液透析安全需求进行的大规模实验评估中，我们表明 VERIMED 中基于 LLM 的方法能够成功减少对歧义敏感的需求，并通过基于 SMT 的查询实现对软件需求的严格审计。
代码质量、安全与缺陷检测
Security Incentivization: An Empirical Study of how Micropayments Impact Code Security
• 作者：Stefan Rass, Martin Pinzger, Rainer W. Alexandrowicz, Georg Sengstbratl, Johann Glock, Alexander Lercher, Fabian Oraze, Christoph Wedenig • arXiv URL：https://arxiv.org/abs/2605.13100v1
Abstract
由于安全并不会直接产出可见价值，开发者往往对其投入不足，因而在实践中长期存在安全投入不足的问题。我们评估了一种对策：将团队级激励与随时间可测量的安全改进挂钩。我们的半自动机制汇总 Bearer、Detekt 和 mobsfscan 的静态分析结果，计算安全问题密度，并根据冲刺之间的相对改进比率对团队进行奖励，从而支持在大规模场景下可重复、可脚本化的报告生成。在一项受控课程实验中，我们对 84 名学生组成的 14 个团队进行了比较：一组采用安全激励条件，即将额外分数与安全扫描器结果挂钩；对照组则采用除这一点之外完全相同的评分方案。处理组在总体上获得了显著更低的安全问题密度（beta 回归：β = -0.396，p = 0.0342），表明在激励下安全性得到可测量的改善。在控制平台之后，我们观察到明显的前端/后端差异：在激励条件下，后端的安全问题更少、改进比率更高，说明不同技术栈层之间的效果并不均一。值得注意的是，这些收益并不是代码量膨胀的副产物，因为各组随时间增长的代码行数基本相似。该测量流水线和工具链证明了其可脚本化与自动化可行性，支持在实践中规模化采用。我们的结果表明，把奖励与自动化安全指标对齐可以显著提升代码安全性，并值得在专业场景和更长开发周期中进一步验证。
Code-Centric Detection of Vulnerability-Fixing Commits: A Unified Benchmark and Empirical Study
• 作者：Nils Loose, Joseph Bienhüls, Kristoffer Hempel, Felix Mächtle, Thomas Eisenbarth • arXiv URL：https://arxiv.org/abs/2605.13138v1
Abstract
自动检测漏洞修复提交（vulnerability-fixing commits，VFC）对于及时部署安全补丁至关重要，因为漏洞公告数据库通常比补丁发布滞后中位数 25 天，而且许多修复从未被正式公告。我们提出一个统一框架，对基于代码语言模型的 VFC 检测进行全面评估，该框架整合了超过 20 个碎片化数据集，覆盖超过 18 万次提交。通过 180 多项实验，对参数规模从 1.25 亿到 140 亿的微调模型进行测试后，我们没有发现任何证据表明模型能仅从代码变更中获得可迁移的安全相关代码理解。当提交消息可用时，它们会主导模型注意力；而当提交消息被移除后，归因分析显示，即使为 diff 增加更多过程内语义上下文，也不会把模型注意力转向代码变更本身。按组划分的评测显示，相比随机划分，性能大约下降 17%；而在聚合数据集上使用时间划分时，由于底层项目分布存在组合漂移，其结果并不可靠。在 0.5% 的假阳性率下，所有微调后的仅代码模型都会漏掉超过 93% 的漏洞。更大且更多样的数据，或者生成式方法，虽然带来初步改进，但都无法解决这些根本限制。为了支持未来关于基于代码的 VFC 检测研究，我们发布了统一框架和评测套件。
Automatic Detection of Reference Counting Bugs in Linux Kernel Drivers
• 作者：Joe Hattori, Naoki Kobayashi, Ken Sakayori • arXiv URL：https://arxiv.org/abs/2605.13246v1
Abstract
Linux 内核驱动中的引用计数 bug 可能导致严重的资源管理错误和安全漏洞。我们提出 DrvHorn，这是一种通过将引用计数验证规约为断言检查问题、并利用 Linux 驱动接口来检测此类 bug 的新工具。借助高效的 Linux 内核建模和激进的程序切片，DrvHorn 在 Linux v6.6 内核中所有平台驱动上发现了 545 个 bug，其中 424 个此前未被发现；其假阳性率为 29.9%，低于先前研究。为应对这些新发现 bug 的根因，我们向 Linux 内核提交了补丁，其中 45 个已经合并。
Robust Mutation Analysis of Quantum Programs Under Noise
• 作者：Sophie Fortz, Eñaut Mendiluze Usandizaga, Shaukat Ali, Paolo Arcaini, Mohammad Reza Mousavi • arXiv URL：https://arxiv.org/abs/2605.13279v1
Abstract
变异分析长期以来一直用于经典软件测试，近年来也被用于评估量子软件测试技术的鲁棒性。然而，现有研究通常假设执行是理想且无噪声的，从而忽略了量子硬件噪声的影响。本文对面向噪声的量子程序变异分析进行了实证研究。我们分析了噪声如何影响突变体检测，使用 41 个量子程序，在无噪声模拟器以及模拟三台具有不同噪声特征的 IBM 设备的有噪声模拟器上执行这些程序。我们比较了多种距离度量和阈值策略，以评估在真实噪声下的突变体检测效果。结果表明，噪声会显著改变程序与突变体之间的行为距离，使等价突变体更难与真实缺陷区分。密度矩阵度量的区分效果最好，误分类率最高可达 16.77%，但它们无法在真实硬件上使用。在可行的替代方案中，输出分布度量的准确率最高可达 73.03%，F1 分数最高可达 74.89%。面向噪声的阈值比无噪声阈值进一步提升了检测效果。我们还发现，噪声效应与算法和电路特征的相关性，比与变异类型的相关性更强。总体而言，我们的结果表明，变异分析以及更一般的量子程序比较方法，都需要针对目标量子设备的噪声特征进行适配。
The Readability Spectrum: Patterns, Issues, and Prompt Effects in LLM-Generated Code
• 作者：Hengzhi Ye, Fengyuan Ran, Weiwei Xu, Minghui Zhou • arXiv URL：https://arxiv.org/abs/2605.13280v1
Abstract
随着大语言模型（LLM）正在改变软件开发，生成代码的功能质量已成为关注焦点，而可读性这一关键非功能属性则长期被忽视。由于 LLM 生成的代码在被采用前仍需要人工审查，理解其可读性，尤其是与人类编写代码相比的可读性，以及提示设计对其影响，是非常重要的。因此，我们开展了一项关于 LLM 生成代码可读性的系统性研究。为了系统量化代码可读性，我们建立了一个综合性的可读性模型，将代码的文本、结构、程序和视觉特征融合在一起。基于该模型，我们在 5,869 个场景下评估了主流 LLM 生成的代码，这些场景取自 World of Code（WoC）和 LeetCode 等大型代码库。我们发现，当前 LLM 生成的代码在整体可读性上与人类编写代码相当，但呈现出不同的可读性问题模式。我们进一步考察了不同提示维度如何影响 LLM 生成代码的可读性，发现函数签名、约束和风格描述是最具影响力的因素，而提示设计的整体影响仍然有限。我们的发现表明，一方面，LLM 生成代码在可读性上至少与人类编写代码相当，这从非功能角度验证了其系统性融入软件工作流的潜力；另一方面，独特的可读性问题模式和有限的提示工程效果揭示了潜在的技术债，说明未来需要进一步研究如何提升 LLM 生成代码的可读性，从而确保其长期可维护性。
SieveFL: Hierarchical Runtime-Aware Pruning for Scalable LLM-Based Fault Localization
• 作者：Mahdi Farzandway, Fatemeh Ghassemi • arXiv URL：https://arxiv.org/abs/2605.13491v1
Abstract
自动化故障定位需要把一次观测到的测试失败关联到成千上万个候选方法中的责任方法，而纯统计方法在精度上有限，而 LLM 由于 token 成本过高和信号稀释，尚无法在整个项目规模上胜任这项任务。我们提出 SieveFL，这是一个五阶段的分层框架，通过激进的 LLM 前过滤来化解这一矛盾。SieveFL 先把失败测试转换为自然语言的失败描述，再使用稠密向量检索把搜索范围缩小到少量可疑文件，随后通过 JaCoCo 运行时轨迹剔除所有在失败测试中未被执行的方法。只有存活下来的候选才会被送入 LLM，由其逐个筛查每个方法，并在一次比较式推理中重新排序确认的嫌疑项。我们在 Defects4J v1.2.0 的 395 个 bug 上评估了 SieveFL，所用的是部署在普通工作站上的中等规模、公开可得的 MoE 模型（32 GB 内存、8 GB GPU），通过 Ollama 运行，不需要前沿 API 或数据中心级硬件。将 12 次不完整运行视为失败后，SieveFL 取得了 41.8% 的 Top-1 准确率（395 个 bug 中命中 165 个）和 0.469 的 MRR，在 Top-1 上比最强的先前代理式基线 AgentFL 高出 2.1 个百分点。运行时剪枝移除了 79% 的候选方法，并将输入 token 消耗降低了 49%，同时还提升了排序质量：Top-1 保持完全不变，而 Top-3 到 Top-10 最多提升 2.4 个百分点。这些结果表明，只要有合适的过滤架构，强大的故障定位并不一定需要专有的前沿模型。
测试、评测与可复现性基础设施
UIBenchKit: A unified toolkit for design-to-code model evaluation
• 作者：Chinh T. Le, Trevor Ong Yee Siang, Jingyu Xiao, Yuxuan Wan, Yintong Huo • arXiv URL：https://arxiv.org/abs/2605.13141v1
Abstract
近年来，自动化设计到代码生成取得了显著进展，许多方法被提出用于根据网页截图生成 HTML 和 CSS。然而，缺乏标准化评测平台使得这些方法难以被公平比较，也限制了实际采用与系统性研究进展。为弥补这一缺口，我们提出 UIBenchKit，这是一套开源的一体化工具包，旨在统一设计到代码任务的评测。UIBenchKit 抽象了环境搭建、模型推理与代码渲染的复杂性，为研究人员提供即插即用的架构，使其能够在一致条件下比较不同方法。此外，它还提供了用于多项指标比较的分析界面。借助 UIBenchKit，我们对现有工具开展了基准研究，并据此归纳出若干结果，以指出未来改进方向。通过为实验与评测提供流畅的环境，UIBenchKit 旨在加速未来网页工程领域的基准研究与创新。该评测平台和工具包可在项目页面 https://www.uibenchkit.com/ 获取。
ReproScore: Separating Readiness from Outcome in Research Software Reproducibility Assessment
• 作者：Sheeba Samuel, Daniel Mietchen, Jungsan Kim, Waqas Ahmed, Martin Gaedke • arXiv URL：https://arxiv.org/abs/2605.13275v1
Abstract
数字图书馆收藏了数以百万计的研究软件工件，但缺乏可规模化的基础设施来评估这些工件是否仍然可执行。现有自动评估工具把仓库的静态完整性，即仓库包含什么，视为执行成功，即它是否能运行的代理。我们把这种现象称为 readiness-outcome 混淆，并提出 ReproScore，这是一种两层框架，显式地区分可复现准备度（reproducibility readiness，RRS）和可复现结果（reproducibility outcome，ROS），并将二者结合为一个具备覆盖率自适应能力的综合分数（Composite Score，RCS）。RRS 由五个类别下的 26 个子指标构成；ROS 在沙箱基础设施可用时提供基于执行的探针；社区 rubric 则通过版本化 YAML 配置文件外化权重优先级。我们在一个大型真实值语料库中的 423 个 GitHub 仓库上进行了评估，该语料库覆盖五种失败模式。结果得到两个互补发现：环境类别对失败模式具有很强的区分力，说明静态信号能够捕获有意义的结构差异；但 RRS 与二元成功结果几乎没有相关性，经验性地量化了仓库规模上的 readiness-outcome 差距。总体而言，这些发现验证了这种架构性分离既必要又非平凡，并将 ReproScore 定位为数字图书馆工作流中支持可复现性感知策展的可规模化基础设施。
AI Harness Engineering: A Runtime Substrate for Foundation-Model Software Agents
• 作者：Hailin Zhong, Shengxin Zhu • arXiv URL：https://arxiv.org/abs/2605.13357v1
Abstract
基础模型已经改变了自动化代码生成的格局，但在真实软件开发环境中，自主软件工程代理仍然不够可靠。主流解释通常把这一差距归因于模型能力不足。我们提出另一种解释：软件工程能力产生于一个模型-支撑系统-环境的整体，其中运行时底座，即 harness，决定了基础模型代理如何观察项目、对项目采取行动、接收反馈，以及如何判定一次变更是否完成。我们将这一底座形式化为 AI Harness Engineering，并识别出 11 项组件职责：任务规范、上下文选择、工具访问、项目记忆、任务状态、可观测性、失败归因、验证、权限、熵审计以及干预记录。我们通过一个四级阶梯（H0-H3）对 harness 进行操作化，该阶梯逐级向代理暴露运行时支持；同时，我们提出一种基于轨迹的评测协议，将每次代理运行转化为可审计的 episode 包。在一个受控验证任务上应用该框架后，得到的 episode 包在证据结构上会随着 harness 级别系统性变化：较低级别只产生最终补丁，而更高级别会产生复现实验日志、失败归因、确定性需求检查以及结构化验证报告。该框架把自主软件工程的核心问题从“基础模型能否生成补丁”转变为“模型-支撑系统-环境整体能否生成一个可验证正确、可归因且可维护的变更”。我们据此勾勒出一个面向基础模型软件代理所需运行时系统的研究计划。
Integration of an Agent Model into an Open Simulation Architecture for Scenario-Based Testing of Automated Vehicles
• 作者：Christian Geller, Daniel Becker, Jobst Beckmann, Lutz Eckstein • arXiv URL：https://arxiv.org/abs/2605.13539v1
Abstract
仿真式和基于场景的测试是自动驾驶系统安全保证中的关键方法。为了确保仿真结果可靠，必须以足够的保真度对真实世界建模，这不仅包括静态环境，还包括测试车辆周围的交通流。因此，交通代理模型的可用性具有普遍意义，因为它们可以像人类驾驶员一样对自然化且可参数化的行为进行建模。不同仿真环境之间的代理模型可替换性是一项重大挑战，这要求实现方法的协调与标准化。为解决这一挑战，我们提出一种标准化、模块化的仿真集成架构，使得交通代理模型能够以工具无关的方式集成。该架构以 Open Simulation Interface（OSI）作为结构化消息格式，并以 Functional Mock-up Interface（FMI）作为动态模型交换机制。与其再提出一个新的模型或仿真工具，我们提供的是一个可复用的参考实现，它把这些标准转换为实际可用的集成蓝图，其中包含清晰的接口、数据映射和执行语义。通过把一个示例代理模型集成到三种广泛使用的仿真环境中，即 OpenPASS、CARLA 和 CarMaker，展示了该架构的通用性。评测结果表明，该模型在所有仿真平台上都能产生一致行为，从而验证了所提架构的互操作性、模块化和标准符合性。该参考实现降低了集成门槛，可作为未来研究的基础，并已在 github.com/ika-rwth-aachen/agent-model-integration 公开提供。
Learning Responsibility-Attributed Adversarial Scenarios for Testing Autonomous Vehicles
• 作者：Yizhuo Xiao, Haotian Yan, Ying Wang, Zhongpan Zhu, Yuxin Zhang, Xintao Yan, Mustafa Suphi Erden, Cheng Wang • arXiv URL：https://arxiv.org/abs/2605.13751v1
Abstract
为建立可信的自动驾驶系统（ADS）安全保证，必须提供证据证明故障源于可避免的系统缺陷，而不是不可避免的交通冲突。当前的对抗性仿真方法能够高效暴露碰撞，但通常缺乏区分这两类本质不同失效模式的机制。本文提出 CARS（Context-Aware, Responsibility-attributed Scenario generation），这是一个将责任归因直接集成到对抗性场景生成中的框架。CARS 把上下文感知的对抗者选择与一个在闭环仿真中优化的生成式对抗策略结合起来，从而构造既物理可行、又能在诊断上归因的碰撞场景。我们在跨异质国家交通环境的基准数据集上表明，在多种法规规定的谨慎驾驶员与胜任驾驶员模型下，CARS 都能稳定发现可行的碰撞场景，并具有较高的归因率。通过将对抗生成与规范性责任评估耦合，CARS 使仿真测试从单纯发现碰撞，迈向构造可解释、与法规对齐且可扩展的 ADS 验证安全证据。
形式化验证与程序逻辑
LFPL: Revisited and Mechanized
• 作者：Nathaniel Glover, Jan Hoffmann • arXiv URL：https://arxiv.org/abs/2605.12893v1
Abstract
Hofmann（1999）提出了函数式编程语言 LFPL，用仿射类型系统刻画可在多项式时间内计算的函数。LFPL 支持自然的编程风格，包括嵌套递归，并启发了自动成本分析的类型系统、线性依赖类型理论以及函数式编程语言中的高效内存管理的发展。尽管 LFPL 具有重要地位，但此前一直没有一个自洽的呈现，更遑论对 LFPL 及其核心元理论进行完整的形式化机械证明。本文给出 LFPL 及其元理论的现代化阐述与机械化证明，目标是做到自包含且易于理解，同时简化最强的已知可靠性与完备性结果。可靠性证明针对语言 LFPL+ 展开，后者是在 LFPL 上加入了额外语言特性的扩展版本。该证明具有新意，它借鉴 Aehlig 和 Schwichtenberg（2002）的方法，为 LFPL+ 表达式构造显式多项式，从而在大步成本语义下对其计算代价进行界定。完备性证明表明，LFPL 程序可以模拟多项式时间图灵机，而且只依赖受限形式的线性函数和列表。其结构与 Hofmann（2002）的原始证明相同，但通过一种新的栈式数据结构显著简化了核心论证；该数据结构由一等函数和列表实现。整个机械化过程包含完整的可靠性与完备性证明，并且作为近期开发的证明助手 Istari 中元理论机械化的首批案例研究之一。
Scalable Deductive Verification of Data-Level Parallel Programs
• 作者：Lars B. van den Haak, Anton Wijs, Marieke Huisman • arXiv URL：https://arxiv.org/abs/2605.13616v1
Abstract
本文提出若干技术，以提升对数组和矩阵等数据级程序进行演绎式验证的可扩展性。首先，我们引入一种重写包含（嵌套）量词的表达式的方法，以便为这些表达式生成合适的触发器（trigger）。我们已在定理证明器中证明该重写技术正确。其次，我们通过提供规范构造来简化对可能重叠数组的推理：这些构造可指明并验证两个数组并非别名，或者它们是不可变的，因此可以将其建模为数学序列。我们所有的技术都已实现在 VerCors 程序验证器中。我们通过大量实验说明这些技术如何提升可扩展性。将这些技术用于一组典型 GPU 内核时，验证时间平均缩短到原来的 1/9，最极端的情况快了 150 倍。此外，把这些技术应用到更早的实验以及一个射电望远镜管线的早期案例研究中后，我们得以验证此前无法获得的结果，并显著缩短了验证时间。
First Steps Towards Probabilistic Iris: Harmonizing Independence, Conditioning, and Dynamic Heap Allocation
• 作者：Janine Lohse, Tim Rohde, Jimmy Xin, Niklas Mück, Iona Kuhn, Derek Dreyer, Deepak Garg, Emanuele D'Osualdo • arXiv URL：https://arxiv.org/abs/2605.13765v1
Abstract
近年来，概率分离逻辑（probabilistic separation logics）领域取得了令人振奋的进展。这一类中的一个重要子类，包括 PSL、Lilac、Bluebell 和 pcOL，在本文中被称为通用概率逻辑（general-purpose probabilistic logics，简称 GPL），它们为程序状态上的概率分布提供原始的 Hoare 风格断言，并配备诸如独立性（independence）与条件化（conditioning）之类强大的模块化原则。然而，这些逻辑都不支持对动态分配内存（即指向堆的指针）进行推理，更不用说支持像 Iris 这样的现代分离逻辑所具有、基于资源代数的 ghost state 了。我们认为，这源于一个根本障碍：由于内存的形状（以及内存位置的身份）可能会在不同随机结果下发生变化，因此难以将指针所有权与概率独立性和条件化协调起来。此外，现有 GPL 都未在证明助手中完成机械化。在本文中，我们以 Amaryllis 的形式，向把 GPL 与像 Iris 这样的现代分离逻辑结合迈出了重要一步。Amaryllis 是第一个同时支持独立性与条件化推理、并且还能处理动态内存分配的 GPL。为克服上述障碍，我们提出了一种新的“索引赋值”（indexed valuation）式概率断言模型，在这一模型下，标准 Iris 风格资源（例如堆）的所有权可以以一种通用方式提升到分布层面的所有权。随后，我们展示如何调整 Iris 的核心概念，包括 frame-preserving update、authoritative resource algebras 以及 weakest precondition 模态，使其在概率推理下保持可靠，并能验证动态分配。最后，我们在 Rocq 证明助手中机械化了全部结果，并开发了一个基于 Iris 的证明模式，用于在 Amaryllis 中进行证明。
On the Complexity of Checking Soundness of Natural Reductions (Extended Version)
• 作者：Constantin Enea, Azadeh Farzan, Dominik Klumpp • arXiv URL：https://arxiv.org/abs/2605.13780v1
Abstract
对规约的验证，即对交错执行的代表性子集进行验证，可以简化参数化并发程序的正确性证明。我们引入了一类表达力更强的语法规约，称为自然规约（natural reductions）。自然规约通过在参数化程序的线程模板中引入原子块和全局会合点来指定。我们研究如下问题：给定一个自然规约，以及给定一个（半）可交换关系，判断该自然规约是否相对于该关系是可靠的（sound）。在不存在线程同步的情况下，我们给出一个可靠且完备的多项式时间算法。在考虑同步的情况下，我们提供了该问题的一个一般下界（其参数化于所采用的同步机制），并证明即使在锁定（locking）这样简单的机制下，该问题也已经是 coNP-困难的。
自动机与计算理论
Decoupled Planning for Multiple Omega-Regular Objectives
• 作者：Guy Avni, Thomas A. Henzinger, Kaushik Mallik, Suman Sadhukhan, K. S. Thejaswini • arXiv URL：https://arxiv.org/abs/2605.13185v1
Abstract
我们研究在图上生成路径以满足一组 ω-正则目标的问题。我们提出一个解耦框架，其中每个目标都分配给一个独立代理，由它选择局部策略，而一个调度器则不关心图结构和目标本身，动态地把这些策略组合成一条单一路径。我们研究：在假设这些目标的合取是可实现的前提下，这种组合何时能够满足所有目标。该框架使策略设计具备模块化，但也带来了根本性的组合挑战。我们证明，即使是极其公平的确定性调度器也不能保证正确性，而随机调度器虽然必要，却在缺乏协调时仍然不足。对于安全目标，我们证明完全去中心化的实现是不可能的，并提出一种在最大安全动作上进行同步的协议。对于非安全目标，我们引入 conventions，即在图或目标揭示之前由所有代理预先约定的一些简单先验限制，只要所有代理都遵守这些限制，就能保证满足所有目标。我们刻画了 ω-正则目标主要子类中的最小约束 conventions。特别地，Büchi 目标允许无需调度器通信即可对有限记忆策略进行普遍组合；co-Büchi 目标只需要知道代理是否被调度；而 parity 目标还额外需要知道是哪一个代理被调度。
Universal Design and Physical Applications of Non-Uniform Cellular Automata on Translationally Invariant Lattices
• 作者：Xiang-You Huang, Jie-Yu Zhang, Peng Ye • arXiv URL：https://arxiv.org/abs/2605.13379v1
Abstract
晶格几何深刻地影响着诸如子系统对称性和定向渗流（directed percolation, DP）之类的物理现象。在各种晶格几何中，双曲晶格具有恒定的负曲率和非阿贝尔平移对称性，为研究这种几何与物理的相互作用提供了丰富平台。然而，指数增长的晶格规模和非平凡的平移对称性使得为欧几里得晶格开发的方法无法直接适用，这一点在均匀细胞自动机（cellular automata, CA）中尤为明显。为了解决这一问题，我们提出一种高阶非均匀细胞自动机（non-uniform cellular automata, NUCA）算法，它既适用于平移不变的规则欧几里得晶格，也适用于双曲晶格。在该算法中，非均匀更新规则通过一种晶格变形过程引入了非平凡的几何数据。我们通过在双曲 {5,4} 晶格上的若干应用展示了该算法的广泛适用性。利用线性 NUCA，我们生成了子系统对称性保护拓扑（SSPT）态，以及与规则或不规则子系统对称性相关、而在欧几里得晶格上无法获得的自发子系统对称性破缺态。我们设计了多点奇异关联函数（multi-point strange correlators）来探测非平凡的 SSPT 态，并为由非阿贝尔平移不变 NUCA 生成的模型推导出一个充分条件。进一步地，我们将 NUCA 推广到非均匀 Clifford 量子细胞自动机（CQCA），从而生成双曲 cluster 态的子系统对称性，扩展了平移不变 CQCA 与子系统对称性之间已知的对应关系。此外，我们还通过一种继承了晶格树状结构的概率 NUCA 来模拟 DP 过程，并数值估计渗流阈值与相图。
Exact Accepting-State Spectrum for Reversal of Permutation Automata
• 作者：Samuel German • arXiv URL：https://arxiv.org/abs/2605.13385v1
Abstract
我们精确确定了置换自动机（permutation automata）在取反（reversal）操作下的接受状态谱（accepting-state spectrum），从而证明了 Rauch-Holzer 猜想在这一操作上的成立。对于每个 m ≥ 2 和每个 α ≥ 2，我们构造一个二元置换自动机 A_{m,α}，使得 asc(L(A_{m,α})) = m 且 asc(L(A_{m,α})^R) = α。结合平凡情形 m = 0 和 m = 1，以及先前已知的“1 对每个 m ≥ 2 都是 magic”的事实，可得到精确谱 g^{asc}{R,PFA}(0) = {0}、g^{asc}{R,PFA}(1) = {1}，以及对于每个 m ≥ 2，g^{asc}{R,PFA}(m) = N{≥2}。因此，对于置换自动机而言，取反操作具有在接受状态谱意义下最简单的精确形式，只受到值 1 这一唯一非平凡障碍的约束。该证明使用了一个统一的群论见证族：正向自动机的状态是 [n] 的 α-子集，其中 n = m + α - 1，并由一个 n-循环和一个换位生成的作用驱动，而接受状态形成一个单一的 star family。取反之后，可达的子集状态恰好就是这些 stars。借此我们能够精确计数可达的接受状态，并证明反向自动机中可达状态的最小性。
Liquid Tree Automata
• 作者：Ashish Mishra, Suresh Jagannathan • arXiv URL：https://arxiv.org/abs/2605.13456v1
Abstract
基于组件的合成（component-based synthesis, CBS）通过从库组件中组合无循环程序来满足逻辑查询。尽管更具表达力的规格和更精确的查询能够简化解空间，却也使传统 CBS 过程更难找到可行的执行路径。随着约束变得更加精确，搜索必须在越来越稀疏的有效路径空间中前进。我们通过推理探索路径之间的“逻辑相似性”来应对这一挑战。我们考虑配有 refinement type 规格的库方法，这些规格通过逻辑限定符细化基础类型，以精确约束值空间。为了高效探索该空间，我们提出 Liquid Tree Automata（LTA），这是一种由 refinement typing 规则驱动构造的新型树自动机变体。LTA 利用子类型约束识别语义上相似的状态，并在搜索过程中尽早将其合并。这样的合并避免了对等价路径的冗余探索，显著提升了合成效率。我们将这一方法实现为工具 Hegel。评测结果表明，Hegel 能够综合出复杂查询的解，而这些查询已超出现有最先进工具的能力范围。
