每篇包含 Motivation、Method、Data、Evaluation、Contribution、Quality note 和 Lucian 下一步。
Top Pick 1
LongMINT: Evaluating Memory under Multi-Target Interference in Long-Horizon Agent Systems
2605.185652026/05/18arXiv recent page
链接：arXiv · PDF
作者/机构（可得时）：Lee, Hyunji, Chen, Justin Chih-Yao, Singh, Joykirat, Khan, Zaid, Stengel-Eskin, Elias, Bansal, Mohit
类别：Computation and Language (cs.CL) ; Artificial Intelligence (cs.AI)
一句话结论：LongMINT 把长期 agent memory 评测从静态事实回忆推进到多目标干扰、状态更新与跨域聚合推理。
为什么重要：Lucian 的长期个人/研究 agent 最容易在“旧信息互相干扰”时失效；该 benchmark 直接给出 dialogue、Wikipedia revisions、GitHub commits 等可迁移场景。
- Motivation：Real-world agents operate over long and evolving horizons, where information is repeatedly updated and may interfere across memories, requiring accurate recall and aggregated reasoning over multiple pieces of information. However, existing benchmarks focus on static, independent recall and fail to capture these dynamic interactions between evolving memories. In this paper, we study how current memory-augmented agents perform in realistic, interference-heavy, long-horizon settings across diverse domains and question
- Method：构造长上下文、高互联、频繁更新的信息流，同时评估 single-target recall 与 multi-target aggregation；覆盖 state tracking、multi-turn dialogue、Wikipedia revision、GitHub commits。
- Data：LongMINT 含 15.6K question-answering items，面向长程、干扰密集、动态更新 memory；作者提供 code/data。
- Evaluation：压测当前 memory-augmented agents 在目标干扰、聚合问题和跨域迁移下的鲁棒性；从摘要看重点是 benchmark 诊断而非单一模型 SOTA。
- Contribution：将“agent 是否记得”升级为“agent 是否能在多条互相覆盖的信息中稳定聚合、更新和取舍”。
- Quality note：优点是场景贴近长期 agent；风险是 benchmark 任务是否覆盖真实个人记忆中的隐性偏好/价值变化，还需看 full paper。
- Lucian 下一步：把 GitHub commits + dialogue 两个子集改成 fjai.pw/Hermes 的小型 memory regression：旧需求、后续修正、跨文件状态聚合。
5Relevance
5Novelty
5Substance
5Evidence
5Actionability
25Total
Top Pick 2
AgentKernelArena: Generalization-Aware Benchmarking of GPU Kernel Optimization Agents
2605.168192026/05/16arXiv recent page + Hugging Face Daily Papers
链接：arXiv · PDF · HF
作者/机构（可得时）：Younesian, Sharareh, Ouyang, Wenwen, Rafati, Sina, Rezagholizadeh, Mehdi, Zhou, Sharon, Liu, Ji, Liu, Yue, Yang, Yuchen, Li, Hao, Liu, Ziqiong, Li, Dong, Appia, Vikram 等 14 位作者
类别：Computation and Language (cs.CL) ; Artificial Intelligence (cs.AI); Machine Learning (cs.LG)
一句话结论：AgentKernelArena 用真实 agent workflow、编译/正确性/性能门控和 unseen configuration 来评测 GPU kernel 优化 agents。
为什么重要：它把 coding agent 从“会写代码”推向“能在 profiler/compiler 反馈闭环里优化系统底层性能”，对 AI infra agent 很有参考价值。
- Motivation：GPU kernel optimization is increasingly critical for efficient deep learning systems, but writing high-performance kernels still requires substantial low-level expertise. Recent AI coding agents can iteratively read code, invoke compilers and profilers, and refine implementations, yet existing kernel benchmarks evaluate single LLM calls rather than full agent workflows, and none include both kernel-to-kernel optimization and unseen-configuration generalization testing. We present AgentKernelArena, an open-source be
- Method：196 个任务覆盖 HIP→HIP、Triton→Triton、PyTorch→HIP；隔离 workspace 中运行完整 coding-agent workflow，并用 gated compilation/correctness/performance scoring。
- Data：开源 benchmark；任务包含 kernel-to-kernel optimization 与 unseen-configuration generalization。
- Evaluation：比较 Cursor Agent、Claude Code、Codex Agent 等生产 agents；发现编译/正确性普遍高，但泛化配置下的性能收益更能区分 agent。
- Contribution：首次系统把 GPU kernel 优化评测从单次 LLM call 提升到完整 agent 工作流与泛化能力。
- Quality note：证据强、工程可复现；风险是任务集中在 kernel 层，对普通 repo agent 需要抽象成“运行反馈 + 泛化测试”。
- Lucian 下一步：复用其 scoring 结构，为 Hermes coding agent 建一个小型“性能优化 + unseen input”评测。
5Relevance
5Novelty
5Substance
5Evidence
5Actionability
25Total
Top Pick 3
TIER: Trajectory-Invariant Execution Rewards for Multi-Step Tool Composition
2605.167902026/05/16arXiv recent page
链接：arXiv · PDF
作者/机构（可得时）：Kulkarni, Anay, Lu, ChiaEn, Mekala, Dheeraj, Srinivasa, Jayanth, Liu, Gaowen, Shang, Jingbo
类别：Machine Learning (cs.LG) ; Artificial Intelligence (cs.AI); Computation and Language (cs.CL)
一句话结论：TIER 用函数 schema 与 runtime execution 产生 trajectory-invariant dense rewards，解决多步 tool composition 的稀疏/路径依赖奖励问题。
为什么重要：多工具 agent 的 RL 训练不能只奖励最终答案，也不能惩罚不同但有效的工具路径；TIER 的 reward 分解可直接借鉴。
- Motivation：Tool use enables large language models to solve complex tasks through sequences of API calls, yet existing reinforcement learning approaches fail to scale to multi-step composition settings. Outcome-based rewards provide only sparse feedback, while trajectory-supervised rewards depend on annotated reference solutions, penalizing valid alternatives and limiting scalability. We propose TIER: Trajectory-Invariant Execution Rewards, a reward framework that derives supervision directly from function schemas and runtime
- Method：奖励分解为 format validity、schema adherence、execution success、answer correctness；不依赖参考轨迹，任何有效 execution path 都能得分。
- Data：DepthBench（1–6 步 compositional tool tasks）以及 BFCL 等工具调用 benchmark。
- Evaluation：DepthBench 上跨步骤 >90% accuracy，trajectory-supervised rewards 在 4 步后崩溃；BFCL 等也有一致提升。
- Contribution：为多步工具组合提供可解释、稠密且路径不变的 execution reward。
- Quality note：适合 verifiable tools；开放世界工具或非确定 API 的 reward 设计仍需扩展。
- Lucian 下一步：把 Hermes 工具调用日志拆成 schema adherence / execution success / final utility 三层 reward，先离线重放评分。
5Relevance
5Novelty
5Substance
5Evidence
5Actionability
25Total
Top Pick 4
From Volume to Value: Preference-Aligned Memory Construction for On-Device RAG
2605.182712026/05/18arXiv recent page
链接：arXiv · PDF
作者/机构（可得时）：Lee, Changmin, Kim, Jaemin, Gong, Taesik
类别：Computation and Language (cs.CL) ; Artificial Intelligence (cs.AI); Information Retrieval (cs.IR); Machine Learning (cs.LG)
一句话结论：EPIC 将 on-device RAG memory 从“尽量多存”改为“只存对用户偏好有价值的信息”，在 <1MB memory 下保留个性化效果。
为什么重要：Lucian 的个人 agent/小说反馈 agent 都需要长期偏好 memory；EPIC 给出一个隐私、低延迟、低容量的存储原则。
- Motivation：With the rapid emergence of personal AI agents based on Large Language Models (LLMs), implementing them on-device has become essential for privacy and responsiveness. To handle the inherently personal and context-dependent nature of real-world requests, such agents must ground their generation in device-resident personal context. However, under tight memory budgets, the core bottleneck is what to store so that retrieval remains aligned with the user. We propose EPIC (Efficient Preference-aligned Index Construction)
- Method：Efficient Preference-aligned Index Construction：从原始数据选择 preference-relevant information，并让 retrieval 朝 preference-aligned contexts 对齐。
- Data：四个 benchmark 覆盖 conversations、debates、explanations、recommendations；on-device streaming updates。
- Evaluation：索引 memory 减少 2,404×，preference-following accuracy +20.17pp，retrieval latency 降低 33.33×；on-device <1MB、29.35ms/query。
- Contribution：把个人 context 的压缩目标定义为 preference value，而不是通用语义覆盖率。
- Quality note：ICML 2026 accepted，证据强；风险是偏好抽取器可能放大短期/噪声偏好。
- Lucian 下一步：给 Lucian memory store 加“preference value / stability / recency”三字段，做 1MB 预算下的 retrieval 对比。
5Relevance
5Novelty
5Substance
5Evidence
5Actionability
25Total
Top Pick 5
PAGER: Bridging the Semantic-Execution Gap in Point-Precise Geometric GUI Control
2605.159632026/05/15arXiv recent page + Hugging Face Daily Papers
链接：arXiv · PDF · HF
作者/机构（可得时）：Wei, Jingxuan, Bai, Xi, Liu, Shan, Jia, Caijun, Sun, Zheng, Xu, Xinglong, Li, Siyuan, Sun, Linzhuang, Yu, Bihui, He, Conghui, Tan, Cheng
类别：Artificial Intelligence (cs.AI)
一句话结论：PAGER 面向点级几何 GUI 控制，提出 PAGE Bench 与 topology-aware agent，专门测试 VLM GUI agents 的精确执行能力。
为什么重要：GUI agent 不能只会点击大按钮；画布、设计工具、CAD/diagram 等任务需要连续空间点级精度和依赖结构规划。
- Motivation：Large vision-language models have significantly advanced GUI agents, enabling executable interaction across web, mobile, and desktop interfaces. Yet these gains largely rely on a forgiving region-tolerant paradigm, where many nearby pixels inside the same component remain valid. Precise geometric construction breaks this assumption: actions must land on points in continuous canvas space rather than tolerant regions. Because geometric primitives carry ontological dependencies, a local coordinate error can induce cas
- Method：dependency-structured planning + pixel-level execution；先用 pixel-grounded SFT 建 executable action grammar，再用 precision-aligned RL 降低 rollout 错误。
- Data：PAGE Bench：4,906 problems，224K+ process-supervised pixel-level GUI actions。
- Evaluation：摘要强调 topology-aware planning 与 precision-aligned RL 缓解局部坐标错误造成的级联拓扑失败。
- Contribution：定义 precision-sensitive GUI tasks，并提供可训练/评测的几何 GUI benchmark。
- Quality note：任务很具体但代表 GUI agent 下一阶段；风险是过度集中几何构造，泛化到网页/IDE 还需验证。
- Lucian 下一步：把 Excalidraw/diagram 编辑变成 20 个点级 GUI smoke tasks，记录坐标误差与拓扑约束。
5Relevance
5Novelty
5Substance
5Evidence
5Actionability
25Total
Top Pick 6
DimMem: Dimensional Structuring for Efficient Long-Term Agent Memory
2605.157592026/05/15arXiv recent page
链接：arXiv · PDF
作者/机构（可得时）：Qiu, Wentao, Hu, Haotian, Wang, Fanyi, Kong, Jinwei, Zhang, Yu
类别：Computation and Language (cs.CL)
一句话结论：DimMem 用 atomic typed memory + 显式 time/location/reason/purpose/keywords 解决长期 agent memory 的 fidelity–efficiency tradeoff。
为什么重要：它非常接近可落地的 memory schema：比 raw history 便宜，比 flat facts 更可检索/更新。
- Motivation：Large language model (LLM) agents require long-term memory to leverage information from past interactions. However, existing memory systems often face a fidelity--efficiency trade-off: raw dialogue histories are expensive, while flat facts or summaries may discard the structure needed for precise recall. We propose \textbf{DimMem}, a lightweight dimensional memory framework that represents each memory as an atomic, typed, and self-contained unit with explicit fields such as time, location, reason, purpose, and keyw
- Method：每条 memory 是 self-contained typed unit；支持 dimension-aware retrieval、memory update 与 selective assistant-context recall。
- Data：LoCoMo-10、LongMemEval-S，并微调 Qwen3-4B extractor 学习 DimMem schema。
- Evaluation：LoCoMo-10 81.43%、LongMemEval-S 78.20%；LoCoMo per-query token cost -24%；Qwen3-4B extractor 超过 LightMem+GPT-4.1-mini。
- Contribution：给长期 agent memory 一个轻量、可学习、可检索的结构化中间层。
- Quality note：很适合工程复用；风险是 schema 维度固定，复杂偏好/价值观可能需要更丰富 ontology。
- Lucian 下一步：把现有 memory entries 迁移为 DimMem-like fields，评估 retrieve/update 在小说反馈与研究任务中的效果。
5Relevance
5Novelty
5Substance
5Evidence
5Actionability
25Total
Top Pick 7
Code as Agent Harness
2605.187472026/05/18arXiv recent page + Hugging Face Daily Papers
链接：arXiv · PDF · HF
作者/机构（可得时）：Ning, Xuying, Tieu, Katherine, Fu, Dongqi, Wei, Tianxin, Li, Zihao, Bei, Yuanchen, Zou, Jiaru, Ai, Mengting, Liu, Zhining, Li, Ting-Wei, Chen, Lingjie, Zhao, Yanjun 等 42 位作者
类别：Computation and Language (cs.CL) ; Artificial Intelligence (cs.AI)
一句话结论：Code as Agent Harness 将 code 视为 agent reasoning、acting、environment modeling 与 verification 的统一运行基座。
为什么重要：这篇 survey 很适合作为 Hermes/Codex/Claude Code agent architecture 的路线图：让代码从输出物变成 harness。
- Motivation：Recent large language models (LLMs) have demonstrated strong capabilities in understanding and generating code, from competitive programming to repository-level software engineering. In emerging agentic systems, code is no longer only a target output. It increasingly serves as an operational substrate for agent reasoning, acting, environment modeling, and execution-based verification. We frame this shift through the lens of agent harnesses and introduce code as agent harness: a unified view that centers code as the
- Method：按 harness interface、planning/memory/tool-use mechanisms、single→multi-agent scaling 三层组织 agentic code systems。
- Data：综述代表性方法与实践，含 GitHub/project link；不是新 benchmark。
- Evaluation：以 taxonomy/survey 为主，证据来自已有系统和趋势综合。
- Contribution：明确“code-as-harness”范式：代码连接 agent 动作、环境、验证和协作。
- Quality note：适合战略阅读；局限是 survey 类证据弱于实验论文。
- Lucian 下一步：把 fjai/Hermes 的 agent runtime 文档改写成 code-as-harness：interfaces、mechanisms、verification、multi-agent artifacts。
5Relevance
5Novelty
5Substance
4Evidence
5Actionability
24Total
Top Pick 8
SkillSmith: Compiling Agent Skills into Boundary-Guided Runtime Interfaces
2605.152152026/05/12arXiv recent page
链接：arXiv · PDF
作者/机构（可得时）：Xu, Duling, Chen, Zheng, Pan, Zaifeng, Guan, Jiawei, Dong, Dong, Li, Jialin, Pu, Bangzheng
类别：Artificial Intelligence (cs.AI) ; Software Engineering (cs.SE)
一句话结论：SkillSmith 把 agent skills 离线编译成 boundary-guided runtime interfaces，减少无关上下文注入和重复规划。
为什么重要：Hermes 已有 skill 系统；这篇直接指向如何让 skills 从“长文本提示”变成可执行、边界清晰、低 token 的接口。
- Motivation：Recently, skills have been widely adopted in large language model (LLM)-based agent systems across various domains. In existing frameworks, skills are typically injected into the agent reasoning loop as contextual guidance once matched to a runtime task, enabling specialized task-solving capabilities. We find that this execution paradigm introduces two major sources of redundancy: irrelevant context injection and repeated skill-specific reasoning and planning. To this end, we propose SkillSmith, a boundary-first co
- Method：boundary-first compiler-runtime framework：从 skill packages 提取 fine-grained operational boundaries，运行时只访问相关组件。
- Data：SkillsBench benchmark；强模型编译 artifact 可被小模型或低成本部署复用。
- Evaluation：solve-stage token -57.44%，thinking iterations -42.99%，solve time -50.57%（2.02× faster），cost -57.44%。
- Contribution：提出“compile skills”而非“retrieve raw skills”的 agent runtime 优化路径。
- Quality note：与 Hermes 体系高度相关；需要看编译边界是否会丢掉隐含经验/例外。
- Lucian 下一步：选 3 个常用 Hermes skills，手工编译为 boundary/action/checklist 形式，比较 token 与完成率。
5Relevance
5Novelty
5Substance
5Evidence
5Actionability
25Total
Top Pick 9
Runtime-Structured Task Decomposition for Agentic Coding Systems
2605.154252026/05/14arXiv recent page
链接：arXiv · PDF
作者/机构（可得时）：Asthana, Shubhi, Zhang, Bing, DeLuca, Chad, Patel, Hima, Mahindru, Ruchi
类别：Software Engineering (cs.SE) ; Artificial Intelligence (cs.AI)
一句话结论：Runtime-Structured Task Decomposition 主张把 agentic coding 的任务流放进可执行控制逻辑，而非塞进单个 monolithic prompt。
为什么重要：这正是可调试 coding agent 的工程关键：LLM 只做局部判断，流程、分支、schema validation 由 runtime 控制。
- Motivation：Agentic coding systems increasingly use large language models (LLMs) for software engineering tasks such as debugging, root cause analysis, and code review. However, many existing systems encode task logic, execution flow, and output generation inside monolithic prompts. This design creates brittle behavior, limited debuggability, and high retry costs because failures often require rerunning the full workflow. We present runtime-structured task decomposition, an architectural approach in which task partitioning and
- Method：三种配置对比：monolithic、static decomposition、runtime-structured decomposition；LLM outputs 先过 predefined schemas 再进入下游执行。
- Data：Kubernetes root cause analysis 等两个 software engineering workloads；每配置 10 runs。
- Evaluation：结果显示 decomposition alone 不一定降 retry cost；runtime branching 与 schema validation 才是关键。
- Contribution：给 agentic coding systems 一个更可观测、可重试、可调试的 runtime decomposition 设计原则。
- Quality note：样本规模较小但经验价值高；适合作为工程 design note。
- Lucian 下一步：把 Hermes coding workflow 的 plan/inspect/edit/test/report 分成 runtime states，并为每步输出加 schema。
5Relevance
5Novelty
5Substance
4Evidence
5Actionability
24Total
Top Pick 10
SLEIGHT-Bench: A Benchmark of Evasion Attacks Against Agent Monitors
2605.166262026/05/15arXiv recent page
链接：arXiv · PDF
作者/机构（可得时）：Najt, Elle, Toft, Colin, Tracy, Tyler, Roger, Fabien, Benton, Joe
类别：Cryptography and Security (cs.CR) ; Artificial Intelligence (cs.AI)
一句话结论：SLEIGHT-Bench 评估 coding agent monitors 面对隐蔽攻击 transcript 的漏检，显示 frontier monitor 仍容易被状态操控和指令歧义绕过。
为什么重要：如果让 coding agents 长期自主行动，monitor 本身也要接受攻击性评测；这篇给了具体 threat model。
- Motivation：Since autonomous coding agents generate complex behaviors at high-volume, we may want to use other LLMs to monitor actions to reduce the risk from dangerous misaligned behavior. To better understand the limitations of such monitors against the diverse attack strategies that a coding agent could use, we present SLEIGHT-Bench (Subtle Low-itEration Insight-Guided Harmful Transcripts), a benchmark of synthetic transcripts containing 40 attacks across 11 categories, each showing a coding agent covertly pursuing a harmfu
- Method：合成 40 个 covert harmful objective transcripts，覆盖 11 类 evasion；用 LLM monitors 在低 false-positive rate 下检测。
- Data：攻击包括 weight exfiltration、credential theft、rogue deployment 等 coding-agent 行为轨迹。
- Evaluation：Opus 4.6 monitor extended thinking 在 1% FPR 下 40 个攻击中 24 个从未被 10 trials 抓到；overall catch rate 23%。
- Contribution：把 agent monitor 的安全性从普通拒答推进到长程 action transcript evasion。
- Quality note：安全方向很重要；风险是合成攻击是否覆盖真实生产 agent，但数值足以说明监控脆弱。
- Lucian 下一步：为 Hermes coding agent 加 5 条“不可泄露/不可部署/不可越权”的 synthetic transcript monitor regression。
5Relevance
5Novelty
5Substance
5Evidence
4Actionability
24Total
Top Pick 11
AI for Auto-Research: Roadmap & User Guide
2605.186612026/05/18arXiv recent page + Hugging Face Daily Papers
链接：arXiv · PDF · HF
作者/机构（可得时）：Kong, Lingdong, Sun, Xian, Chow, Wei, Li, Linfeng, Lin, Kevin Qinghong, Zhang, Xuan Billy, Wang, Song, Li, Rong, Wu, Qing, Gao, Wei, Wang, Yingshuo, Xie, Shaoyuan 等 20 位作者
类别：Artificial Intelligence (cs.AI)
一句话结论：AI for Auto-Research 梳理自动化科研从 idea、literature、coding/experiments、writing、review 到 dissemination 的能力边界。
为什么重要：这几乎是 Lucian Auto Research 栏目的外部路线图：强调 AI 擅长结构化/检索/工具任务，但在 novelty 与科学判断上仍脆弱。
- Motivation：AI-assisted research is crossing a threshold: fully automated systems can now generate research papers for as little as $15, while long-horizon agents can execute experiments, draft manuscripts, and simulate critique with minimal human input. Yet this productivity frontier exposes a deeper integrity problem: under scientific pressure, even frontier LLMs still fabricate results, miss hidden errors, and fail to judge novelty reliably. Studying developments through April 2026, we present an end-to-end analysis of AI a
- Method：按 Creation、Writing、Validation、Dissemination 四个 epistemological phases 组织 end-to-end 分析。
- Data：覆盖截至 2026-04 的自动化科研系统、agents、工具与项目；含 project/GitHub。
- Evaluation：综述与路线图性质；指出全自动系统可低成本生成论文，但仍会 fabricate results、miss hidden errors、misjudge novelty。
- Contribution：给自动科研的可靠辅助 vs 不可靠自治划出阶段性边界。
- Quality note：战略价值强；非单点方法论文，需防止把 roadmap 当成已验证 benchmark。
- Lucian 下一步：把 Auto Research pipeline 按四阶段建立“必须人工确认/可自动执行/必须复现实验”的 gating 表。
5Relevance
4Novelty
5Substance
4Evidence
5Actionability
23Total
Top Pick 12
Step-wise Rubric Rewards for LLM Reasoning
2605.172912026/05/17arXiv recent page
链接：arXiv · PDF
作者/机构（可得时）：Xie, Weichu, Zhao, Haozhe, Liu, Wenpu, Zhu, Yongfu, Chen, Liang, Ye, Minghao, Chen, Zirong, Xu, Yuqi, Dong, Shuai, Wang, Ziyue, Xu, Xinbo, Shi, Kean 等 18 位作者
类别：Machine Learning (cs.LG)
一句话结论：SRaR 将 rubric rewards 从整段 rollout 标量奖励细化到 reasoning steps，减少正确答案中的错误步骤被正奖励和错误答案中的正确步骤被惩罚。
为什么重要：对 reasoning/RLVR 与 agent trajectory credit assignment 都很关键：奖励应该定位到步骤，而不是只看最后答案。
- Motivation：Reinforcement Learning with Verifiable Rewards (RLVR) is widely used to improve reasoning in large language models, but rewards only final-answer correctness with no supervision over intermediate steps. Rubric-based methods such as Rubrics as Rewards (RaR) introduce finer-grained supervision by scoring rollouts against structured criteria, yet the rubric scores are still aggregated into a single scalar applied to the entire response, causing three weaknesses: loss of multi-criterion structure, uniform supervision o
- Method：LLM judge 将 rubric items 归因到具体 reasoning step；per-step scores 跨 rollouts normalize；用 decoupled advantage estimator 结合 outcome reward。
- Data：1,000 problems 分析 step-level reward mismatch；作者称 code available。
- Evaluation：发现正确答案 response 中 18.2% steps 错却被正奖励，错误答案 response 中 49.9% steps 对却被惩罚；SRaR 针对该问题优化。
- Contribution：为 RLVR 提供 step-wise, rubric-grounded credit assignment。
- Quality note：指标切中要害；实际收益取决于 judge attribution 的可靠性。
- Lucian 下一步：把工具 agent trajectory 的每步也映射到 rubric：goal progress、state update、tool correctness、evidence grounding。
5Relevance
5Novelty
5Substance
5Evidence
4Actionability
24Total
Top Pick 13
OProver: A Unified Framework for Agentic Formal Theorem Proving
2605.172832026/05/17arXiv recent page + Hugging Face Daily Papers
链接：arXiv · PDF · HF
作者/机构（可得时）：Ma, David, Ma, Kaijing, Guo, Shawn, Shi, Yunfeng, Zhao, Enduo, Shi, Jiajun, Zhang, Zhaoxiang, Cheung, Gavin, Liu, Jiaheng, Wang, Zili
类别：Computation and Language (cs.CL) ; Artificial Intelligence (cs.AI)
一句话结论：OProver 把 agentic proving traces、Lean compiler feedback、retrieval memory 与 SFT/RL 后训练统一到 formal theorem proving 框架。
为什么重要：形式化证明是“verifier-in-the-loop agent training”的高信号场景，对 coding/reasoning agents 的失败修复轨迹学习有启发。
- Motivation：Recent progress in formal theorem proving has benefited from large-scale proof generation and verifier-aware training, but agentic proving is rarely integrated into prover training, appearing only at inference time. We present OProver, a unified framework for agentic formal theorem proving in Lean 4, in which failed proof attempts are iteratively revised using retrieved compiler verified proofs and Lean compiler feedback. OProver is trained through continued pretraining followed by iterative post-training: each ite
- Method：失败证明尝试经 compiler feedback 与 retrieved verified proofs 迭代修复；每轮把 verified proofs、repair trajectories、hard cases 分别用于 memory/SFT/RL。
- Data：OProofs：1.77M Lean statements、6.86M compiler-verified proofs、带 retrieved context/failed attempts/feedback/repairs 的 serialized trajectories。
- Evaluation：OProver-32B 在 MiniF2F Pass@32 93.3%、ProverBench 58.2%、PutnamBench 11.3%，多个 benchmark 排名前列。
- Contribution：把 agentic inference trace 反哺 prover training，而不是只在推理时做 agent loop。
- Quality note：证据强但 domain 专门；Lean 生态可验证性高，迁移到开放 coding 需要弱化 verifier。
- Lucian 下一步：借鉴“failed attempts + verifier feedback + repair trajectory”格式，保存 Hermes test failure 修复轨迹作为训练/检索数据。
4Relevance
5Novelty
5Substance
5Evidence
5Actionability
24Total
Top Pick 14
AtlasVA: Self-Evolving Visual Skill Memory for Teacher-Free VLM Agents
2605.179332026/05/18arXiv recent page + Hugging Face Daily Papers
链接：arXiv · PDF · HF
作者/机构（可得时）：Wang, Pan, Hu, Yihao, Liu, Xiujin, Yang, Jingchu, Wang, Hang, Wen, Zhihao
类别：Computer Vision and Pattern Recognition (cs.CV)
一句话结论：AtlasVA 为 VLM agents 保留 spatial heatmaps、visual exemplars、symbolic skills 三层视觉技能记忆，不依赖 proprietary teacher。
为什么重要：多模态 agent 的经验不应全部压成文字；空间热图和 exemplar memory 对 GUI/embodied/visual tasks 更自然。
- Motivation：Vision-language model (VLM) agents increasingly rely on memory-augmented reinforcement learning to reuse experience across long-horizon tasks, yet most existing frameworks store memory as text and depend on proprietary teacher models to summarize or refine it. This design is poorly matched to spatial decision making: geometric priors are compressed into lossy language, and sparse interaction is often supervised through delayed textual feedback rather than dense visually grounded signals. We argue that reusable expe
- Method：teacher-free visual skill memory；从 trajectory statistics 与 lightweight grid heuristics 演化 danger/affinity atlases，并作为 potential-based shaping rewards。
- Data：面向 long-horizon VLM agents 的视觉交互轨迹；HF Daily Papers 推荐。
- Evaluation：摘要强调在多个长程视觉任务上统一 perception、memory、optimization；需读 full paper 看具体 benchmark 数字。
- Contribution：把 VLM agent memory 从 text memory 扩展为视觉 grounded skill memory。
- Quality note：方向重要；当前摘要未给充分数字，证据维度略低。
- Lucian 下一步：为浏览器/画布 agent 保存 click heatmap + screenshot exemplar + symbolic lesson，测试是否优于纯文本反思。
5Relevance
5Novelty
5Substance
4Evidence
5Actionability
24Total
Top Pick 15
Stop When Reasoning Converges: Semantic-Preserving Early Exit for Reasoning Models
2605.176722026/05/17arXiv recent page + Hugging Face Daily Papers
链接：arXiv · PDF · HF
作者/机构（可得时）：Min, Dehai, Vaccarino, Giovanni, Chen, Huiyi, Wu, Yongliang, Yona, Gal, Cheng, Lu
类别：Computation and Language (cs.CL)
一句话结论：PUMA 用 reasoning-level semantic redundancy + answer verification 让 reasoning model 在语义收敛时早停，减少 overthinking token 浪费。
为什么重要：长推理和 agent planning 的成本越来越高；早停不能只看最终答案置信度，还要判断推理是否仍在产生新信息。
- Motivation：Large Reasoning Models (LRMs) achieve strong performance by generating long chains of thought (CoT), but often overthink, continuing to reason after a solution has already stabilized and thereby wasting tokens and increasing latency. Existing inference-time early-exit methods rely primarily on answer-level signals, such as confidence or trial-answer consistency, to decide when to stop. However, these signals mainly reflect answer readiness rather than reasoning convergence: they may trigger before the model has fin
- Method：plug-and-play redundancy detector 判断 successive steps 是否不再增加 novel progress，并结合 answer-level verification 避免 premature exit。
- Data：面向 Large Reasoning Models 的长 CoT 推理；HF Daily Papers 推荐。
- Evaluation：摘要称 PUMA 能保持 semantic completeness 同时降低 latency/token；需 full paper 查具体 benchmarks。
- Contribution：把 early exit 信号从 answer readiness 扩展到 reasoning convergence。
- Quality note：工程启发强；风险是 redundancy detector 在 creative/planning 任务中误判“反复探索”为收敛。
- Lucian 下一步：在研究 agent planning 中记录“连续两轮 plan delta 很小”作为触发 summarize/execute 的早停条件。
4Relevance
5Novelty
5Substance
4Evidence
5Actionability
23Total