目录

智能体安全与执行控制

• • Don't Let AI Agents YOLO Your Files: Shifting Information and Control to Filesystems for Agent Safety and Autonomy
• • Bounded Autonomy for Enterprise AI: Typed Action Contracts and Consumer-Side Execution
• • Benchmarks for Trajectory Safety Evaluation and Diagnosis in OpenClaw and Codex: ATBench-Claw and ATBench-CodeX
• • Atropos: Improving Cost-Benefit Trade-off of LLM-based Agents under Self-Consistency with Early Termination and Model Hotswap
• • From Procedural Skills to Strategy Genes: Towards Experience-Driven Test-Time Evolution

智能软件工程与开发流程

• • Asking What Matters: Reward-Driven Clarification for Software Engineering Tasks
• • AIPC: Agent-Based Automation for AI Model Deployment with Qualcomm AI Runtime
• • SWE-TRACE: Optimizing Long-Horizon SWE Agents Through Rubric Process Reward Models and Heuristic Test-Time Scaling
• • Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Study
• • Towards Understanding Android APIs: Official Lists, Vendor Customizations, and Real-World Usage
• • Applying SHAPR in AI-Assisted Research Software Development: Lessons Learnt from Building a Share Trading System
• • HintPilot: LLM-based Compiler Hint Synthesis for Code Optimization
• • AI-Assisted Requirements Engineering: An Empirical Evaluation Relative to Expert Judgment
• • Enhancing Large Language Models with Retrieval Augmented Generation for Software Testing and Inspection Automation

编程语言、编译与程序优化

• • VeriGraphi: A Multi-Agent Framework of Hierarchical RTL Generation for Large Hardware Designs
• • Nautilus: An Auto-Scheduling Tensor Compiler for Efficient Tiled GPU Kernels
• • What if we have 90 minutes only to teach programming?
• • Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
• • Prism: Symbolic Superoptimization of Tensor Programs
• • Pure Borrow: Linear Haskell Meets Rust-Style Borrowing

形式模型与计算复杂性

• • CBCL: Safe Self-Extending Agent Communication
• • Measuring the Computational Power of Finite Patches of Cellular Automata
• • Complexity of Fungal Automaton Prediction

研究方向：智能体安全与执行控制

Don't Let AI Agents YOLO Your Files: Shifting Information and Control to Filesystems for Agent Safety and Autonomy

• • 作者：Shawn Wanxiang Zhong, Junxuan Liao, Jing Liu, Mai Zheng, Andrea C. Arpaci-Dusseau, Remzi H. Arpaci-Dusseau
• • arXiv URL：https://arxiv.org/abs/2604.13536

Abstract

AI 编码智能体直接在用户文件系统上运行，因此经常发生数据损坏、文件删除以及秘密信息泄露。现有方法被迫在安全性与自主性之间做取舍：不受限制的访问会带来风险，而频繁的权限提示又会给用户增加负担并阻碍智能体执行。为理解这一问题，我们开展了首个关于智能体误用文件系统的系统性研究，分析了 13 个框架中的 290 份公开报告。分析表明，当前智能体对其文件系统影响掌握的信息有限，对这些影响的控制也不足。因此，我们主张将这类信息与控制能力转移到文件系统自身。基于这一原则，我们设计了面向智能体的原生文件系统 YoloFS，并提出三项技术。Staging 在提交前隔离所有修改，从而赋予用户纠正性控制；Snapshots 将这种控制扩展给智能体，使其能够检测并修正自身错误；Progressive permission 则以最少交互对访问进行门控，为用户提供预防性控制。为评估 YoloFS，我们提出一种能够刻画用户—智能体—文件系统交互的新方法。在 11 个带有隐藏副作用的任务中，YoloFS 使智能体在其中 8 个任务上实现自我纠错，同时将所有影响保持在可暂存、可审查状态；在 112 个常规任务上，YoloFS 在与基线成功率相当的同时，需要更少的用户交互。

Bounded Autonomy for Enterprise AI: Typed Action Contracts and Consumer-Side Execution

• • 作者：Sarmad Sohail, Ghufran Haider
• • arXiv URL：https://arxiv.org/abs/2604.14723v1

Abstract

大语言模型正越来越多地被用作企业软件的自然语言接口，但将其直接作为系统操作者仍然并不安全。模型错误可能传播为未经授权的操作、格式错误的请求、跨工作空间执行以及其他代价高昂的故障。我们认为这首先是一个执行架构问题。本文提出一种有界自主架构：语言模型可以解释意图并提出动作建议，但所有可执行行为都受类型化动作契约、具备权限感知的能力暴露、作用域化上下文、副作用前验证、消费者侧执行边界以及可选人工审批的约束。企业应用仍然是业务逻辑与授权的真实来源，而编排引擎则围绕一个显式发布的动作清单运行。我们在一个已部署的多租户企业应用中，在三种条件下评估该架构：人工操作、不受约束且禁用安全层的 AI，以及完整的有界自主。在覆盖七类失效家族的 25 个场景试验中，有界自主系统完成了 25 个任务中的 23 个，且没有一次不安全执行；而不受约束的配置只完成了 25 个中的 17 个。有两次对错误实体的修改逃过了所有由消费者侧提供的防护层；只有消歧与确认机制能够拦截这类情况。两种 AI 条件都相较人工操作实现了 13 至 18 倍加速。关键在于，移除安全层反而让系统更不实用：结构化验证反馈能够引导模型用更少轮次得到正确结果，而不受约束的系统则会幻觉式地宣称成功。若干安全性质由代码在结构上强制执行，并拦截了所有目标违规行为，而不受模型输出影响。结果表明，这是一种使并不完美的语言模型在企业系统中具备实际运行价值的可部署架构。

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.14858v1

Abstract

随着智能体系统进入越来越多样化的执行场景，面向轨迹级安全评估与诊断的基准也需要随之演化。ATBench 是一个用于安全评估与诊断的、多样且贴近真实的智能体轨迹基准。本文报告提出 ATBench-Claw 与 ATBench-CodeX，这两个面向特定领域定制的扩展将 ATBench 分别带入 OpenClaw 以及 OpenAI Codex / Codex-runtime 场景。其核心适配机制是：针对每一种新场景，分析该场景特点，围绕风险来源、失效模式和现实危害定制三维安全分类体系，然后利用这一分类体系定义由共享 ATBench 构建流水线消费的基准规范。之所以需要这种可扩展性，是因为智能体框架在架构层面通常较稳定，但其具体执行场景、工具生态和产品能力却变化很快。具体而言，ATBench-Claw 面向 OpenClaw 场景中涉及工具、技能、会话与外部动作的敏感执行链；ATBench-CodeX 则面向 OpenAI Codex / Codex-runtime 场景中的轨迹，覆盖仓库、Shell、补丁、依赖、审批以及运行时策略边界。本文因此重点强调在共享 ATBench 生成框架之下的分类体系定制、领域特定风险覆盖以及基准设计。

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.15075v1

Abstract

开放权重的小型语言模型（SLM）能够以更低的经济成本提供更快的本地推理，但其性能可能无法达到规模大几个数量级的商业大语言模型（LLM）。因此，软件工程智能体等最新 LLM 应用往往只在较大模型上进行评测，使得如何改善此类应用的成本—收益权衡这一问题被忽视。本文提出 Atropos，一种预测式提前终止分析与模型热切换技术，旨在提升采用自洽性机制的 LLM 智能体的成本—收益比。ATROPOS 的核心组件是一个基于 LLM 推理结构性质的预测模型：在把多个智能体推理路径合并为图表示后，ATROPOS 利用图卷积网络（GCN）预测当前进行中的推理最终是否会成功。若一个在源 LLM 上运行的智能体任务实例被预测为将失败，ATROPOS 随后执行热切换，即把当前推理上下文迁移到能力更强的目标 LLM 上；之所以可行，是因为 LLM 上下文本身是无状态的。基于三个近期 LLM 智能体的实证评估表明，ATROPOS 在推理进行到中点时，就能够以 0.85 的准确率预测那些最终会失败的推理并提前终止。对这类推理执行 LLM 热切换，最高可将其中 27.57% 转化为成功。最终，ATROPOS 以仅 23.9% 的成本，实现了封闭式 LLM 74.35% 的性能。

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.15097v1

Abstract

这份 beta 技术报告探讨：可复用经验应当如何表示，才能既作为有效的测试时控制机制，又作为迭代进化的基础载体。我们在 45 个科学代码求解场景中的 4,590 次受控试验中研究了这一问题。结果发现，以文档为导向的 Skill 包提供的控制并不稳定：其有用信号较为稀疏，而把一个紧凑的经验对象扩展为更完整的文档包往往无助于提升效果，甚至会拉低整体平均水平。我们进一步表明，表示形式本身是一阶因素。紧凑的 Gene 表示在总体平均效果上最强，在经历显著结构扰动时仍具竞争力，并优于与其预算匹配的 Skill 片段；而重新附加面向文档的材料通常会削弱而非增强其效果。除了单次控制之外，我们还表明，Gene 也是更好的迭代式经验积累载体：附加失败历史在 Gene 中比在 Skill 或自由文本中更有效，可编辑结构本身的重要性超越了内容本身，而失败信息在被蒸馏为紧凑警示时最有用，简单追加反而较差。在 CritPt 上，基于 gene 演化的系统相对其配对基础模型分别从 9.1% 提升到 18.57%，以及从 17.7% 提升到 27.14%。这些结果表明，经验复用的核心问题不在于如何提供更多经验，而在于如何把经验编码成一种紧凑的、面向控制且为进化做好准备的对象。

研究方向：智能软件工程与开发流程

Asking What Matters: Reward-Driven Clarification for Software Engineering Tasks

• • 作者：Sanidhya Vijayvargiya, Vijay Viswanathan, Graham Neubig
• • arXiv URL：https://arxiv.org/abs/2604.14624v1

Abstract

人类在指定任务时往往并不完整，因此助手必须知道何时以及如何提出澄清性问题。然而，在软件工程任务中实现有效澄清仍然具有挑战性，因为并非所有缺失信息都同等有价值，而且提问必须指向用户现实中能够提供的信息。我们通过量化哪些类型的信息最会影响任务成功，以及哪些问题能够从模拟用户那里获得有用回答，来研究真实软件工程任务中的澄清行为。借助 Shapley 归因和分布比较，我们识别出有效澄清的两个关键属性：任务相关性（哪些信息能够预测成功）与用户可回答性（用户现实中能够提供什么信息）。我们将这两个属性操作化为多阶段强化学习奖励，并据此训练了一个 80 亿参数的澄清模块 CLARITI。该模块在信息不充分的问题上达到与 GPT-5 相当的解决率，同时提出的问题数量减少了 41%。结果表明，把奖励设计建立在对信息影响和用户可回答性的经验分析之上，能够提升澄清效率。

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.14661v1

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 已经能够为执行、故障定位和有界修复提供实际支持。

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.14820v1

Abstract

利用自治智能体解决真实世界的软件工程问题，需要复杂的长时程推理。当前流水线受制于未优化的示范数据、稀疏的执行奖励以及计算代价高昂的推理扩展，这些问题共同加剧了 token 膨胀、奖励投机以及策略退化。本文提出 SWE-TRACE（Trajectory Reduction and Agentic Criteria Evaluation），这是一个统一框架，从数据整理、强化学习到测试时推理三个方面优化 SWE 智能体生命周期。首先，我们引入一种 LLM 多任务级联方法，利用逐步的 oracle 验证，从 6 万条实例的监督微调语料中蒸馏出严格偏向 token 高效、最短路径轨迹的数据。其次，为克服稀疏结果奖励的不稳定性，我们设计了一个带记忆增强的智能体强化学习流水线，并引入基于评分细则的过程奖励模型（PRM）。辅助性的 Rubric-Agent 会对中间步骤提供稠密、细粒度的启发式反馈，以引导模型完成长时程任务。最后，我们通过把 PRM 重新用于启发式引导的测试时扩展（TTS），打通训练与推理：在每一步动态评估并剪枝动作候选，从而在不引入标准并行采样延迟开销的情况下，实现更优的搜索效率。在标准 SWE 基准上的大量实验表明，SWE-TRACE 在显著降低 token 消耗和推理延迟的同时，显著推进了当前最优水平并最大化了解决率。

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.14867v1

Abstract

Vibe coding 天生假设要通过反馈回路对 LLM 生成的代码进行迭代式改进。尽管这一方式对常规软件任务有效，但其在运行时自适应系统中的可靠性尚不明确，尤其是在生成代码不经过人工检查的情况下。本文研究了对 LLM 生成的集体自适应系统（CAS）中的适应管理器进行基于反馈的自动验证。我们关注“验证在环”中的关键挑战：如何在运行时检测生成代码的失效，以及如何把这些失效精确地报告给 LLM，以便其进行修复。我们将适应循环与 vibe-coding 反馈循环相结合，并依据两类约束检查正确性：其一是通用架构约束，其二是用 Functional Constraints Logic（FCL）形式化的功能约束；FCL 是一种作用于可能有限轨迹上的新型一阶时序逻辑。通过 Dragon Hunt CAS 案例研究，我们表明，细粒度的约束违规能够提供可执行的反馈，通常只需数轮迭代便可得到有效的适应管理器，而简单的粗粒度指标反馈往往会停滞不前。研究结果表明，对于由没有编程技能的领域专家设计的系统而言，反馈精度是实现可靠 vibe coding 的主导因素，从而无需人工进行代码检查。

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.14943v1

Abstract

Android 应用建立在对 Android 核心系统功能进行抽象的 API 之上。这些 API 被正式记录在随 Android 源代码或 SDK 分发的多种文件中，我们统称其为 Android API Lists（AALs）。以往 Android 研究依赖特定的 AAL，且常把它们视作可互换的“真实标准”。然而，近期研究表明，不同 AAL 会导致显著不同的研究结果，从而引发了对基于 Android API 分析之有效性与可复现性的担忧。为解决这一问题，本文首次对四种在既有工作中广泛使用的官方 AAL 展开深入实证研究。我们系统刻画其内容，并分析它们在不同 Android 版本中的演化。随后，我们对每个 AAL 所记录的 API 进行细粒度比较，以揭示其底层的 API 纳入策略与不一致性。为评估这些差异的实际影响，我们进一步考察九台 Android 设备（包括原生 Android 与厂商定制系统）上的 API 可用性。最后，我们分析了 17,759 个真实世界 Android 应用（包括开源应用、商业应用和恶意软件）中的 API 使用情况，以量化 AAL 选择对 Android 实证研究的影响。结果表明，官方 AAL 既不稳定，也彼此不一致，这些差异会显著影响研究结论。我们还观察到，普通应用会主动使用厂商定制 API，但这一现象在既有研究中大多被忽视。基于这些发现，本文讨论其对 Android API 研究的启示，并给出可操作建议，以帮助研究人员更可靠地选择和解释 AAL。

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.15020v1

Abstract

生成式 AI 正在改变研究软件的开发方式，但快速的 AI 辅助开发也可能削弱连续性、可追踪性与方法学清晰度。SHAPR（Solo, Human-centred, AI-assisted PRactice）被提出为一种用于组织 AI 辅助研究软件开发的框架。本文给出了一个将 SHAPR 应用于模块化股票交易系统开发的文档化案例。从项目一开始，研究者便采用了受 SHAPR 启发的工作配置，用以塑造交互、实现和文档组织方式。在迭代式开发周期中，项目生成了结构化证据基础，包括反思笔记、开发周期回顾笔记、事实来源文档、契约、快速捕捉记录、工作流笔记以及不断演化的代码工件。该案例表明，在快速捕捉和 AI 辅助润色的支持下，持续更新文档有助于在整个开发过程中维持有组织且可用的项目知识。研究总结出五条反复出现的经验：契约能够稳定 AI 辅助编码；维护良好的 source-of-truth 层提高了整体一致性；周期边界快照增强了连续性；代码与文档通过快速捕捉和迭代式改进实现共演化；而环境配置本身也会促进知识生成。该案例还展示了一种实用的 SHAPR 运行配置：使用 ChatGPT Project 与按周期划分的对话来支持交互、推理、总结与编码协作，使用 PyCharm 支持工件实现，使用 Obsidian 支持外部工作记忆、结构化文档、反思、连续性以及面向仓库的笔记组织，同时保持与 SHAPR 工具无关原则一致。本文为开展 AI 辅助研究软件开发的研究者提供了实践指导与良好实践。

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.15041v1

Abstract

代码优化始终是软件开发中的核心目标，但现代编译器难以在庞大的优化空间中进行有效搜索。尽管近期研究尝试利用大语言模型（LLM）直接优化源代码，但这类方法可能引入语义错误，并错过编译器层面的细粒度优化机会。本文提出 HintPilot，通过综合编译器提示（即用于引导编译器行为的注解），把基于 LLM 的推理与传统编译器基础设施连接起来。HintPilot 基于编译器文档执行检索增强式合成，并结合基于性能剖析的迭代细化，以合成既保持语义正确又切实有效的提示。在 PolyBench 和 HumanEval-CPP 基准上，HintPilot 在保持程序正确性的同时，相较 -Ofast 实现了最高 6.88 倍的几何平均加速。

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.15222v1

Abstract

人工智能正越来越多地被引入系统工程活动，尤其是在需求工程中，因为需求质量评估与验证在很大程度上仍依赖专家判断。尽管近期 AI 工具在需求分析与生成方面展现出可观能力，但它们在正式系统工程流程中的角色，以及它们与既有 INCOSE 标准的一致性，仍缺乏充分理解。本文研究基于 AI 的工具在多大程度上能够支持系统工程师评估需求质量，而不是取代专业经验。研究采用结构化的系统工程方法，将 AI 辅助的需求评估与人工专家评估进行比较。在一项受控研究中，经验丰富的系统工程师与一套基于 AI 的评估工具，分别依据既有 INCOSE “良好需求”准则对系统需求进行评估。评估重点包括一致性、完整性、清晰性与可测试性，不仅考察准确性，也分析每项评估背后的决策逻辑。结果表明，AI 工具能够提供一致且快速的初步评估，尤其适用于句法与结构层面的质量属性。然而，对于语境解释、歧义消解与权衡推理，专家判断仍然必不可少。研究并不将 AI 定位为系统工程师的替代者，而是支持其在需求工程生命周期中作为决策支持机制发挥作用。从系统工程视角看，本文为如何在保持可追踪性、问责性与工程一致性的同时，将 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.15270v1

Abstract

本文关注软件开发生命周期（SDLC）中两类被广泛使用的验证与确认（V&V）活动的自动化：软件测试和软件检查（亦即代码审查）。对于前者，我们聚焦于利用大语言模型（LLM）自动生成测试用例；对于后者，我们使 LLM 能够对源代码进行检查。为应对 LLM 已知的幻觉问题——即模型会高置信地产生错误输出——我们实现了一条检索增强生成（RAG）流水线，以整合补充性知识源并为 LLM 提供额外上下文。实验结果表明，通过 RAG 流水线引入外部上下文，对测试用例生成与代码检查总体上都具有积极影响。这种新方法通过节省人工测试人员/检查人员的时间来降低项目总成本；同时，实验研究也表明，它提升了这些 V&V 活动的效果与效率。

研究方向：编程语言、编译与程序优化

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.14550v1

Abstract

对于大型分层硬件设计，生成可综合的 Verilog 仍是大语言模型（LLM）面临的一项重大挑战，因为它们难以复现人类专家在把复杂规格转化为 RTL 时所采用的结构化推理。当任务要求生成分层 Verilog 时，LLM 往往会在模块之间丢失上下文、幻觉出接口、虚构模块间连线，并且无法保持结构一致性；而随着设计复杂度上升、规格中包含难以直接操作化的非正式文本、图和表，这些问题会进一步加剧。为解决这些挑战，我们提出 VeriGraphi，一个将以规格为锚点的知识图谱引入为 RTL 生成流水线架构基础的框架。VeriGraphi 构建 HDA——一种结构化知识图谱——将模块层级、端口级接口、连线语义以及模块间依赖关系显式编码为一等图实体与关系。该知识图谱通过对规格进行迭代式多智能体分析构建，在代码生成之前提供了一个确定性的、可机器检查的结构支架。在知识图谱引导下，渐进式编码模块逐步生成伪代码和可综合 RTL，并在每个子模块阶段强制保证接口一致性与依赖正确性。我们在由美国国家标准与技术研究院的三个代表性规格文档及其对应实现构成的基准上评估 VeriGraphi，并以 RV32I 处理器为详细案例展示完整流程。结果表明，VeriGraphi 能够以极少人工干预实现面向 RISC-V 的可靠分层 RTL 生成，在保持较强功能正确性的同时，为 LLM 生成硬件设计树立了一个重要里程碑。

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.14825v1

Abstract

本文提出 Nautilus，这是一种推动从数学描述到内核优化全自动化的新型张量编译器。Nautilus 将张量算子的高层代数规格编译为高效的分块 GPU 内核。其逐级 lowering 设计使高层优化、表达式重写以及分块优化能够在一个端到端系统中联合应用。Nautilus 提出了一种新型自动调度器，能够发现高层优化序列，同时保持分块优化器所需的规则程序结构。该自动调度器能够捕获高层优化中的复杂交互与权衡，包括诸如高级归约融合之类的激进全局变换。Nautilus 是首个端到端张量编译器，能够从类似数学公式的 attention 描述出发，自动发现类似 FlashAttention-3 的内核，把全部优化负担从程序员转移给编译器。在基于 NVIDIA GH200 与 RTX 5090 GPU 的五个 Transformer 模型和 150 个评测配置上，Nautilus 在 GH200 上的吞吐量最多比最先进编译器高 23%，在 RTX 5090 上最多高 42%，并且在许多长序列配置上与手写 cuDNN 内核持平或更优。

What if we have 90 minutes only to teach programming?

• • 作者：Attila Egri-Nagy
• • arXiv URL：https://arxiv.org/abs/2604.14942v1

Abstract

自动化编码工具的发展，未来可能会降低人们学习计算机编程的意愿。我们认为，计算性问题求解能力不仅具有直接经济收益，而且是人类理解世界的重要组成部分。随着学习动机减弱，我们希望降低入门门槛。于是我们提出问题：能否在极短时间内教授编程思想？本文描述了一个面向初学者的课程方案，用于介绍编程与计算基础，只假设学习者具备基础数学背景。该方案要求使用一种非主流的、函数式且连接式的语言，以减少偶然复杂性。该语言源于范畴论研究的副产物，能够以一种富有娱乐性、类似解谜的方式，让学习者直接接触诸如递归这样的基础思想，以及如哥德尔编码这样的进阶概念。

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.15266v1

Abstract

本文提出一种用于安全性证明的增量式方法，把一个需要复杂归纳不变式的证明分解为一系列更简单的证明步骤。我们的证明系统结合了三类规则：(i) 使用归纳不变式的前向推理；(ii) 使用时间反演系统归纳不变式的后向推理；以及 (iii) 通过为存在量化性质增加见证的 prophecy 步骤。我们证明了每条规则的正确性，并给出一种构造方法，能够从增量式证明中恢复出单一的安全归纳不变式。该不变式的构造表明，与增量式证明中所使用的不变式公式相比，单一归纳不变式的复杂度更高：前者往往可以具有更简单的布尔结构，以及更少的量词和量词交替。在对可用不变式公式施加自然限制的条件下，每条规则都能严格提升证明能力，也就是说，在相同公式集合下，每条规则都能证明更多安全性问题。因此，这种增量式方法能够减少证明给定系统安全性所需搜索的不变式公式空间。针对 Paxos、若干变体以及 Raft 的案例研究表明，前向—后向步骤能够移除复杂的布尔结构，而 prophecy 能够消除量词及量词交替。

Prism: Symbolic Superoptimization of Tensor Programs

• • 作者：Mengdi Wu, Xiaoyu Jiang, Oded Padon, Zhihao Jia
• • arXiv URL：https://arxiv.org/abs/2604.15272v1

Abstract

本文提出 Prism，这是首个面向张量程序的符号超优化器。其核心思想是 sGraph——一种符号化、层次化表示，可通过对部分执行参数进行符号表示来紧凑编码大类张量程序。Prism 将优化组织为两层搜索：先构建表示程序族的符号图，再将其具体化为实际实现。该形式化使得可以基于算子语义、代数恒等式和硬件约束的符号推理，对可证明次优的搜索空间区域进行结构化剪枝。我们提出了高效符号图生成、基于 e-graph 重写的等价性验证，以及通过自动调优进行参数实例化等技术。这些组件共同使 Prism 在穷举搜索的严谨性与现代机器学习工作负载所要求的可扩展性之间建立桥梁。在五种常用 LLM 工作负载上的评测表明，Prism 相较最佳超优化器可实现最高 2.2 倍加速，相较最佳基于编译器的方法可实现最高 4.9 倍加速，同时端到端优化时间最多降低 3.4 倍。

Pure Borrow: Linear Haskell Meets Rust-Style Borrowing

• • 作者：Yusuke Matsushita, Hiromi Ishii
• • arXiv URL：https://arxiv.org/abs/2604.15290v1

Abstract

一种有前景的函数式与命令式编程范式统一路径，是利用线性类型或仿射类型把可变性局部化。纯函数式语言 Haskell 近期由 Bernardy 等人扩展出了线性类型，形成所谓 Linear Haskell。然而，此前尚不清楚这样一种纯语言能否安全地支持 Rust 风格的非局部“借用”：在这种机制下，每个借用者都可以自由拆分和丢弃，而无需把所有权直接传回出借者。本文对此给出肯定回答，并提出 Pure Borrow——一种在保持纯性的前提下，在 Linear Haskell 中实现 Rust 风格借用的新框架。值得注意的是，与 IO、ST monad 以及现有 Linear Haskell API 不同，它能够在纯计算内部使用仿射可变引用实现并行状态修改；同时，与 Rust 不同，它还保有纯性、惰性求值、一等多态性以及无泄漏性。我们将 Pure Borrow 简单实现为 Linear Haskell 中的一个库，并通过并行计算案例研究展示其能力。我们形式化了 Pure Borrow 的核心，并构建了一套元理论，以逐步建立其安全性、无泄漏性与合流性，其中引入了一种新的、基于历史的借用模型。

研究方向：形式模型与计算复杂性

CBCL: Safe Self-Extending Agent Communication

• • 作者：Hugo O'Connor
• • arXiv URL：https://arxiv.org/abs/2604.14512v1

Abstract

智能体通信语言（ACL）使异构智能体能够在多样化领域中共享知识并进行协同。这种多样性要求语言具有可扩展性，但表达能力很强的扩展机制可能会把输入语言推向无法进行完全验证的复杂度类别之外。本文提出 CBCL（Common Business Communication Language），一种将所有消息——包括运行时语言扩展——都限制在确定性上下文无关语言（DCFL）类别内的智能体通信语言。CBCL 允许智能体把特定领域的“方言”扩展定义、传输并采纳为一类一等消息；三条安全不变式（R1--R3）在 Lean 4 中经过机器检验，并在 Rust 参考实现中得到执行，用于防止无界扩张、施加已声明的资源限制并保持核心词汇。我们在 Lean 4 中形式化了该语言及其安全性质，在 Rust 中实现了参考解析器和方言引擎，并结合基于性质的测试与差分测试，进一步提取出经过验证的解析器二进制文件。结果表明，同像式协议设计——即扩展定义与普通消息共享同一种表示形式——可以做到可证明安全。随着自治智能体越来越多地扩展自身通信能力，形式化地界定它们彼此之间可表达的内容，是实现监督的前提。

Measuring the Computational Power of Finite Patches of Cellular Automata

• • 作者：Attila Egri-Nagy, Chrystopher L. Nehaniv
• • arXiv URL：https://arxiv.org/abs/2604.14966v1

Abstract

可以通过为计算装置赋予一种代数结构来度量其计算能力。本文把 Conway 生命游戏的一个小型局部块转换为一个变换半群。这一转换不仅刻画时间演化，也刻画交互式操作。通过这种方式，元胞自动机变得可以被直接编程。在完成这种度量之后，我们将层次化分解应用于所得代数对象，以作为理解该对象的一种手段。这些分解建立在受统计力学启发的宏观/微观状态划分之上。然而，元胞自动机具有数量巨大的全局状态，因此我们重点关注状态空间的划分，并构造可作为宏观层描述的态射像近似。本文提出的方法并不限于元胞自动机，而是更普遍地适用于离散动力系统。

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.15177v1

Abstract

真菌自动机是一类受自然启发的计算模型，其中某条规则会在垂直方向与水平方向交替应用。本文研究所有半径为 1 的真菌冻结全计数一维规则在动态预测上的计算复杂性，并展示了其多种行为。尽管在大多数情况下，该问题可以高效预测（可用非确定性对数空间算法解决），但仍有一条非线性规则的刻画尚未解决。我们还进一步研究了冻结多数规则（它也是全计数规则），并证明当半径为 1.5 时，其预测问题变为 P-完全。