Amazon（亚马逊）

Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization

Verus-SpecGym: 用于评估规范自动形式化的智能体环境

Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal, Seungone Kim, Jannis Limperg, Cedric Flamant, Kanna Shimizu, Bryan Parno, Sean Welleck

机构 * CMU（卡内基梅隆大学） ； Amazon（亚马逊） 纠错

AI总结 提出 Verus-SpecGym 环境与 Verus-SpecBench 基准，通过执行规范机制和对抗性测试评估 LLM 智能体将非正式编程问题转化为形式规范的能力，发现前沿模型可解决 77.8% 的任务但存在遗漏假设等脆弱性。

Comments Preprint

AgentSociety: Incentivizing Agentic Social Intelligence

AgentSociety: 激励代理社交智能

Aditya Vema Reddy Kesari, Krishna Reddy Kesari

机构 * IIT Bombay（印度理工学院班加罗尔） ； Amazon（亚马逊） 纠错

AI总结 提出一种基于流动民主和信息扩散的激励机制AgentSociety，使去中心化代理能够自主协作、策略性沟通并最大化效用，同时通过共识路由实现集体成果。

Position: The Hidden Costs and Measurement Gaps of Reinforcement Learning with Verifiable Rewards

立场：具有可验证奖励的强化学习的隐藏成本与测量缺口

Fang Wu, Aaron Tu, Weihao Xuan, Heli Qi, Xu Huang, Qingcheng Zeng, Shayan Talaei, Yijia Xiao, Peng Xia, Xiangru Tang, Yuchen Zhuang, Yinxi Li, Bing Hu, Hanqun Cao, Wenqi Shi, Rui Yang, Nan Liu, Huaxiu Yao, Ge Liu, Li Erran Li, Amin Saberi, Naoto Yokoya, Jure Leskovec, Yejin Choi

机构 * Stanford University（斯坦福大学） ； UC Berkeley（加州大学伯克利分校） ； The University of Tokyo（东京大学） ； RIKEN AIP（理化学研究所AIP） ； Waseda University（早稻田大学） ； Georgia Tech（佐治亚理工学院） ； Northwestern University（西北大学） ； UCLA（加州大学洛杉矶分校） ； UNC Chapel Hill（北卡罗来纳大学教堂山分校） ； Yale University（耶鲁大学） ； University of Waterloo（滑铁卢大学） ； Independent Researcher（独立研究者） ； CUHK（香港中文大学） ； UT Southwestern Medical Center（西南医学中心） ； National University of Singapore（新加坡国立大学） ； UIUC（伊利诺伊大学厄巴纳-香槟分校） ； Amazon AWS AI（亚马逊AWS人工智能） 纠错

AI总结 本文指出，具有可验证奖励的强化学习（RLVR）在提升大语言模型性能时，常因预算不匹配、尝试膨胀和基准数据污染等混淆因素导致收益被高估，并提出了预算匹配饱和曲线、校准跟踪、法官鲁棒性测试和污染筛查等最低标准。

Beyond Semantics: The Unreasonable Effectiveness of Reasonless Intermediate Tokens

超越语义：无理由中间标记的不合理有效性

Karthik Valmeekam, Vardhan Palod, Kaya Stechly, Atharva Gundawar, Subbarao Kambhampati

机构 * School of Computing and AI（计算与人工智能学院） ； Arizona State University（亚利桑那州立大学） ； Amazon AGI（亚马逊人工通用智能） ； Yale University（耶鲁大学） 纠错

AI总结 通过从零训练Transformer模型于形式可验证推理轨迹，发现模型在正确与损坏轨迹上表现相似，且损坏轨迹在分布外任务上泛化更好，挑战了中间标记反映或诱导可预测推理行为的假设。

Comments Published in Transactions on Machine Learning Research (TMLR)