Y Combinator Paper Club 聚焦 AI 安全：从飞机防撞到 LLM 验证
斯坦福两位教授和 François Chollet 一起聊 AI 安全，把飞机防撞系统的验证方法搬到 LLM 上，还有用 Lean 证明代码正确的 CSLib 演示，硬核但好懂。
Y Combinator 本期 Paper Club 主题为 AI 安全，邀请 Stanford Center for AI Safety 联合主任 Clark Barrett 与 Mykel Kochenderfer，以及 François Chollet 参与。内容涵盖 OpenAI 与 Hugging Face 事件的拆解，CSLib 工具在 Lean 中证明代码正确性的方法。节目还介绍自适应压力测试如何从飞机碰撞规避系统迁移到 LLM 验证，飞机安全领域“十亿飞行小时一次灾难性故障”的标准被用作参照。讨论还提出 AI 或许需要类似 NTSB 的事故调查机构。
This week’s Paper Club is all about AI safety. Not the headlines, but the science. AI safety has been a research field for decades, with its own conferences, methods, and a track record in systems like aircraft collision avoidance, where the standard is one catastrophic failure per billion flight hours. We'll hear from @ClarkBarrett7 and Mykel Kochenderfer ( @aiprof_mykel ), Stanford professors and co-directors of the Stanford Center for AI Safety. Together with @FrancoisChauba1 , they break down the OpenAI–Hugging Face incident, how formal verification can mathematically prove properties of code, how aircraft safety techniques are being adapted to language models, and why AI may need its own NTSB. 00:00 - Science fiction vs. science fact 04:32 - Engineering problem, or P(doom) 06:04 - What actually happened at Hugging Face 07:53 - Where "10% in 10 years" comes from 11:21 - The real risk: open weights in the wrong hands 17:25 - Clark Barrett: when AI met automated reasoning 20:35 - CSLib: proving code correct in Lean 24:32 - From English spec to verified code in one click 27:55 - Mykel Kochenderfer: how do we know a system is safe 32:11 - Adaptive stress testing, from aircraft to LLMs 36:57 - Verifying neural networks 40:30 - Runtime monitoring and BetterBench 43:53 - Panel: reacting to the past three weeks 45:55 - An NTSB for AI 52:18 - Is cybersecurity solvable in five years 55:00 - If you were CISO of Bank of America 1:03:06 - The Swiss cheese model 1:05:43 - Audience Q&A Your browser does not support the video tag. 🔗 View on Twitter 💬 12 🔄 8 ❤️ 55 👀 9328 📊 19 ⚡
