AI Safety Fact vs. Fiction | YC Paper Club

斯坦福教授 Clark Barrett 用 Lean 把 Rust 代码转成数学定理来证明"永不被黑"，3 万行加密库原本 5 个专家写 3 个月，AI 代理 11 小时跑完。

过去三周 AI 安全讨论从"科学"滑向"恐慌"：有人说 AI 有 10% 概率让人类灭绝，但那份被反复引用的论文问的其实是 100 年尺度。这期 YC 讲座请来两位斯坦福教授，一个用数学证明代码不可被黑，一个用"瑞士奶酪"模型给大模型做安全测试——他们不谈末日，只谈怎么验证。

Clark Barrett 的核心主张很硬：软件工程至今靠"写完测一测、祈祷别出事"，但数学上我们其实知道怎么证明代码正确。他把 Rust 代码翻译成 Lean 定理，再用自动工具逐个证完。

• Lean 是什么：一个定理证明器，每一步都机器检查，不给你犯错的机会——相当于给代码写一份"数学体检报告"，而不是跑几个测试用例碰运气。
• 实测数字：一个 3 万行的 Rust 加密库，5 个专家写了 3 个月；用他们的验证代理自动跑，11 小时完成全部证明。
• Varys Forge 演示：输入一句英文需求（"找 32 位整数数组最大值"），工具自动生成规格、Rust 代码和证明，全程人工只点一次"同意"；Clark 在 Google workshop 上说"所有代码都形式化验证就不可能被黑"，没人想听，因为传统验证太贵。

Michael Kogen 讲的是另一条路：语言模型太复杂，证明不了它不出错，那就学航空业——用多层防御，每层漏洞别对齐。

• 瑞士奶酪模型：航空防撞靠分层——高度分层、空管、机载防撞系统，每层都有洞，关键是别让洞串成一条线。大模型同理：训练数据清洗、RLHF、发布前红队测试、上线后运行时监控。
• 毒性的量化难题：飞机碰撞定义明确（水平 500 英尺、垂直 100 英尺），但"毒性"要靠另一个神经网络（如 Llama Guard）打分，定义本身就模糊。
• 自适应压力测试：不是随机采样，而是主动搜索"低复杂度、高毒性"的失败案例；航空安全标准是 10⁻⁹/小时，直接模拟一次故障得跑 10 亿小时，所以他们用重要性采样把算力集中在关键场景。

两人都认为 AI 需要类似 NTSB（美国国家运输安全委员会）的独立调查机构，但也都清楚新建政府机构太慢。

• NTSB 模式：1967 年成立的独立机构，事故调查不追责，鼓励全行业共享安全信息——航空业因此比 1970 年代安全了 80 倍。
• Clark 的公司：在做"独立评估员"，发的不是"信我"的证书，而是可被任何人独立复核的证明；Michael 则警告别把所有安全责任交给前沿实验室，也别交给自称独立的关联方。

"如果有人告诉你他造出了一个和真实世界交互、而且绝对安全的系统，我不会相信。"

• 如果你的产品涉及代码生成，可以关注"生成代码 + 自动形式化证明"这条链路：短期内在加密、金融交易等"错了就赔钱"的模块先试点，比全面铺开更现实。
• 给大模型做安全评估时，别只跑标准 benchmark——学"自适应压力测试"，主动搜索低复杂度、高毒性的失败样本，比随机采样更快暴露问题。