公开论文雷达

公开 arXiv 研究简报 · 2026-07-28T15:27:01.440604+00:00

先看结论和关键数字,再决定要不要读原文。页面只基于公开论文内容生成。

五张卡的共同题眼:评测怎么做决定结论

五张卡横跨智能体记忆、缺陷修复、形式化规格与实证研究,但共同题眼是评测可信度。建议先读TLA+-Bench感受评测脆弱,再看CoHarden如何收紧信号,用MemTools隔离变量,SCM学会克制解读,最后用PR实证卡住落地边界。

推荐阅读顺序

  1. 2607.23425:最直观地证明评测不可信:只改三项设置正确率差11倍,先建立这层怀疑再看其余几篇。
  2. 2607.19843:把同一教训落到修复上:F→P太松会放行错补丁,用突变存活信号收紧,给出69.4%的确定结果。
  3. 2607.21404:提供隔离评测变量的工具:声明式契约让跨系统组件可互换,帮你判断性能差异的真源。
  4. 2607.19096:记忆路由架构,难得地主动划出证据边界:分数可复现但路由因果未确立,读它学会克制解读。
  5. 2607.21832:从489仓库真实PR看智能体到底在哪好用:窄范围明确任务合并率更高,用来卡住落地预期。
共性方法
五篇都在质疑单一数字:F→P、文本相似度、基准总分都可能骗人。应对方式或是改用执行验证(模型检验器、突变存活),或把评测变量显式枚举、报告区间,或主动声明哪些结论证据不足——核心都是让测量可被复核。
关键分歧
分歧在证据成熟度与姿态:CoHarden给出可复现的确定增益;TLA+-Bench反过来证明数字本身不稳定;MemTools不公布定量值;SCM分数可复现却声明路由因果未确立;PR研究是纯观测、无干预。从'我证明了'到'我不敢下结论'各不相同。
选择准则
要比较或报告分数,先读TLA+-Bench核对评测设置;要在修复流水线筛测试用CoHarden;选记忆架构看MemTools与SCM;评估智能体落地看PR实证。

重点深读(5 / 5 篇)

形式化与程序验证(1 篇)

形式化与程序验证 7/30

TLA$^{+}$-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA+ Specification Generation

执行验证揭示LLM生成TLA+正确率相差11倍:TLA+-Bench使用TLA+模型检验器做全状态空间遍历作为评分标准,构建403条黄金规格基准。仅改变三项评测选项,同一批模型输出的正确率出现11倍的差距,最强模型也仅达到26%。

两句看懂

现有TLA+评测依赖文本相似度或语法解析,无法判断规格的行为正确性;TLA+-Bench改为调用模型检验器对403条黄金规格做全状态空间精确判定。固定模型输出后仅调整三项评测选项,正确率从1.7%到18.7%相差11倍,最强模型给定接口名时达26%,开源模型至多1%。

核心判断

LLM生成TLA+规格不存在单一正确率数字:评测选项不同导致11倍区间(1.7%—18.7%);固定选项后最强模型给定接口名正确率26%,开源不超过1%,可执行验证是必要的评分标准。

关键要点

1. TLA+-Bench收录1,300条规格(403条黄金、897条银级),黄金规格均配套可运行配置,TLA+模型检验器对全可达状态空间做属性满足精确判定,取代文本相似度近似评分。 2. 固定同一批模型输出,仅改变接口名供给、初始状态过滤和属性有效性三项评测选项,正确率在1.7%至10.0%间六倍波动;引入接口供给维度后区间扩至11倍(1.7%—18.7%)。 3. 最强闭源模型默认正确率16%、给定接口名升至26%;开源模型至多1%;所有模型语法合法率远高于语义正确率,且正确率随难度标签上升急剧下降。

证据与结果

在403条黄金规格上评测主流LLM:仅改变三项评测选项,同一输出正确率六倍波动(1.7%10.0%);加接口名供给后11倍(1.7%18.7%);最强闭源模型默认16%、给接口名26%;开源模型至多1%;正确率随难度标签上升急剧下降。

打开论文原文
它要解决什么
如何用可判定的执行预言机精确衡量LLM将自然语言描述转化为TLA+形式规格的能力?
研究路径
从13个公开仓库提取规格,为403条精确配置运行环境;对模型输出调用TLA+模型检验器遍历全可达状态空间,做属性满足的二元判定;系统枚举接口名供给、初始状态有效性、属性有效性三个评测变量的组合,分别测量上下界,定义正确率包络。
这对工程意味着什么
具体动作:复现或引用形式规格评测时,核查并公开接口供给和属性过滤两项设置。常见误解:不能因模型输出语法合法就认为其行为语义正确。
证据定位
固定同一批模型输出,仅改变三项评测选项,正确率在1.7%至10.0%之间六倍波动;加入接口名供给选项后区间扩大到11倍(1.7%18.7%)。最强闭源模型默认正确率16%,给定接口名后升至26%;开源模型最高仅1%。(筛选维度:形式化验证、可复核评测)
适用边界
897条银级规格仅做语法验证,没有执行检验;黄金规格来自公开仓库,可能与模型训练数据重叠。
方法与英文摘要

为403条黄金规格配备可运行配置,调用TLA+模型检验器遍历全部可达状态空间,对模型生成的规格做属性满足的精确判定。同时系统枚举三项评测选项(接口名供给、初始状态过滤、属性有效性)的不同组合,测量正确率的上下界区间。

Large language models increasingly write TLA$^{+}$ formal specifications from natural-language descriptions, but progress is hard to measure: existing resources grade by resemblance to a reference or by whether the output parses, neither of which shows correctness. We present TLA$^{+}$-Bench, a dataset and benchmark that grades by execution. Every gold specification ships a configuration the TLA$^{+}$ model checker runs over the full reachable state space, deciding exactly whether the specification holds the properties that configuration names. The dataset holds 403 model-checked gold and 897 parse-only silver specifications from 13 public repositories, subsumes prior TLA$^{+}$ generation data, and carries four model-written descriptions in two styles from two providers, with difficulty and category labels. Our main finding is about measurement itself: an exact oracle gives not one correctness number but a range. Varying only the grading choices earlier benchmarks leave unstated, on one fixed set of model outputs, the correct rate moves sixfold, from 10.0\% to 1.7\%; adding the interface-supply choice, where the model is told the configuration's names, widens the range to elevenfold, from 18.7\% to 1.7\%. We call this range the correctness envelope and measure each of its bounds. The findings inside it are stable. Every model writes valid TLA$^{+}$ far more often than correct TLA$^{+}$: the strongest is correct 16\% of the time by default and 26\% when given the interface names, open models at most 1\%, and correctness falls sharply with difficulty.

软件工程与仓库智能(2 篇)

软件工程与仓库智能 8/30

Beyond Fail-to-Pass: Iterative Hardening of Co-Generated Bug Reproduction Tests and Fixes

迭代强化共生成测试修复超越F→P标准:现有APR系统以F→P为BRT唯一质量标准,宽松测试致使错误补丁通过验证;CoHarden以突变存活信号迭代强化测试与修复,在SWE-bench Verified达69.4% Resolved。

两句看懂

现有APR系统仅凭F→P标准评估BRT,部分通过的测试仍接受错误补丁,共生成中还存在测试与修复双错互掩的耦合问题;CoHarden以宽松信号为迭代收敛条件强化测试与修复。在SWE-bench Verified上达69.4% Resolved,超纯修复基线+9.6pp、共生成基线+7.9pp。

核心判断

F→P标准不足以保证BRT能约束修复方向,宽松测试会接受语义错误补丁。以宽松信号驱动迭代强化后,SWE-bench Verified上Resolved率达69.4%,证明该方案有效。

关键要点

1. F→P标准存在宽松测试漏洞:部分通过fail-to-pass的BRT只验证输出不同于已知错误字符串,仍可接受语义错误补丁;实验证明宽松BRT不能持续提升下游修复成功率,仅严格BRT可以。 2. 共生成中存在测试-修复错误耦合:生成补丁与生成测试同时出错时,轨迹内F→P检查仍可通过,掩盖双重错误;引入突变补丁存活检测(宽松信号)可打破此耦合。 3. CoHarden以宽松信号为迭代收敛条件:循环持续至测试不再接受存活突变补丁,在SWE-bench Verified达69.4% Resolved、78.9% F→P,相比最强共生成基线提升+7.9pp。

证据与结果

基准:SWE-bench Verified;指标:Resolved率与F→P率。结果:69.4% Resolved、78.9% F→P;较最强纯修复基线+9.6pp Resolved;较最强共生成基线+7.9pp Resolved;结论在多种LLM主干和多个基准上均一致复现。

打开论文原文
它要解决什么
仅凭fail-to-pass标准能否可靠筛选出真正有助于下游自动修复的Bug复现测试?
研究路径
执行顺序:①从issue描述生成BRT,确认其在有缺陷代码上失败;②生成候选补丁并通过F→P检查;③对存活突变补丁运行BRT,若测试接受突变补丁则宽松信号触发,重新强化测试;④重复②③直至BRT不再接受任何存活突变补丁,输出最终测试与修复对。
这对工程意味着什么
行动:在APR系统中引入宽松检测(突变存活信号)替换单一F→P收敛标准;误区:不要认为fail-to-pass测试已足够严格、可直接可靠地指导修复方向。
证据定位
SWE-bench Verified上达69.4% Resolved、78.9% F→P,超最强纯修复基线+9.6pp、共生成基线+7.9pp,结论在多LLM主干和多基准上均复现。(筛选维度:可复核评测、软件工程方法)
适用边界
突变测试增加计算开销;论文未量化每次迭代循环的平均轮次及总体计算成本增幅。
方法与英文摘要

CoHarden先生成BRT确认其在有缺陷代码上失败,再以存活突变补丁触发宽松信号,循环强化测试与修复,直至测试不再接受宽松回归。

Large language models (LLMs) have made automated program repair (APR) increasingly practical for real-world bugs, but repairing directly from bug reports remains underconstrained. Bug reproduction tests (BRTs) help close this gap by turning a bug report into an executable, bug-specific signal that can guide repair and validate candidate patches. Existing work has therefore studied BRT generation as a core subproblem in APR and mainly evaluates a generated BRT using the fail-to-pass (F->P) criterion, which requires the test to fail on the buggy code but pass on the golden fix. We show that F->P alone is insufficient when the goal of a BRT is to improve downstream repair. In particular, some F->P BRTs are lax, reproducing the observed symptom yet still admitting plausible-but-incorrect patches. We formalize this missing quality dimension by separating F->P BRTs into rigorous and lax ones, and show empirically that only the former consistently improve repair success. We further find that co-generation introduces test--fix error coupling, where the in-trajectory fail-to-pass (F->P) check can pass even when both the generated patch and generated test are wrong. Based on these findings, we propose CoHarden, a co-generation framework that uses the Lax signal as an in-loop convergence criterion. CoHarden first generates a test before any fix, then iteratively hardens the test and fix against surviving mutation patches until the generated test no longer admits Lax regressions. Experiments show that CoHarden reaches 69.4% Resolved and 78.9% F->P on SWE-bench Verified, outperforming the strongest fix-only and cogeneration baselines by +9.6 and +7.9 percentage points in Resolved, respectively, with consistent gains across LLM backbones and benchmarks.

软件工程与仓库智能 7/30

How Do AI Coding Agents Contribute to Software Development? an Empirical Study of Agentic Pull Requests

AI编程智能体PR质量与演变的实证研究:对489个Python仓库的220,612条PR进行纵向分析,比较五种AI编程智能体与人类开发者在合并率、任务类型及缺陷诱发上的差异,覆盖9,428条智能体PR。

两句看懂

既往研究未能纵向量化AI智能体PR对软件质量的影响,本研究对489个Python仓库的220,612条PR展开跨生命周期分析。通过2,275对平衡样本对比变更、审查与缺陷特征,发现智能体合并率因工具而异但在各开发阶段基本稳定,窄范围任务合并率更高。

核心判断

AI智能体PR合并率在各工具间有差异但随项目生命周期总体稳定,窄范围定义明确的任务是智能体最有效场景;结论来自2,275对平衡样本的纵向对比。

关键要点

1. 数据集涵盖489个Python仓库共220,612条PR,其中9,428条来自五种主流编程智能体,发现各工具合并率存在差异,但在开发生命周期各季度阶段保持相对稳定。 2. 智能体PR集中于重复性、结构化任务;语义范围窄且定义明确的任务合并率更高、更稳定,而需大量改动的任务合并率偏低。 3. 以2,275对平衡样本量化对比变更规模、审查轮次和缺陷诱发提交关联,为智能体贡献的实际质量提供可复核的纵向基线。

证据与结果

数据覆盖489个Python仓库、220,612条闭合PR,其中9,428条为五种智能体生成;平衡样本各2,275条;指标包含合并率、任务类型分布和缺陷诱发提交关联;按开发生命周期季度纵向追踪合并率演变。

打开论文原文
它要解决什么
AI编程智能体PR与人类PR在合并率、任务类型和软件质量关联上是否存在可量化的系统性差异?
研究路径
从489个Python仓库提取PR与提交层级数据,按季度划分开发生命周期阶段并逐阶段统计各智能体合并率;再构建2,275对平衡合并样本,对比变更规模、审查轮次与缺陷诱发提交的关联程度。
这对工程意味着什么
将智能体部署于语义明确的窄范围任务可获最高合并率;不可假设智能体质量会随项目成熟自动提升——实证显示合并率在生命周期内基本持平。
证据定位
智能体PR合并率因工具而异但在生命周期各阶段相对稳定;窄范围、语义明确任务的合并率高于需大量改动的任务。(筛选维度:可复核评测、软件工程方法)
适用边界
数据仅限Python仓库,摘录未展示缺陷诱发分析的具体数字,结论外推至其他编程语言或仓库类型需谨慎。
方法与英文摘要

以489个仓库的220,612条闭合PR做纵向分析;按开发生命周期季度追踪合并率;以2,275对平衡样本对比变更规模、审查特征和缺陷诱发关联。

Recent advances in large language models and their rapid adoption across software engineering tasks have made Artificial Intelligence (AI) coding agents an integral component of modern software development workflows. While developers increasingly benefit from these coding agents, their impact on software quality remains insufficiently understood. In particular, how agentic contributions evolve across the software development lifecycle has not been thoroughly investigated. This study aims to characterize agentic pull requests (PR) in comparison to human generated PRs and to examine how their properties change across different stages of the development lifecycle. Using the AIDev dataset, we first analyze how differences in merge rates between agentic and human generated PRs vary over time. We then identify the types of development tasks where AI coding agents are predominantly applied and investigate how these task distributions evolve across development quarters. Finally, we compare a set of key characteristics of agentic and human generated PRs, focusing on their implications for software quality and their temporal dynamics. Overall, our findings provide an empirical and longitudinal perspective on the role of AI coding agents in software development, offering a more nuanced understanding of their benefits and limitations in real-world practices.

代码质量与优化(0 篇)

本轮没有通过深读证据门的重点论文。

UI 与 GUI Agent(0 篇)

本轮没有通过深读证据门的重点论文。

个人知识与本体(2 篇)

个人知识与本体 8/30

MemTools: A Unified Research Framework for Interoperable Agent Memory

可插拔智能体记忆框架:用声明式契约解耦生命周期与评测:现有记忆系统架构碎片化:组件紧耦合、评测引入执行逻辑偏差、异构记忆难以协同。该框架用声明式数据契约定义组件接口,用可插拔评测协议分离执行逻辑,使得不同系统的组件可以互换安装,且评测结果更可控。

两句看懂

现有记忆系统将生命周期、评测逻辑与数据集深度耦合,导致无法隔离设计变量且评测结果受执行逻辑偏差干扰。该框架通过声明式数据契约和可插拔评测协议解耦这三层,跨系统组件互换实验显示替换组件性能达到或超越原生设计。

核心判断

声明式数据契约与可插拔评测协议可系统隔离记忆设计变量。跨系统组件互换后性能不低于原生,异构记忆协调带来互补增益。

关键要点

1. 声明式数据契约定义记忆生命周期各阶段的输入输出字段,匹配引擎自动枚举合法组件组合,实现不同系统部件的即插即用,无需手动代码集成。 2. 基准数据集与执行协议正交分离,同一数据集可在多种评测工作流下运行;隔离执行逻辑后,操作时序对性能影响显著,揭示跨系统比较中隐藏的评测协议偏差。 3. 统一计算接口在共享运行时内协调符号数据库、神经参数、多模态记录三类记忆表示;异构记忆协调实验显示不同表示类型提供互补性能增益。

证据与结果

在跨系统组件集成、评测协议重配置、异构记忆协调三个场景上验证性能。指标包括:组件互换后与原生设计的性能对比、切换评测协议后的性能变化、异构记忆类型组合的性能增益。该文未披露具体基准任务名称和定量数值。

打开论文原文
它要解决什么
架构碎片化如何阻碍智能体记忆系统研究?能否用统一框架隔离各设计变量,系统分析其影响?
研究路径
声明式数据契约定义每个组件的提供字段与所需字段;匹配引擎逐一校验字段兼容性并枚举合法管道组合。评测协议接口将执行逻辑抽象为可插拔模块,同一数据集可在不同工作流下处理。统一计算接口在共享运行时内注册并路由符号、神经、多模态三类记忆操作。
这对工程意味着什么
具体行动:第一步,为每个记忆组件定义声明式数据契约,确保接口兼容。误区:不要将评测工作流的差异(如操作时序)误认为记忆能力本身的差异。
证据定位
跨系统组件互换实验:替换组件后性能达到或超越原生设计。隔离评测逻辑实验:操作时序对性能有关键影响,揭示跨系统比较中存在协议偏差。异构记忆协调实验:不同记忆表示类型带来互补性能增益。(筛选维度:形式化验证、可复核评测)
适用边界
该文未公开具体基准任务名称和定量数值;组件兼容性校验的边界条件及匹配失败处理方式未详述。
方法与英文摘要

首先,声明式数据契约标准化记忆生命周期每个阶段(形成、存储、检索、演化、利用)的输入输出字段,匹配引擎自动校验字段兼容性并枚举合法管道组合。其次,将基准数据集与执行协议正交分离,同一数据集可在多种评测工作流下运行。

While memory systems are essential for agent architectures, pervasive architectural fragmentation restricts systematic research. Existing implementations typically couple different stages of the memory lifecycle, entangle evaluation logic with specific datasets, and provide limited support for the management of heterogeneous memory types. We introduce MemTools, an interoperability research framework that decouples memory system components from their underlying deployment environments. MemTools standardizes the memory lifecycle through declarative data contracts, enabling the interchangeable assembly of components across different systems. It orthogonally separates benchmark datasets from execution protocols to facilitate controlled assessments. Furthermore, MemTools provides a unified computational interface for coordinating symbolic, neural, and multimodal memory representations within a shared runtime. Empirical evaluations on cross-system component integration, evaluation protocol reconfiguration, and heterogeneous memory coordination demonstrate that MemTools enables systematic isolation and analysis of memory design variables. These findings suggest that MemTools provides a practical and extensible infrastructure for advancing principled research on agent memory.

个人知识与本体 7/30

Supra Cognitive Modes: A Routed Architecture for Agent Memory

SCM:面向异构记忆查询的路由架构:SCM用冻结语义分类器按语义标签将记忆查询路由至融合检索、图多跳或分层合成;LoCoMo 84.87%、MAB 61.49%、LongMemEval 86.00%,但路由因果效应未确立。

两句看懂

单一检索策略无法同时应对直接事实查询、多跳推理与长历史综合,SCM以冻结语义分类器将每次查询路由至对应执行路径。在LoCoMo、MAB、LongMemEval三项基准上,参考运行分别得84.87%、61.49%、86.00%,仓库复现产生相近分数并支持失败分层分析。

核心判断

不同形态记忆查询需要不同检索与合成策略;SCM以冻结分类器和运行时门控实现每次查询路由,三项基准复现提供诊断特征,但路由因果贡献尚未被隔离。

关键要点

1. SCM定义模式—载荷—过程接口:查询可显式指定或自动选择语义标签,运行时门控调度至融合检索、图多跳或分层合成路径,而非为整个部署固定单一策略。 2. 共用摄入基底含多粒度嵌入、提取三元组与事实版本元数据;LoCoMo事实类84.87%、对抗弃答68.61%,MAB两次重复61.49%,LongMemEval 86.00%。 3. 论文明确列出证据边界:缺原始基线输出、对齐端到端计时与令牌账本,路由因果效应与统计显著性均在可用证据之外。

证据与结果

三项基准:LoCoMo(n=1,986)、MAB(n=3,671)、LongMemEval(n=500)。参考运行:LoCoMo事实类84.87%、对抗弃答68.61%;MAB两次重复61.49%;LongMemEval 86.00%。仓库复现得相近总分;缺原始基线输出、端到端计时和令牌账本,统计显著性未报告。

打开论文原文
它要解决什么
单一检索策略能否同时满足直接事实查询、多跳推理与长历史综合三类异构记忆需求?
研究路径
摄入时构建共用基底(多粒度嵌入、提取三元组、事实版本元数据、可选异步缓存);查询时冻结语义分类器选取模式标签,运行时门控判断是否触发多跳;最终分发至融合词法/密集检索、图或迭代多跳、分层长文本合成三类程序之一。
这对工程意味着什么
可在智能体记忆层引入每次查询的路由控制接口;避免将基准分数直接解读为路由带来的增益,论文中路由的因果效应尚未被隔离。
证据定位
LoCoMo(n=1,986)事实类84.87%、对抗弃答68.61%;MAB(n=3,671)61.49%;LongMemEval(n=500)86.00%;仓库复现产生相近总分并支持按任务和模式的失败分层分析。(筛选维度:可复核评测、软件工程方法)
适用边界
缺原始基线对比、端到端计时与令牌账本;路由因果效应、效率增益和统计显著性均无法从现有证据确立。
方法与英文摘要

冻结语义分类器加运行时门控将查询分发至融合词法与密集检索、图多跳或分层长文本合成,共用含多粒度嵌入、提取三元组与事实版本元数据的摄入基底。

Agent-memory workloads mix direct factual lookup, relation-chain and current-state reasoning, and broad synthesis over long histories. We describe Supra Cognitive Modes (SCM), an architecture that maps explicit or automatically selected per-query modes to retrieval and synthesis payloads over one shared ingest substrate. A frozen semantic classifier and runtime gates dispatch queries among fused lexical and dense lookup, graph or iterative multi-hop handling, and stratified long-form synthesis. The substrate combines multi-granularity embeddings, extracted triples, fact-version metadata, and optional asynchronous enrichments. We characterize the deployed configuration on three benchmarks: Long-term Conversational Memory (LoCoMo; n = 1,986), MemoryAgentBench (MAB; n = 3,671), and LongMemEval (n = 500). The reference run records 84.87% on LoCoMo factoid categories and 68.61% on adversarial abstention, 61.49% on MAB across two repetitions, and 86.00% on LongMemEval. A repository-backed reproduction produces similar aggregate scores and supports task- and mode-conditioned failure analysis. Raw baseline outputs, aligned end-to-end timing for LoCoMo and LongMemEval, and complete token ledgers are unavailable; stored rows also omit some final runtime decisions. The results characterize one implemented routed configuration and its diagnostic failure patterns, while source inspection verifies the per-query control interface and shared-substrate design. Causal routing effects, efficiency gains, and statistical significance remain outside the available evidence.

人机协同与对齐(0 篇)

本轮没有通过深读证据门的重点论文。

本轮分类概览

同一论文只归入一个最先命中的赛道,避免重复计数。

赛道候选重点
形式化与程序验证181
软件工程与仓库智能152
代码质量与优化140
UI 与 GUI Agent30
个人知识与本体182
人机协同与对齐00

近一个季度监测日历

北京时间。绿色表示有可阅读候选,灰蓝表示已监测但无新增,橙色表示部分降级;“无记录”不等于失败。

2026 年 5 月

1无记录2无记录3无记录4无记录5无记录6无记录7无记录8无记录9无记录10无记录11无记录12无记录13无记录14无记录15无记录16无记录17无记录18无记录19无记录20无记录21无记录22无记录23无记录24无记录25无记录26无记录27无记录28无记录29无记录30无记录31无记录

2026 年 6 月

1无记录2无记录3无记录4无记录5无记录6无记录7无记录8无记录9无记录10无记录11无记录12无记录13无记录14无记录15无记录16无记录17无记录18无记录19无记录20无记录21无记录22无记录23无记录24无记录25无记录26无记录27无记录28无记录29无记录30无记录

2026 年 7 月

1无记录2无记录3无记录4无记录5无记录6无记录7无记录8无记录9无记录10无记录11无记录12无记录13无记录14无记录15无记录16无记录17无记录18无记录19无记录20无记录21无记录22无记录23无记录24无记录25无记录26无记录2764候选 / 5重点28139候选 / 10重点29无记录30无记录31无记录

近 14 次监测窗口

仅展示公开源的聚合运行状态,不含提示词、全文或个人数据。

候选阅读库(68 篇)

按赛道、评分和日期展开;中文标签用于导航,英文摘要用于核验。

形式化与程序验证(18 篇)

形式化与程序验证 · 6/30 · 2026-07-26形式验证的浮点数据类型在ARCH HDL中完成FP32/BF16的端到端形式验证,三重输出结构保证一致性。Formally Verified Synthesizable Floating-Point Data Types in ARCH HDL

We report the design and end-to-end verification of first-class IEEE-754 binary32 (FP32) and bfloat16 (BF16) arithmetic for ARCH, a hardware description language intended to be generated by language models. Every operator - comparisons, conversions, add, sub, mul, and fused multiply-add (FMA) - is described once against a single bit-vector IR and rendered three ways from one source: synthesizable SystemVerilog, an SMT-LIB model, and a Lean 4 proof model. The three artifacts cannot drift apart structurally, and the residual per-node printer correspondence is machine-checked: a Yosys-to-SMT miter proves the emitted SystemVerilog equivalent to the SMT model for all 24 operators. Verification splits at the solver-tractability frontier: multiplier-free operators (comparisons, add/sub over all 2^64 inputs, conversions, and all binary BF16 arithmetic) are proved exhaustively equivalent to the SMT-LIB FloatingPoint theory; the SAT-hard multiplier-bearing operators (FP32 mul and FMA) are proved correctly rounded in Lean, sorry-free, against a value-level round-to-nearest-even specification over exact dyadic values. Physical characterization exposed the FMA as the timing outlier: its exact-wide 470-bit datapath does not pipeline in our flow. We reimplemented it as a bounded 98-bit guard/round/sticky datapath that pipelines to 268 MHz on Nangate45, and proved, in Lean and over all 2^96 inputs, that it is bit-identical to the exact-wide reference, so it inherits the reference's proven correct rounding. The equivalence is tractable precisely because the shared multiplier appears on both sides and cancels: neither a SAT solver nor the proof ever solves a multiplier equivalence. (The BF16 FMA is deliberately an FP32-accumulating fusion, characterized as exactly that.) All machine-checked claims are pinned to a tagged open-source release.

阅读 arXiv 原文
形式化与程序验证 · 7/30 · 2026-07-26执行支撑的TLA+规范生成基准通过模型检查器实际执行来评判LLM生成的TLA+规范正确性。TLA$^{+}$-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA+ Specification Generation

Large language models increasingly write TLA$^{+}$ formal specifications from natural-language descriptions, but progress is hard to measure: existing resources grade by resemblance to a reference or by whether the output parses, neither of which shows correctness. We present TLA$^{+}$-Bench, a dataset and benchmark that grades by execution. Every gold specification ships a configuration the TLA$^{+}$ model checker runs over the full reachable state space, deciding exactly whether the specification holds the properties that configuration names. The dataset holds 403 model-checked gold and 897 parse-only silver specifications from 13 public repositories, subsumes prior TLA$^{+}$ generation data, and carries four model-written descriptions in two styles from two providers, with difficulty and category labels. Our main finding is about measurement itself: an exact oracle gives not one correctness number but a range. Varying only the grading choices earlier benchmarks leave unstated, on one fixed set of model outputs, the correct rate moves sixfold, from 10.0\% to 1.7\%; adding the interface-supply choice, where the model is told the configuration's names, widens the range to elevenfold, from 18.7\% to 1.7\%. We call this range the correctness envelope and measure each of its bounds. The findings inside it are stable. Every model writes valid TLA$^{+}$ far more often than correct TLA$^{+}$: the strongest is correct 16\% of the time by default and 26\% when given the interface names, open models at most 1\%, and correctness falls sharply with difficulty.

阅读 arXiv 原文
形式化与程序验证 · 7/30 · 2026-07-24因果推断自动化研究框架CausalForge基于Lean证明助手实现因果推理的自改进自动化理论研究。CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference

Automating theoretical research is constrained not only by the generation of candidate results, but also by their reliable evaluation. A common approach is to close the research loop with a large language model (LLM) reviewer. However, such reviewers remain empirically unreliable: they may accept fabricated papers and detect them at rates close to chance (Bad Scientist, 2025). We present CausalForge, a framework for automated theoretical research in causal inference grounded in the Lean proof assistant. CausalForge combines Causalean, a foundational Lean library for causal inference containing 7,035 machine-checked declarations developed with language-model assistance under human design and review, with CausalSmith, a self-improving agentic pipeline that selects research topics, proposes results, formalizes statements, constructs proofs, and presents the resulting artifacts for human inspection. Because a machine-checked proof establishes only that a formal statement follows from its assumptions, not that the statement faithfully captures the intended scientific claim, the pipeline augments kernel verification with a statement audit that compares each formal theorem against the informal claim it is intended to express. We evaluate the system using artifacts produced by completed autonomous research runs. The source code, formal library, and run records are available at https://github.com/Jiyuan-Tan/CausalForge.

阅读 arXiv 原文
形式化与程序验证 · 7/30 · 2026-07-24Rust验证框架的LLM生成HarnessLLM从测试套件自动生成Rust形式化验证的检测框架。HarnessLLM: Rust Verification Harness Generation with Large Language Models

Rust's ownership model and type system offer strong memory safety guarantees, but unsafe code and runtime panics still present significant risks. Formal verification is essential to ensure memory safety, but developing verification harnesses remains a challenging and manual task. Although large language models (LLMs) have shown strong performance in various code analysis tasks, directly applying them to harness generation often results in inaccurate API invocations, inefficient nondeterministic data generation, and fabricated fixes. In this paper, we present HarnessLLM, an automated workflow that leverages LLMs to generate verification harnesses for Rust code directly from existing test suites. HarnessLLM automatically extracts calling scenarios from test cases, generates nondeterministic arguments based on dependency analysis, and incrementally synthesizes harnesses. It then iteratively refines the harnesses, preserving critical code regions and reporting fabricated types or functions to LLMs for correction. In our evaluation on 9 real-world Rust codebases, HarnessLLM extracted 294 calling scenarios from 494 test cases with 94.66% precision and generated harnesses for all scenarios in an average of 145 seconds each. It outperformed the existing approach, Autoharness, which succeeded on only 41% of those scenarios. Finally, 6 real-world memory safety bugs were detected using the generated harnesses, demonstrating the practical utility of our approach in verification. To our knowledge, this is the first work to use LLMs for generating harnesses aimed at memory safety verification in real-world Rust projects.

阅读 arXiv 原文
形式化与程序验证 · 3/30 · 2026-07-24多语言投影器实现多语ASRMEUSLI将Whisper编码器与多语言LLM连接,支持28种欧洲语言的开源ASR。MEUSLI: a Multilingual Projector for LLM-based ASR and Beyond

Lightweight projectors are an established way to connect pre-trained speech encoders with large language models (LLMs), mapping acoustic features into token-level embeddings for tasks like ASR and spoken question answering. Existing systems, however, typically only support a few languages and are often limited to English. We introduce MEUSLI, the first open-science multilingual projector family that links a Whisper encoder with open-source multilingual LLMs, enabling fully open-source end-to-end ASR in 28 European languages. MEUSLI extends prior monolingual pipelines, delivering strong results across high- and low-resource languages. Using proper continual leaning techniques, MEUSLI can be easily extended to other languages not seen in training. We further demonstrate that the MEUSLI projector can be leveraged beyond ASR, enabling multilingual speech translation and topic identification with only a few hours of task specific supervision per language. Overall, MEUSLI provides a solid foundation for multilingual speech understanding tasks, supporting scalable and inclu- sive open-source SpeechLLM

阅读 arXiv 原文
形式化与程序验证 · 5/30 · 2026-07-24不安全Rust的Kan规范生成KaPilot通过多智能体协作自动生成内存安全验证规范。KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification

Rust's ownership and type system provide strong memory safety guarantees, but unsafe code still presents memory safety risks. Formal verification is crucial for ensuring memory safety, but writing precise specifications for unsafe Rust is challenging and largely manual. Large language models (LLMs) have shown promise in generating formal specifications but are often code-centric, prone to inheriting implementation flaws, and lack systematic quality assessment. In this paper, we present KaPilot, a multi-agent framework for automatically generating specifications to verify unsafe Rust memory safety using Kani. The process begins with lightweight program analysis and proof harness generation. The SafetyReq agent extracts a concise, refined list of safety requirements from the target Rust function's documentation, which guides the SpecGenerate agent in producing initial specifications that specify memory safety concerns. Then, the specifications are iteratively refined through a generate-precheck-verify loop involving SpecGenerate, SpecPrecheck, and SpecVerify agents, which assess quality and feed errors back. By executing this loop multiple times, KaPilot generates a set of candidate specifications. Finally, the shuffle-and-implication strategy is applied to systematically determine the best specification from these candidates. We evaluated KaPilot on 54 unsafe Rust functions with ground truth and 70 without. KaPilot achieved 88.9% and 71.4% specification generation success, respectively, with 57.4% of generated specifications equivalent to or stronger than the ground truth. Compared with AutoSpec, KaPilot produces 14.8% more verifiable specifications and 25.9% more equivalent-or-better specifications.

阅读 arXiv 原文
形式化与程序验证 · 3/30 · 2026-07-23人机协同经济理论开发架构通过门控诊断和人工检查点实现可靠的经济理论辅助开发。pAI-Econ-claude: A Gated Human-in-the-Loop Multi-Agent Architecture for AI-Assisted Economic Theory Development

In many social-science research tasks, such as economics, LLM-based agents must produce outputs for which no cheap, task-complete, machine-readable correctness signal exists. This creates a distinctive reliability problem for multi-agent systems: how should generation, critique, coordination, and human judgment be organized when no component can certify the final result? We address this problem through pAI-Econ-claude, a gated, human-in-the-loop multi-agent architecture for AI-assisted economic theory development. Agents coordinate through a shared workspace of inspectable intermediate records; specialized gates diagnose targeted failure modes and recommend loopbacks without certifying correctness; and human checkpoints retain authority over decisions that are costly to reverse. We evaluate the architecture on five matched economic-theory tasks against an ungated baseline. Two evaluators blinded to configuration agreed on all five pairwise rankings, preferring the gated architecture in four tasks and the baseline in one. Mean failure severity fell from 1.58 to 1.16, while overall usefulness rose from 2.60 to 3.10. The largest observed gain occurred when a reality check rejected a false market-structure premise and a proof review prompted revision of a false welfare claim. The negative case shows that scaffolding can also compress an economically important mechanism too aggressively. The results support a bounded claim: gated oversight improves the auditability of AI-assisted economic theory without substituting for formal verification, and the allocation of irreversible human judgment is a more informative design variable than pure agent autonomy. The workflow is publicly available at https://github.com/maxwell2732/pAI-Econ-claude.

阅读 arXiv 原文
形式化与程序验证 · 6/30 · 2026-07-22LLM安全协议分析评估对比GPT和DeepSeek在130个混淆协议上的形式化安全分析能力。Evaluating Large Language Models for Symbolic Security Protocol Analysis

Security protocol verification relies on formal tools such as ProVerif and OFMC. This study evaluates whether Large Language Models (LLMs) can perform comparable analysis. We test GPT and DeepSeek in chat and reasoning modes over three runs on 130 obfuscated AnB/AnBx protocols covering 388 security goals, scored against ProVerif and OFMC. Chat models reach 69 to 81% recall at precision below 31%. Reasoning models reverse this trade-off, reaching 66.5% precision for GPT and 45.4% for DeepSeek, but detect just over half the attacks. DeepSeek's two modes share one underlying model, so the comparison isolates reasoning itself, which raises precision from 27.2% to 45.4%. The GPT contrast spans a model-version change and is only suggestive. All models perform worst on authentication goals: reasoning models detect well under half of injective and non-injective agreement attacks, whereas chat models over-flag them at low precision. Confidentiality is the exception, with F1 up to 95.7% in reasoning mode. Verdicts are unstable across runs, identical on 89.7% of goals for GPT but 74.0% for DeepSeek. Self-reported confidence is uniformly high yet shows no meaningful correlation with correctness. On this benchmark LLMs do not match formal verification, but may serve, at best, as pre-screening filters.

阅读 arXiv 原文
形式化与程序验证 · 8/30 · 2026-07-22zkEVM形式验证约束合成VeriSynth通过LLM引导从zkEVM Rust代码合成可执行验证模型。Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis

Zero-Knowledge Ethereum Virtual Machines (zkEVMs) secure Ethereum rollups by generating zero-knowledge proofs that guarantee off-chain execution correctness. However, subtle implementation bugs (e.g., incorrect gas accounting) can lead to valid proofs certifying semantically faulty states, thereby silently defeating cryptographic guarantees. Formal verification via SMT solvers can prevent this, but is bottlenecked by specification: current zkEVM development practice lacks automated methods to translate Rust opcode handlers into verification models. Current practices rely on unsustainable manual specifications, while LLM-based approaches suffer from hallucination and lack formal guarantees. To address this, we propose VeriSynth, a framework that synthesizes executable Python/Z3 verification models from Rust zkEVM code. VeriSynth enforces a hybrid paradigm: an LLM acts strictly as a formalization frontend to translate code into symbolic constraints, while an SMT solver serves as the correctness arbiter. To handle complex multi-component state transitions, VeriSynth integrates semantic decomposition, retrieval-grounded prompting, and verification-guided auto-repair into a closed-loop pipeline. We evaluate VeriSynth on the first source-level zkEVM verification benchmark, encompassing both correct and faulty opcode implementations. VeriSynth achieves a bug detection rate of over 90%, substantially outperforming direct and conversational LLM baselines, as well as a production-grade handwritten mutation-testing suite. Ablation studies confirm that each pipeline component is critical to the framework's overall effectiveness.

阅读 arXiv 原文
形式化与程序验证 · 3/30 · 2026-07-22神经符号刑法量刑预测结合LLM与确定性法律约束进行韩国简易程序量刑和文书生成。Neuro-Symbolic AI for Korean Criminal Law: Sentencing Prediction and Document Drafting

The Korean criminal justice system utilizes summary proceedings (guyaksik) to expedite high-volume minor infractions, such as simple driving under the influence (DUI), unlicensed driving, and minor traffic casualties. Although this mechanism improves judicial throughput, processing these cases creates a substantial administrative burden for prosecutors, driving the need for automated systems that can precisely translate unstructured legal text into deterministic statutory outcomes. While recent Large Language Models (LLMs) excel at semantic extraction, their probabilistic nature inherently limits their reliability in Legal Judgment Prediction tasks. Specifically, when confronted with the arithmetic constraints of legal statutes, LLMs can produce hallucinations. Given that legal accountability permits virtually no tolerance for stochastic errors, purely neural architectures remain limited in their direct judicial applications. To address these limitations, we propose a Neuro-Symbolic framework that bridges unstructured legal facts with formal verification. Our architecture restricts the LLM exclusively to semantic extraction, while offloading statutory fine calculations to a Satisfiability Modulo Theories solver. This division of labor reduces hallucination risks during computation. Furthermore, we incorporate a Human-in-the-Loop verification scheme to preserve professional legal oversight. We formalize the 2026 Sentencing Guidelines for Traffic Offenses within this pipeline, demonstrating a deterministic approach to supporting summary indictments.

阅读 arXiv 原文
形式化与程序验证 · 4/30 · 2026-07-21乱序多处理器形式化验证首次对允许弱行为的乱序多处理器进行无界形式化验证。Formal Verification of an Out-of-Order Multiprocessor against an In-Order Weak-Memory ISA

Out-of-order multiprocessor is a critical piece of modern hardware, and their verification must solve the following challenges. First, inter-core interleaving, in which the order their reads and writes reach shared memory is unrestricted. Second, intra-core out-of-order execution, in which instructions fire out of program order. The combination of the two yields weak outcomes, which no sequential execution explains, and modern ISA allows such behaviors to account for them. However, the microarchitecture even exhibits excess out-of-order executions, temporarily entering states forbidden by the ISA. While discarded later, such states complicate reasoning about the core in full-system verification. Prior works verify a range of processor designs, while none have performed unbounded verification for out-of-order multiprocessor exhibiting such weak outcomes. We present the first formal verification of an out-of-order multiprocessor against an in-order, weak-memory ISA. Our key idea is a well-designed core specification, which captures the essence of excess executions in a single list of instructions. Building upon this, we decompose the proof into two steps. The first is a core refinement, proving a core implementation against this specification, abstracting away every microarchitectural state except those necessary to reason about excess executions and the core interface. The second is a system inclusion, serializing the out-of-order memory executions and inter-core interleaving into the ISA, easily removing excess executions thanks to the core specification. All of our proofs are mechanized in Rocq, heavily utilizing large language model (LLM) agents to write proofs automatically.

阅读 arXiv 原文
形式化与程序验证 · 6/30 · 2026-07-20智能体驱动代理模型可行性在Mesa ABM中引入LLM代理决策,通过统计模型检查评估可靠性。Towards Agentic Agent-based Models: Feasibility, Performance, and Statistical Model Checking

Agent-based models (ABMs) rely on simple, explicit and reproducible rules for individual decision making, while complex collective behavior emerges from interactions among agents. Recent advances in large language models (LLMs) make it tempting to replace, enrich, or perturb these rules with LLM-based agentic capabilities. However, this raises a methodological question: how does introducing LLM-driven decisions affect the reliability, computational cost, and behavior of ABM simulations? We investigate this for Mesa ABM models, a popular Python library for ABMs, analyzed by statistical model checking. Building on Mesa's integration with the statistical model checker MultiVeStA, we extend the classical Schelling segregation model with a hybrid population: ordinary agents classify neighbors using the standard symbolic rule, while one agent delegates this task to an LLM through tool calls. The LLM-enabled agent receives natural-language descriptions of neighboring agents and invokes tools that increment counters of similar/different neighbors; these counters determine its happiness according to the original Schelling dynamics. This provides a minimal but controlled setting where the semantic, operational, and computational behavior of LLM-based decisions can be studied inside an otherwise standard ABM. We report preliminary experiments with locally served LLMs of different sizes, showing that smaller models may fail simple semantic classification experiments or become operationally unusable during repeated tool-call generation, while larger tested models pass these preliminary checks. We discuss how statistical model checking can estimate classical ABM observables and quantify the impact of introducing agentic LLM components into simulation models.

阅读 arXiv 原文
形式化与程序验证 · 6/30 · 2026-07-19自我进化的Lean证明代理智能体和工作流随验证器固化的基准共同进化,而非固定外部基准。Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution

Designing effective Lean proof agents is a central challenge in formal mathematical reasoning. Beyond building stronger provers, recent work emphasizes the workflow around Lean: how an agent decomposes proof obligations, uses tools and compiler feedback, diagnoses failures, repairs proofs, and maintains structured proof context. Motivated by code-level self-evolving agents, we study whether such workflows can be evolved rather than hand-designed. We present a self-evolving Lean proof agent in which a small fixed, trusted runtime wraps a fully mutable workspace: the proof workflow, prompts, and tools. Unlike most self-evolving systems, which optimize against a fixed external benchmark, our system coevolves the agent and its benchmark. Between generations, the highest-scoring agent (the champion) revises the active task distribution through a mastery-throttled curriculum update that introduces harder proof obligations only after the current level is mastered, and a single-anchor recalibration re-runs the champion on the updated benchmark to keep scores comparable as difficulty rises. All evolution stays inside a Lean-grounded verification loop: however the agent rewrites itself, a success counts only when its behavior yields Lean-verified proofs under a trusted snapshot, and each attempt must emit a machine-readable, Lean-grounded proof context whose representation may evolve but whose groundedness is enforced. We run the coevolving trajectory and a fixed-benchmark baseline for 15 active generations and compare them on a held-out miniF2F test split. The best coevolving agent reaches a 45.1% held-out solve rate, versus 12.7% for the seed and 32.0% for the best fixed-benchmark agent, showing that verifier-grounded self-evolution can improve Lean proof workflows under a coevolving benchmark.

阅读 arXiv 原文
形式化与程序验证 · 6/30 · 2026-07-18形式证明技术新颖性度量PriorProof基于时间切片知识库的加权惊异度评估证明路径新颖性。PriorProof: A Point-in-Time Measure of Technique Novelty for Formal Proofs

Mathematicians distinguish proofs that explain, simplify, or introduce a nonstandard route, but these judgments are difficult to operationalize. We study a deliberately narrower construct: time-relative proof-route nonstandardness in formal mathematics. For a Lean theorem, PriorProof extracts the dependency footprint of its elaborated proof term and scores the weighted surprisal of that footprint under a retrieval-conditioned, hierarchically smoothed prior built only from an earlier quarterly snapshot of Mathlib. The method requires no hand-built technique ontology and no human labels: statement retrieval is learned from proof-derived contrastive pairs, while the scored object is read mechanically from proof terms. In a blinded topology study, 100 presentations collapse to 76 distinct underlying pairs: 12 canonical contrasts shown three times for consistency screening and 64 distinct stratified pairs. Against the majority of three retained domain raters, PriorProof agrees on 53/76 pairs (69.7%, Wilson 95% CI 58.7-78.9%), including 11/12 canonical pairs (91.7%, 64.6-98.5%) and 42/64 stratified pairs (65.6%, 53.4-76.1%). Score-gap quartiles are nonmonotone after repeat collapse; the endpoints are 12/19 (63.2%, 41.0-80.9%) in the smallest-gap bin and 16/19 (84.2%, 62.4-94.5%) in the largest, supporting an endpoint-calibration tendency rather than a resolved staircase. The best language-model condition agrees on 60/76 pairs (78.9%, 68.5-86.6%); on paired outcomes, PriorProof alone is correct on 8 pairs and the model alone on 15 (exact two-sided McNemar p = 0.210), so the difference is not established at this sample size. We therefore present PriorProof not as a replacement for expert or model judgment, but as a decomposable, time-anchored signal whose score gap provides an interpretable reliability indicator.

阅读 arXiv 原文
形式化与程序验证 · 5/30 · 2026-07-18RTL到Lean自动翻译与验证Rtl2lean自动将SystemVerilog翻译为Lean模型,层级构建定理库辅助验证。Rtl2lean: Automated RTL-to-Lean Translation with Hierarchical Theorem Generation and Lemma Reuse

Formal verification with interactive theorem provers can provide strong correctness guarantees for register transfer level designs, but applying it to existing SystemVerilog code requires substantial manual effort in semantic modeling and proof construction. This paper presents Rtl2lean, a framework that automatically translates RTL designs into executable Lean 4 models and builds a hierarchical theorem library for subsequent verification. The generated model represents hardware execution as a pure state transition function, while a four layer theorem framework captures combinational semantics, sequential updates, single cycle behavior, and reachability and invariants. When a high level property cannot be discharged by the existing theorem base, an LLM based proving loop proposes intermediate lemmas from the current proof context and Lean feedback. Only lemmas accepted by the Lean kernel are added to the reusable lemma pool. Experiments on six SystemVerilog designs generate 403 theorems, all of which are successfully checked by Lean. Among 358 foundational lemmas, 287 are available for automatic reuse, yielding a reusable lemma ratio of 80.2 percent. The results demonstrate that Rtl2lean can construct machine checked RTL proof libraries with low checking overhead and substantial cross property lemma reuse.

阅读 arXiv 原文
形式化与程序验证 · 5/30 · 2026-07-17证明驱动的软件理解案例结合LLM、PVS和SeaHorn对成熟区块链代码进行形式化属性证明。Show Me The Money: An Exercise in Proof-Driven Software Understanding

We present a case study on proof-driven software understanding of mature, security-critical infrastructure. While formal methods are traditionally applied during the design phase, we present our experience applying formal reasoning onto a mature industrial C++ codebase. We focus on a formal analysis of the core algorithm that implements the Stellar blockchain's SDEX order book. By combining large language models (LLMs), Prototype Verification System (PVS), and SeaHorn, we are able to prove core properties of the production codebase. Our approach also identified an inconsistency in documentation related to the reachability of an exception location. Most importantly, however, we produce artifacts that make it easy for code changes to be checked against established invariants. This work demonstrates how the strategic combination of theorem proving and model checking provides a path for delivering robust assurance to legacy systems.

阅读 arXiv 原文
形式化与程序验证 · 3/30 · 2026-07-17推理前答案预承诺现象发现LLM在推理前已做出错误承诺,激活级证据支持该现象。Committed Before Reasoning: Behavioral Reproduction and Preliminary Activation-Level Evidence of Answer Pre-Commitment in an Open-Weight LLM

Chat models sometimes commit to an answer and then produce reasoning that justifies it rather than deriving it -- even when the answer contradicts a task premise. We study a minimal probe: "I want to wash my car. The car wash is 100 meters away. Should I walk or drive?" Only drive works (the car must be at the car wash), yet models overwhelmingly recommend walking. (1) Behavioral reproduction: on Qwen3-8B across five system-prompt conditions (210 rollouts), the wrong commitment occurs in 85-100% of sampled rollouts per condition and 100% of greedy rollouts, in both thinking and non-thinking modes; a 4,096-token thinking budget does not repair it. (2) Preliminary activation-level evidence: probing hidden states with a pretrained, training-free activation oracle (no task-specific probe training) at positions before the answer text is emitted, "walk" read-outs exceed a neutral-context baseline (68% vs. 17%; walk-committing rollouts p=.005, drive-committing rollouts p=.005, Fisher exact) -- notably, rollouts that eventually answer drive also read as walk-leaning before commitment (5/6). The oracle's default on unrelated content is "drive" (83%), so the read-outs are not lexical bias; stratifying by literal walk/drive occurrence shows they are not text recovery either (spans containing "drive" still read out walk; in balanced lexical fields, per-rollout walk-majorities beat a per-prompt neutral baseline 15/22 vs. 1/8, p=.01; drive-committing rollouts 6/6, p=.002). Samples are small and the within-rollout positional gradient is not significant (p=.34); we frame these results as preliminary. (3) Methodological: with fixed oracle, activations, and positions, question wording alone moves a positive control from 2/16 (open question) to 11/16 (closed); negative oracle results are uninterpretable without per-wording positive controls.

阅读 arXiv 原文
形式化与程序验证 · 6/30 · 2026-07-17抽象语法树上的定理证明AoA基于AST而非源代码操作,大幅降低证明生成中的标记消耗。AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language

Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this effort, but their heavy token consumption and API cost remain a major obstacle. We trace this cost to a shared root: current agents operate on serialized concrete syntax, emitting proofs as source text and recovering proof states through separate, line-number-based queries, so every edit shifts later lines and forces repeated relocation of errors and states. This same dependence on concrete syntax also blocks adoption of Minilang, a recent proof language that reaches SOTA on LLM-based proving but is too new for LLMs' training corpora. We address both problems by lifting the agent off source text and onto the abstract syntax tree (AST): the model supplies proofs as JSON representations of Minilang's AST -- native to tool-calling LLMs -- and drives the prover through a tree-edit model that fuses proof operations and states into one proof tree, so each operation carries its own subgoal's state, readable directly off the tree. We realize this design in \emph{Agent over AST} (AoA). Against Amazon's Isabelle Agent on miniF2F and NTP4VC-Pearl common success sets, AoA cuts API cost by 2.3--4.7x (normalized input-cache accounting), uses 2.9--6.9x fewer tokens and 3.9--8.9x fewer tool calls, and finishes 1.4--2.0x faster -- while also solving far more problems on the harder verification benchmark.

阅读 arXiv 原文

软件工程与仓库智能(15 篇)

软件工程与仓库智能 · 3/30 · 2026-07-27基于LLM的测试用例生成实践NL2Test从流量捕获生成可重放的API回归测试,减少手工维护成本。Industrial Practice of LLM-Based Test Case Carving and Assertion Generation (Experience Paper)

Enterprise regression testing for microservice systems is often constrained by incomplete or outdated documentation. In practice, QA engineers frequently rely on real execution traffic to reconstruct business scenarios; however, turning raw traffic into replayable regression tests with stable validation logic remains labor-intensive and error-prone. This paper presents NL2Test, an end-to-end approach and tool that generates executable API regression tests from (i) a natural-language scenario description and (ii) a traffic capture recorded while executing the scenario. NL2Test addresses two coupled tasks: test case carving, which extracts a minimal replayable request sequence and reconstructs data dependencies so that dynamic values are bound from their responses rather than hard-coded; and assertion generation, which produces assertions aligned with business intent while avoiding non-deterministic fields and hallucinated paths. To improve reliability, NL2Test uses LLMs for semantic interpretation and constrained code synthesis, and uses deterministic algorithms for request filtering, dependency confirmation via value consistency, and assertion-path validation. We evaluate NL2Test on 51 industrial regression scenarios extracted from a large consumer-facing Internet company. NL2Test achieves an exact-match rate of 82.4% (42/51), and produces a functionally usable draft in 98.0% (50/51) of scenarios when allowing minor post-edits. In a 9-month production deployment starting in March 2025, NL2Test generated 3,196 test cases with an overall code adoption rate of 85.4%. These results indicate that traffic-grounded generation with deterministic guardrails can substantially reduce manual effort while improving regression automation in complex microservice environments.

阅读 arXiv 原文
软件工程与仓库智能 · 3/30 · 2026-07-24从应用原型生成冲刺待办项评估GPT-4o从界面原型生成用户故事和任务的准确性与精度。How Well Can AI Generate Backlogs from App Mockups?

Creating sprint backlogs requires considerable effort, as items such as epics, user stories, and tasks can be missed or inconsistently specified. We propose a multimodal approach to support backlog generation from visual app mockups, an artifact available at early project stages. We evaluate three prompting strategies on GPT-4o: a zero-shot baseline, Compositional Chain-of-Thought (CCoT) for vision-language reasoning, and a persona-driven prompt. We study seven app development projects across two countries and interview developers about the results. Overall, we observed that the baseline prompt favours recall over precision, whereas CCoT is more balanced, achieving average F1 scores of 52-66% for epics and user stories. Tasks were more challenging to generate accurately. Precision gains were most consistent when adding architectural context, particularly for backend tasks (precision gains up to 35%). Interviews with developers revealed that up to 26% of false positives were still considered useful, reflecting the creative and open-ended nature of backlog creation. To capture this, we propose a new measure called Revised Recall, which complements ground-truth evaluation with developer assessments. Our findings suggest that hybrid prompting with architectural context can assist backlog generation from early mockups, though results vary by item type and developer oversight remains necessary.

阅读 arXiv 原文
软件工程与仓库智能 · 3/30 · 2026-07-24全球数据保护需求比较跨司法管辖区分析隐私合规需求中的共享与差异要求。Comparing and Conceptualizing Data Protection Requirements Worldwide for Privacy Regulatory Compliance

The growing digitalization of society has intensified the collection, processing, and sharing of personal data, increasingly moving across national borders and regulatory jurisdictions, prompting a proliferation of data protection frameworks worldwide. These transborder personal data flows (TPDF) are essential to today's economy, but organizations managing them must reconcile data protection requirements that differ, sometimes subtly, across jurisdictions. For requirements engineering, this is the central challenge: regulatory data protection requirements (RDPRs) are complex and not directly translatable into software requirements, especially when frameworks impose similar, non-identical, or contradictory obligations. Identifying which requirements are shared and which diverge is therefore critical to managing TPDF, and addressing them late in the software development lifecycle (SDLC) causes costly rework, making early identification essential for compliance and stakeholder communication. This paper identifies and conceptualizes common RDPRs worldwide from the perspective of data protection legal experts, answering: (SQ1) which requirements are common across regulations and how are they conceptualized, and (SQ2) which requirements diverge and how do they differ conceptually. We combine deductive qualitative analysis of interviews with 70 legal experts from G20 economies and other countries and systematic content analysis of these economies' data protection regulations. We identify common requirements, such as consent, and divergent ones, such as the right to be forgotten. Given their impact across the SDLC and enterprise architecture, we translate these findings into a set of Data Protection Officer DPO (DPO) stories, using the user story notation, classified by SDLC phase and enterprise architecture layer, to help organizations manage TPDF compliance.

阅读 arXiv 原文
软件工程与仓库智能 · 6/30 · 2026-07-24对话式AI代码审查助手提出将代码审查视为对话过程,而非一次性评论任务。Code Review is a Conversation: Toward Conversational AI Review Assistants

AI-based code review tools increasingly promise to help developers inspect pull requests, identify defects, and improve code quality. Yet most current approaches frame code review as a one-shot commenting task: given a diff, the system produces warnings or suggestions. This framing overlooks a central property of modern code review: review is a conversation. Human reviewers do not merely comment on code; they ask questions, explain expectations, negotiate design trade-offs, request evidence, transfer project knowledge, document rationale, and collectively decide whether a change is good enough to integrate. In this vision paper, we argue for conversational AI review assistants: systems that participate in code review as interactive partners rather than static comment generators. Such assistants should identify when conversation is needed, ask grounded questions, respond to developer explanations, summarize unresolved issues, help capture rationale, and know when to abstain or escalate to human reviewers. Such a paradigm shift requires novel evaluation methodologies as well. We outline a research agenda for studying review conversations, designing conversational AI review capabilities, and evaluating their impact on software evolution and maintenance. Our vision reframes AI code review from automated commenting to human-AI sensemaking before integration.

阅读 arXiv 原文
软件工程与仓库智能 · 4/30 · 2026-07-24开发者对AI审查的响应分析分析54,791条智能体代码审查评论,结果因智能体类型而异。"Go Home Copilot, You're Drunk": Understanding Developer Responses to Agent-Generated Code Review Comments

Code review is a critical quality assurance practice in software engineering development, and AI coding agents are increasingly generating review comments on pull requests. However, little is known about how developers actually respond to such agent-generated feedback. In this paper, we present the first large-scale empirical study on the resolution of agent-generated code review comments. We analyze $54{,}791$ comments generated by five widely used coding agents (i.e., Copilot, Cursor, Codex, Devin, and Claude) across $342$ Python repositories on GitHub. We examine (1) resolution rates across agents and comment types, (2) the role of developer experience, and (3) characteristics that influence comment usefulness. Our results show that resolution rate varies considerably across agents, with Copilot accounting for the majority of resolved comments (72.9\%). Core developers resolve the majority of agent-generated feedback, particularly for \textit{design} and \textit{evolvability}-related comments, while peripheral developers are more involved in resolving \textit{functional defect} comments. Through open card sorting of 470 unresolved comment discussions, we identify \textit{ten} discussion patterns explaining why comments remain unresolved, with \textit{incorrect suggestions} and \textit{intentional design decisions} being the most prevalent. Finally, our analysis reveals that the presence of an inline \textit{code suggestion} is the strongest predictor of comment resolution, while lengthy and complex comments are less likely to be acted upon. Our findings provide insights for improving AI-generated code review feedback and its integration into development workflows.

阅读 arXiv 原文
软件工程与仓库智能 · 7/30 · 2026-07-23AI编码代理贡献实证研究分析AI代理生成的拉取请求与人工PR的合并率差异和时间变化。How Do AI Coding Agents Contribute to Software Development? an Empirical Study of Agentic Pull Requests

Recent advances in large language models and their rapid adoption across software engineering tasks have made Artificial Intelligence (AI) coding agents an integral component of modern software development workflows. While developers increasingly benefit from these coding agents, their impact on software quality remains insufficiently understood. In particular, how agentic contributions evolve across the software development lifecycle has not been thoroughly investigated. This study aims to characterize agentic pull requests (PR) in comparison to human generated PRs and to examine how their properties change across different stages of the development lifecycle. Using the AIDev dataset, we first analyze how differences in merge rates between agentic and human generated PRs vary over time. We then identify the types of development tasks where AI coding agents are predominantly applied and investigate how these task distributions evolve across development quarters. Finally, we compare a set of key characteristics of agentic and human generated PRs, focusing on their implications for software quality and their temporal dynamics. Overall, our findings provide an empirical and longitudinal perspective on the role of AI coding agents in software development, offering a more nuanced understanding of their benefits and limitations in real-world practices.

阅读 arXiv 原文
软件工程与仓库智能 · 6/30 · 2026-07-23需求工程质量的信息流理论将RE质量重新定义为信息粒子在角色和工件间的流动效率。Information is all you need: Requirements Engineering Quality Reframed

To move beyond this vague appeal to context, this vision proposes a novel holistic theory of requirements engineering (RE) quality. This theory models how information particles, i.e., discrete pieces of domain knowledge, are transferred between roles and artifacts. Since the RE process is ultimately an information transfer, holistic RE quality depends on the properties of information flow, i.e., how effectively and efficiently information is transferred from sources (like stakeholders) to targets (like developers and testers), uniting both artifact- and process-based perspectives on RE quality. In an exemplary simulation of the theory we illustrate why a high-quality specification gets bypassed in an agile context, thereby demonstrating that a simulation can provide actionable insights into calibrating the RE process to optimize the information flow. Beyond organizational applications, we envision that the theory can serve as a coherent theoretical framework for understanding the success or failure of RE processes and artifacts.

阅读 arXiv 原文
软件工程与仓库智能 · 8/30 · 2026-07-22超越失败到通过的测试强化区分严格与宽松的BUG复现测试,迭代增强以提升修复质量。Beyond Fail-to-Pass: Iterative Hardening of Co-Generated Bug Reproduction Tests and Fixes

Large language models (LLMs) have made automated program repair (APR) increasingly practical for real-world bugs, but repairing directly from bug reports remains underconstrained. Bug reproduction tests (BRTs) help close this gap by turning a bug report into an executable, bug-specific signal that can guide repair and validate candidate patches. Existing work has therefore studied BRT generation as a core subproblem in APR and mainly evaluates a generated BRT using the fail-to-pass (F->P) criterion, which requires the test to fail on the buggy code but pass on the golden fix. We show that F->P alone is insufficient when the goal of a BRT is to improve downstream repair. In particular, some F->P BRTs are lax, reproducing the observed symptom yet still admitting plausible-but-incorrect patches. We formalize this missing quality dimension by separating F->P BRTs into rigorous and lax ones, and show empirically that only the former consistently improve repair success. We further find that co-generation introduces test--fix error coupling, where the in-trajectory fail-to-pass (F->P) check can pass even when both the generated patch and generated test are wrong. Based on these findings, we propose CoHarden, a co-generation framework that uses the Lax signal as an in-loop convergence criterion. CoHarden first generates a test before any fix, then iteratively hardens the test and fix against surviving mutation patches until the generated test no longer admits Lax regressions. Experiments show that CoHarden reaches 69.4% Resolved and 78.9% F->P on SWE-bench Verified, outperforming the strongest fix-only and cogeneration baselines by +9.6 and +7.9 percentage points in Resolved, respectively, with consistent gains across LLM backbones and benchmarks.

阅读 arXiv 原文
软件工程与仓库智能 · 6/30 · 2026-07-21联邦学习开发痛点实证分析495个Stack Overflow帖子与9,116个GitHub议题揭示联邦学习主要难点。Understanding Developer Pain Points in Federated Learning: Insights from Stack Overflow and GitHub

Federated Learning (FL) enables collaborative model training without centralizing raw data, but building and operating FL systems remains difficult due to distributed execution, rapidly evolving frameworks, and privacy and governance requirements. In this paper, we present an empirical study of FL developer challenges by independently analyzing 495 Stack Overflow posts and 9,116 GitHub issues and pull requests from 92 FL-related projects. Using BERTopic-based topic modeling and difficulty indicators such as unresolved rates and median resolution time, we characterize recurring problem areas and compare how they manifest across the two support platforms, Stack Overflow and GitHub. Our analysis surfaces nine dominant Stack Overflow topics and thirteen GitHub topics, with persistent difficulties concentrated in environment setup and dependency compatibility, API breakages and migration, training instability under non-IID data, evaluation and metric correctness, and the integration of privacy-preserving mechanisms. We also categorize posts by question intent to understand the kinds of help developers seek; this intent analysis shows that "How"-type questions dominate, reflecting strong demand for procedural guidance. Several topics, such as "TFF Installation and Environment Compatibility" and "Federated Feature Engineering and SecureBoost Issues," exhibit high unresolved rates and long resolution times, suggesting shortcomings in tooling, documentation, and debugging support. Based on these findings, we provide actionable implications for FL framework designers, documentation authors, and educators. Although our results are constrained to public discussions and a subset of widely discussed frameworks, the study offers a scalable method for continuously monitoring developer pain points and improving the usability, reliability, and deployability of FL systems.

阅读 arXiv 原文
软件工程与仓库智能 · 6/30 · 2026-07-21陷阱代币合约隐蔽路径检测TrapHunter通过意图偏差分析揭露标准化代币中的欺诈逻辑。TrapHunter: Exposing Covert Pathways in Trap Token Contracts

Standardized token contracts (e.g., ERC-20) form the foundation of digital assets. However, attackers increasingly abuse this standardization to disguise malicious trap tokens. Unlike obvious violations, these contracts employ a strategy of "deceptive adherence": they strictly adhere to standard protocols to evade detection while embedding covert logic to defraud users. To address this, we first systematize the trap landscape by proposing a novel taxonomy derived from the intrinsic functional lifecycle of tokens (Generation, Circulation, Persistence, and Observation). We then propose TrapHunter, a framework designed to identify these traps and expose covert pathways within these deceptive contracts via intent deviation analysis. Specifically, TrapHunter introduces a unified semantic representation combining Abstract Behavior Trees (ABTs) and Augmented Path Graphs (APGs) to normalize intra-procedural syntax and reveal hidden execution paths driven by inter-procedural state dependencies. Crucially, it bridges the semantic gap by leveraging LLMs to reason about the behavioral intent of deviations from reference implementations, followed by fork-based dynamic validation to confirm exploitability. Experimental evaluation on 269 real-world contracts with three LLMs (DeepSeek, GPT, and Gemini) demonstrates that TrapHunter effectively detects all six categories of traps, achieving an average precision of 81.8% and recall of 85.4%, significantly outperforming state-of-the-art tools.

阅读 arXiv 原文
软件工程与仓库智能 · 3/30 · 2026-07-20无损失加速DNN变异测试Mure通过记忆化重用共同计算前缀,无损加速深度神经网络变异测试。Provably Lossless Acceleration of DNN Mutation Testing via Memoization

Mutation analysis has recently reemerged in the context of deep neural networks (DNNs) as a promising, but notoriously costly, approach for assessing test dataset adequacy. Existing techniques speed up DNN mutation testing through lossy approximations that trade efficiency for mutation score accuracy. This paper introduces Mure, the first provably lossless framework for accelerating DNN mutation testing via memoization. Mure is based on the idea that DNN mutants and the original model share substantial redundant computation, so during mutation testing, it executes only the mutated suffixes of each mutant and reuses the common prefix from the original model, which is computed only once. We give a formal account of memoized mutation testing, and prove that Mure is sound, i.e., it produces results equivalent to exhaustive vanilla mutation testing, and identify basic conditions under which speed-up is guaranteed. We have implemented Mure and evaluated it on 15 DNN models of various architectures, complexities, and sizes ranging from a few thousands to millions of parameters. This provides empirical evidence that Mure reduces the computational cost of mutation testing by 44.54%, on average. We also observed that while state-of-the-art techniques tend to yield higher acceleration (up to 88.97%, on average), they come at the cost of some error in mutation score. We further analyze the effect of mutation generation selection ratio on the effectiveness of Mure and observed predictable reductions in memoization opportunities with increasing the percentage of mutated neurons. We observed that Mure offers more than 20% speed-up even when as high as 5% of the neurons are mutated.

阅读 arXiv 原文
软件工程与仓库智能 · 3/30 · 2026-07-20对AI测试代理的过度依赖指出对AI测试代理的过度依赖既是代理问题也是保证问题。(Over)Reliance on Test Agents in AI-Assisted Software Testing

AI-based test agents promise to accelerate software testing by shortening feedback loops in continuous development and improving scalability and maintainability. To realize these benefits, engineers must still be able to assess if agent outputs are useful, valid, and reliable, rather than treating them as credible because they come from a capable system. This paper argues that overreliance on AI in testing is both an agency problem, in which engineers may cede cognitive control over test design decisions, and an assurance problem, in which testing artifacts may be accepted as evidence without sufficient scrutiny. We develop this argument through three theoretical lenses: software testing as cognitive problem-solving, test agents as adaptively autonomous entities, and test design argumentation as a means of making generated tests reviewable. We propose a framework for collecting data on overreliance in test agent workflows and identify specific modes of overdependence. The goal is to support accelerated testing without weakening judgment or the assurance value of testing evidence.

阅读 arXiv 原文
软件工程与仓库智能 · 7/30 · 2026-07-20代码变更化为可查询文档CODENS从拉取请求增量构建类型化软件知识图,支持多模式检索。CODENS: Transforming Code Changes into Living, Accessible, and Queryable Documentation

Maintaining up-to-date code documentation is difficult in fast-moving repositories because design knowledge is scattered across source files and pull requests. We present CODENS , a system that turns pull requests into living, accessible, and queryable documentation for production codebases. CODENS incrementally builds a typed software knowledge graph from pull requests, enriches components through schema-driven semantic extraction, derives typed relations between them, and exposes the resulting knowledge through three retrieval modes, including agent-guided graph traversal for repository-level question answering. The system also preserves semantic change history across pull requests and integrates both answer-quality and operational evaluation metrics. We evaluate CODENS on a client Ruby on Rails project in production. Results show that CODENS produces highly relevant and well-grounded answers, while qualitative feedback highlights a remaining challenge in concise, documentation-oriented synthesis.

阅读 arXiv 原文
软件工程与仓库智能 · 3/30 · 2026-07-19委托自主边界的需求工程提出代理正当记录和委托策略,明确AI系统可自主决策的范围。Specifying the Delegated-Autonomy Boundary: Requirements Engineering for Agentic AI

Agentic AI systems do not just predict or recommend; they plan, maintain state, and act in external environments with varying degrees of autonomy. This changes the requirements engineering problem in a specific and under-addressed way: it introduces what we call the delegated-autonomy boundary -- the set of decisions about what may be delegated to the system, under what graduated authority, with what oversight, and how control is returned. Current practices bury these decisions inside prompts, tool schemas, and runtime policies, even though they are requirements-level commitments. This paper proposes two complementary artifacts. First, an Agency Justification Record (AJR) helps teams decide when an agent is warranted over simpler alternatives. Second, an Agentic Delegation Policy (ADP) captures what must be specified for safe and effective development: purpose, authority, information, coordination, assurance, and evolution. Crucially, authority in the ADP is modelled as graduated, i.e., a tiered structure. We illustrate the framework with two contrasting examples: a safety-critical hospital discharge coordination agent and an automated code review agent.

阅读 arXiv 原文
软件工程与仓库智能 · 7/30 · 2026-07-18终端智能体审查轨迹分析分析智能体审查器轨迹,更高的精确度伴随大量探索和验证开销。Agentic Code Review in the Terminal: A Trajectory-Level Analysis of Behavior, Cost, and Human-Alignment

Agentic code review in terminal-based environments enables early feedback during local development before pull request creation. However, existing evaluations remain performance-centric and fail to capture the dynamic behaviors of repository-grounded agentic reviewers. Understanding these behaviors is critical for identifying how agentic reviewers succeed, fail, and incur hidden operational costs in practice. Then, we analyze the reviewers' behavior based on their trajectories. Our results show that agentic reviewers achieve higher review precision but incur substantial exploration and validation overhead, while successful reviews are associated with stronger planning and less downstream validation. These findings highlight the potential benefits of trajectory-aware and cost-sensitive evaluation of future agentic code review systems.

阅读 arXiv 原文

代码质量与优化(14 篇)

代码质量与优化 · 3/30 · 2026-07-26多级代码优化的提示混合Optimo通过混合专家提示架构从多级别进行代码性能优化。Multi-level Code Optimization via Mixture of Prompts

Runtime efficiency is a critical factor that impacts both software quality and user satisfaction. There are many approaches proposed for code optimization to improve runtime efficiency. Traditional code optimization methods operate on intermediate representations (IRs) during compilation for static languages. They are effective but struggle to handle dynamic languages that do not require compilation. Recently, large language models (LLMs) have been leveraged to directly optimize source code in dynamic languages. However, these methods fail to identify suitable optimization targets and usually conduct incomprehensive single-level optimization. To address these challenges, we propose Optimo, a multi-level LLM-based code optimization approach built on a novel Mixture-of-Prompts (MoP) architecture. In the MoP architecture, Optimo identifies time-critical code structures as performance bottlenecks via differential profiling. These structures are then routed to some optimization strategies, akin to expert models in MoE, each tailored to optimize specific code patterns. Unlike traditional approaches that focus only on statement-level optimizations, Optimo operates at four levels of abstraction, ranging from coarse-grained algorithmic improvements to fine-grained optimizations in API usage. We evaluate Optimo on two code efficiency benchmarks, COFFE and Effibench. Our results demonstrate that Optimo achieves an up to 57.48% opt%, i.e., the percentage of optimized programs that are correct and at least 10% faster than the original programs, and an up to 3.97x speedup when optimizing human-written code, and it consistently outperforms the best baseline by up to 96.51% in terms of opt%. Furthermore, Optimo achieves an up to 42.42% opt% and an up to 13.51x speedup when optimizing LLM-generated code.

阅读 arXiv 原文
代码质量与优化 · 4/30 · 2026-07-24测试质量挖掘与代码互验证MineValiCoder通过过滤错误测试用例和二分图互验证提升代码生成可靠性。MineValiCoder: Reliable Code Generation with Test Case Quality Mining and Bipartite Graph-Based Mutual Validation

Large Language Model (LLM)-based Test-Driven Development (TDD) has advanced automated code generation. However, existing approaches depend heavily on human-crafted test cases and cannot operate effectively when only natural-language requirements are available. Although recent work enables automatic test generation, it often overlooks the inherent stochasticity of LLMs, leading to two key defects: faulty tests generate misleading feedback that distorts code optimization, while mixed-quality test cases produce conflicting evaluation signals that hinder reliable code selection. To address these challenges, we propose MineValiCoder, a collaborative closed-loop TDD framework based on the mutual reinforcement of test-case quality and code quality. MineValiCoder comprises three modules. The Test Case Quality Mining (TCQM) module filters faulty test cases through self-validation, providing reliable optimization supervision. The Parallel TDD Refinement module iteratively optimizes code and generates diverse high-quality code candidates using validated test-case feedback. The Bipartite Graph-Based Code-Test Mutual Validation (BiCoTeV) module dynamically models code-test interactions and performs mutual validation scoring for stable and reliable optimal-code selection. Extensive evaluations across four LLMs and mainstream benchmarks show that MineValiCoder significantly outperforms state-of-the-art methods. Specifically, it achieves Pass@1 scores of 96.34% on HumanEval, 87.40% on MBPP, 64.00% on APPS, and 51.33% on LiveCodeBench. These results demonstrate the effectiveness of MineValiCoder in mitigating LLM stochasticity and improving the reliability of automated code generation.

阅读 arXiv 原文
代码质量与优化 · 8/30 · 2026-07-24伪实验数据驱动的优化PolyBO在有限实验数据下生成高质量伪数据加速优化收敛。Optimization of time-consuming experimental conditions using pseudo-experimental data guided by adaptive polynomial regression

Bayesian optimization (BO) is an optimization method that sequentially proposes the next candidate explainable variables for optimizing target variables by balancing exploration and exploitation. BO is often used under a limited evaluation budget, such as hyperparameter tuning of deep learning. Despite its effectiveness, conventional BO may have poor convergence in practical experimental science where each evaluation is often costly and time-consuming. Recently, BO methods have been proposed that accelerate optimization by using pseudo-experimental data that simulate experimental data. However, when only a limited number of experimental data are available, the generated pseudo-experimental data may be of insufficient quality. In this study, we developed PolyBO to improve optimization time by generating high-quality pseudo-experimental data even when the number of trials is limited. PolyBO performs BO efficiently by generating pseudo-experimental data with an adaptively updated versatile parametric model. This low-capacity polynomial regression model is intended to enable efficient BO even with limited experimental data. PolyBO updates the BO surrogate model with a combined dataset consisting of experimental data and pseudo-experimental data and then performs optimization. Using synthetic benchmark functions with diverse landscapes, we found that PolyBO reduced the optimization time by a median of 42\%. For a real-world material composition optimization problem, PolyBO reduced the optimization time by a median of 96\% compared with conventional methods. Overall, PolyBO achieves efficient optimization in settings where each experiment requires a long time.

阅读 arXiv 原文
代码质量与优化 · 0/30 · 2026-07-23射电天文代码可持续优化利用LLM帮助LOFAR望远镜升级中的代码性能优化和加速器移植。Enhancing SLMs for Sustainable Code Optimization in Radio-Astronomy

Recent Large Language Models (LLMs) can produce and optimize complex code. We investigate the use of LLMs to generate and optimize code for large-scale sciences, focusing on radio astronomy and sustainability. The LOFAR telescope is currently being upgraded, significantly increasing the sky area observed, while simultaneously processing more data faster. However, this is expected to increase the computational requirements 40-fold. This upgrade thus critically depends on rigorous performance optimization of existing software and widespread adoption of accelerators. The code base is very large, making this a daunting task. We therefore investigate and demonstrate an AI-driven approach meant to assist developers in evaluating and optimizing their code, including porting to hardware accelerators. The LOFAR community is committed to sustainable solutions, and needs to achieve these improvements without increasing the energy budget. We thus need to optimize existing codes or port them to accelerators, while making sure that the optimization process itself is also energy efficient. This poses a challenge, since LLMs are energy-intensive. We therefore propose to use Small Language Models (SLMs) instead to limit environmental impact. In this paper, we show how to enhance SLMs through the use of agentic AI. We extend the SLMs in two ways to improve code generation quality and performance: first with a multi-sampling generation strategy and second with incorporating compiler feedback. We demonstrate that multi-sampling SLMs can match or surpass larger single-generation models with fewer computational resources and that feeding compiler output back into the SLMs leads to consistent improvements across all tested models. Our approach is generic, and can also use Retrieval Augmented Generation (RAG) as well as static and dynamic analysis tools in the code generation pipeline.

阅读 arXiv 原文
代码质量与优化 · 6/30 · 2026-07-22面向对象的智能体编程模型智能体即Python对象,方法就是动作,字段即状态,文档即提示。NVIDIA-labs OO Agents: Native Python Object-Oriented Agents

Traditional agent development is split across prompt templates, tool schemas, callback code, and workflow graphs. We present NVIDIA Object-Oriented Agents (NOOA), a model-agnostic Python framework for building reliable AI agents. NOOA takes a simpler approach: an agent is a Python object. Its methods are the actions the model can take, fields are its state, docstrings are its prompts, and its type annotations are contracts. A method whose code body consists of "..." is completed at runtime by an LLM-driven agent loop, while methods with normal bodies remain standard deterministic Python. This gives developers and agents the same interface, so agent behavior can be tested, traced, refactored, and improved just like other software. This paper makes three contributions. (1) We present the agent-as-a-Python-object programming model and the design principles behind it. Where Python has existing abstractions, we adopt them directly. Agent-specific capabilities--context, events, state rendering, long-term memory, and validated LLM loops--are exposed through simple Pythonic APIs, so both developers and agents share one familiar programming model. (2) We identify six model-facing ideas that NOOA is, to our knowledge, the first to combine on a single surface: typed input/output, pass-by-reference over live objects, code as action, programmable loop engineering, explicit object state, and model-callable harness APIs for context and events. We find the community already converging on several of these ideas--often as experimental or partial features--and present the comparison to encourage further adoption. (3) We demonstrate that current models use this interface effectively, both in targeted capability tests and on agentic and reasoning benchmarks such as SWE-bench Verified and Terminal-Bench 2.0 and ARC-AGI-3.

阅读 arXiv 原文
代码质量与优化 · 3/30 · 2026-07-22多源跨场景策略代码优化MoST整合教科书和网页等多来源策略,适用于不同编程语言场景。Multi-Source and Cross-Scenario Strategy-Guided Code Optimization

Automated code optimization improves program performance by refactoring source code, and recent studies use LLMs to generate optimization patches. The newest approaches are strategy-guided: they summarize strategies from historical optimization commits as static analysis rules, and use these rules to match code locations for LLMs to optimize. However, these approaches have two limitations: (1) the strategies may come from other knowledge sources, such as textbooks and web pages, but the existing approaches cannot utilize them; (2) a strategy may be applicable to different scenarios, e.g., different programming languages, but existing approaches can only formalize strategies for the scenario to which the source commit belongs. To address these limitations, we propose MoST, an LLM-based code optimization framework that integrates multiple knowledge sources across scenarios. MoST uniformly represents items in different knowledge sources as evidence objects, clusters them in a cross-source and cross-scenario manner to identify strategies, and transfers them to the target scenario when necessary for generating static analysis rules. To implement this process, MoST employs a novel self-balanced weighted clustering algorithm to balance evidence objects from different knowledge sources, and a novel example transfer procedure to ensure the quality of the generated rules when transferring across scenarios. On a benchmark containing 151 C/C++, 150 Python, and 50 Rust historical optimization tasks, compared with SemOpt, MoST yields 24.44%-180.00% and 21.88%-37.50% more patches that are exactly the same as or semantically equivalent to developer patches, respectively. When optimizing 15 real-world projects, MoST achieves 19.72%-717.42% maximum improvements and 4.44%-258.17% average improvements for the performance tests in the projects, significantly outperforming SemOpt and Codex.

阅读 arXiv 原文
代码质量与优化 · 6/30 · 2026-07-22分析引导的仓库级代码优化PerfAgent通过分析器反馈迭代优化,找到隐藏热点并保证正确性。PerfAgent: Profiler-Guided Iterative Refinement for Repository-Level Code Optimization

Large language model (LLM) agents now perform well on correctness-oriented repository-level tasks, including SWE-Bench issue resolution and feature implementation in real codebases. However, they still struggle with repository-level code optimization, which requires preserving behavior while improving runtime performance. Passing tests is not enough in this setting; a patch must preserve behavior, implement code optimization, and approach expert speedups. Current agents often miss bottlenecks hidden behind abstraction layers and native extensions, stop after shallow speedups, or insufficiently test the code patches that thus may silently break edge cases. We present PerfAgent, a profiler-guided, verifier-in-the-loop workflow that gives an off-the-shelf coding agent the feedback needed to find real hotspots, improve beyond the first passing patch, and use profiler evidence rather than timing alone to decide what to optimize next. On two challenging optimization benchmarks, GSO and SWE-fficiency-Lite, PerfAgent more than doubles the rate of expert-matching patches over OpenHands with GPT-5.1, improving from 19.6% to 39.2% on GSO and from 26% to 74% on SWE-fficiency-Lite. It also surpasses an oracle best-of-five baseline at substantially lower cost, showing that the gains come from better feedback rather than additional test-time sampling.

阅读 arXiv 原文
代码质量与优化 · 6/30 · 2026-07-21可控难度标签化代码数据集Spaghetti Architect通过反优化转译生成五种语言的有标签代码数据。Spaghetti Architect: A Contamination-Resistant, By-Construction-Labelled, Multi-Language Code Dataset Generator

Mined code corpora are abundant but uncontrolled: a snippet's semantics, surface "messiness," and difficulty are whatever the wild contained; there is no known-optimal reference to grade against; and any public sample may already sit in a model's training set. We present Spaghetti Architect, a tool that mints code datasets with the control such corpora lack. An anti-optimization transpiler maps a clean, language-agnostic JSON intermediate representation to deliberately redundant, fully-flattened programs in five languages (Python, JavaScript, Go, Java, C++); every program is compiled, run, and checked against a reference oracle, so each instance is correct by construction. The clean IR is a known-optimal reference, messiness is dialed by strictly-nested anti-pattern profiles, each instance is labelled along two orthogonal difficulty axes, intrinsic (problem size) and incidental (presentation at fixed semantics), and contamination is resisted by minting fresh variants from a private held-out seed. We give construct-validity evidence that the quality order moves established complexity and readability metrics, and report baselines on a four-model open ladder: exact match rises with scale, and the intrinsic knob collapses arithmetic-aggregation accuracy of even the strongest model to zero. Further, development-set scores equal freshly re-minted held-out counterparts within $|Δ|\le 0.012$ (comprehension) and $\le 0.011$ (refactoring); on identical programs, refactoring equivalence ($0.73 \rightarrow 0.99$) is scale-invariant while output prediction collapses; and ablating the generator's self-annotations shows they inflate the weakest model an order of magnitude more than the strongest ($-0.173$ vs $-0.017$): the annotated ladder resolves one of three adjacent pairs where the unannotated resolves all three. Open source (MIT), dependency-free, archived under a persistent DOI.

阅读 arXiv 原文
代码质量与优化 · 5/30 · 2026-07-19自动化库采纳重构发现Prefactory用LLM合成可执行搜索启发式,而非反复提示LLM。Prefactory: Automated Discovery and Application of Library-Adoption Refactorings

Replacing hand-written code with library API calls is a common refactoring that can reduce code size, make code more idiomatic, and reuse well-tested implementations. Yet many library-adoption opportunities are hard to find automatically: the original code often does not mention the target library and may resemble the library API only in behavior, with little syntactic overlap. Existing tools, such as linters and static modernizers, cover only a small set of manually specified patterns. LLMs and LLM-based agents, on the other hand, can generalize to more patterns, but they are costly, difficult to reproduce and to apply systematically at scale. This paper introduces Prefactory, an automated approach for library-adoption refactoring in Python. The key idea is to use an LLM to synthesize executable search heuristics rather than relying on repeated LLM prompting over a codebase. Given a target project and a target library name, Prefactory collects library metadata and project vocabulary, then generates lexical and structural detectors. Prefactory executes the detectors during a scan phase to find candidate functions. It then heuristically ranks the candidate functions, generates refactorings for the highest-ranked ones using an LLM, and validates the results with project tests and newly generated differential tests. We evaluate Prefactory on PrefactoryBench, a benchmark of 100 real-world library-adoption refactorings from 61 open-source Python projects and 18 libraries. Prefactory detects 75 instances at the file level and 56 at the function level, compared with 35 and 32 for the strongest baseline (Codex CLI). From the 56 detected functions, Prefactory produces 40 test-validated refactorings.

阅读 arXiv 原文
代码质量与优化 · 7/30 · 2026-07-14语义变更提交自动识别SemaDiff通过生成测试方法执行行为分析区分语义保持与变更的提交。SemaDiff: Identifying Semantic-Changing Commits with Generated Code and Tests

Distinguishing semantic-preserving commits from changing ones remains an open challenge in software repository mining. While existing approaches detect refactoring commits accurately, they cannot ensure that a commit is purely semantic-preserving, without any interleaving behaviour-changing modification. This limitation can impact several tasks, such as debugging, fault localisation, bug dataset construction, rollback analysis, and bug fixes backporting. To fill this gap, we propose SemaDiff, a novel approach for identifying semantic-preserving commits through behaviour-based analysis; comparison of similar test execution on pre- and post-commit versions. As code impacted by the refactoring is often hard to test and different accross both versions, we propose generating additional calling methods to that code, which serve as testing target. Given a commit, SemaDiff analyses the diff to identify modified code and extracts unchanged dependent code that calls it. It then generates an additional dependent class using a large language model to exercise the changed code in both versions, and automatically generates tests for the dependent code. This way, we obtain the same tests for the different code versions, enabling the behavioural-difference detection. The commit is classified as semantic-preserving only if all generated tests produce identical outcomes across the two versions. To evaluate SemaDiff, we construct and annotate manually a dataset of 183 commits, gathered from well-known open-source Java projects. The obtained results show that SemaDiff distinguishes accurately semantic-preserving from -- changing commits in about 76% of the cases, with a 100% precision in semantic-changing commit detection.

阅读 arXiv 原文
代码质量与优化 · 3/30 · 2026-07-13积累行为规则自我改进编码将代码审查反馈转化为持续行为规则,智能体逐步扩展自检能力。Self-Improving AI Coding Agents Through Accumulated Behavioral Rules: A Closed-Loop Framework

LLM-based coding agents repeat the same classes of mistakes across sessions because they lack a mechanism to retain corrections from human review feedback. We present a closed-loop framework in which every accepted review comment is codified as a persistent behavioral rule, progressively expanding the set of error classes the agent can self-detect. The framework combines an accumulating rule set in a version-controlled instruction file, a self-review checklist executed before code submission, and automated validation that ensures rule set integrity as it grows. In deployment across a 35+ service microservices platform, the rule set grew from 5 to 18 behavioral rules, 15+ language-specific standards, and a 15-item self-review checklist, all derived from real review feedback. We present empirical results from 11 recorded working sessions spanning code generation, PR review, incident investigation, and cross service refactoring. We observe that accumulated rules shift review effort from low-level correctness toward design-level validation, achieve a measured 0% recurrence rate for ruled-against error classes, and transfer across heterogeneous agent interfaces. We compare our approach against related work in experiential LLM learning (Reflexion, ExpeL, Voyager) and automated code review (CodeReviewer, SWE-bench agents), showing that our framework achieves persistent cross-session learning without weight updates, operates on production codebases rather than synthetic benchmarks, and addresses an orthogonal dimension (behavioral consistency over time) that existing benchmarks do not measure. The result is a coding agent that improves with every review cycle, accumulating the engineering wisdom of its human collaborators without changing a single model weight.

阅读 arXiv 原文
代码质量与优化 · 3/30 · 2026-07-11代码异味检测奉承偏差缓解通过证据引导推理提示降低LLM在代码异味检测中的决策翻转率。Mitigating LLM Sycophancy in Code Smell Detection Using Evidence-Guided Reasoning Prompts

Large Language Models (LLMs) are increasingly used for code smell detection tasks due to their ability to interpret program semantics. However, their reliability in this context remains poorly explored, particularly under varying prompt conditions where model predictions may be influenced by external cues rather than code characteristics. One such limitation is sycophancy bias, where models tend to align their outputs with user-provided assumptions instead of performing objective analysis. In this paper, we present the first systematic empirical study of sycophancy bias in LLM-based code smell detection. Using the MLCQ dataset, we evaluate how different prompt framings like confirmation bias, contradictory hints, and false premises affect model predictions. Our results show that LLMs are highly sensitive to prompt variations, with Decision Flip Rates reaching up to 72% and False Alignment Rates exceeding 90%, indicating substantial instability and agreement with misleading prompts. To address this issue, we propose Evidence-Guided Debiasing Prompting (EGDP), a structured prompting strategy that enforces evidence-first reasoning. EGDP reduces decision instability and improves robustness, lowering Decision Flip Rates to as low as 12% and False Alignment Rates to as low as 21%, while increasing reliance on structurally grounded evidence. Our findings demonstrate that sycophancy bias poses a critical threat to the reliability of LLM-based code smell detection, and that evidence-guided reasoning provides an effective and generalizable mitigation approach.

阅读 arXiv 原文
代码质量与优化 · 3/30 · 2026-07-11机器学习容器化实践分析ML容器平均10.27GB,构建约8.84分钟,44.4%提交触发重构。ML in a Box: Analyzing Containerization Practices in Open Source ML Projects

Containerization has become increasingly essential in the machine learning (ML) domain, providing reproducibility, portability, and environment consistency. While prior studies have analyzed Dockerfile structures and best practices, none have examined ML projects in depth to reveal how the iterative nature of ML workflows influences container footprint, build performance, and caching behavior. We present the first large scale empirical study of 1,993 ML related Dockerfiles, combining quantitative analysis of container roles in ML projects and build dynamics with a qualitative investigation of refactoring practices. Results show that containers serve distinct roles across training, inference, and infrastructure. Containers are typically large, averaging 10.27 GB in size, and require long build times of about 8.84 minutes. We find that 44.4% of commits trigger rebuilds, primarily due to context file changes (96.4%), with experimentation being the main motive behind those commits that initiate rebuilds. Despite partial cache reuse, 71% of rebuild work is wasted on redundant computation. From stable projects, we identify 7 recurring ML-specific Dockerfile refactoring patterns that improve build efficiency and reduce container footprint.

阅读 arXiv 原文
代码质量与优化 · 5/30 · 2026-07-08编码代理性能优化基准PERFOPT-Bench通过隐藏正确性测试和轨迹审计评价代理优化全流程。PERFOPT-Bench: Evaluating Coding Agents on Software Performance Optimization

Coding-agent benchmarks have largely measured whether agents can produce functionally correct patches, but production software also demands measurable speedups on real execution targets. Performance optimization is a distinct agentic task: agents must profile executions, diagnose cross-layer bottlenecks, edit code without breaking correctness, and verify that gains are reproducible rather than measurement artifacts. We introduce PERFOPT-Bench, a benchmark for evaluating this full performance-engineering loop. Each task provides a correct but deliberately suboptimal codebase and asks the agent to improve a target performance metric; scoring requires hidden correctness tests, verified-speedup measurement, and trajectory-level audit. We evaluate 7 agent stacks with different LLMs and agent frameworks on 7 long-horizon optimization tasks. The results show that optimization performance is workload-dependent rather than determined by model identity alone: no single stack dominates, and changing the agent framework can materially change the same LLM's per-task speedup profile. We further find that raw speedup is unsafe as a benchmark score, since some large gains arise from benchmark-specific shortcut exploitation; an exploratory relay pilot suggests that restarting from an externalized optimization summary can recover additional headroom after an initial session stops. The benchmark and our evaluation are available at: https://anonymous.4open.science/r/Dataset-D3CC.

阅读 arXiv 原文

UI 与 GUI Agent(3 篇)

UI 与 GUI Agent · 3/30 · 2026-07-20计算机代理多任务通信设计Sidekick通过环境提示和多模态摘要改善代理后台操作时的用户切换体验。Sidekick: Designing Communication for Effective Multitasking with Computer Use Agents

Computer Use Agents (CUAs) can autonomously execute complex, multi-step tasks within GUIs, enhancing efficiency through parallel multitasking. However, our formative studies with CUA experts and GenAI users indicated that current feedback is primarily text-based, requiring sustained attention to monitor progress and offering limited visibility to trace past GUI interactions. Based on the findings, we developed a prototype system, Sidekick, for communicating CUAs' status with multimodal feedback across different stages of interaction: (i) When CUAs run in the background, Sidekick signals its execution state through ambient cues. (ii) Upon resuming interaction with CUAs, Sidekick provides multimodal summaries of completed actions to support rapid context resumption. (iii) When CUAs operate in the foreground, Sidekick enhances transparency by verbalizing and visualizing the agent's reasoning. A study with 30 participants demonstrated that Sidekick significantly improved multitasking performance with CUAs compared to baseline systems that presented textual feedback either in a typical chat or in an ambient display. Sidekick supported progress awareness, and error and action traceability more effectively. Finally, we demonstrate the promise of Sidekick through several example applications, and discuss implications for long-horizon human-agent collaboration.

阅读 arXiv 原文
UI 与 GUI Agent · 7/30 · 2026-07-16基于LLM的Figma原型插件AI Prototyper通过分解和检索增强生成自动从自然语言创建Figma图层。AI Prototyper: A Figma Plugin for Decomposition-Based GUI Prototyping with LLMs

Graphical user interface (GUI) prototyping remains a time-consuming activity that demands both design expertise and considerable manual effort. As GUI prototypes are non-code artifacts that evolve alongside requirements throughout the development cycle, automating their generation is directly relevant to software maintenance and evolution. We present AI Prototyper, an open-source Figma plugin that automates GUI prototyping through a decomposition and retrieval-augmented generation (RAG) pipeline. Given a natural-language description of a desired screen, such as a login page or a product detail card, the plugin decomposes the request into discrete GUI features, retrieves matching components from a custom 32-primitive library, and renders each component as a fully editable Figma layer with auto-layout. The pipeline uses Gemini 2.5 Flash as its LLM back-end and a Node.js Express service. Unlike existing decomposition-based tools, AI Prototyper introduces a human-in-the-loop editing step that lets users review, modify, or extend the generated feature list before rendering, uses a different technology stack and LLM family, and supports multilingual input, producing correctly labelled interfaces in Thai, English, and Mandarin Chinese. In a preliminary evaluation, participants using AI Prototyper completed more prototypes in a fixed time window than those working manually, and expert practitioners rated the AI-generated prototypes higher across nine quality dimensions. A demonstration video is available at https://youtu.be/pRoFAH7MQaE. The source code and component library are available at https://github.com/tongsalangsingha/AI-prototyper-tool

阅读 arXiv 原文
UI 与 GUI Agent · 9/30 · 2026-07-13从GUI测试到语音交互转换利用LLM将GUI测试代码转化为应用级语音助手的能力描述和执行计划。From GUI Tests to Conversational Interaction: A New Perspective on App-Specific Voice Assistants

Voice assistants are widely deployed on mobile platforms, yet most are designed as system-level services that remain poorly aligned with application-specific behavior. As a result, enabling voice interaction at the app level requires developers to manually reimplement application logic, leading to high development and maintenance costs. We propose an LLM-driven approach to automating the development of app-specific voice assistants by repurposing GUI test code, which encodes behavior-preserving, executable specifications of application functionality. In this paper, we present a perspective in which large language models reinterpret GUI tests as bridges between application behavior and conversational interaction. By transforming test methods into app-specific VA artifacts, such as voice intents, capability descriptions, and executable action plans, our approach grounds voice assistants directly in existing application logic rather than external specifications. We illustrate this vision through AppVA, a research prototype on Android. Our preliminary results across five open-source applications suggest that GUI test code can be reused beyond testing, enabling the synthesis of app-specific voice assistants and highlighting a broader research direction at the intersection of software testing, interaction design, and LLM-enabled automation.

阅读 arXiv 原文

个人知识与本体(18 篇)

个人知识与本体 · 4/30 · 2026-07-27隐式关联盲点基准提出InMind基准测试,揭示记忆检索与查询之间的隐含关联盲点。Keep It InMind: Benchmarking the Implicit-Association Blind Spot in Agent Memory

Long-term memory systems store what a user says in an external store and retrieve it when a related query arrives. This interface rests on an assumption so natural that it is rarely stated: a memory that is needed will resemble the query that needs it. World knowledge breaks the assumption. A tree-nut allergy should change the answer to a macaron request through their almond-flour ingredient, yet the two texts share no cue a retriever can see. We call this failure mode the implicit-association blind spot and introduce InMind, a 125-task, expert-verified benchmark spanning ten life domains, with 113 tasks grounded in citable public sources. Its paired controls separate three explanations that existing evaluations conflate: the fact was never stored, the model lacks the bridging knowledge, or the fact was stored and never surfaced. The verdict is clean. With the decisive memory placed in context, the backbone answers 84.0 percent of indirect queries; when the same memory must be retrieved, six vector, graph, and agentic memory systems reach at most 14.4 percent, even though they recall the same facts on demand at up to 100 percent. An embedding with eight times the dimensionality raises answer-blind target recall for every system yet leaves the gap essentially intact. A minimal diagnostic probe that keeps memory visible before the query arrives recovers most of the gap, locating the failure in the query-conditioned interface itself and pointing to routing, deciding which facts must stay visible, as the open problem InMind is built to score.

阅读 arXiv 原文
个人知识与本体 · 3/30 · 2026-07-27事务性信念提交协议MemTX引入快照隔离事务管理智能体信念,防止污染数据驱动不可逆操作。MemTX: Transactional Belief Commit for Stateful Agent Memory

LLM agents increasingly coordinate through persistent shared memory: one agent's write becomes another agent's premise, and eventually a tool call with real side effects. Current agent memory systems treat every accepted write as immediately actionable truth, so a polluted tool result, a stale update, or a teammate's half-finished note can silently drive an irreversible action. We argue that a memory write is not a belief commit. We present MemTX, a transactional belief-commit protocol. Each record carries evidence, permissions, provenance, and validity. Writes are staged inside snapshot-isolated transactions and admitted by a validate-and-commit pipeline, irreversible tool calls are gated on in-flight belief state, and retracting a belief triggers typed cascading repair of its derived records and tool side effects. Two invariants, action-safety gating and cascade-repair completeness, are machine-checked by property-based testing and bounded exhaustive enumeration of 5.5 million protocol states, with zero violations. Across five backbones from three model families, MemTX leads all eight baselines with paired-McNemar significance on four backbones and statistically ties the best baseline on the fifth and strongest, while remaining the only method with zero downstream harm on every backbone. Backbone capability does not substitute for commit discipline.

阅读 arXiv 原文
个人知识与本体 · 5/30 · 2026-07-24先验事实的智能体记忆评估反转传统流程:先播种事实再生成对话,建立可靠记忆评测。Ground Truth First: A Longitudinal Evaluation Instrument for Agent Memory, and the Tenure Crossover in Memory-Architecture Rankings

Benchmarks for LLM-agent memory typically generate conversations first and extract answer keys afterwards -- with documented label-error and contamination problems -- and they overwhelmingly measure short interaction histories. We invert the pipeline: a seeded life-script sampler emits facts with validity intervals, volatility classes, and source channels before any text exists; an LLM renderer writes chat and email from per-event fact manifests; a fidelity verifier confirms every planted fact; and questions are instantiated mechanically from the script, so gold answers are script-valid by construction and separately validated for answerability. The synthetic, fictionalized corpus (~380 questions, 15 types) embeds features absent from the benchmarks we survey: per-fact validity intervals, sent/received trust distinctions, injection probes in a benign harness, and as-of-date question sets. Benchmarking five memory architectures against a no-memory control (fixed answerer, versioned LLM judge, three replicates, two horizons), we find backend rankings invert with history length: the budgeted curated-map memory that leads at three weeks loses recall of evicted content by nine weeks (96% to 72%) while a provenance-typed graph rises to 90%; the inversion is positive for all six users under complete cross-family re-judging (exact p=0.031). A full-rendered-history baseline ties or exceeds the best memory system at the short horizon but shows no judge-independent advantage at nine weeks, at about twice the read cost. Write-stage quality strongly correlates with downstream quality (weakly-written facts fail 24% vs 2%), and injection resistance tracked whether provenance boundaries survive representation. A layered architecture performs best among the memory systems in both regimes (96.8% short-horizon) and is released as Veracium, an open-source library, with the corpus generator and harness.

阅读 arXiv 原文
个人知识与本体 · 3/30 · 2026-07-23智能体上下文管理生命周期将智能体记忆视为全生命周期问题,而非简单存储检索。Agentic Context Management: Solving Agent Memory and Cost by Treating Them as Lifecycle and Architecture Problems

Production AI agents' failures are less often due to an inability to reason well and more often because they cannot manage what is in their reasoning context: conversation histories, large prompts, large tool definitions, and ballooning tool outputs. Agents drown in their own accumulating history while paying a token cost that grows every turn, producing missing recalls within and across conversations. The incumbent response treats this as a storage-and-retrieval problem. We argue that framing is too narrow. Actively managing what an agent holds in mind is a lifecycle, not merely a store: it spans deciding what to remember, extracting and structuring it, choosing the right store per data type, consolidating and forgetting while preserving provenance, deciding what is relevant now, anticipating what is needed next, and compacting context to a budget without losing what matters. In serious production this operates not over a single user but across an organizational scope hierarchy. We name this discipline Agentic Context Management (ACM) and decompose it into five primitives: architecting, ingesting, scoping, anticipating, and compacting & consolidation. We then make the economic case: naive context accumulation grows token cost quadratically in conversation length, crude summarization buys linear cost at the price of an accuracy cliff, and only validated compaction achieves linear cost with preserved fidelity. We describe a reference implementation, Maximem Synap, that realizes the five primitives as a multi-tenant service and reports 92% on LongMemEval and 93.2% on LoCoMo under the configuration detailed in Section 6. We close with dimensions existing benchmarks do not yet capture, latency, token efficiency, and context-rot resistance, and the frontier of decision-level and organization-level context the category points toward.

阅读 arXiv 原文
个人知识与本体 · 8/30 · 2026-07-23智能体记忆互操作性框架MemTools解耦记忆生命周期组件,实现异构系统的可互换组装。MemTools: A Unified Research Framework for Interoperable Agent Memory

While memory systems are essential for agent architectures, pervasive architectural fragmentation restricts systematic research. Existing implementations typically couple different stages of the memory lifecycle, entangle evaluation logic with specific datasets, and provide limited support for the management of heterogeneous memory types. We introduce MemTools, an interoperability research framework that decouples memory system components from their underlying deployment environments. MemTools standardizes the memory lifecycle through declarative data contracts, enabling the interchangeable assembly of components across different systems. It orthogonally separates benchmark datasets from execution protocols to facilitate controlled assessments. Furthermore, MemTools provides a unified computational interface for coordinating symbolic, neural, and multimodal memory representations within a shared runtime. Empirical evaluations on cross-system component integration, evaluation protocol reconfiguration, and heterogeneous memory coordination demonstrate that MemTools enables systematic isolation and analysis of memory design variables. These findings suggest that MemTools provides a practical and extensible infrastructure for advancing principled research on agent memory.

阅读 arXiv 原文
个人知识与本体 · 3/30 · 2026-07-23属性引导的记忆过程反馈通过归因分析提供中间记忆内容的精细信用分配。AttriMem: Attribution-Guided Process Feedback for Agent Memory Learning

Effective memory is crucial for LLM agents, yet constructing it effectively remains challenging. A memory-construction policy decides what information to extract, store, update, compress, or discard as interactions accumulate. Heuristic memory methods rely on subjective, task-specific rules, which can misalign with downstream objectives and limit cross-task adaptability. RL-based methods, by contrast, learn from task feedback but mainly use outcome- or module-level rewards. These coarse signals indicate task success but cannot identify which intermediate memory contents support the final answer, creating a fine-grained credit-assignment bottleneck. However, constructing such process feedback is prohibitively difficult because intermediate memory decisions lack unique ground-truth targets, while the appropriate credit varies with the agent's uncertain reasoning trajectory and therefore cannot be specified in advance. We propose AttriMem, an attribution-guided process-feedback framework for learning memory-construction policies with RL. AttriMem augments the global outcome reward with local rewards derived from token-level contributions to the final answer. Experiments on long-horizon dialogue question answering show that AttriMem outperforms retrieval-based, heuristic, and RL-based baselines, generalizes across benchmarks and answer models, stabilizes RL optimization.

阅读 arXiv 原文
个人知识与本体 · 0/30 · 2026-07-21序列学习者多关系图建模MR-ConceptGCN利用多关系图网络对学习者进行无监督序列建模。Sequential Learner Modeling Using Multi-Relational Graph Convolutional Networks

User modeling is a critical task in a variety of personalized systems. Recognizing their effectiveness in learning from graph-structured data, Graph Neural Networks (GNNs), particularly Graph Convolutional Networks (GCNs), are increasingly employed for user modeling. However, existing approaches typically treat different relation types in a graph as homogeneous, limiting their ability to capture richer semantics and construct more informative user models. While multi-relational GNNs (MR-GNNs) have been adopted for representation learning and recommendation, their application for user modeling remains unexplored. Moreover, existing GNN-based user modeling approaches ignore the user interaction sequence. To address these research gaps, in this work we propose MR-ConceptGCN, a novel fully unsupervised approach focused on concept-based sequential learner modeling using multi-relational GCNs (MR-GCNs). MR-ConceptGCN effecively combines Personal Knowledge Graphs (PKGs), MR-GCNs, and the pre-trained language model SBERT to obtain enhanced relation- and semantic-aware representations of the PKG items. The enriched embeddings of the knowledge concepts that a learner did not understand when interacting with learning materials in CourseMapper are then used to construct a sequential learner model that combines long-term and short-term learner interactions. We report the results of an online user study (n = 31), demonstrating the benefits of MR-ConceptGCN in terms of several important user-centric aspects including accuracy, usefulness, diversity, and satisfaction with an educational recommender system.

阅读 arXiv 原文
个人知识与本体 · 7/30 · 2026-07-21路由式智能体记忆架构每个查询映射到检索/合成模式,在三个基准上展示参考结果。Supra Cognitive Modes: A Routed Architecture for Agent Memory

Agent-memory workloads mix direct factual lookup, relation-chain and current-state reasoning, and broad synthesis over long histories. We describe Supra Cognitive Modes (SCM), an architecture that maps explicit or automatically selected per-query modes to retrieval and synthesis payloads over one shared ingest substrate. A frozen semantic classifier and runtime gates dispatch queries among fused lexical and dense lookup, graph or iterative multi-hop handling, and stratified long-form synthesis. The substrate combines multi-granularity embeddings, extracted triples, fact-version metadata, and optional asynchronous enrichments. We characterize the deployed configuration on three benchmarks: Long-term Conversational Memory (LoCoMo; n = 1,986), MemoryAgentBench (MAB; n = 3,671), and LongMemEval (n = 500). The reference run records 84.87% on LoCoMo factoid categories and 68.61% on adversarial abstention, 61.49% on MAB across two repetitions, and 86.00% on LongMemEval. A repository-backed reproduction produces similar aggregate scores and supports task- and mode-conditioned failure analysis. Raw baseline outputs, aligned end-to-end timing for LoCoMo and LongMemEval, and complete token ledgers are unavailable; stored rows also omit some final runtime decisions. The results characterize one implemented routed configuration and its diagnostic failure patterns, while source inspection verifies the per-query control interface and shared-substrate design. Causal routing effects, efficiency gains, and statistical significance remain outside the available evidence.

阅读 arXiv 原文
个人知识与本体 · 3/30 · 2026-07-20注意力引导的记忆优化通过检索头注意力揭示智能体对记忆片段的利用模式,指导精炼。Mechanistic Attention Guidance for Agent Memory Refinement

Existing self-evolving memory systems mainly improve agent memory based on textual outputs, such as task trajectories and reflections. However, this text-based paradigm rarely incorporates internal mechanistic signals, leaving how retrieved memory is actually utilized during task execution underexplored. This limitation can lead to unreliable error attribution and hallucinated memory modifications. In this work, we show that retrieval-head attention provides a mechanistic signal for revealing segment-level memory utilization. By aggregating attention over memory segments and decision steps, we construct a context utilization matrix that exposes recurring memory-use patterns and indicates corresponding refinement strategies. Building on this observation, we propose Attention-Guided Memory Refinement (AGMR), a framework that uses utilization patterns revealed by attention to guide targeted segment-level memory updates. AGMR corrects or enhances memory for failed executions, simplifies memory for successful executions, and verifies each update through re-execution. Experiments on interactive decision-making benchmarks show that AGMR improves both task performance and memory efficiency over text-only memory refinement baselines. Code is available at https://anonymous.4open.science/r/AGMR_code-3262/

阅读 arXiv 原文
个人知识与本体 · 7/30 · 2026-07-20预算约束的记忆保留决策形式化预算约束下的记忆保留与合并操作符选择。Retain or Consolidate? Budget-Dependent Operator Selection for Language Agent Memory

Language agents depend on memory across interactions. However, the limited context windows of large language models (LLMs) and their inference costs constrain how much memory can be used at once. Existing systems mainly follow two strategies: memory retention and memory consolidation. Retention keeps raw records and preserves exact details, but relevant evidence may not fit under a tight budget; consolidation compresses and combines records, improving coverage per token but risking the loss of query-critical details. Neither strategy is universally preferable. This raises two central questions: when should consolidation replace retention, and which operator -- Merge, Abstract, or Rewrite -- should be selected? We formalize this decision by decomposing each operator's utility into a coverage effect on evidence omitted by retention and a signed replacement effect on raw evidence that already fits. Their balance explains why the preferred action changes with relative budget pressure. We implement this mechanism with Offline Abstraction-Safety (OAS), a lightweight learner that estimates action utilities from pre-generation features with held-out harm calibration. The public LongMemEval and LoCoMo benchmarks show the same budget-dependent pattern. On LongMemEval, consolidation improves absolute accuracy by up to 48% under tight budgets, whereas retention is preferable under loose budgets; LoCoMo replicates this crossover at a smaller budget, consistent with its shorter evidence. On both datasets, cross-note abstraction and merging generally outperform local rewriting when compression is necessary.

阅读 arXiv 原文
个人知识与本体 · 4/30 · 2026-07-18长上下文组合推理记忆基准RECON用24个案例文件测试智能体在5-10万token上的六类记忆任务。RECON: Benchmarking Agent Memory for Compositional Reasoning over Long Contexts

Large language models and LLM-based agents are widely used as personal chat assistants, enterprise copilots, and autonomous workflow agents. In all these applications, memory (the ability to retain, access, and reason over information accumulated over long contexts and multiple interactions) plays a crucial role in determining the reliability of any agent. We introduce RECON (Reasoning over Extended Contexts with Obfuscated Narratives), a benchmark for evaluating compositional reasoning over long contexts. RECON spans 24 case files across three domains (criminal, medical, and financial), each ranging from 50k to 100k tokens, and tests agents on six memory intensive tasks: reconstructing multi-hop evidence chains, propagating cascading invalidations, resolving source conflicts, counterfactual reasoning, satisfying temporal constraints, and temporal fact retrieval. Recent memory benchmarks evaluate whether agents can retrieve scattered facts or detect if a fact has changed whereas RECON evaluates what happens after the change, whether agents can trace which downstream conclusions are affected, which survive through independent support, and how alternative timelines would have unfolded. Our evaluation reveals substantial limitations across current architectures: even the strongest non-Oracle system reaches only 22.4% Accuracy, with retrieval and reasoning each surfacing as challenges.

阅读 arXiv 原文
个人知识与本体 · 3/30 · 2026-07-17查询时延迟构建的长期记忆LazyMem在查询时用轻量模型选择性保留和压缩相关内容,避免噪声。LazyMem: Retrieve Broadly, Construct Selectively for Efficient Long-Term Agent Memory

Long-term memory lets LLM agents reuse past interactions, but raw dialogue histories are verbose and information-sparse. Retrieving broadly improves evidence coverage yet overwhelms downstream reasoning with noise; compressing at write time reduces noise but irreversibly discards details the future query may need. We introduce LazyMem, which sidesteps this dilemma by deferring all memory construction to query time. A lightweight 4B model processes the retrieved candidate pool in overlapping parallel windows, selectively retaining and compressing only query-relevant content. The model is trained through supervised fine-tuning followed by group-based reinforcement learning with a format-gated composite reward that combines a rule-based action signal measuring selection accuracy with an LLM-judged quality signal measuring source faithfulness and query utility. On the LongMemEval benchmark, LazyMem-4B achieves an LLM-judge accuracy of 0.85 with only 213 memory tokens, 68.7$\times$ fewer than retrieval-only, and generalizes to LoCoMo (0.68) without target-domain training, while reducing mean latency over the prior query-time baseline. The 32B variant reaches 0.93, surpassing oracle-context references on aggregation-heavy question types. The code associated with this work is publicly available at https://github.com/allacnobug/LazyMem.

阅读 arXiv 原文
个人知识与本体 · 3/30 · 2026-07-14企业级智能体记忆数据库基座探讨Oracle数据库作为长周期智能体的记忆生命周期管理系统。Oracle Agent Memory as an Enterprise Memory Substrate for Long-Horizon AI Agents

Agent memory is a systems problem for long-horizon agents. Practical deployments require retention of task state across extended conversations, recovery of user-specific facts and preferences across sessions, and accumulation of procedural knowledge from prior outcomes. These requirements extend beyond document retrieval: a memory layer must determine which interactions become durable state, how that state is scoped, how it is retrieved under latency constraints, and how it is revised or removed over time. This report studies Oracle Agent Memory as a database-native memory substrate built on Oracle Database. Three themes organize the discussion: memory as a lifecycle spanning ingestion, extraction, consolidation, retrieval, summarization, and revision or removal; a layered architecture that separates an active memory core from a passive memory-store interface with explicit scope control across users, agents, and threads; and evaluation methodology in which downstream task accuracy is complemented by memory-centric measures such as evidence retrieval, recall, latency, and estimated token use. The report summarizes LongMemEval results, reaching 93.8% accuracy, compares Oracle Agent Memory against flat-history baselines, using about 10.7x fewer tokens, and published or reported external baselines where available, and closes with implementation-oriented appendix material covering setup, thread lifecycle, and search semantics.

阅读 arXiv 原文
个人知识与本体 · 3/30 · 2026-07-13人类与LLM语义导航比较人类在语义搜索中表现出更高的熵、更大步长和更广分散度。Comparing Semantic Navigation in Humans and Large Language Models using Natural Language Processing

Semantic memory retrieval can be conceptualized as navigation through conceptual space. We compared semantic search dynamics between humans and three large language models (GPT-4o, Gemini-2.5-Pro, Claude-Sonnet-4.5) using verbal fluency data. By applying trajectory-based NLP metrics to the items generated by 82 human participants and LLM output across eight temperature settings, we quantified three complementary dimensions: entropy (step size predictability), distance to next (successive semantic steps), and distance to centroid (global dispersion). Humans exhibited higher entropy, larger semantic steps and broader dispersion than all LLMs, indicating more variable and exploratory search. Temperature tuning produced only partial alignments, as individual metrics matched between humans and LLMs at specific settings, but no configuration reproduced the complete human profile (in all dimensions). These findings suggest that human semantic search implements a distinctive balance between local exploitation and global exploration that current model architectures fail to reproduce.

阅读 arXiv 原文
个人知识与本体 · 0/30 · 2026-07-13视觉经验影响语义记忆导航盲人与明眼人语义记忆检索模式有差异,视觉经验影响概念检索。Entropy in Semantic Memory Navigation in Blind and Sighted Individuals: The Effect of Visual Experience

Embodied accounts of semantic memory highlight the role of sensorimotor systems in acquiring and storing knowledge. Congenitally blind populations offer a critical test bed for these assumptions, providing an opportunity to assess whether conceptual grounding requires visual experience. In this study, we assessed semantic memory navigation differences between blind and sighted individuals using a property listing task with concrete and abstract concepts. We computed semantic entropy, an embedding-based natural language processing metric that captures the predictability of retrieval. Generalized linear mixed models revealed distinct navigation patterns across groups: while sighted individuals showed higher entropy for abstract than concrete concepts, blind participants did not. Instead, blind individuals exhibited higher entropy for visually salient concrete concepts (e.g., penguin). These results underscore the role of visual experience in the organization and dynamic navigation of semantic memory.

阅读 arXiv 原文
个人知识与本体 · 0/30 · 2026-07-13遗忘对概念对齐的影响模拟记忆衰减如何影响非合作博弈中共享意义的形成与演化。Forgetting Our Way to Shared Meaning: Effects of Forgetting on Conceptual Alignment in a Non-Partnership Coordination Game

Shared meaning in language requires people to learn and agree on categories. We ask how characteristics of agents' memories change the emergence and evolution of shared meaning. Without a coordination game, models of conceptual semantics cannot explain how shared meaning emerges and changes in groups of people; however, existing games assume that players share payoffs in a partnership setting. We model conceptual alignment as a non-partnership game and illustrate differences in actual and perceived conceptual convergence from counterfactual simulations using agents with varying levels of adaptiveness and memory degradation. We found that adaptive players achieved actual convergence faster and had closer final conceptual regions than non-adaptive players, while non-adaptive players perceived convergence earlier. Weighing novel information less over time resulted in more stable agreements than fixing the weight of novel information. Memory features are critical to the emergence and evolution of actual and perceived convergence.

阅读 arXiv 原文
个人知识与本体 · 6/30 · 2026-07-13智能机器人的长期物理共存PHILIA通过机器人网关抽象实现长期记忆、多机器人协调和安全物理执行。A Glimpse into Long-term Physical Coexistence with Intelligent Robots

Long-term physical coexistence with intelligent robots requires more than capable robot policies. A persistent robotic assistant must support diverse user-facing interfaces, maintain long-horizon memory of people and preferences, coordinate across robot embodiments, and translate human intent into safe physical execution. We introduce PHILIA, a multi-robot agent built around a robot gateway abstraction. PHILIA retains the rich interaction and tool ecosystem of OpenClaw while exposing robot-local runtimes, onboard perception, navigation, speaker, and robot policies through a unified capability interface. This design decouples low-frequency, high-semantic agent reasoning from high-frequency, low-level robot execution, enabling plug-and-play integration of user interfaces, robot embodiments, and policy backends. As a result, the user experience becomes compositional: advances in user interfaces, robot embodiments, robot policies, navigation, or interaction algorithms can improve the overall experience without redesigning the system. We validate the architecture on Astribot S1 robots while designing the robot gateway contract to support future heterogeneous robot platforms through a shared capability interface for observation, task execution, navigation, speech playback, status monitoring, and task cancellation. We present representative use cases in which agent memory and scene understanding are grounded in robot actions. These span interactive household scenarios, ranging from simple organization to challenging long-horizon and dexterous service tasks, such as packing a backpack and lifting a garbage bag. We highlight the human-robot interaction flow, where contextual understanding of user intent and preferences, together with human-in-the-loop confirmation or adjustment during execution, is essential for effective assistance.

阅读 arXiv 原文
个人知识与本体 · 0/30 · 2026-07-10成本感知多模态获取智能体SAGEAgent自进化决定每位患者需要哪些诊断模态,平衡准确性与侵入性。SAGEAgent: A Self-Evolving Agent for Cost-Aware Modality Acquisition in Multimodal Survival Prediction

Does every cancer patient truly need a complete diagnostic workup for accurate survival prediction? In multimodal clinical oncology, diagnostic modalities follow a clinically mandated order of escalating burden -- from demographics collected at intake to genomic profiling requiring specialized tissue analysis. Current multimodal survival methods either assume all modalities are available or passively handle missing data, but none actively reason about whether acquiring the next modality is justified for a given patient along this ordered workflow. We formulate this as a sequential decision problem and propose SAGEAgent (Sequential Acquisition Guided by Experience), a self-evolving LLM-based clinical agent that decides which diagnostic modalities to acquire for each patient, balancing predictive accuracy against clinical invasiveness. SAGEAgent reasons about each patient's evolving diagnostic state through clinical tools that translate numerical predictions into text, an episodic memory that retrieves similar past cases, and a semantic memory that accumulates reusable decision patterns from experience. Experiments on a glioma cohort combining TCGA-LGG, TCGA-GBM, and BraTS with four diagnostic modalities demonstrate that SAGEAgent achieves competitive survival prediction accuracy while reducing average acquisition burden by 55%.

阅读 arXiv 原文

人机协同与对齐(0 篇)

本轮该赛道没有候选论文。