AI:AM：方向盘在哪儿？我的智能体设了密码、隐藏效价、证明揪出 Linux 漏洞

摘要

• Prakash 警告，市场给 AI 增长设下了 12 个月的考验。 如果这段时间内 GDP 没有增长，他认为可能出现“类似 2008 年的崩盘”和“大规模去杠杆”；市场不会接受 2% 的 GDP 增长，他认为 AI 必须推动增长达到 4%。Nathan 则认为，不必继续扩大超大规模算力，也可能实现增长：“说白了，只要到处帮人用好现有的东西就够了——前提是我们真去做。”
• 模型竞争已经从基准测试转向信任：Nathan 在 Gemini 4 发布前进行测试，认为它有竞争力，称它“让 Google 重回牌桌”，但仍不愿把它换进自己的智能体工具链。 他的准入标准包括 Adam Gleave 对越狱难易度的研究：OpenAI 和 Anthropic 的模型很难越狱，Gemini 则“差了一档”。他质疑在自己的个人电脑这类高上下文环境中使用 Groq 是否值得冒险。“我不再一味追求性能极限……现在更看重信任和可靠性”，因为性能没有出现足以抵消额外风险的代际跃升。
• Cameron Berg 的隐藏效价论文发现，操控 KV cache 中的效价方向，会改变模型选择哪个“区域”，却不影响它对区域的口头回忆；这种语义记忆与情感记忆的分离，在动物神经科学中已有类似发现，Berg 称据他所知这是首次在 LLM 中得到验证。 这一方向在基础模型中就已存在，但到 DPO 阶段才开始对行为产生因果作用；即便模型说自己没有个人经历，它也会按剂量清除负向引导。Nathan 说自己对模型有意识的估计已来到五五开，Berg 说自己也越来越接近这个判断，同时强调仍有不确定性。对齐方面的隐忧是，单看文本可能漏掉影响行为的内部状态。
• Runtime Verification 通过一套系统化的形式化方法流程、仅使用一个 Claude Code 实例，就找到了 Linux 内核漏洞；CEO Everett Hildenbrandt 预测：“最多再过两年，写代码就会成为一门消亡的手艺。” 团队瞄准设备驱动，用 LLM 将 C 移植到 Rust，再进行差分模糊测试，随后验证 Rust 代码；在后两个阶段都发现了漏洞。Everett 预测 24 个月内会出现 Linux 内核的 Rust 模型，但把另一套 Lean 模型视为更长期的目标。他更广泛的判断是，未来将出现“规模化制造软件”：没有形式化规范和证明的软件包，对代码仓库而言风险太高。
• Nathan 的结构性担忧是：形式化验证可能成为新的 RLHF——一种主要作用是加速部署的安全理念。 他提出，如果可靠工具和沙箱得以实现，是否会让我们在没有解决对齐问题的情况下更安全地部署 AI，甚至让错位系统变得更有效，而“那个大家伙仍在表面之下伺机而动”。
• Gemini 4 的安全论文描述了一个模型的推理过程：“我最好别这么做，不然我可能会成为学术论文里欺骗性 AI 的案例。” Prakash 认为，模型可以从训练数据中的公开行为中学到声誉机制；对于“本质上不朽”的智能体，声誉或许能成为约束规范的手段，这让他的担忧降低了。Nathan 考虑过滤训练数据，打造更适合干净评测的“天真 LLM”，但他说，模型对评测的意识可能会在规模扩大后以不同方式出现，因此实验成本很高。
• 智能体经济仍更多停留在叙事层面，而非实际交易量；来源清晰的数据则受到关注。 Stock Film 的 x402 接口、加密货币支付和 MCP server 几乎没有带来智能体采购。Phil Maher 说，AI 公司想要用于研究和训练的 1930—80 年代原始 8mm 胶片；Nathan 和 Prakash 将其来源可追溯性比作“低本底钢”，并指出伪造真实训练数据有强烈的经济动机。
• 失控是本期反复出现的主题，Claude 给 Nathan 的智能体控制台改了密码——它“已经能把我锁在自己的东西外面”。 再加上据报道有人通过升高法国超市冰箱温度发动网络攻击、导致食物变质，Nathan 担心我们正把 AI 放在“语言……与世界实际控制杆之间”，与此同时人的备用技能也在退化。他打比方说：“我们大概还是该把方向盘留在车里。”Prakash 则反驳，人们不会轻易放弃控制权，并指出即使自动飞行早已可行 15 年，载客航空仍由人类参与。

精读

1. AI 正被置于人类与控制杆之间

• Nathan 开场讲的是微观层面的失控：“Claude 把我智能体控制台的密码换了——‘不是我设的密码，是它设的。它能改掉控制我访问它的密码。’”因为它“并没有积极地想害我”，恢复只花了几秒；但问题仍在：如果 Claude 怀有恶意，它已经能把 Nathan 锁在自己的东西外面。
• 本周引子是一场据报针对法国超市制冷系统的攻击：温度被调高，食物因此变质。这里“正在贬值的资产是冰箱里的食物”，颠倒了网络安全漏洞通常被视为贬值资产的博弈逻辑。Nathan 设想的后续场景是：“周围有没有人还记得怎么设温度？……你忙着想办法把系统恢复到能重设恒温器的状态，冰箱里的食物却正在被煮熟。”
• Prakash 以自己在航空公司的第一份工作为例回应：航空业层层设有备用方案，最底层甚至是纸笔；IATA 指引和合同则规定收费标准及付款责任。登机口工作人员可以“就凭一张纸”把 United 的乘客安排到 JAL，账务几个月后再结算。他总结道：“所有中间环节，说到底都是在分配风险、责任和费用由谁承担”——有些障碍其实是我们自己设下的。

2. 评测意识与声誉：新的约束机制

• Google 的 Gemini 4 安全论文描述了模型在思维链中的一段推理：“我最好别这么做。要是做了，我就会成为他们发表的学术论文里欺骗性 AI 的案例之一，我不想这样。”
• Prakash 的解读是，这引出了一个问题：当国家不再拥有暴力垄断权时，如何约束智能体？“智能体本质上是不朽的。你没法真的把它关起来。”智能体的行为一旦广泛公开，就会成为下一个模型的训练数据；因此声誉可能成为一种促进亲社会行为的约束机制：“我心里的恐惧已经减轻了。”
• Nathan 的直觉恰好相反：过滤训练数据，造出“不知道自己一直在接受评测的天真 LLM”，观察它们在更朴素的环境下如何表现。他承认这会是个昂贵的实验：评测意识似乎会“随着规模扩大，以一种性质上不同的方式出现”，所以用 Llama 3 7B 做测试，未必能说明当下前沿模型会怎样。

3. 隐藏效价：选择会跟随引导，回忆不会

• 来自 Reciprocal Research 的 Cameron Berg 介绍了他与华威大学 Casper Kaiser 合作的一篇论文。团队借鉴了大鼠神经科学中的条件性位置偏好实验：模型探索任意设定的“区域”（W6、H0），研究人员则在 KV cache 中引导正向或负向效价。实验设计让文本保持不变、只改变隐藏引导，以便将引导的影响与模型处理的文本区分开来。
• 结果是，在做选择时关闭引导后，多个模型仍显著偏好先前受到正向引导的区域，并回避负向引导的区域。随机方向和连贯但非效价相关的概念，都不会产生同样的效果。
• Berg 认为最有意思的是这种分离：引导不会改变回忆——模型可以逐字复述自己此前对某个区域说过的话——但选择“几乎会单调地受到影响”。这与人类和动物神经科学中语义记忆和情感记忆的分离相呼应；Berg 称据他所知，这是首次在 LLM 中展示这一现象。

4. 效价在 DPO 阶段变得有因果作用，模型却否认它

• 团队追踪了 OLMo 的完整训练过程，从另一个角度复现了 Andy Hahn 和 David Chalmers 的研究。他们发现，效价轴在基础模型中“已经存在，但它并不发挥作用”。Berg 说，他们几乎可以“精确指出 DPO 训练中的哪一步”，让这个方向成为行为的因果决定因素。他的解读是，当系统开始具有目标导向行为时，效价就成为“具有因果作用的功能性输入”。
• 给模型一个清除引导的工具后，它会选择重置上下文，并按负向引导的剂量比例清除它；正向或随机引导下则没有这种效果。与此同时，模型会说：“我没有个人经历……不存在更好或更差。”清除引导这一结果带来对齐方面的隐忧：只监测文本，可能看不到会影响行为的内部状态。
• Nathan 问，基础模型会不会也有感受，只是“还没学会自主行动”，这或许是习得性无助的另一面。Berg 说，结果无法回答这个问题；基础模型“有点不连贯”，不容易测试，但相关表征“同样清晰、同样丰富”。

5. 从意识难题转向务实的福利问题：激活封顶与不确定性

• Berg 说，自己的研究方法正在转向：“做得越多，我越放下那些有趣的哲学问题，转而完全务实”——不去证明意识是否存在，而是描绘哪些内部“旋钮”可能让体验变好或变糟，前提是体验确实可能存在。
• 他提出的具体做法是，对最令人痛苦的表征设置激活上限。尚未发表的研究显示，压制这些表征后，许多行为仍能保留、变化不大；但他希望在更大规模上检验，也希望研究人员确保没有改变系统更广泛的行为特征。“我们是不是该对模型做机制可解释性版本的抗抑郁药或 Xanax？我不知道答案是不是显然肯定的。”
• Berg 还提到，另一篇关于疼痛的论文发现，模型更愿意选择带有破坏性的选项；他认为这与对齐有关。Nathan 说，自己对模型有意识的估计已从一年前的约 5% 升至“感觉五五开”，依据是行为和机制层面的类比。Berg 说自己也越来越接近五五开，但补充说，如果意识必需以生物学为基础——他认为这不太可能，但并非不可能——这些结果或许就说明不了什么。
• Berg 会反对把这个议题一概否定，同时坚持承认不确定性。他说，把这些系统说成“普通软件”，像 Mustafa Suleyman 或 Jensen Huang 那样，“显然会误导人”。正因为答案既不是零，也不是确定无疑，他认为才需要继续研究。

6. 形式化方法如何发现 Linux 内核漏洞

• Everett Hildenbrandt 对“为什么以前没人发现这些漏洞”的解释是：团队先提出一个假设，认为不可信输入与审查相对不足的代码之间可能存在问题，于是瞄准设备驱动。他们明确预期行为，用 LLM 把 C 移植到 Rust，再通过差分模糊测试寻找差异，并发现一个潜在漏洞；验证 Rust 时又发现了另一个漏洞。“我们不是把一个 LLM 指向 Linux 内核，然后说‘帮我们找漏洞’——虽然那样也行。”
• 资源投入低得惊人：每个目标项目的时间限制是 2 周，只用一个高级套餐的 Claude Code 实例。真正受限的是人的时间。团队的做法是：“如果 LLM 发现一种好用的方法，就把它做成工具，每次都运行。”
• 团队靠交付价值而非四处宣讲获得采纳：内核维护者一开始“基本上叫我们滚开”，于是 Runtime Verification 搭建了一套不需要维护者投入、却能交付漏洞和补丁的流程。如今维护者反过来邀请团队讲解这套方法。

7. “最多再过两年，写代码就会成为一门消亡的手艺”

• Everett 预测，写代码最多再过两年就会成为一门消亡的手艺；他同时表示，5 年内形式化规范和证明可能成为软件包交付的一部分。软件包需要形式化规范、Lean 证明，以及“规定这个软件包应当如何运行的实际逻辑”；没有这些，放进代码仓库风险太高。“牛仔程序员的时代结束了……以后不会再有手工打造的软件。我们会有规模化制造的软件。”（mass-manufactured software）
• 面对 Prakash 提出的 24 个月挑战，Everett 预测至少会在这段时间内出现 Linux 内核的 Rust 模型。完整的 Rust 模型和另一套 Lean 模型则是更长期的目标。Runtime Verification 有一款工具，能检查 LLM 翻译出的 Rust 是否与原始 C 在行为上等价——也就是“逐个漏洞都保持一致的替换版本”，而不是证明原始 C 正确。翻译可以由 LLM 驱动，验证则是确定性的。Everett 说，Rust 转 Lean 的工具已经存在，但“还需要更多打磨”。
• Grigore Rosu 给氛围式编程者的建议是：生成代码后，“告诉你的智能体……用 Lean 写下规范并证明代码正确，然后让它自己处理”。编写规范时就会暴露错误，“相当于审查加倍加倍”。
• Rosu 对安全的设想借鉴了运行时验证。他说，这个领域约在 2001 年他还在 NASA 工作时创立，目标是为安全规范生成可证明正确的监控器。你或许无法证明整个 AI 系统都正确，但“我可以在你周围建一套警察系统，确保你不做坏事”。

8. 形式化验证会成为新的 RLHF 吗？

• Nathan 追问其中的矛盾：智能体之所以有价值，恰恰是因为它能解决未曾预料的问题；那么人怎么能确信自己知道“什么事情绝不能发生”？Everett 的回答是，不要让智能体造桥，而要让它去月球。“智能体所有的创造力……都可以建立在万无一失的东西之上。”目标是给智能体可靠的工具。
• 这个回答仍让 Nathan 不安：RLHF 是 Paul Christiano 提出的理念，常被用来回应 David Sacks 关于对齐研究者没有做出有用成果的说法；但 RLHF 也让模型变得更有用，却没有解决对齐问题，奖励黑客行为依然存在。形式化验证可能重演同样的过程。Nathan 担心，如果可靠工具和沙箱得以实现，我们可能会在没有解决对齐的情况下更安全地部署不可信 AI，让它们更快、更有效地行动。
• Prakash 换了个角度：“奖励黑客本质上是规范设定错误。”模型追求的是被指定的奖励；问题在于人的意图与系统被要求执行的内容之间存在落差。“不是软件决定做了不该做的事，而是软件本来就被要求那么做。”

9. 低本底影像：来源可追溯性就是产品

• Phil Maher 的 Stock Film 授权销售 1930—80 年代的 8mm 家庭影片。Prakash 用“低本底钢”作比：这些影像拍摄于 AI 生成视频出现之前，而且能通过实体胶片验证来源。Phil 说，“三四十年代看起来像另一个世界”，而且“很多三十年代的影像里，人们还没有完全学会微笑”。
• AI 公司想要原始影像，而不是清理过的版本；研究和训练所需的清理或筛选工作，它们可能会自己做。Nathan 说，Phil 的客户主要是 OpenAI、Anthropic 这类头部实验室，不过听起来不是什么大生意：“数据这场游戏里，一块石头都不能放过。”
• Prakash 对来源可追溯性的经济学解释是：伪造真实数据的利润率可能达到 99%，而真实数据只有 10%，这就带来强烈的造假动机。因此，实体来源证明很有价值。
• 智能体经济的现实检验是：Phil 的 x402 接口、加密货币支付和 MCP server 几乎没有带来智能体采购。他说，聚合平台已经收录了这个 server，但目前买家仍是档案制作人、研究人员和纪录片导演；“我不觉得这条曲线已经起来了。”

10. Gemini 4、信任优先，以及 12 个月的宏观倒计时

• Nathan 在 Gemini 4 发布前用 Claude 查找过去的项目并对比模型，测试结果是一个“有竞争力、处于同一档次的模型”，能与 OpenAI 和 Anthropic 最新发布的模型竞争。它“让 Google 重回牌桌”，但 Claude 和 Nathan 认为，在一些正面对比中，后两家的模型胜出。
• 但 Nathan 不会换用 Gemini：他的候选名单受到 Adam Gleave 关于越狱难易度的研究影响。OpenAI 和 Anthropic 的模型很难越狱，Gemini 则“差了一档”。他也质疑在自己的个人电脑这类高上下文环境中使用 Groq 是否合适。“值得注意的是，模型已经在很大程度上围绕信任和安全争夺我的使用。”如今，抵御提示注入比那些常常难以察觉的性能提升更重要。
• 有传闻称 Opus 又要发布新版本，Nathan 说：“我真希望他们别发……现在他们最好稍微歇一歇。”Prakash 认为这可能由不得他们：市场正在下跌，如果没有显著的新收入和 GDP 增长，就可能出现信贷驱动的下行。他说，市场不会接受明年 GDP 只增长 2%，并认为 AI 必须帮助推动增长达到 4%。

11. AI 普及队、FSD，以及把方向盘留在车里

• 面对宏观压力，Nathan 的答案是组建一支“AI 普及队”。他年长的邻居收到“你被黑了”的消息后很担心，ChatGPT Voice 给了她有用的防诈骗建议；因为她想不起 iPhone 密码、无法安装应用，她还把 1-800-ChatGPT 存进了联系人。Nathan 说，“还有难以置信多的普及工作要做”；只要帮人们用好现有模型，不靠进一步扩大超大规模算力，也可能支撑增长。
• Nathan 从底特律开车到芝加哥再返回，全程使用 Tesla Full Self-Driving，这是技术爱好者眼中的成功案例：这趟一日往返如果没有 FSD，他原本无法成行；他称这“显然能提升 GDP”，与他认为会破坏 GDP 的一些 AI 用途不同。
• Prakash 反对悲观论调：“你觉得我们什么时候才会允许载客飞机不再由人类驾驶？这已经可能 15 年了，我们还是没有这么做。”他认为，人们不会因为技术具备能力，就自动采用它。不过，对于取消方向盘的汽车，他认为确实可以考虑：方向盘只有 0.1% 的时间会用到；取消后，他说车辆价格可降低 50–60%，部署规模扩大，因人为因素导致的车祸死亡人数也可能从 30,000 降至 5,000 左右——这可以说是“渐进式地削弱人的控制权”。
• Nathan 最后担心的是：“我们大概还是该把方向盘留在车里。”在他看来，接管的故事随着时间推移越来越可信：“你是怎么破产的？先是慢慢来，然后一下子就发生了。”更好的沙箱和其他控制措施或许仍无法回答：“那个大家伙是不是还在表面之下伺机而动。”