新论文称 Lean 验证不能为 OpenAI 的 Navier-Stokes 自然语言证明背书

剑桥大学与伦敦国王学院的研究者发表论文，论证 AI 自动形式化无法保证语义忠实，因此 Lean 对 OpenAI 所宣称 Navier-Stokes 方程解爆破证明的形式化验证，不能证明其自然语言证明正确。作者指出，消解数学自然语言歧义所需的难度在可解性复杂度层级（SCI）中为无穷大，比停机问题（SCI=1）更难，并给出多个 AI 把自然语言陈述与证明翻译成 Lean 时发生错译的实例。在 OpenAI 的 Navier-Stokes 证明中，Lean 形式化与自然语言论文并不对应：论文 Lemma 8.6 的估计用 m+4 阶导数，而对应 Lean 定理 norm_derivativeWord_inverse_le 用了 m+5 阶导数，结论更弱；压力通量估计（10.19）的界与证明思路也与 Lean 版本不同。

推荐理由论文用可解性复杂度层级论证语义忠实的自动形式化比停机问题更难，并给出 OpenAI Navier-Stokes 证明中 Lean 与自然语言不一致的具体例子。

立场论文：AI 智能体设计正削弱人类监督能力

一篇立场论文（arXiv:2608.23642）指出，当前 AI 智能体的设计与部署方式不仅妨碍有效的人类监督，长期使用 AI 系统还会削弱监督者所需的认知能力。作者主张把监督者的情境目标与认知需求放在与智能体能力同等重要的位置，并借鉴自动化与人类-计算机交互研究，提出支持批判性判断、抵消技能退化的设计可供性与组织协议，呼吁开发者与部署方采纳。

面向自主科学发现的智能体经济基础设施

论文提出为 AI for Science 构建"科学智能体经济、市场与制度"基础设施，以在推理能力提升之外补齐资源管理这一科学发现的关键瓶颈。该基础设施旨在让 AI 智能体与人类科学家协作确定研究优先级、分配贡献归属、追踪问责与责任，并防范恶意使用与信息安全风险。文章还讨论了（半）自主科学发现的宏观社会影响，以支撑治理政策制定，确保 AI 驱动发现及其衍生技术的公平分配。

研究：生成式 AI 模型中的概率性复制与版权认定

Mark A. Lemley 与 A. Feder Cooper 在论文中讨论，已有研究显示可从部分大语言模型中提取某些受版权作品的逐字或近似逐字文本，说明模型权重以某种形式编码了这些作品。作者指出 LLM 并非以数据库格式存储信息，而是存储从训练数据中学到的 token 间统计关系，生成过程常是概率性的而非确定性的。版权法此前未处理过这种可能产生相似输出、也可能不产生的信息存储是否构成复制。作者认为，现行法下最可能的结果是采取功能性路径，即只有当某作品能被直接提取到输出中时，才认定模型包含该作品的复制，并指出这一结果在政策层面并不令人满意，提出了可能的修法方向。论文即将发表于 Berkeley Technology Law Journal。

多作者论文评估 AI 研发自动化触发智能爆炸的可能与政策应对

一篇 arXiv 论文评估了 AI 研发自动化可能触发智能爆炸的证据，并分析其影响与政策回应。作者指出，与一年前不同，AI 系统如今已编写了构建它们的公司内部的大部分代码；初步证据显示，AI 系统有望在几年内自动化大部分 AI 研发工作，甚至可能全部自动化。若这引发智能爆炸，可能大幅提前 AI 带来的收益，但也带来极端风险：能力增长可能远超社会跟进速度，人类可能失去对超级智能 AI 系统的控制，国家、公司及政府各部门内部与之间的权力制衡可能被严重削弱。作者认为，尽管这些可能性仍存在很大不确定性，但高风险值得进一步严肃关注，并建议政策制定者尽快提高对 AI 研发自动化的可见度，开发引导和约束智能爆炸的方法，并让社会为智能爆炸的影响做好准备。

研究：EdTech 平台将隐私与 AI 披露推迟到产品后期

一项混合方法研究考察了教育科技（EdTech）平台如何处理学生隐私与 AI 披露。研究者对 12 名 EdTech 从业者进行半结构化访谈，并对 48 家平台的隐私政策按五个维度编码审计，评分者间信度较高（平均 Cohen's Kappa = 0.781）。访谈显示，隐私虽被认可为重要，却常在产品生命周期中被推迟，组织优先考虑功能、增长、融资和即时教学效果，并把责任转嫁给云服务商、政策文件或下游机构。政策审计发现，平台对收集哪些数据描述较充分，但对数据后续治理说明明显不足：33% 的平台在存在可见 AI 功能的情况下未做有意义的 AI 披露，73% 只提供笼统的问责与泄露响应措辞。K-12 平台在监管有明确要求时对儿童同意的处理更好，但这一优势未延伸到 AI 治理或问责。

研究者质疑 Alignment Whack-a-Mole 的书籍记忆化结论，称其测量方法无效

研究者 A. Feder Cooper 发布 arXiv 评论文章，认为 Alignment Whack-a-Mole 中关于微调导致书籍记忆化的核心结果使用了无效的测量流程。她指出，这些结果依赖的书籍记忆化覆盖率指标所统计的序列匹配长度远短于领域公认的记忆化证据标准，用于诱发记忆化的提示词流程还可能把待提取文本泄露进提示词中。论文缺少负对照实验，无法判断结果中有多少来自假阳性，即在生成内容与训练数据的匹配可能源于其他因素时仍宣称提取成功。她据此认为，论文关于微调可让用户提取受版权保护书籍中足以替代原作的相当部分内容的说法缺乏结果支持，且未报告实验成本这一威胁模型的重要组成。她提到，过去一个月有潜在原告联系她，希望将该论文作为正在和可能发生的版权诉讼中的有效证据。

面向智能体的高效 HPC 系统：挑战与机遇

编码智能体已成为 HPC 系统的真实用户，但现有 HPC 抽象、接口与策略仍为人类工作流设计。测量显示，编码智能体用户仅占观测人群的 19.5%，却贡献了 55.8% 的作业提交、29.1% 的 CPU 核心时和 42.7% 的 GPU 时；其命令下发速率是人类的 20.8 倍，并以细粒度 explore-modify-execute 循环和跨昼夜的试错方式追求开放式目标。这给调度器控制面、元数据密集型 I/O、跨会话记忆复用以及提示注入与策略执行带来压力，作者主张将智能体视为一等主体、以协同设计应对。