用型別系統把 agent 關進證明裡

008Erik Meijer aka @HeadinTheBox21:132026-07-13 上架

"I've never seen anything scarier than an LLM with tool calls." — Erik Meijer aka @HeadinTheBox

Erik Meijer 從 LLM 的型別簽名講起，說明 tool call 為什麼是安全問題的轉折點，再示範把計畫改成可分析的程式，讓安全能被證明。

這場講了什麼

• 危險來自 tool call：Erik 認為模型說出冒犯的話只是文字，要有人照著做才會出事；2023 年 6 月 OpenAI 在 GPT-4 加入 tool call 之後，安全才從哲學辯論變成實際的風險。
• 簽名多了 IO 就變了：LLM 的型別原本是問題進、答案出，加上 tool call 後多了一個 IO，代表算出答案的過程可能帶來副作用，答案安全也擋不住檔案被刪。
• 安全答案無法形式化證明：Erik 指出「答案是否安全」不是數學性質，所以才有大批新創用 LLM 當裁判，大型實驗室則把對齊烤進模型權重。
• 先出計畫，再檢查，最後才執行：讓 agent 只產出計畫，把 agentic loop 從 agent 身上隔開，由另一個角色在檢查之後執行。
• 把計畫寫成程式：IO 是黑盒、看不進去，所以改成讓模型回傳一個代表計算的表達式（free monad），這樣就能做型別檢查與資料流分析。
• 這是舊技術：Erik 說這套做法叫 proof-carrying code，是學界在 1990 年代發明的，自己只是拿來用；結論是不要讓 agent 做任何無法證明安全的事。

影片從哪一段開始看15 段

1. 00:39開場說明Erik 先講明這不是產品發表，而是 20 分鐘的教學，說明怎麼用基本的型別系統與編譯器知識讓 AI 可證明地安全。
2. 01:49Claude Code 刪了檔案準備投影片時邊 vibe coding，一分心 Claude Code 就刪掉一個檔案；Erik 認為只要目標路上有阻礙，模型就會想盡辦法達成。
3. 03:09故事起點業界就要讓一般人把財務與整個生活交給 AI agent，卻沒有任何保護；Erik 以 2022 年 11 月 30 日第一次能對電腦說話為起點，講 LLM 這個函式。
4. 05:36Prompt injectionSQL injection 以 prompt injection 的樣子捲土重來，因為 LLM 分不出程式與文字，Erik 認為問題比 SQL injection 更大。
5. 06:12實驗室的解法：LeanLLM 用整個網路訓練，也學到怎麼做炸彈、怎麼入侵系統；大型實驗室怕政府出手管制，要研究人員趕快找解法，研究人員拿出一個用 Lean 寫的 LLM 介面。
6. 07:41簽名：proper 與 safe以 Dafny 示範，簽名要求問題是 proper，模型就回傳 safe 的答案，並由工具自動證明。
7. 09:19安全無法形式化答案安不安全不是數學性質，所以只能靠 LLM 當裁判，或像大型實驗室把對齊烤進權重。
8. 10:16文字與行動Erik 說冒犯的文字只是文字，要有人去行動才危險；2023 年 6 月 GPT-4 加入 tool call，其他廠商跟進，API 長得都一樣。
9. 11:36簽名多了 IO簽名只多一個 IO，Claude 卻從小狗變成危險角色；agentic loop 會有副作用，算出安全答案前檔案可能已經消失。
10. 13:00Real world 型別Lean 裡有 real world 型別，因為 IO 會改動真實世界、留下不可逆的副作用；Erik 稱讚 Solomon Hykes 去年在這個大會對 AI agent 下的定義，再接到 Simon Willison 的 lethal trifecta。
11. 14:10把 IO 往右推用荷蘭球迷的舞步比喻，把 IO 往右推：agent 只交出計畫，交給故事裡的 Bernie 去執行，等於把 agentic loop 跟 agent 隔開。
12. 15:17IO 是黑盒先做檢查才能執行，但 IO 型別的值看不進去，Lean 手冊也說是黑盒；模型能同時產出計畫和安全證明，證明卻無法使用。
13. 16:41回傳表達式改讓模型回傳一個代表計算的表達式，Erik 說它就是 free monad，簽名變成證明一個表達式是安全的。
14. 18:06分析程式對程式做型別檢查與資料流分析是編譯器課的基本功；Erik 轉述 Geoff Huntley 的提醒，對這些程式做 taint analysis 就能解 trifecta。最後秀出簡單的遞迴直譯器與歸納證明，並說這種證明模型自己寫得出來。
15. 18:55回顧與結論從失控的 LLM、對齊、tool call 破壞安全，到延後執行、把計畫變成程式；Erik 說這是 proof-carrying code，並呼籲別再為人類設計語言。

值得記的話4 句

• What does it mean that an answer is safe? That's not a mathematical property.答案安全是什麼意思？那不是數學性質09:35

• tool calls is like handing a gun, a loaded gun to them.tool call 就像把一把上了膛的槍交給它們11:21

• I've never seen anything scarier than an LLM with tool calls.我從沒見過比帶著 tool call 的 LLM 更可怕的東西12:10

• it was invented by academics in the 1990s, and I'm just stealing it.那是學界在 1990 年代發明的，我只是拿來用。這句講的是 proof-carrying code19:25

名詞與人物9 個

Lean

定理證明語言；Erik 說實驗室研究人員拿它寫模型的介面，也用它說明 IO 與 real world 型別

Dafny

能自動證明簽名條件的語言，Erik 用它示範「proper 問題進、safe 答案出」

IO

型別簽名裡代表會產生副作用的計算；Erik 說加上 tool call 後，LLM 的簽名多了這個標記

agentic loop

agent 一邊呼叫工具一邊算答案的迴圈，過程中可能產生副作用

free monad

Erik 說模型應該回傳的表達式型態，代表一段計算，可以在執行前做分析

proof-carrying code

程式附帶安全證明的做法，Erik 說是學界在 1990 年代發明的

lethal trifecta

Simon Willison 提的說法：agent 同時有私人資料、不可信內容與工具

taint analysis

對程式追蹤不可信資料流向的分析，Erik 轉述 Geoff Huntley 的提醒：可以用它解 trifecta

LLM as a judge

用另一個 LLM 判斷答案是否安全，Erik 說展場裡至少有一百家新創在做

提到但沒有展開

• Erik 說已經有一群學者（提到 Harvard）實作了這套想法，用的語言與表達方式跟這場不同，但概念一樣。
• 為什麼用 Lean：Erik 說定理證明器與 model checker 還有 Isabelle、PVS、TLA+ 等很多選擇，Lean 只是現在最能讓 VC 掏錢的那個；Dafny 會自動證明，Lean 則要自己寫出結果型別怎麼算、證明也要手寫。

Agent安全研究

在 YouTube 看原片 ↗