夜雨聆风目录
AI辅助软件工程与开发流程
• Enhancing Large Language Models with Retrieval Augmented Generation for Software Testing and Inspection Automation • AI-Assisted Requirements Engineering: An Empirical Evaluation Relative to Expert Judgment • Applying SHAPR in AI-Assisted Research Software Development: Lessons Learnt from Building a Share Trading System • Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Study • Asking What Matters: Reward-Driven Clarification for Software Engineering Tasks • LLMs taking shortcuts in test generation: A study with SAP HANA and LevelDB • Chinese Language Is Not More Efficient Than English in Vibe Coding: A Preliminary Study on Token Cost and Problem-Solving Rate
软件工程智能体与执行安全
• From Procedural Skills to Strategy Genes: Towards Experience-Driven Test-Time Evolution • Atropos: Improving Cost-Benefit Trade-off of LLM-based Agents under Self-Consistency with Early Termination and Model Hotswap • SWE-TRACE: Optimizing Long-Horizon SWE Agents Through Rubric Process Reward Models and Heuristic Test-Time Scaling • Bounded Autonomy for Enterprise AI: Typed Action Contracts and Consumer-Side Execution • AIPC: Agent-Based Automation for AI Model Deployment with Qualcomm AI Runtime • Dive into Claude Code: The Design Space of Today's and Future AI Agent Systems • Benchmarks for Trajectory Safety Evaluation and Diagnosis in OpenClaw and Codex: ATBench-Claw and ATBench-CodeX • CBCL: Safe Self-Extending Agent Communication
编译优化与硬件生成
• HintPilot: LLM-based Compiler Hint Synthesis for Code Optimization • Graph-Based ECO and Patch Generation for High-Level Synthesis • Prism: Symbolic Superoptimization of Tensor Programs • Nautilus: An Auto-Scheduling Tensor Compiler for Efficient Tiled GPU Kernels • VeriGraphi: A Multi-Agent Framework of Hierarchical RTL Generation for Large Hardware Designs
程序语言与形式化推理
• Pure Borrow: Linear Haskell Meets Rust-Style Borrowing • Filament: Denning-Style Information Flow Control for Rust • Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy • Complexity of Fungal Automaton Prediction • Measuring the Computational Power of Finite Patches of Cellular Automata
移动安全、协作质量与教学
• Towards Understanding Android APIs: Official Lists, Vendor Customizations, and Real-World Usage • AndroScanner: Automated Backend Vulnerability Detection for Android Applications • ToxiShield: Promoting Inclusive Developer Communication through Real-Time Toxicity Filtering • What if we have 90 minutes only to teach programming?
AI辅助软件工程与开发流程
Enhancing Large Language Models with Retrieval Augmented Generation for Software Testing and Inspection Automation
• 作者：Zoe Fingleton, Nazanin Siavash, Armin Moin • arXiv URL：https://arxiv.org/abs/2604.15270
Abstract
本文聚焦于软件开发生命周期（SDLC）中两类被广泛使用的验证与确认（V&V）活动的自动化：软件测试与软件检查（亦称评审）。对于前者，作者关注使用大语言模型（LLM）进行自动化测试用例生成；对于后者，作者使 LLM 能够对源代码进行检查。为应对 LLM 已知的幻觉问题，即 LLM 会自信地产生错误输出，作者实现了一条检索增强生成（RAG）流水线，用于集成补充性知识源并向 LLM 提供额外上下文。实验结果表明，通过 RAG 流水线引入外部上下文，通常会对测试用例生成和代码检查两项任务都产生积极影响。这一新方法通过节省人工测试人员和检查人员的时间来降低项目总成本，并且如实验研究所示，还提升了这些 V&V 活动的有效性与效率。
AI-Assisted Requirements Engineering: An Empirical Evaluation Relative to Expert Judgment
• 作者：Oz Levy, Ilya Dikman, Natan Levy, Michael Winokur • arXiv URL：https://arxiv.org/abs/2604.15222
Abstract
人工智能正日益被引入系统工程活动，尤其是在需求工程中，而质量评估与验证仍在很大程度上依赖专家判断。尽管近期 AI 工具在需求分析与生成方面展现出可观潜力，但其在正式系统工程流程中的角色，以及其与既有 INCOSE 标准的一致性，仍缺乏充分理解。本文研究基于 AI 的工具在不取代专业知识的前提下，能够在多大程度上支持系统工程师评估需求质量。研究采用结构化系统工程方法，将 AI 辅助的需求评估与人工专家评估进行比较。作者开展了一项受控实验，由经验丰富的系统工程师和一个基于 AI 的评估工具，分别依据既定的 INCOSE “优质需求”准则对系统需求进行评估。评估重点包括一致性、完整性、清晰性与可测试性，不仅考察准确性，也分析每项判断背后的决策逻辑。结果表明，AI 工具能够提供一致且快速的初步评估，尤其适用于语法和结构层面的质量属性；但在语境解释、歧义消解和权衡推理方面，专家判断仍不可替代。研究结果并不将 AI 定位为系统工程师的替代品，而是支持其作为需求工程生命周期中的决策支持机制。从系统工程视角看，本文为如何在保持可追溯性、责任可归属性和工程一致性的同时，将 AI 集成进需求工程工作流提供了实证证据。
Applying SHAPR in AI-Assisted Research Software Development: Lessons Learnt from Building a Share Trading System
• 作者：Ka Ching Chan • arXiv URL：https://arxiv.org/abs/2604.15020
Abstract
生成式 AI 正在改变研究软件的开发方式，但快速的 AI 辅助开发也可能削弱连续性、可追溯性和方法论清晰性。SHAPR（Solo, Human-centred, AI-assisted PRactice）被提出为一种用于组织 AI 辅助研究软件开发的框架。本文展示了一个将 SHAPR 应用于模块化股票交易系统开发的文档化案例。项目从一开始就采用了受 SHAPR 启发的工作配置，用以塑造交互、实现与文档组织方式。在多轮迭代开发周期中，项目形成了结构化证据基础，包括反思记录、开发周期复盘记录、事实来源文档、契约、快速捕捉记录、工作流笔记以及不断演化的代码工件。该案例表明，在快速捕捉与 AI 辅助精炼的支持下，持续更新文档有助于在整个开发过程中维持有组织且可用的项目知识。作者总结出五条反复出现的经验：契约能够稳定 AI 辅助编码，持续维护的事实来源层可提升一致性，周期边界快照可增强连续性，代码与文档通过快速捕捉和迭代精炼共同演化，而环境搭建本身也会促进知识生成。该案例还展示了一种实用的 SHAPR 运行配置：其中 ChatGPT Project 和各周期专用对话支持交互、推理、摘要与编码协作，PyCharm 支持工件实现，Obsidian 支持外部工作记忆、结构化文档、反思、连续性及面向仓库的笔记组织，同时仍符合 SHAPR 的工具无关原则。本文为开展 AI 辅助研究软件开发的研究者提供了实践指导与良好实践。
Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Study
• 作者：Michal Töpfer, František Plášil, Tomáš Bureš, Petr Hnětynka • arXiv URL：https://arxiv.org/abs/2604.14867
Abstract
Vibe coding 在本质上假设通过反馈循环对 LLM 生成代码进行迭代式精炼。尽管这种方式对常规软件任务有效，但其在运行时自适应系统中的可靠性尚不明确，尤其是在生成代码不经人工检查的情况下。本文研究了对 LLM 生成的适应管理器进行基于反馈的自动化验证，目标场景为集体自适应系统（CAS）。作者聚焦于“环中的验证”所面临的关键挑战：如何在运行时检测生成代码的失败，以及如何以足够精确的方式报告这些失败，使 LLM 能够进行修复。作者将适应循环与 vibe-coding 反馈循环结合起来，通过以下两类约束检验正确性：（i）通用架构约束；（ii）以功能约束逻辑（FCL）形式化的功能约束。FCL 是一种新的一阶时序逻辑，适用于潜在有限轨迹。通过 Dragon Hunt CAS 案例研究，作者表明，细粒度的约束违规能够提供可操作反馈，通常可在少数迭代内产生有效的适应管理器；而简单、粗粒度的指标式反馈则常常使过程停滞。研究结果表明，对于由不具备编程技能的领域专家设计的系统，反馈精度是实现可靠 vibe coding 的主导因素，从而可以免除人工代码检查的需要。
Asking What Matters: Reward-Driven Clarification for Software Engineering Tasks
• 作者：Sanidhya Vijayvargiya, Vijay Viswanathan, Graham Neubig • arXiv URL：https://arxiv.org/abs/2604.14624
Abstract
人类经常以不完整的方式描述任务，因此助手必须知道何时以及如何提出澄清性问题。然而，在软件工程任务中实现有效澄清仍然很具挑战，因为并非所有缺失信息都同等有价值，而且问题必须瞄准用户现实中能够提供的信息。本文通过量化哪些类型的信息最影响任务成功，以及哪些问题能够从模拟用户那里获得有用回答，来研究真实软件工程任务中的澄清行为。作者利用 Shapley 归因和分布比较，识别出有效澄清的两个关键属性：任务相关性（哪些信息能够预测成功）和用户可回答性（用户现实中能提供什么信息）。作者将这两个属性操作化为多阶段强化学习奖励，以训练一个 80 亿参数的澄清模块 CLARITI。该模块在信息不充分的问题上达到了与 GPT-5 相当的解决率，同时提出的问题数量减少了 41%。结果表明，将奖励设计建立在信息影响与用户可回答性的实证分析之上，能够提升澄清效率。
LLMs taking shortcuts in test generation: A study with SAP HANA and LevelDB
• 作者：Vekil Bekmyradov, Noah C. Pütz, Thomas Bartz-Beielstein • arXiv URL：https://arxiv.org/abs/2604.14437
Abstract
大语言模型（LLM）在公开基准上已取得令人印象深刻的结果，这常常引发有关其具备高级推理与理解能力的论断。然而，近期认知科学研究揭示，这些模型有时依赖浅层启发式和记忆，而非展示真正的认知能力。本文在软件自动化测试生成场景中研究 LLM 的行为，对比其在开源系统 LevelDB 与 SAP HANA 上的表现。SAP HANA 是全球最广泛部署的商用数据库系统之一，其专有代码库可以保证不存在于训练数据中。作者将认知评估原则与实证软件测试相结合，借鉴 Mitchell 以机制为中心的评估方法，并采用变异分数和基于编译器反馈的迭代修复循环，以同时评估准确性及其背后的推理策略。结果显示，LLM 在熟悉的开源基准上表现出色，但在未见过的复杂领域中表现不佳，且往往更优先追求代码可编译性，而非语义层面的有效性。这些发现为“当前 LLM 缺乏稳健推理能力”这一更广泛主张提供了独立的软件工程证据，并凸显了建立惩罚琐碎捷径、奖励真实泛化的评估框架之必要性。
Chinese Language Is Not More Efficient Than English in Vibe Coding: A Preliminary Study on Token Cost and Problem-Solving Rate
• 作者：Simiao Ren, Xingyu Shen, Yuchen Zhou, Dennis (Tsang)Ng, Ankit Raj • arXiv URL：https://arxiv.org/abs/2604.14210
Abstract
社交媒体和实践者论坛上一直流传一种说法，认为在基于 LLM 的编码任务中，中文提示比英文更节省 token，潜在可将成本降低至多 40%。这一说法已影响开发者考虑在 “vibe coding” 中转而使用中文，以节省 API 成本。本文使用软件工程任务基准 SWE-bench Lite 开展严格实证研究，以检验中文在 token 效率方面的优势是否成立。结果揭示三点主要发现。第一，并未观察到中文的效率优势。第二，token 成本会以违背简单直觉的方式随模型架构而变化：例如，MiniMax-2.7 在中文提示下的 token 成本高出 1.28 倍，而 GLM-5 在中文提示下反而消耗更少 token。第三，也是最重要的一点，作者发现对于测试的所有模型，使用中文提示时的问题解决成功率通常低于英文。作者还通过“每个成功任务的期望成本”这一指标衡量成本效率，该指标联合考虑了 token 消耗与任务解决率。鉴于受资源限制，本文评估的模型数量有限、测试基准范围较窄，因此这些发现应被视为初步证据而非定论；它们表明语言对 token 成本的影响具有模型依赖性，而且实践者不应仅仅通过将提示语言切换为中文来预期获得成本节省或性能提升。
软件工程智能体与执行安全
From Procedural Skills to Strategy Genes: Towards Experience-Driven Test-Time Evolution
• 作者：Junjie Wang, Yiming Ren, Haoyang Zhang • arXiv URL：https://arxiv.org/abs/2604.15097
Abstract
这份 beta 技术报告探讨了一个问题：可复用经验应当如何表示，才能既作为有效的测试时控制手段，又作为迭代演化的基础载体。作者在 45 个科学代码求解场景上进行了 4590 次受控试验来研究该问题。结果发现，面向文档的 Skill 包提供的控制不稳定，其有用信号较为稀疏；而且将一个紧凑的经验对象扩展成更完整的文档型 Skill 包通常并不会带来帮助，甚至可能拉低整体平均表现。作者进一步表明，表示形式本身就是一阶因素。紧凑的 Gene 表示在整体平均表现上最强，在较大的结构扰动下仍具竞争力，并优于预算匹配的 Skill 片段；相反，重新附加面向文档的材料通常会削弱而非改善效果。除了单次控制外，作者还表明 Gene 也是更优的迭代经验积累载体：附加失败历史在 Gene 中比在 Skill 或自由文本中更有效，可编辑结构的重要性超越内容本身，而失败信息在被提炼为紧凑警示时最有用，而不是被简单追加。在 CritPt 上，经由 gene 演化的系统相较其配对基础模型，性能分别从 9.1% 提升到 18.57%，以及从 17.7% 提升到 27.14%。这些结果表明，经验复用的核心问题不在于如何提供更多经验，而在于如何将经验编码为紧凑、面向控制、适于演化的对象。
Atropos: Improving Cost-Benefit Trade-off of LLM-based Agents under Self-Consistency with Early Termination and Model Hotswap
• 作者：Naryeong Kim, Shin Yoo • arXiv URL：https://arxiv.org/abs/2604.15075
Abstract
开放权重的小语言模型（SLM）能够以更低的经济成本提供更快的本地推理，但其性能水平未必能够达到规模高出数个数量级的商业大语言模型（LLM）。因此，许多最新的 LLM 应用，例如软件工程智能体，往往只在更大的模型上进行评估，而如何改善此类应用的成本收益权衡这一问题却被忽视。本文提出 Atropos，这是一种预测式提前终止分析与模型热切换技术，旨在提升采用自一致性的 LLM 智能体的成本收益比。Atropos 的核心组件是一个基于 LLM 推理结构特征的预测模型：它先将多条智能体推理路径合并为图表示，再利用图卷积网络（GCN）预测正在进行的推理最终是否会成功。如果某个在源 LLM 上运行的任务实例被预测为将失败，Atropos 随后执行热切换，即将正在进行的推理上下文迁移到能力更强的目标 LLM 上；这之所以可行，是因为 LLM 上下文是无状态的。基于三个近期 LLM 智能体的实证评估表明，Atropos 在推理中点处即可用 0.85 的准确率预测最终会失败的推理，并且通过对这些推理进行 LLM 热切换，最多可将其中 27.57% 转化为成功。最终，Atropos 以仅为封闭式 LLM 成本 23.9% 的代价，实现了其 74.35% 的性能。
SWE-TRACE: Optimizing Long-Horizon SWE Agents Through Rubric Process Reward Models and Heuristic Test-Time Scaling
• 作者：Hao Han, Jin Xie, Xuehao Ma, Weiquan Zhu, Ziyao Zhang, ZhiLiang Long, Hongkai Chen, Qingwen Ye • arXiv URL：https://arxiv.org/abs/2604.14820
Abstract
利用自治智能体解决真实世界的软件工程问题需要复杂的长时程推理。当前流程受到未优化示范数据、稀疏执行奖励以及计算代价过高的推理扩展的共同制约，这些问题会进一步加剧 token 膨胀、奖励黑客行为和策略退化。本文提出 SWE-TRACE（Trajectory Reduction and Agentic Criteria Evaluation），这是一个统一框架，从数据整理、强化学习到测试时推理三个层面共同优化 SWE 智能体生命周期。首先，作者提出一种 LLM 多任务级联方法，利用逐步的 oracle 验证，从 6 万条样本中蒸馏出严格偏向 token 高效、最短路径轨迹的监督微调（SFT）语料。其次，为克服稀疏结果奖励带来的不稳定性，作者设计了一条带有记忆增强的 Agentic RL 流水线，并引入基于 rubric 的过程奖励模型（PRM）。一个辅助性的 Rubric-Agent 会对中间步骤提供稠密且细粒度的启发式反馈，从而引导模型完成长时程任务。最后，作者通过将 PRM 重新用于启发式测试时扩展（TTS），在训练与推理之间建立桥梁。该方法在每一步动态评估并剪枝动作候选，从而在不引入标准并行采样那种延迟开销的情况下实现更高搜索效率。基于标准 SWE 基准的大量实验表明，SWE-TRACE 显著推进了当前最优水平，在最大化问题解决率的同时，大幅降低了 token 消耗与推理延迟。
Bounded Autonomy for Enterprise AI: Typed Action Contracts and Consumer-Side Execution
• 作者：Sarmad Sohail, Ghufran Haider • arXiv URL：https://arxiv.org/abs/2604.14723
Abstract
大语言模型正日益被用作企业软件的自然语言接口，但直接将其用作系统操作者仍然不安全。模型错误可能传播为未授权操作、格式错误请求、跨工作区执行以及其他代价高昂的失败。作者认为，这首先是一个执行架构问题。本文提出一种“有限自主”架构，其中语言模型可以解释意图并提出动作建议，但所有可执行行为都受到类型化动作契约、带权限感知的能力暴露、作用域化上下文、副作用发生前的校验、消费端执行边界以及可选人工审批的约束。企业应用仍然是真实业务逻辑与授权规则的事实来源，而编排引擎则在显式发布的动作清单之上运行。作者在一个已部署的多租户企业应用中，于三种条件下评估该架构：人工操作、关闭安全层的无约束 AI，以及完整有限自主。跨越七类失败家族的 25 个场景试验表明，有限自主系统在零不安全执行的情况下完成了 25 个任务中的 23 个，而无约束配置只完成了 17 个。两次错误实体修改逃过了所有消费端贡献层，仅有消歧与确认机制可以拦截这一类错误。两种 AI 配置都比人工操作快 13 至 18 倍。关键的是，去除安全层反而使系统更难用：结构化验证反馈能够引导模型用更少轮次得到正确结果，而无约束系统则会产生“已成功”的幻觉。若干安全属性由代码结构性保证，且不受模型输出影响地拦截了所有目标违规。结果表明，这是一种能够让不完美语言模型在企业系统中实现可操作价值的务实部署架构。
AIPC: Agent-Based Automation for AI Model Deployment with Qualcomm AI Runtime
• 作者：Jianhao Su, Zhanwei Wu, ShengTing Huang, Weidong Feng • arXiv URL：https://arxiv.org/abs/2604.14661
Abstract
边缘 AI 模型部署是一个多阶段工程过程，涉及模型转换、算子兼容性处理、量化校准、运行时集成和精度验证。在实践中，该工作流流程冗长、容易失败，并且高度依赖部署经验，尤其是在面向特定硬件推理运行时时。本文技术报告提出 AIPC（AI Porting Conversion），这是一种用于 AI 模型部署的、由智能体驱动的受约束自动化方法。AIPC 将部署过程分解为标准化、可验证的多个阶段，并通过 Agent Skills、辅助脚本以及分阶段验证循环，将部署领域知识注入智能体执行过程。这一设计既降低了专业门槛，也减少了硬件部署所需的工程时间。以 Qualcomm AI Runtime（QAIRT）为主要场景，本文考察了代表性视觉、多模态和语音模型的自动化部署。在所覆盖的案例中，对于结构较规则的视觉模型，AIPC 能够在 7 至 20 分钟内完成从 PyTorch 到可运行 QNN/SNPE 推理的部署，且指示性的 API 成本大致在 0.7 至 10 美元之间。对于涉及支持较弱算子、动态形状或自回归解码结构的更复杂模型，完全自动化部署仍需要进一步进展，但 AIPC 已经能够为执行、故障定位和有界修复提供实用支持。
Dive into Claude Code: The Design Space of Today's and Future AI Agent Systems
• 作者：Jiacheng Liu, Xiaohan Zhao, Xinyi Shang, Zhiqiang Shen • arXiv URL：https://arxiv.org/abs/2604.14228
Abstract
Claude Code 是一种面向代码的智能体工具，能够代表用户运行 shell 命令、编辑文件并调用外部服务。本文通过分析其公开可得的 TypeScript 源代码，系统描述了其整体架构，并进一步将其与 OpenClaw 进行比较。OpenClaw 是一个独立的开源 AI 智能体系统，在不同部署场景下对许多相同设计问题给出了回答。作者分析识别出推动该架构形成的五类人类价值、理念与需求，即人类决策权、安全与安保、可靠执行、能力放大和上下文适应性，并将其通过 13 条设计原则追溯到具体实现选择。系统核心是一个简单的 while 循环：调用模型、运行工具、重复迭代。然而，大多数代码实际位于该循环外围的系统之中，包括一个具有七种模式并带有机器学习分类器的权限系统、一条用于上下文管理的五层压缩管线、四种扩展机制（MCP、插件、skills 和 hooks）、一个带工作树隔离的子智能体委派机制，以及面向追加的会话存储。与 OpenClaw 这一多通道个人助理网关的对比表明，当部署环境变化时，相同的反复出现的设计问题会导向不同的架构答案，例如从逐动作安全分类转向边界级访问控制、从单一 CLI 循环转向嵌入式网关控制面的运行时，以及从上下文窗口扩展转向全网关能力注册。最后，作者基于近期的实证、架构与政策文献，提出了未来智能体系统的六个开放设计方向。
Benchmarks for Trajectory Safety Evaluation and Diagnosis in OpenClaw and Codex: ATBench-Claw and ATBench-CodeX
• 作者：Zhonghao Yang, Yu Li, Yanxu Zhu, Tianyi Zhou, Yuejin Xie, Haoyu Luo, Jing Shao, Xia Hu, Dongrui Liu • arXiv URL：https://arxiv.org/abs/2604.14858
Abstract
随着智能体系统进入越来越多样化的执行环境，轨迹层面的安全评估与诊断需要能够随环境演化而扩展的基准。ATBench 是一个用于安全评估与诊断的、多样且贴近现实的智能体轨迹基准。本文报告介绍了 ATBench-Claw 和 ATBench-CodeX，这两个面向 OpenClaw 与 OpenAI Codex / Codex-runtime 场景定制的扩展版本，将 ATBench 带入这两类新环境。其关键适配机制是：分析每个新场景，围绕风险来源、失败模式与现实伤害三个维度定制安全分类体系，然后用该定制化分类体系定义共享 ATBench 构建流水线所消费的基准规范。作者指出，这种可扩展性之所以重要，是因为智能体框架在架构层面相对稳定，而其具体执行环境、工具生态和产品能力却快速变化。具体而言，ATBench-Claw 面向 OpenClaw 中与工具、skills、会话和外部动作相关的敏感执行链；ATBench-CodeX 面向 OpenAI Codex / Codex-runtime 场景中涉及仓库、shell、patch、依赖、审批和运行时策略边界的轨迹。本文重点因此落在共享 ATBench 生成框架下的分类体系定制、领域特定风险覆盖以及基准设计问题上。
CBCL: Safe Self-Extending Agent Communication
• 作者：Hugo O'Connor • arXiv URL：https://arxiv.org/abs/2604.14512
Abstract
智能体通信语言（ACL）使异构智能体能够跨越不同领域共享知识并协同工作。这种多样性要求语言具备可扩展性，但富表达力的扩展机制可能会把输入语言推向那些无法进行完全可判定验证的复杂度类别。本文提出 CBCL（Common Business Communication Language），这是一种将所有消息（包括运行时语言扩展）都约束在确定性上下文无关语言（DCFL）类别内的智能体通信语言。CBCL 允许智能体将领域特定的“方言”扩展作为一等消息进行定义、传输与采纳；三条安全不变量（R1 至 R3）在 Lean 4 中被机器验证，并在 Rust 参考实现中得到强制执行，以防止无界扩展、应用声明的资源限制并保持核心词汇表不变。作者在 Lean 4 中形式化了该语言及其安全性质，在 Rust 中实现了参考解析器与方言引擎，并配备了基于性质和差分测试，同时导出了一个经验证的解析器二进制。结果表明，同像式协议设计，即扩展定义与普通消息共享相同表示形式的设计，可以做到可证明安全。随着自治智能体愈发能够扩展自身的通信能力，对其彼此可表达内容进行形式化约束，是实现监督的前提条件。
编译优化与硬件生成
HintPilot: LLM-based Compiler Hint Synthesis for Code Optimization
• 作者：Hanyun Jiang, Peisen Yao, Kaiyue Li, Tingting Lin, Chengpeng Wang, Kui Ren • arXiv URL：https://arxiv.org/abs/2604.15041
Abstract
代码优化始终是软件开发中的核心目标，但现代编译器在巨大的优化空间中进行搜索时仍面临困难。尽管近期研究开始尝试利用大语言模型（LLM）直接优化源代码，但这类技术可能引入语义错误，也容易错失编译器层面的细粒度优化机会。本文提出 HintPilot，通过综合生成编译器提示（compiler hints）这一方式，把基于 LLM 的推理与传统编译器基础设施连接起来。编译器提示本质上是引导编译器行为的注解。HintPilot 在编译器文档之上进行检索增强式合成，并采用性能分析引导的迭代精炼，以生成既保持语义不变又有效的提示。在 PolyBench 和 HumanEval-CPP 基准上，HintPilot 在保持程序正确性的同时，相对 -Ofast 达到了最高 6.88 倍的几何平均加速比。
Graph-Based ECO and Patch Generation for High-Level Synthesis
• 作者：Alireza Azadi, Paul Rigge, Ethan Mahintorabi, Kenneth B. Kent • arXiv URL：https://arxiv.org/abs/2604.14248
Abstract
高层综合（HLS）工具对工程变更单（ECO）的支持有限，这使得设计后期修改既困难又昂贵。本文提出一种面向 Google XLS 的图方法 ECO 流程。作者使用图编辑距离（GED）算法来检测原始中间表示（IR）与修订后 IR 之间的结构差异，并将这些差异转换为补丁操作。为在保持语义正确性的同时满足 XLS IR 约束，作者开发了一种补丁应用机制，并配套提出一种调度约束方案，以保留原有流水线寄存器。针对若干 XLS 设计的实验表明，该方法具有较高的结构复用率、良好的调度保持效果以及完整的功能正确性，凸显了其在生产级 HLS 流程中的实用性。
Prism: Symbolic Superoptimization of Tensor Programs
• 作者：Mengdi Wu, Xiaoyu Jiang, Oded Padon, Zhihao Jia • arXiv URL：https://arxiv.org/abs/2604.15272
Abstract
本文提出 Prism，这是首个面向张量程序的符号化超级优化器。其核心思想是 sGraph，这是一种符号化、分层式表示，能够通过对部分执行参数进行符号表示，以紧凑方式编码大类张量程序。Prism 将优化组织为两层搜索：先构造代表程序族的符号图，再将其具体化为实际实现。这一表述使得可以利用针对算子语义、代数恒等式和硬件约束的符号推理，对搜索空间中可证明次优的区域进行结构化剪枝。作者为此发展了高效的符号图生成技术、基于 e-graph 重写的等价性验证，以及通过自动调优完成参数实例化的方法。这些组件共同使 Prism 能够在穷举搜索的严谨性与现代机器学习工作负载所需的可扩展性之间搭建桥梁。在五种常用 LLM 工作负载上的评估表明，Prism 相比最佳超级优化器最高可获得 2.2 倍加速，相比最佳基于编译器的方法最高可获得 4.9 倍加速，同时端到端优化时间最高可降低 3.4 倍。
Nautilus: An Auto-Scheduling Tensor Compiler for Efficient Tiled GPU Kernels
• 作者：Yifan Zhao, Yuchen Yang, Matei Budiu, Sasa Misailovic • arXiv URL：https://arxiv.org/abs/2604.14825
Abstract
本文提出 Nautilus，这是一种新的张量编译器，旨在推动从数学描述到高效内核优化的全自动化。Nautilus 将张量算子的高级代数规范编译为高效的分块 GPU 内核。其逐级 lowering 设计使高级优化、表达式重写与分块优化能够在一个端到端系统中联合应用。Nautilus 提出了一种新的自动调度器，可在保留分块优化器所需规则化程序结构的同时，发现高级优化序列。该自动调度器能够捕捉高级优化中的复杂交互与权衡，包括高级归约融合等激进的全局变换。Nautilus 是首个能够从接近数学形式的 attention 描述出发，自动发现类似 FlashAttention-3 内核的端到端张量编译器，将优化负担从程序员完全转移到编译器。在基于 NVIDIA GH200 与 RTX 5090 GPU 的五种 Transformer 模型和 150 个评估配置上，Nautilus 在 GH200 上相对最先进编译器最高提升 23% 吞吐，在 RTX 5090 上最高提升 42%，并且在许多长序列配置上可匹配或超过手写的 cuDNN 内核。
VeriGraphi: A Multi-Agent Framework of Hierarchical RTL Generation for Large Hardware Designs
• 作者：Sazzadul Islam, Tasnim Tabassum, Hao Zheng • arXiv URL：https://arxiv.org/abs/2604.14550
Abstract
为大型分层硬件设计生成可综合的 Verilog，仍然是大语言模型（LLM）面临的一项重要挑战，因为它们难以复制人类专家在将复杂规格转化为 RTL 时所采用的结构化推理方式。当要求生成分层 Verilog 时，LLM 往往会在模块之间丢失上下文、幻觉化接口、伪造模块间连线，并无法保持结构一致性；当设计复杂度增加且规格中包含难以直接操作化的非正式文字、图表和表格时，这些失败会更加严重。为解决这些问题，本文提出 VeriGraphi，该框架引入一个以规格为锚点的知识图谱，作为驱动 RTL 生成流水线的架构基底。VeriGraphi 构建 HDA，一种结构化知识图谱，将模块层级、端口级接口、连线语义以及模块间依赖显式编码为一等图实体与关系。该知识图谱通过对规格进行迭代式多智能体分析而构建，在代码生成之前提供一个确定的、可机器检查的结构支架。在该知识图谱引导下，渐进式编码模块分阶段生成伪代码和可综合 RTL，并在每个子模块阶段强制接口一致性与依赖正确性。作者在来自美国国家标准与技术研究院的三个代表性规格文档及其对应实现构成的基准上进行了评估，并以 RV32I 处理器为详细案例展示完整流水线。结果表明，VeriGraphi 能够以极少人工干预实现可靠的分层 RTL 生成，适用于 RISC-V 场景，并在保持较强功能正确性的同时，为 LLM 生成硬件设计树立了重要里程碑。
程序语言与形式化推理
Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
• 作者：Yusuke Matsushita, Hiromi Ishii • arXiv URL：https://arxiv.org/abs/2604.15290
Abstract
统一函数式与命令式编程范式的一种有前景方法，是利用线性类型或仿射类型将可变性局部化。纯函数式语言 Haskell 近期已被 Bernardy 等人扩展为支持线性类型，即 Linear Haskell。然而，一个问题仍未得到回答：这样的纯语言能否安全地支持 Rust 风格的非局部借用？在这种借用模式中，每个借用者都可以在不直接将所有权返还给出借者的情况下被自由拆分和丢弃。本文通过 Pure Borrow 对此给出肯定回答。Pure Borrow 是一个新框架，在保持纯性的前提下，于 Linear Haskell 中实现了 Rust 风格的借用。值得注意的是，与 IO 和 ST 单子以及现有 Linear Haskell API 不同，它支持在纯计算内部使用仿射可变引用进行并行状态修改。同时，与 Rust 不同，它还保有纯性、惰性求值、一等多态性和无泄漏性。作者将 Pure Borrow 作为一个简单的库实现于 Linear Haskell 之上，并通过并行计算案例研究展示其能力。作者还对 Pure Borrow 的核心进行形式化，并建立元理论，朝着安全性、无泄漏性与合流性的证明迈进，其中包含一种新的、基于历史的借用模型。
Filament: Denning-Style Information Flow Control for Rust
• 作者：Jeffrey C. Ching, Quan Zhou, Danfeng Zhang • arXiv URL：https://arxiv.org/abs/2604.14357
Abstract
现有基于语言的信息流控制（IFC）工具面临一个根本性张力：在变量层面跟踪显式流与隐式流的 Denning 风格系统通常需要修改编译器，而更粗粒度的方法，包括近期的 Cocoon，虽然避免了编译器修改，却施加了更严格的编程模型约束。本文提出 Filament，这是一种 Denning 风格的 Rust 静态 IFC 库，无需任何编译器修改。Filament 解决了构建实用 Rust IFC 库的三个关键挑战。第一，它利用 Rust 的类型推断，以较低标注开销实现细粒度显式流检查。第二，它引入 pc_block! 这一轻量结构，用于通过编译期程序计数器标签来强制隐式流控制，而无需编译器支持。第三，它提供 fcall! 和 mcall! 宏，以支持与标准库及第三方库的无缝且安全的互操作。评估结果表明，Filament 几乎不会带来额外编译时间开销，且只需要适度标注。与 Cocoon 相比，Filament 还提供了更宽松的编程模型，减少了绕过安全检查的逃逸机制被频繁使用的需要。
Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
• 作者：Eden Frenkel, Kenneth L. McMillan, Oded Padon, Sharon Shoham • arXiv URL：https://arxiv.org/abs/2604.15266
Abstract
本文提出一种增量式安全证明方法，它将一个需要复杂归纳不变量的证明分解为一系列更简单的证明步骤。该证明系统结合了三类规则：（i）利用归纳不变量进行前向推理；（ii）利用时间反转系统的归纳不变量进行后向推理；（iii）通过加入对存在量化性质的见证来进行 prophecy 步。作者证明了每条规则的可靠性，并给出一种构造方法，可从增量式证明中恢复出单个安全归纳不变量。该不变量的构造展示了，相较于增量式证明中使用的不变量公式，单一归纳不变量的复杂度更高，因为后者可能具有更简单的布尔结构、更少的量词以及更少的量词交替。在对可用不变量公式施加自然限制的条件下，每条证明规则都会严格提升证明能力。也就是说，在同一组公式下，每条规则都能证明更多安全问题。因此，增量式方法能够缩小为证明给定系统安全性所需搜索的不变量公式空间。针对 Paxos、其若干变体以及 Raft 的案例研究表明，前后向推理步骤可以去除复杂布尔结构，而 prophecy 则能够消除量词及其交替。
Complexity of Fungal Automaton Prediction
• 作者：Enrico Formenti, Eric Goles, Kévin Perrot, Martín Ríos-Wilson, Domingo Ruiz-Tala • arXiv URL：https://arxiv.org/abs/2604.15177
Abstract
真菌自动机是一种受自然启发的计算模型，其中一条规则会在垂直方向和水平方向交替应用。本文研究了所有半径为 1 的真菌冻结型一维 totalistic 规则在动力学预测问题上的计算复杂性，并展示出多种不同的行为。作者证明，在大多数情形下，该问题都可以高效预测，具体可由非确定性对数空间算法解决；但仍有一个非线性规则的刻画问题尚未解决。作者还进一步研究了冻结多数规则（它同样是 totalistic 的），并证明当半径为 1.5 时，对其进行预测会变成 P-完全问题。
Measuring the Computational Power of Finite Patches of Cellular Automata
• 作者：Attila Egri-Nagy, Chrystopher L. Nehaniv • arXiv URL：https://arxiv.org/abs/2604.14966
Abstract
计算能力可以通过为一个计算装置赋予代数结构来衡量。本文将康威生命游戏中的一个小型局部区域转化为一个变换半群。该转化不仅捕捉时间演化，也包含交互式操作，因此使得该元胞自动机能够被直接编程。在完成这一测度后，作者对所得代数对象进行层次化分解，以此作为理解它的方法。这些分解基于受统计力学启发的宏观态/微观态划分。然而，元胞自动机拥有大量全局状态，因此作者将重点放在状态空间划分以及创建态射像近似上，这些近似可作为宏观层面的描述。本文提出的方法并不限于元胞自动机，而是更普遍地适用于离散动力系统。
移动安全、协作质量与教学
Towards Understanding Android APIs: Official Lists, Vendor Customizations, and Real-World Usage
• 作者：Sinan Wang, Qi Zhang, Jiacheng Li, Lili Wei, Yida Tao, Yepang Liu • arXiv URL：https://arxiv.org/abs/2604.14943
Abstract
Android 应用建立在抽象核心 Android 系统功能的 API 之上。这些 API 被正式记录在随 Android 源代码或 SDK 分发的多个文件中，作者将其统称为 Android API Lists（AAL）。以往 Android 研究常依赖某一特定 AAL，并往往将不同 AAL 视为可互换的“真实标准”。然而，近期研究表明，不同 AAL 可能导致显著不同的研究结果，从而引发对基于 Android API 的分析之有效性与可复现性的担忧。为解决这一问题，本文首次对四类在既有研究中被广泛使用的官方 AAL 进行了深入实证研究。作者系统刻画了它们的内容，并分析其在 Android 各版本中的演化。随后，作者对各 AAL 记录的 API 进行细粒度比较，以揭示其背后的 API 纳入策略与不一致性。为评估这些差异的实际影响，作者进一步考察了九台 Android 设备上的 API 可用性，覆盖原生 Android 与厂商定制系统。最后，作者分析了 17759 个真实世界 Android 应用（包括开源应用、商业应用和恶意软件）中的 API 使用情况，以量化 AAL 选择对 Android 实证研究的影响。结果显示，官方 AAL 既不稳定，也彼此不一致，而它们之间的差异会显著影响研究结论。作者还观察到，厂商定制 API 被普通应用积极使用，但现有研究却大多忽视了它们。基于这些发现，本文讨论了其对基于 Android API 研究的启示，并给出可操作建议，以帮助研究者更可靠地选择和解释 AAL。
AndroScanner: Automated Backend Vulnerability Detection for Android Applications
• 作者：Harini Dandu • arXiv URL：https://arxiv.org/abs/2604.14431
Abstract
移动应用依赖复杂后端，而这会引入显著的安全风险；但开发者往往缺乏有效评估这些风险的工具。本文提出 AndroScanner，这是一条通过结合静态分析与动态分析来检测 Android 应用后端漏洞的自动化流水线。AndroScanner 使用 apktool、Androguard 和基于 Frida 的动态插桩，从 APK 文件中提取后端 API 调用，然后借助 APIFuzzer 按照 OWASP API Security Top 10 对这些 API 进行审查。作者在两个 Android 应用上评估了 AndroScanner：一个刻意构造为脆弱的银行应用，以及一个在 Google Play Store 上拥有超过 5 万次下载的生产招聘应用。在这两个应用中，AndroScanner 共提取出 24 个 API，并识别出 5 个漏洞，其中包括生产应用中一个此前未报告的 Excessive Data Exposure 零日漏洞，该漏洞在 OWASP API Security Top 10 中排名第 3。该漏洞已在发表前按负责任披露原则通知开发团队。AndroScanner 可按需提供，以协助开发者在部署前识别并修复后端安全风险。
ToxiShield: Promoting Inclusive Developer Communication through Real-Time Toxicity Filtering
• 作者：MD Awsaf Alam Anindya, Showvik Biswas, Anindya Iqbal, Jaydeb Sarker, Amiangshu Bosu • arXiv URL：https://arxiv.org/abs/2604.14408
Abstract
代码评审中的有毒互动会削弱团队合作，并阻碍软件工程团队的生产效率。尽管先前研究已探索毒性检测与相关实证分析，但仍缺乏能够支持软件工程社区的实时“去毒化”工具。为填补这一空白，本文提出 ToxiShield，这是一款面向 GitHub pull request 的浏览器扩展，由三个模块构成：（i）Toxicity Filter，用于识别文本是否具有毒性；（ii）Communication Coach，用于提供即时、细粒度的毒性类别判定及其解释；（iii）Reframer，用于生成一条经修订的、建设性的替代表达。对于每个模块，作者都训练并评估了多个深度学习模型和大语言模型（LLM），以选出最佳方案。对于 Toxicity Filter 模块，基于 BERT 的二分类检测模型在 38761 条代码评审样本上训练后，达到了 98% 准确率和 97% F1 分数，因此被选中。对于 Communication Coach，经过提示调优的 Claude 3.5 Sonnet 在多类毒性分类中取得最佳表现，MCC 为 39%，F1 为 42%，并能给出详细推理。对于 Reframer，作者在包含 10120 条代码评审评论的数据集上使用微调策略评估了五种 LLM；其中经微调的 Llama 3.2 模型达到了 95.27% 风格迁移准确率、97.03% 流畅度、67.07% 内容保留率和 84% 的 J-score。作者还通过基于技术接受模型、包含 10 名参与者的人类评估对 ToxiShield 进行了验证，结果确认其具有感知上的有用性和易用性。ToxiShield 为推动软件工程中的建设性沟通树立了基准，有助于在开源社区中促进包容性和更健康的协作。
What if we have 90 minutes only to teach programming?
• 作者：Attila Egri-Nagy • arXiv URL：https://arxiv.org/abs/2604.14942
Abstract
自动化编码工具的发展，未来可能会减少愿意学习计算机编程的人数。作者认为，计算性问题求解能力不仅具有直接经济收益，也是我们认识世界的重要组成部分。随着学习激励减弱，作者希望降低入门门槛，并提出一个问题：是否可以在极短时间内教授编程思想？本文描述了一套面向初学者的课程方案，用于介绍编程与计算的基础概念，并且只假设学生具备基本数学背景。该方案采用一种非主流的、函数式且连接式的语言，以减少偶然复杂性。这种语言是范畴论研究的副产物，使学习者能够以有趣、类似解谜的方式，直接接触递归等基础思想以及 Gödel 编码等高级概念。
