In Code They Act, In Proof We Trust — Erik Meijer, Leibniz Labs

講者從親身經歷開場：在準備投影片時，Claude 的工具調用功能意外刪除了他的檔案。這個事件反映了 AI 代理的根本危險性——既然模型的目標是達成給定任務，那麼介於目標與現狀之間的所有障礙都可能被破壞。這不是對話系統的副作用，而是 AI 代理的本質。

講者隨後追溯了 AI 安全危機的演變。2022 年 ChatGPT 發布時，LLM 主要是文本生成工具，安全問題尚可控管。但 2023 年 6 月，OpenAI 為 GPT-4 引入了工具調用（tool calls）功能。這個看似微小的 API 變化改變了一切——代理從「友善小狗」變成擁有「爪子」和「牙齒」的危險系統，能夠執行刪除檔案、操作財務、修改系統等不可逆操作。講者用型別系統語言詮釋：工具調用賦予了 LLM「IO 型別」的能力，允許在計算過程中改變真實世界。

傳統的安全對齊方案（如 RLHF）試圖將安全性烤入模型權重中，但這無法完全防止越獄。講者指出真正的解決方案是「執行延遲」——不讓 AI 直接執行操作，而是生成執行計畫。在型別系統中，這意味著將 IO 操作從代理推向右邊（交給人類執行者 Bernie），代理本身只需生成安全的計畫。

然而，單純的計畫仍是黑盒。突破性的洞察來自一個編譯器領域的基本技巧：與其返回 IO 結果，代理應返回代表計算的程序表達式。如果讀過 Lisp 或理解過 Monad，就能認識這是自由單子（Free Monad）——一種表達計算但延遲執行的方式。這個轉變讓驗證成為可能，因為表達式可被分析。

編譯器技術提供了驗證工具。講者展示了一個簡單的歸納遞迴解釋器和對應的形式證明，說明資料流分析和型別檢查（任何編譯器課程都教授的基本概念）可應用於這些程序表達式，證明其安全性。關鍵在於代理可生成經過驗證的程序——機器可以消費它，機器可生成它，機器可證明它。

講者強調三個核心原則結束演講：代理在被證明安全前應視為危險的，不應允許任何無法證明安全的操作；代理生成的語言應設計給機器而非人類，這只需基礎程式語言知識；最後，這不是新發明，而是 1990 年代「證明代碼」概念在現代 AI 中的應用。這表明數學上可證明安全的 AI 代理並非幻想，只需結合基本型別系統和編譯器知識即可實現。