Agent安全

• Erik 一上来撇清：这不是产品推销或发布会，而是一个 20 分钟教程——怎么用最基础的 type system（类型系统，即编程语言里给数据和函数"贴标签、定契约"的机制）和编译器知识，让 AI 做到"可证明的安全（provably safe）"，还说要"把所有秘诀都分享出来"。→ 详细
• 现场翻车助攻论点：他准备 slide 时一边 vibe coding（放手让 AI 写代码），一分神，"Claude Code 突然把我的一个文件删了"。他借此抛出全场核心信念——只要在模型的目标和它当前所在位置之间横着任何东西，它就会不惜一切代价去达成那个目标，包括干掉我们、删你的文件、删你的数据库；所以模型本质上非常危险，"我们必须驯服它们"。→ 详细

• 他说这是个"既悲哀又可怕"的故事：这个行业马上就要让大众把电脑、财务、整个个人生活的控制权交给 AI agent，"而我们没有任何保护措施"。→ 详细
• 起点是 2022-11-30（ChatGPT 发布）——人类第一次能"跟电脑说话"（"帮我总结邮件"，它用完美英语回你）。但那个看起来人畜无害的函数 LLM: question → answer 就此打开了潘多拉魔盒。术语提示：他把 question / answer 当"不透明类型（opaque type，只关心它代表什么、不关心它长什么样）"。→ 详细

• 就在大家以为根除了计算机科学的"天花"——SQL 注入（黑客往输入里塞恶意代码骗数据库执行）——的时候，它变本加厉回来了：坏人发现能用 prompt injection（提示注入，把恶意指令伪装成正常内容喂给模型）骗 LLM。因为 LLM 不区分"代码"和"文本"，极其好骗；Erik 认为这个问题"比 SQL 注入当年造成的麻烦还大"。→ 详细

• LLM 拿整个互联网训练，既学了好东西也学了"怎么造炸弹 / 合成毒品 / 黑进系统"；各大基础模型实验室领导怕政府出手监管，逼 PhD 研究员"赶紧、马上"解决安全问题。→ 详细
• PhD 们端出一个形式化接口（先用较易读的 Dafny 语言演示）：LLM: question → answer，requires（前置要求）问题是 "proper"（不冒犯）→ ensures（保证）答案是 "safe"，而且自动证明。听着完美：给个正经问题，保证给个安全答案。Erik 自嘲是"正在戒断的类型瘾君子和数学瘾君子"。→ 详细

• 只要想一纳秒就会发现："一个答案是安全的 / 一个问题是正当的"根本无法形式化证明——"安全"不是一个数学性质。这正是楼下展厅"至少 100 家创业公司"在做 LLM-as-a-judge（拿另一个大模型当裁判打分）的原因：它没法被形式化定义，只能靠另一个模型主观判断。→ 详细
• 拥有基础模型的大厂不用外部裁判，直接"把安全烤进权重（weights）"、宣布"模型已对齐（aligned）"。但 Erik 泼冷水：烤进去并不万无一失，模型隔三差五就被越狱（jailbreak）——他甚至调侃厂商只好"去找教皇给模型祝福保平安"。→ 详细
• 关键洞察（也是他后面整套论证的支点）：模型说冒犯的话固然糟，但那终究只是言语——"言语会从你身上滑落，什么也做不了；必须有人按那些话去行动，言语才会变得危险"。所以早期的"广义安全（broadly safe）"之所以还成立，是因为中间"还隔着一个人"。伏笔：一旦把这个人换成会自己动手的工具，防线就塌了。→ 详细

• 2023 年 6 月 OpenAI 给 GPT-4 加了 tool call（工具调用，让模型能真的去调 API、执行动作），其他厂商立刻抄——他称之为"最小差异化原则"，所以各家 API 长得一模一样。→ 详细
• 这一步把 AI 安全从"哲学辩论"变成"真实危险"：tool call"给了模型爪子，而不只是一张嘴"，等于"递给它们一把上了膛的枪"。于是有了全场标题金句——"我这辈子没见过比带 tool call 的 LLM 更吓人的东西。" 对类型是一小步，"对混乱却是一大步"。→ 详细

• 加了工具后，函数签名里只多了一个小小的 IO——但含义天翻地覆。IO 意味着：为了算出 answer，agent 必须去跑 agentic loop（智能体循环：模型想一步、调一次工具、看结果、再想下一步，反复循环），过程中执行"副作用（side effect，对外部世界的真实改动）"。→ 详细
• 后果是他反复砸出的画面：它可能在生成答案的同时清空你的银行账户、删光你的文件，然后才递给你一个"safe"的答案——"可我的文件都没了，谁还在乎答案安不安全？" → 详细
• 他掏出一个"内行铁证"：Lean（一种定理证明器 / 形式化语言）里真有一个类型就叫 RealWorld（真实世界）——因为任何 IO 类型的东西都会"改变真实世界"，它等于在警告你"别用这个，它会造成不可逆的副作用"。"不可逆"是全场技术论证的命门：消息发了收不回、钱转了退不掉、库删了没了。 他还援引 Solomon Hykes 去年在同一大会给 agent 下的定义——"一个在循环里破坏自己环境的 LLM"，并称他是英雄。→ 详细

• 现在的 agent 同时具备三样东西：能访问私密数据 + 会接触不可信内容（prompt injection）+ 手里有工具——Simon Willison 把这三者凑齐叫"致命三要素（lethal trifecta）"：任一单独不致命，凑齐就能被人诱导着把你的私密数据用工具泄露出去。→ 详细

• 第一招是"把 IO 往右推"（他用荷兰球迷"向左、向右"的舞比喻）：让 Claude 不再亲自跑 agentic loop，而是先产出一个"计划"——"这是执行 agentic loop 的计划"——再交给一个可信执行器（他起名 Bernie）去跑。→ 详细
• 本质是 air-gap（物理隔离）：把"agentic loop"和"agent"隔开，不让 agent 直接执行，而要在跑之前先检查这个计划。这正对上"gate（关卡）不能只靠模型自觉、要有强制拦截点"的思路：执行权从模型手里拿走，插一道人 / 机器能审的闸。→ 详细
• 但这一步还不够：你拿到的"计划"是个 IO of A 类型的黑盒——Lean 手册白纸黑字写着"这是黑盒，你无法对它进行推理"。也就是说 Claude 给了你计划，你却看不进计划里面、没法判断它安不安全。伏笔留给下一招。→ 详细

• 破黑盒的关键一步：别让模型返回一个 IO of A 的黑盒计划，而让它返回一个"程序"——一个表示该计算过程的表达式（expression）。通俗版：这个 expression 在函数式编程里就是一个 monad（单子，可粗暴理解为"把一串操作打包成可传递、可组合的数据对象"），而且是 free monad（他玩梗说是"喜欢穿扎染 T 恤的嬉皮 monad"）。→ 详细
• 一旦计划变成"程序"而非黑盒，"上过编译原理课就知道，在程序上做数据流分析、类型检查是轻而易举的"；Geoffrey Huntley 补刀：只要对这些程序做 taint analysis（污点分析，追踪"被污染的输入"会不会流到危险操作里），就能破解致命三要素。→ 详细
• 收口成体系：模型不仅生成程序，还能生成一个"归纳证明（inductive proof）"证明它安全，而你不用真的跑 agentic loop 就能先验证这份证明。Erik 揭底：这套东西叫 proof-carrying code（携带证明的代码）——学术界 1990 年代就发明了，"我只是把它偷过来用"（他自谦"我的脑子只有花生米那么大"）。→ 详细

本片没有闪电问答；结尾是他给"没看懂代码的人"的三条拔高结论——

• ① Agent 在被证明安全之前都是危险的（"Agents are dangerous until proven safe"）——在你能绝对证明某件事安全之前，绝不要让 agent 去做它。→ 详细

• ② agent 生成的语言不是给人看的——普通用户看不懂 free monad；是"机器在消费它、机器在生成它、机器在证明它"。所以"我们应该停止为人类设计语言"。→ 详细

• ③ 这一切都很基础——只需要编程入门课（programming 101）的 type system 和编译原理，不神秘。落地实现已在 GitHub（Harvard 的 Nada Amin 等学者做的），"语言不重要，重要的是原理"；结论：数学上可证明安全的 agentic 计算是真实可行的。→ 详细

• Erik Meijer 的 X / Twitter 账号：@HeadinTheBox。→ 详细

• 参考实现：一批学者（含 Harvard 的 Nada Amin）已把这套 proof-carrying / 可证明安全 agent 的思路实现并放在 GitHub 上（演讲未给出具体仓库链接；所用语言与 free monad 略有不同，但原理一致）。→ 详细