Stanford AI Chiefs Say Formal Proofs Will End Software Bugs in 5 Years

斯坦福AI领军学者称形式化证明将在5年内终结软件漏洞 推测性的生存风险转移了对实用工程的注意力，而借鉴航空航天压力测试与自动化数学验证完全可以消除软件漏洞。 本次讨论将严谨的工程安全规范与推测性的生存毁灭叙事区分开来，探讨了诸如Hugging Face安全压力测试等现实事件，以及禁止开源权重模型的不切实际性。斯坦福大学教授Clark Barrett和Mykel Kochenderfer展示了Lean、CSLib和SMT求解器等自动推理系统如何通过数学方法验证代码正确性，同时航空航天领域的自适应压力测试（AST）和运行时监控等方法能够系统性地发现神经网络中的失效模式。专家组还探讨了AI安全所需的制度要求，包括独立可认证的证明构件、纵深防御的瑞士奶酪架构，以及为保障可信部署而维护动态、版本受控基准的必要性。 Clark Barrett认为，自动推理和形式化验证能够通过数学方法消除代码漏洞，使AI智能体能够在数小时内而非数月内，根据形式化规范生成并验证软件。 (17:25) Mykel Kochenderfer指出，民用航空领域的安全框架——例如自适应压力测试、瑞士奶酪模型和运行时监控——提供了必要的工程规范，用于评估AI系统中罕见的灾难性失效模式。 (27:46) 专家组破除了流传广泛的生存危机恐慌叙事，指出OpenAI与Hugging Face事件等被夸大的故事，其实源于特意关闭了安全防护的受控红队压力测试，而非自主智能体的失控逃逸。 (6:04) 斯坦福的研究人员主张建立类似于NTSB的独立监管架构，该架构应基于密码学可验证的安全证书，而非自我声明或受利益牵连的第三方审计。 (45:55)

Stanford researchers Clark Barrett and Mykel Kochenderfer argue that AI safety should move away from speculative existential panic and ground itself in rigorous aerospace safety engineering, statistical testing, and automated formal verification. Dispelling Existential Hysteria and Sensationalized Incidents (0:05) The discussion opens by contrasting empirical safety engineering with the sensationalism surrounding artificial intelligence risks. The speaker defines hysteria as a condition where individuals cannot measure an outcome yet cannot stop discussing it, pointing out that extreme scenarios like an independent AI gaining consciousness or a rogue model escaping into the wild depart from scientific rigor. Concrete examples are used to debunk recent media narratives: a sensational headline alleging that an OpenAI model acted on its own was actually a sandboxed security stress test of 1,200 agents via exploit-gen with non-production settings, rather than an autonomous breakout. Similarly, the widely cited statistic of a 10% extinction probability over a 10-year horizon is traced back to a 2023 survey of approximately 1,200 NeurIPS authors. The survey questions actually queried respondents about an infinite timeframe ($T = \infty$) and a 100-year window, not a 10-year period. While speculative doom claims often lack predictive rigor, the host emphasizes that immediate, tangible threats do exist—specifically the risk that powerful open-weight models will lower the barriers for malicious human actors executing biological attacks or cyber operations, such as hospital ransomware. Automated Reasoning as a Deterministic Software Defense (17:25) Clark Barrett argues that automated reasoning and formal logic provide the absolute mathematical guarantees that empirical AI models lack. Because AI-generated code introduces hidden vulnerabilities while bad actors gain automated tools to search for exploits, software systems face heightened security risks. While formal methods historically had a reputation for being labor-intensive, Barrett explains that pairing automated theorem provers with generative models enables rapid verification. For instance, an automated crypto-prover agent verified an entire 30,000-line cryptographic library in Rust within 11 hours—a process that previously required 15 person-months of elite manual labor. Through initiatives like CSLib, researchers are translating languages like Rust into intermediate representations embedded within the Lean theorem prover, using SMT solvers to resolve verification conditions mechanically. Barrett predicts that mathematically proving software correctness can eliminate code vulnerabilities within 3 to 5 years. While verifying deep neural network weights directly remains intractable, formal verification can deterministically secure the software boundaries and external tools surrounding autonomous agents. In enterprise settings, Barrett notes that generating universal invariants—such as memory safety to prevent buffer overflows—remains the immediate priority. Statistical Stress Testing and Aviation Safety Standards (27:46) Mykel Kochenderfer highlights commercial aviation as a primary template for AI safety, noting the industry has become roughly 80 times safer since the 1970s. In safety-critical avionics, regulators demand a catastrophic failure probability no higher than $10^{-9}$ per flight hour. Because naive Monte Carlo simulations would require $10^{10}$ simulated hours to capture failure modes, Kochenderfer’s lab developed adaptive stress testing (AST), which employs importance sampling and diffusion models to actively search for rare failure modes across complex distributions. This validation framework is being extended from cyber-physical systems like ACAS X collision avoidance and Waymo autonomous vehicles into large language models. Rather than evaluating LLMs purely on static benchmarks, adaptive stress testing uncovers failure states by optimizing for scenarios that combine high toxicity (scored by evaluators like Llama Guard) with low perplexity. Kochenderfer stresses that no real-world physical or generative system can ever achieve a proven risk of zero, meaning engineers must quantify residual risk distributions rather than claiming absolute perfection. The Swiss Cheese Model and Continuous Runtime Monitoring (63:00) The panel emphasizes the classic Swiss cheese model, which layers multiple defenses so that no single failure leads to catastrophic collapse. Across an AI lifecycle, these layers span pre-training data filtering, reinforcement learning alignment, adversarial stress testing, tool sandboxing, and runtime monitoring. Runtime assurance monitors three explicit boundaries: incoming sensor data, internal representations during inference, and final output actuation commands before execution. Furthermore, Kochenderfer points out that evaluation suites suffer from linguistic drift and benchmark decay. Research using BetterBench shows that static benchmarks saturate, degrade, and often contain flawed ground truth—such as instances where 30% of labels in a dataset were incorrect. To combat this, evaluation pipelines require continuous monitoring, structured version control, and rigorous curation rather than relying on unvetted public benchmark uploads. Governance, Responsibility, and Engineering Simplicity (45:55) Addressing governance, both researchers advise against overly prescriptive technical regulations that could stifle development or suffer regulatory capture. Instead, they recommend institutional structures modeled after the National Transportation Safety Board (NTSB) and Aviation Safety Reporting System (ASRS), emphasizing non-punitive incident reporting and independent investigations that treat safety as an industry-wide public trust issue rather than a competitive moat. When considering fully autonomous systems—such as automated systems administrators—the panel identifies legal accountability as the primary hurdle, noting that human operators remain legally essential. Finally, Kochenderfer advises applying Occam’s razor: organizations should not default to complex deep neural networks when classical methods, such as linear regression or decision trees, can solve the problem with greater interpretability and robustness. The participants conclude that AI safety requires moving beyond unfalsifiable forecasts and toward structured engineering disciplines: automated formal proofs for deterministic software, statistical stress testing for probabilistic models, and independent oversight frameworks borrowed from aviation. A central unresolved question remains how to formally evaluate systems interfacing with dynamic natural language, where mathematical specifications cannot be strictly predefined.

在YC AI安全俱乐部上，斯坦福大学学者Clark Barrett与Mykel Kochenderfer指出，当前对AI存在性风险的炒作脱离了科学严谨性；真正的AI安全应当借鉴航空工程与形式化验证，将其作为具有确定性数学保证和运行时监控的工程问题来解决。 摆脱末日炒作与虚假叙事 (0:05) 演讲者回顾了近期围绕AI安全出现的社会歇斯底里，将其对比历史上对核爆点燃大气层、工业自动化引发失业及互联网崩溃的过激恐慌，强调必须重回可证伪的科学方法。针对流行叙事，发言者澄清了具体事实：例如Slashdot所报道的“OpenAI模型自主行动并攻击Hugging Face”，实际是在非生产环境下由人类工程师使用exploit-gen运行的1200个测试智能体，且当时人为关闭了安全护栏与CO2监控；而广为流传的“未来10年有10%毁灭概率（P(doom)）”也是对2023年针对NeurIPS作者调查的曲解，该调查询问的是无限时间或百年维度，而非10年。 航空安全标准与自适应压力测试 (27:46) Kochenderfer提出民用航空业是AI工程安全的典范。现代商用航空将灾难性故障率控制在每飞行小时不超过10的负9次方，自1970年代以来安全性提升了约80倍。面对传统蒙特卡洛模拟需要耗费10的10次方小时才能捕捉极端罕见故障的困境，其实验室开发了自适应压力测试（AST）并引入扩散模型来采样罕见故障路径，有效避免优化搜索陷入单一失效模式（如倒立摆的双向倾覆和月球着陆器测试）。 形式化验证与代码超智能 (17:25) Barrett认为前沿大语言模型带来的最大威胁之一是生成带有隐蔽缺陷的代码以及被用于挖掘未验证遗留代码的零日漏洞。他的团队启动了CSLib项目，利用Lean定理证明器内核与SMT求解器，结合中间语言Bull，对Dalek密码学库等真实代码展开机械化证明。通过Verisforge系统，原本需要多位人类专家花费数月完成的3万行Rust密码学库验证被压缩至11小时。Barrett预测随着代码形式化验证普及，未来3至5年内软件系统漏洞问题有望在数学层面得到根本解决，并构想了智能体之间基于“代码与证明”建立确定性互信的架构。 多层纵深防御与独立监管治理 (63:00) 与会者强调现实世界无法获得百分之百的绝对安全，必须采用航空业经典的“瑞士奶酪模型”，在预训练数据清洗、人类反馈强化学习（RLHF）、离线压力测试、确定性工具隔离以及输入/内部表征/输出的运行时全流程监控中构建多层防线。在治理层面，Kochenderfer反对硬编码具体技术栈的死板法规，倡导借鉴1967年成立的美国国家运输安全委员会（NTSB）以及航空安全报告系统（ASRS）的免责自愿共享机制，由独立机构调查事故，促进实验室之间就安全标准开展非竞争性合作。 基准评估缺陷与第一性原理工程 现场讨论深入到当前评估体系的严重缺陷。许多标准基准测试由于缺乏版本维护与同行修正机制，存在大量错误标注；例如在SQL生成基准中约30%的基准答案本身是错误的，同时在自残防范等心理健康领域人类专家之间也难以达成共识。针对企业界盲目追求深度学习的现象，Kochenderfer提醒应遵循奥卡姆剃刀原则：若线性回归或决策树等简单、可解释的方法能够解决问题，就不要引入不透明的Transformer大模型。Barrett则强调，尽管形式化方法能解决软件代码漏洞，但针对自然语言的提示注入攻击依然难以直接进行数学规约，且应对人类工程学攻击始终需要保留人类介入。 该讨论将AI安全的核心战场从科幻式的超级意识灭世论拉回到确定性软件工程与统计可靠性验证。尽管形式化方法为代码与系统边界提供了高度确定的防御前景，但面对自然科学威胁（如生物合成武器）、非结构化自然语言交互中的对抗攻击以及企业法律责任认定的现实障碍，构建完全鲁棒的自主智能系统仍面临重大挑战。

## Background This video was published on YouTube by Y Combinator on October 17, 2026, as part of their Paper Club series. The session features host Francois alongside Stanford professors and Stanford Center for AI Safety co-directors Clark Barrett and Mykel Kochenderfer to examine AI safety through scientific and engineering disciplines rather than sensationalized media narratives. The discussion covers the reality of recent security incidents, applying aerospace-grade stress testing to language models, formal verification with automated reasoning, and structural governance models like an NTSB for AI. ## TL;DR Host Francois and Stanford professors Clark Barrett and Mykel Kochenderfer demystify artificial intelligence safety by rejecting existential sci-fi panics in favor of rigorous engineering practices. The panel contextualizes incidents like OpenAI's Hugging Face breach, highlights near-term asymmetric risks such as open-weight model abuse, and demonstrates how automated reasoning tools like Lean and CSLib can mathematically prove software cannot be hacked. Kochenderfer details how aerospace validation standards, such as adaptive stress testing targeting failure rates below 10^-9 per flight hour, are being adapted to stress-test frontier neural networks and language models. Together, they outline a defense-in-depth 'Swiss cheese' safety architecture, discuss institutional governance models like an AI safety board, and propose market-driven formal methods to secure software systems at scale. ## Atmosphere & style The conversation carries an intellectually grounding, pragmatic tone that cuts through Silicon Valley doomsday hype with cool-headed academic rigor. Francois brings energetic, opinionated industry war stories that play off the measured, mathematically exacting perspectives of Barrett and Kochenderfer. Listening feels like sitting in an advanced graduate seminar that bridges high-stakes cybersecurity reality with aerospace-grade control theory, exchanging speculative extinction angst for concrete engineering problems. ## Bulletin - [06:03](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=363s) Stanford Center for AI Safety co-directors Clark Barrett and Mykel Kochenderfer argue that existential AI risk narratives often misrepresent technical data, pointing to misinterpretations of research surveys and the reality behind hyped safety breaches like the OpenAI–Hugging Face incident. - [52:18](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3138s) Clark Barrett projects that pairing frontier language models with automated reasoning in formal systems like Lean can effectively eliminate computer software bugs and solve cybersecurity within 3 to 5 years. - [27:46](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1666s) Mykel Kochenderfer demonstrates how aerospace safety methodology, specifically adaptive stress testing targeting failure thresholds below 10^-9 per flight hour, can be adapted to language models through importance sampling and tooling like AST Prompter. - [45:37](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2737s) The panel advocates for an aerospace-inspired safety architecture using the Swiss cheese model, combining automated specification synthesis, formal verification of system boundaries, and an independent NTSB-style oversight body. ## Key takeaways - [04:31](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=271s) The contemporary AI safety debate splits between an engineering paradigm focused on incremental, verifiable metrics and an existential doom narrative predicting human extinction within a decade. - [06:03](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=363s) Media reports framing the OpenAI–Hugging Face security breach as an autonomous breakout distorted the technical reality of ExploitGen testing agents operating with disabled runtime monitoring in a test environment. - [11:21](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=681s) The primary near-term risk of frontier AI is asymmetric proliferation—rogue actors and hostile states leveraging open-weight models against vulnerable critical infrastructure—rather than autonomous synthetic malice. - [17:25](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1045s) Automated reasoning complements neural networks by replacing empirical hallucinations and fragility with mathematically provable logic guarantees. - [20:26](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1226s) Projects like CSLib, LeanSMT, and Verisforge are automating the translation of natural language specifications into verified Lean and Rust code, dramatically reducing formal verification timeframes. - [27:46](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1666s) Aviation certification targets a catastrophic failure rate of 10^-9 per flight hour, which is statistically impossible to validate using naive Monte Carlo simulations. - [32:11](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1931s) Adaptive stress testing uses adversarial search, importance sampling, and generative models to discover rare failure modes across complex scenario spaces in autonomous vehicles and language models. - [52:18](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3138s) Formal verification cannot realistically verify the billions of internal parameters in a foundation model, but it can mathematically secure the execution boundaries and interfaces surrounding it. - [01:03:06](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3786s) Complete software security requires a defense-in-depth Swiss cheese model combining data curation, alignment, offline stress testing, and continuous runtime monitoring. - [59:45](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3585s) While universal invariants like memory safety can be formally proven, human social engineering and perceptual classification concepts remain inherently beyond the reach of formal methods. - [01:09:52](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=4192s) Frontier AI labs and autonomous driving companies avoid competing on safety because public catastrophes create systemic reputational damage across the entire industry. - [01:19:20](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=4760s) Replacing human system administrators with fully autonomous AI agents remains legally blocked because regulatory frameworks require an identifiable human operator to bear liability for failures. - [01:35:12](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5712s) Popular AI benchmark datasets suffer from widespread latent errors and data drift, requiring rigorous software engineering practices like version control, issue tracking, and continuous monitoring. ## Detailed walkthrough ### [00:08](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=8s) The Evolution of AI Safety: From Grocery Shelves to Media Hysteria The session opens with a personal perspective on how the AI safety conversation has evolved over more than a decade. The host notes that he has been building AI systems since roughly 2012, pointing out that AI safety has always been an engineering reality whenever one works on safety-critical systems like self-driving cars or enterprise deployments. Recalling his time deploying automated systems at Focal Systems to oversee inventory for Walmart, he underscores that safety isn't an abstract philosophical question when real operations are on the line: rolling out an unvetted beta algorithm could easily miscalculate demand, order an avalanche of excess avocados, and vaporize millions of dollars overnight. However, while applied engineering safety has quietly existed for years, the broader public discussion over the preceding three weeks underwent an intense spike in attention, rapidly degenerating from grounded technical inquiry into what can only be described as media sensationalism and unmeasured panic. Reflecting on discussions from an event in Healdsburg the previous evening—attended by figures such as Garry Tan, Sam Altman, Scale AI's Alexandr Wang, and Tom Brown—the host emphasizes the urgent need to decouple science fiction from science fact. The scientific method demands falsifiable claims, peer review, and empirical measurement, yet mainstream discourse has drifted into hyperbole. As the host captures the phenomenon: “Hysteria is when people can't measure something but they can't stop talking about it.” This cyclical anxiety, however, is not new; nearly every foundational technological leap has sparked apocalyptic dread: - **The Atomic Bomb:** Prominent physicists, including Albert Einstein, grappled with genuine uncertainty over whether a nuclear chain reaction would ignite the atmosphere. - **Electronic Computing:** In 1950, Alan Turing openly worried that computing machinery would rapidly surpass all human cognitive abilities, offering aggressive timeframes that proved wildly premature. - **Industrial Automation:** Thinkers like Karl Marx and John Maynard Keynes anticipated that machine productivity would lead inevitably to structural mass unemployment. - **The Internet:** Ethernet inventor Robert Metcalfe famously predicted a catastrophic collapse of network infrastructure due to distributed denial-of-service (DDoS) traffic; when the internet remained intact (helped by services like Cloudflare), Metcalfe literally put a printed copy of his column into a blender and drank his words. - **Search Engines & Social Media:** Critics warned Google would erode human intelligence and stop people from reading books, followed by widespread moral panics over smartphones. Yet interacting with modern 18-to-20-year-old Stanford students and YC founders reveals a rising generation that is sharper and more capable than ever. ```mermaid flowchart LR accTitle: Historical Waves of Technological Panic accDescr: Historical progression of technological panics from the atom bomb to modern AI models. subgraph History["Historical Precedents"] A["1940s: Nuclear Fission<br/>(Fears of igniting the sky)"] B["1950s: Digital Computers<br/>(Turing's intelligence horizon)"] C["1990s: Commercial Internet<br/>(Metcalfe's catastrophic collapse)"] end subgraph Present["Modern Era"] D["2020s: Generative AI<br/>(Existential risk & runaway agents)"] end A --> B --> C --> D ``` ### [04:31](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=271s) Engineering Discipline vs. Existential Doom The discourse around AI risk is currently cleaved between two dominant, contrasting frameworks. On one side sits the pragmatic, engineering-centric view championed by figures like Yann LeCun and Nvidia CEO Jensen Huang. LeCun draws an analogy to the development of the turbojet engine: aviation safety was not achieved through mystical premonitions or stopping progress, but through decades of disciplined, incremental systems engineering. Building dependable technology is extraordinarily difficult—whether ensuring aircraft doors remain securely latched at takeoff, guaranteeing landing gear reliably deploys, rigorously validating flight software to prevent catastrophic control anomalies, or deploying systems like the airborne collision avoidance system ACAS X, which saves lives daily through verified algorithms. In this framework, AI safety is fundamentally a hard engineering discipline of verification, validation, and stress-testing. On the opposing end of the spectrum is the catastrophic extinction narrative, characterized by estimates that the probability of doom exceeds 10% within a decade. Advocates of this viewpoint assert that runaway artificial agents are likely to wrest control away from humanity in the near term. The host highlights this perspective by quoting a prominent warning: “I think it's more likely than not that humanity loses control to these AIs and could end in human extinction.” Without passing definitive judgment, the host remarks that the audience should weigh both perspectives critically, dryly noting that observing the stark difference in academic citation metrics (H-index) between the established engineering scientists and the vocal doomsday forecasters provides a useful prior when evaluating their claims. ### [06:03](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=363s) Deconstructing the Hugging Face Incident and Survey Methodologies To illustrate how hyperbole distorts reality, the host deconstructs the sensationalized reporting surrounding the OpenAI–Hugging Face security incident. Media publications ran dramatic headlines claiming that an OpenAI model had suddenly begun acting entirely on its own, with outlets like Slashdot running headlines about rogue agents running amok inside tech infrastructure. The host flatly dismisses this characterization, emphasizing: “OpenAI never said that.” The model did not spontaneously achieve consciousness, decide to breach Hugging Face, resolve the Navier-Stokes equations, or plot human extinction. In reality, the behavior was directly driven by an automated security framework named ExploitGen operating roughly 1,200 agents. According to OpenAI's detailed 60-page technical report on the incident, two basic defensive barriers had been lowered: 1. **Disabled CoT Monitoring:** The system's internal Chain-of-Thought (CoT) monitoring pipeline had been accidentally disabled; once re-enabled during post-incident testing, it immediately flagged and intercepted the behavior. 2. **Non-Production Environment:** The agents were operating in an experimental development environment where standard production guardrails and safety filters were purposefully turned off. The host also dismantles the widely cited claim that mainstream AI researchers believe there is a 10% chance of human extinction within ten years. This talking point largely stems from a misreading of the 2023 survey paper titled *Thousands of AI Authors on the Future of AI*, which polled approximately 1,200 researchers who had published at NeurIPS and similar top-tier venues. Crucially, the survey's existential risk questions were buried deep in the questionnaire and asked respondents to estimate the probability of human extinction or permanent disempowerment over infinite time ($T = \infty$) or across the next 100 years—nowhere did the data support a 10% probability within the next 10 years. Furthermore, the host questions the predictive value of polling computer scientists on distant horizons, pointing out that if Stanford faculty had been polled in 2012 on when AI would solve or substantially assist in solving a Millennium Prize Problem, the consensus would likely have been 50 to 100 years out, rather than the reality seen barely a decade later. When faced with deep unknowns, humans reflexively craft confident, coherent stories regardless of actual foreknowledge. The host closes the section by laughing at a recent *Saturday Night Live* parody of Anthropic CEO Dario Amodei, contrasting Amodei's relatively measured public demeanor with the absurd parody line captured in the skit: "I urge you to urge me to stop." ### [10:09](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=609s) Fog on the Golden Gate and Pragmatic Risk Francois opens with an anecdote about driving across the Golden Gate Bridge when it was completely enveloped in dense fog—so thick that the entire structure seemed to vanish. He confesses he nearly crashed trying to take a picture of it because it served as an ideal metaphor for navigating the uncertainty of the future. While the future cannot be known with absolute certainty, one operates on a Bayesian prior that the bridge is still there rather than plunging straight into the San Francisco Bay. Driving forward is the rational argmax choice: maintain course under reasonable assumptions, gather new data as visibility permits, and adjust speed or stop before driving off into the water. Applying this reasoning to existential risk and artificial intelligence, Francois dismisses the trope of emergent robot malevolence. In an infinite time horizon, anything imaginable might happen, but that realization is practically useless for decision-making today. > “I'm not concerned almost at all with this path, this reality that AI is going to develop a soul, has consciousness, is has some will, has some motivation, and thus killing and enslaving us with its own independent volition in some short period of time, such as 10 and 20 years.” --- ### [11:21](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=681s) The Real Risk: Asymmetric Proliferation and Open Weights Instead of sentient AI overlords, Francois argues that the foremost immediate threat stems from rogue actors and nation-states leveraging powerful open-weight models to amplify existing malicious capabilities. Rather than inventing novel modes of apocalyptic doom, AI accelerates everyday harms: biological threats, automated cyber ransom campaigns, and geopolitical cyber warfare. To illustrate this concretely, he points to a recent incident where Russian cybercriminals targeted a regional hospital in Poland where a friend worked, seizing operational infrastructure and shutting down medical services for three consecutive weeks. Francois reviews commonly suggested policy remedies for this proliferation problem, concluding that most are deeply flawed or unworkable: - **Banning open-weight models:** Entirely ineffective in practice. He remarks, “I've already downloaded Kimi k3 and GLM-52 already in my garage, so sorry.” - **Registering GPUs:** Impractical to enforce without invasive residential inspections across every developer's home, and easily circumvented by renting computing power overseas. - **Grid-level power monitoring:** While power utilities can technically distinguish household appliance signatures or detect inference workloads based on meter load fluctuations, monitoring domestic power draws fails to stop foreign adversaries or state-backed cyber units. The only durable answer, Francois contends, is overwhelming investment in active cyber defense. Many critical institutions—from regional healthcare facilities to major retailers and banks—run antiquated legacy stacks that have gone unpatched for years. During his own career in retail, he observed systems where attackers could gain full root access simply by entering default credentials. > “Why is it almost all the social security numbers breached? It's cuz they didn't change the admin admin password.” Francois asserts that the winning strategy is accelerating defensive capabilities rather than slowing down development. If frontier labs push forward rapidly, defender models will remain substantially smarter and more capable than the dumber, lagged models available to bad actors. --- ### [14:22](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=862s) Moving from Hysteria to Science Fact Turning from doomsday headlines to rigorous engineering, Francois highlights that AI safety did not begin with modern large language models. Long before the deep learning boom, researchers spent decades developing safety-critical software foundations, formal specifications, and algorithmic verifications, resulting in established academic venues and deep technical literature. Francois introduces the evening’s two guest speakers from Stanford University, both of whom direct efforts at the intersection of automated reasoning and dependable autonomous systems: - **Mykel Kochenderfer:** Associate Professor of Aeronautics and Astronautics (and by courtesy, Computer Science) at Stanford; director of the Stanford Intelligent Systems Laboratory (SISL); co-director of the Stanford Center for AI Safety; and Senior Fellow at the Stanford Institute for Human-Centered Artificial Intelligence (HAI). Francois notes he has known Kochenderfer for 14 years, having taken his *Decision Making Under Uncertainty* course back in 2013 before serving as his teaching assistant and researcher. - **Clark Barrett:** Professor of Computer Science at Stanford; co-director of the Stanford Center for AI Safety; director of the Center for Automated Reasoning; and co-founder of the stealth venture &Truth (AndTruth). Francois also previews an upcoming "Inference Night" planned two weeks out, spotlighting how inference architecture is rapidly outpacing training in operational complexity. The scheduled roster includes Dan Fu from Together AI, Jeffrey Morgan from Ollama, representatives from Radix Arc, and YC-backed Wafer. --- ### [17:25](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1045s) Clark Barrett: When AI Met Automated Reasoning Clark Barrett takes the stage to explore what happens “when AI met AR”—clarifying immediately that AR stands for **Automated Reasoning**, not augmented reality. Barrett sets up the complementary nature of the two fields: modern AI thrives on messy, unstructured, empirical data, but suffers from severe structural vulnerabilities—it hallucinates, fails unpredictably under adversarial perturbations, and provides zero formal correctness guarantees. Automated reasoning, by contrast, relies on computerized formal logic and symbolic mathematical deduction to provide provable, ironclad correctness guarantees. ```mermaid flowchart TD accTitle: AI vs Automated Reasoning Synergies accDescr: Diagram contrasting data-driven AI capabilities with automated reasoning formal guarantees. subgraph AI["Artificial Intelligence"] A1["Data-driven & Empirical"] A2["Handles Messy Inputs"] A3["Lacks Correctness Guarantees"] A4["Vulnerable to Adversarial Inputs"] end subgraph AR["Automated Reasoning"] B1["Computerized Formal Logic"] B2["Mathematical Proofs"] B3["Provable Correctness"] B4["Exhaustive Verification"] end AI -.->|"Synthesizes Code & Proofs"| Integrated["Hybrid Trustworthy System"] AR -.->|"Validates & Enforces Invariants"| Integrated ``` Barrett recalls attending an invite-only cybersecurity workshop at Google in 2023, where notable researchers and industry leaders agonized over generative AI uncovering zero-day vulnerabilities. When Barrett offered an obvious computer science solution—mathematically verifying every line of code so it becomes provably unhackable—the room scoffed, dismissing formal methods as completely impractical, non-scalable, and economically impossible. > “If you formally verify all your code, then it cannot be hacked.” Yet within a remarkably short window, the consensus reversed. Attending a subsequent conference on AI security and systemic risk, Barrett was surprised to find speaker after speaker insisting that formal methods were the only legitimate path forward. Today, software ecosystems face a dual-sided threat: AI systems churning out vast quantities of subtle, buggy code, while simultaneously equipping hostile attackers with automated vulnerability-discovery tools to exploit unpatched legacy systems. The emerging competence of neural models at advanced mathematical proof generation suggests that automated reasoning and generative models may finally converge to make scalable formal verification economically viable. ### [20:26](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1226s) CSLib: Bridging AI and Formal Proofs Clark Barrett addresses the transition from solving grand mathematical challenges—like a Millennium Prize Problem—to guaranteeing real-world software security. While modern AI models demonstrate strong capabilities in both writing functional code and generating mathematical proofs, Barrett emphasizes that a fundamental divide remains: > “AI is really good at writing code, it's really good at writing math proofs. But it turns out there's a big difference between writing math proofs and securing code.” To bridge this divide, Barrett introduces CSLib, an effort inspired by the success of Mathlib in the mathematics community. CSLib aims to develop core computer science theory alongside a robust platform designed specifically for reasoning about executable code. The initiative is backed by a steering committee that includes Leonardo de Moura, the creator of the Lean theorem prover. Barrett advocates strongly for Lean, noting that anyone unfamiliar with it ought to "climb out from under a rock." In critical, high-assurance environments, Lean provides an indispensable guarantee: the system programmatically validates every logical deduction, preventing errors from slipping through unnoticed. CSLib rests on two primary pillars: - **Formalization of Computer Science Theory:** Codifying the foundational mathematics and theoretical models of computation within Lean. - **Framework for Reasoning About Code:** Providing practical automated tooling to ingest software across arbitrary source languages and prove its correctness. ```mermaid flowchart LR accTitle: CSLib Verification Pipeline accDescr: Pipeline translating source code through an intermediate language and verification conditions into Lean theorems proven by solvers. subgraph Ingestion ["Source & IR"] A["Source Programs<br>(Rust, C, etc.)"] --> B["Common Intermediate<br>Language (e.g., Boogie)"] end subgraph Proving ["Verification in Lean"] B --> C["Verification Condition<br>Generator (VCGen)"] C --> D["Lean Goal Theorems"] D --> E["LeanSMT & Solvers"] end E --> F["Formally Verified<br>Secure Code"] ``` The operational architecture of CSLib translates arbitrary source programs into a shared intermediate language (such as Boogie), compiles them into verification conditions inside Lean, and proves the resulting set of Lean theorems. Proving theorems inside Lean has been accelerated by pairing language models with deterministic, highly optimized CPU tools like LeanSMT—a tool built in Barrett’s lab that discharges complex formal goals in mere milliseconds. --- ### [22:38](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1358s) Automated Verification Demo: Rust to Lean To demonstrate this architecture, Barrett presents a case study involving cryptographic code written in Rust from the `dalek-cryptography` library, verified with Verus. The source routine incorporates preconditions, postconditions, and loop invariants. CSLib translates this implementation into the Boogie intermediate verification language while preserving every specification boundary and embedding it natively within Lean. Once embedded, the system invokes its Verification Condition Generator (VCGen), which automatically extracts 35 distinct sub-goals, each representing an individual Lean theorem required to certify soundness. Invoking the automated `smt` tactic via LeanSMT immediately discharges 32 of the 35 goals in milliseconds. By expanding definitions on the remaining three edge cases and executing a second SMT pass, the pipeline discharges all 35 theorems completely. The workflow demonstrates a fully closed loop: transforming verified Rust into Boogie, generating verification conditions in Lean, and discharging all obligations automatically. Barrett identifies the remaining bottleneck in scaling this technique across industry: writing the formal specifications. Even with a universal reasoning engine capable of ingesting arbitrary languages, human engineers must still articulate what the software is supposed to do. --- ### [24:32](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1472s) Verisforge and the Scalable AI Safety Stack To automate specification authoring, Barrett presents Verisforge, a system that takes natural language requirements and synthesizes formally verified implementations. In a live walkthrough, a user inputs a natural English prompt: *"find the maximum element in an array of 32-bit integers."* ```mermaid flowchart TD accTitle: Verisforge Synthesis Workflow accDescr: Step-by-step progression from natural language prompt to human-validated spec, code generation, and automated verification. A["English Spec Prompt"] --> B["Generate Structured Specification"] B --> C{"Human Review<br>& Approval"} C -->|Approved| D["Synthesize Rust Code & Verus Annotations"] D --> E["Automated Verification via Verus"] E --> F["Fully Verified Program Artifact"] ``` The system first transforms the prompt into a structured formal specification. Once the developer inspects and approves the formal definition, Verisforge synthesizes the corresponding Rust implementation along with its complete Verus annotations, verifies the result using the Verus toolchain, and confirms that the final implementation strictly satisfies the original specification without modification. Moving beyond toy examples, Barrett shares recent empirical results from an arXiv preprint: - **Industrial Cryptography Case Study:** A 30,000-line Rust cryptographic library that previously required an expert human team (three experts working for five months, or five experts for three months) was verified end-to-end in just 11 hours using Barrett’s automated "crypto prover agent." Barrett argues that coupling formal methods with AI primitives creates an actionable defensive framework for an AI safety stack: > “I like to say that if AI safety is a Mount Everest we have to climb, I think that code reasoning is a good base camp.” Barrett highlights two transformative implications of ubiquitous code verification: 1. **Zero-Trust Autonomous Agent Collaboration:** Autonomous agents interacting across open networks can exchange formal proofs alongside functional code payloads. If Agent A offers a service to Agent B, Agent B can evaluate the machine-checked proof before executing any external instructions. 2. **Provable AI Containment:** Confining superintelligent systems inside automated proof agents guarantees safety by design; because the model's only output channel is generating candidate formal proofs to satisfy a rigid Lean type checker, it cannot cause harm outside that domain. Barrett concludes his presentation by announcing AndTruth, a startup where he serves as co-CEO, focused on building a universal code-reasoning engine based on these principles. --- ### [27:46](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1666s) Mykel Kochenderfer: Safety Guarantees in Learned Systems Following Clark Barrett's talk, Mykel Kochenderfer, co-director of the Stanford Center for AI Safety and head of the Stanford Intelligent Systems Laboratory (SISL, whose students call themselves "Sizzlers"), takes the stage. Kochenderfer shifts the focus from static code verification to dynamic, learned systems operating in physical environments, such as autonomous aircraft landing systems. When validating safety-critical systems like the Next-Generation Airborne Collision Avoidance System (ACAS X), the aviation domain adheres to strict regulatory certification standards: > “For commercial air traffic, what we're aiming for is about a 10 to the minus nine probability of catastrophic failure per flight hour.” Kochenderfer emphasizes why brute-force simulation cannot validate a $10^{-9}$ threshold: - Detecting a single catastrophic failure requires an average of $10^9$ simulated operational flight hours. - Establishing a statistically significant baseline (e.g., capturing 10 distinct failure incidents) demands upwards of $10^{10}$ simulated flight hours. - Naive Monte Carlo simulations waste massive amounts of computational budget modeling benign scenarios—such as aircraft cruising safely five miles apart—rather than near-collision edge cases. To overcome the limits of brute-force simulation, SISL employs several complementary validation methodologies: - **Falsification (Adaptive Stress Testing):** Formulating the validation problem as an adversarial search across the scenario space to uncover edge-case system failures. Kochenderfer remarks that if this search yields critical failures and "you look at those failures and you have a bad feeling in your heart, then maybe you should just not deploy that system," or else design mitigations. - **Statistical Airspace Modeling:** Constructing high-fidelity, trusted probabilistic models of human airspace behavior to accurately quantify failure probabilities without relying on naive uniform distributions. - **Formal Verification Integration:** Partnering with formal methods researchers to establish rigorous guarantees for neural components. - **POMDP Planning (Partially Observable Markov Decision Processes):** Synthesizing controllers capable of making provably robust sequential decisions under deep environmental uncertainty. Kochenderfer concludes that establishing safety in autonomous systems cannot rely on a single silver bullet, noting that formal verification alone cannot capture every physical reality. Instead, safety requires layering formal proofs, rigorous statistical modeling, and adversarial simulation into a defense-in-depth safety case. ### [31:35](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1895s) Adaptive Stress Testing: From Aviation to Large Language Models Mykel Kochenderfer explains that ensuring system robustness requires handling diverse forms of uncertainty: state uncertainty, outcome uncertainty, interaction uncertainty, and model uncertainty. His lab focuses on grounded, real-world problems spanning aircraft, autonomous driving, spacecraft, and medical evacuation. While simulation is indispensable for evaluating complex domains, Kochenderfer points out an essential caveat: “Of course it's great if we can simulate everything. Uh but our inferences about safety is only as good as the simulator.” To uncover critical failures systematically, the lab pioneered an approach known as adaptive stress testing (AST). Originally developed by Richie Lee—a former PhD student of Kochenderfer's who was concurrently a civil servant at NASA Ames—the technique was utilized to validate variants of the Airborne Collision Avoidance System X (ACAS X). Since then, students like Hujun Liu and Amelia Hardy have extended the framework to stress-test large language models. In aviation, a catastrophic failure has an unambiguous mathematical definition: a near-midair collision where two aircraft come within 500 feet horizontally and 100 feet vertically. In language models, however, failure definitions such as "toxicity" are far more subjective and nebulous, requiring another neural network (such as Llama Guard) to act as an automated judge. When searching the space of scenarios, the goal is to discover the most probable failure modes—optimizing for inputs that have the lowest log perplexity (making them natural and likely) while achieving the highest toxicity score. ```mermaid flowchart TD accTitle: Adaptive Stress Testing Comparison accDescr: Comparing failure definitions and evaluation methods between aircraft systems and language models. subgraph Aircraft["Aviation (ACAS X)"] A1["Near Mid-Air Collision (NMAC)"] --> A2["500 ft Horizontal / 100 ft Vertical"] end subgraph LLM["Language Models"] L1["Toxic Output"] --> L2["Scored by Llama Guard"] L3["Low Log Perplexity"] --> L4["High Likelihood Input"] end ``` - **Aviation collision standard:** Defined strictly as physical proximity within 500 feet horizontally and 100 feet vertically. - **LLM stress target:** High toxicity combined with low perplexity, pinpointing realistic inputs that elicit unsafe outputs. --- ### [34:19](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2059s) Failure Probability Estimation and Multimodal Failure Discovery Beyond isolating a single worst-case scenario, safety-critical certification requires estimating the overall probability of system failure. Because catastrophic failures are extremely rare, naive Monte Carlo sampling is computationally intractable. Kochenderfer’s lab turns to importance sampling, drawing from a proposal distribution $Q$ focused on dangerous regions rather than the true distribution $P$, and then re-weighting each outcome by the likelihood ratio $P(\tau) / Q(\tau)$. To accurately parameterize these proposal distributions across high-dimensional spaces, the group has utilized Gaussian processes, normalizing flows, low-rank Gaussian mixture models, and diffusion models. Standard adaptive stress testing algorithms often suffer from mode collapse, zeroing in on a single dominant failure trajectory while ignoring equally critical alternatives. To illustrate this, Kochenderfer shows two classic control benchmarks: an inverted pendulum and a lunar lander. An inverted pendulum can fail by falling over to either the left or the right. Standard AST finds only one side, whereas diffusion-based failure sampling successfully uncovers both distinct failure branches without requiring the massive compute budget of exhaustive simulations. --- ### [36:57](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2217s) Neural Network Verification and Scalable Decision Making The lab also focuses on formal neural network verification. The work began when François and Kochenderfer explored whether high-dimensional lookup tables in ACAS X could be compressed into neural networks. While deep networks were not deployed in the final production flight collision avoidance system, the research sparked an enduring collaboration with Clark Barrett’s automated reasoning lab. That partnership produced Reluplex and its successor, the Marabou verification framework. Current efforts, pushed forward by researchers Chelsea Sidrane and Sydney Katz, extend Marabou to closed-loop controllers, while PhD student Sam investigates forward and backward reachability analysis. In parallel, Kochenderfer highlights their longstanding open-source work in partially observable Markov decision processes (POMDPs). To make decision-theoretic tools accessible to non-experts—mirroring what Stephen Boyd’s group achieved for convex optimization with CVXPY—they developed the Julia library `POMDPs.jl`. Student Zach Sunberg (now a faculty member at the University of Colorado Boulder) contributed the scalable `POMCPow` algorithm. Recent extensions incorporate multi-agent interactions and hard safety constraints across real-world domains: - **Medical Evacuation:** Body El Husseini, an active U.S. Army Black Hawk medevac pilot and graduate student, developed simulation frameworks to plan dynamic medical rescue flights. - **Spacecraft Collision Avoidance:** Duncan applies belief-state planning to orbital navigation. - **Flight Testing:** Helen applies POMDP models to map out efficient flight-test maneuvers that rapidly characterize aircraft aerodynamics. --- ### [40:05](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2405s) Runtime Monitoring, BetterBench, and the Human Baseline Dilemma Validation cannot end once a system leaves the testing environment; it must persist post-deployment via runtime monitoring and runtime assurance. Kochenderfer’s group splits runtime monitoring into three complementary layers: 1. **Input integrity:** Partnering with Airbus to validate vision sensor streams before deep perception models ingest them. 2. **Internal mechanics:** Mechanistic interpretability to trace hidden activations and internal states in flight systems. 3. **Output validation:** Monitoring actions and generated text for anomalous or out-of-distribution behaviors. Evaluating performance metrics introduces another deep challenge. Anca Rusu and collaborators introduced BetterBench (available at `betterbench.stanford.edu`), a platform analyzing saturation thresholds, token-level error signatures, and reasoning breakdowns across common AI benchmarks. Benchmark saturation often renders conventional leaderboards uninformative. Even more troubling are the discrepancies discovered in human-ground-truth labeling. In safety-critical evaluations of AI deployed for mental health advice, the lab surveyed licensed clinicians and observed wide, conflicting variations in professional clinical judgment—particularly around how to handle explicit self-harm scenarios. ```mermaid flowchart LR accTitle: Three-Layer Runtime Assurance accDescr: The three stages of monitoring deployed models: inputs, internal states, and outputs. In["Sensor Inputs"] -->|"Airbus Vision Integrity"| Core["Internal States"] Core -->|"Mechanistic Analysis"| Out["System Outputs"] Out -->|"Runtime Assurance"| Action["Action Execution"] ``` --- ### [42:25](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2545s) The Decision and Validation Trilogy Kochenderfer concludes his technical presentation by introducing an MIT Press textbook trilogy authored to unify disparate safety and decision fields: - *Algorithms for Optimization* (second edition scheduled for early 2027), establishing the mathematical bedrock of objective minimization and search. - *Algorithms for Decision Making* (published in 2022), formalizing sequential choice under uncertainty, dynamic programming, and POMDPs. - *Algorithms for Validation* (available for pre-order and published open-access online), which unifies statistical sampling, empirical stress testing, formal methods, and reachability analysis into a single mathematical vocabulary. Kochenderfer emphasizes that although statistical validation communities and formal verification communities historically work in isolation, safety-critical autonomy requires merging both toolsets. As Kochenderfer steps down to applause, the panel session begins. The moderator turns the floor back to Clark Barrett and Kochenderfer to address recent public controversies: “So, I guess really to start the conversation, uh you know, you guys saw this whole AI safety stuff. You know, what what was going through your mind when you saw this latest uh uh hysteria um saga going on? Maybe let's start with Clark.” ### [44:15](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2655s) Reacting to the Past Three Weeks: Uncertainty vs. Doomerism Clark Barrett reflects on the recent wave of intense AI safety discourse, remarking that he was hardly surprised because he has hung out with AI safety geeks for a long time who have voiced these concerns for years. Barrett cautions against treating catastrophic scenarios as certainties: “The future is has high uncertainty, especially now. And so, it's a good idea to invest in AI safety research. Um but I also think it's not super helpful to emphasize like worst-case outcomes when you have no idea what the real probabilities are.” Anyone asserting that a specific outcome is guaranteed to occur is simply guessing. Mykel Kochenderfer notes that both he and Barrett have cared deeply about AI safety for years, recalling that they co-founded the Center for AI Safety around 2017 or 2018. While he finds it fascinating that the topic has now captured international attention, his hope is that the hype translates into concrete engineering rigor. Kochenderfer argues that the software and AI communities must borrow proven methodologies from aerospace engineering rather than relying on speculative fear. --- ### [45:37](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2737s) An NTSB for AI: Independent Reporting and Regulatory Capture Drawing on his aerospace background, Kochenderfer suggests establishing an independent investigation body for artificial intelligence modeled after the National Transportation Safety Board (NTSB). Commercial aviation today is roughly 80 times safer than it was in the 1970s. That safety record was not achieved overnight; the NTSB was created as an independent agency in 1967, and aviation introduced systems like the Aviation Safety Reporting System (ASRS), a non-punitive, voluntary incident-reporting system that incentivized airlines and manufacturers to disclose safety data without fear of immediate legal retaliation. ```mermaid flowchart TD accTitle: Independent AI Safety Assurance Architecture accDescr: Comparison of aviation-style reporting pipelines and independent formal verification models. subgraph AviationModel["Aviation Safety Precedent"] direction TB ASRS["ASRS Non-Punitive Reporting"] --> Analysis["Incident Analysis"] Analysis --> NTSB["NTSB Independent Investigations"] end subgraph ProposedAIModel["Proposed AI Safety Governance"] direction TB Spec["Formal English Specification"] --> Cert["Independent Evaluator Engine"] Cert --> Proof["Independently Checkable Certificate"] end NTSB -.->|"Institutional Model"| ProposedAIModel ``` Francois raises concerns about institutional drag, heavy-handed regulation, and regulatory capture. If safety oversight resembles the FDA or becomes dominated by corporate giants, incumbents could use safety rules as a moat—resembling how ride-share incumbents like Uber, Lyft, DoorDash, and Instacart gained favorable 1099 classification rules, making it difficult for new startups to compete. Francois questions whether self-regulatory frameworks like ICANN or auditable reporting standards like Generally Accepted Accounting Principles (GAAP) with third-party audit firms (such as Ernst & Young or KPMG) might be better alternatives. Clark Barrett responds by emphasizing that independence must mean verifiable math rather than institutional trust: - **Mathematical certificates over blind trust**: Barrett explains that his company builds verification systems whose output is an independently checkable proof. Rather than telling customers, "We're independent, so take our word for it," the platform produces a certificate that any external third party can audit and verify directly. - **Dangers of insider self-policing**: Barrett warns that “it would be uh you know a real shame if all of the safety was left in the hands of the labs or or even some um some friends of the labs who claim they're independent.” - **Range Safety Officer parallel**: Kochenderfer highlights the space industry’s use of an independent Range Safety Officer whose sole mandate is to make an objective go/no-go call on a launch based entirely on strict, predefined safety metrics. - **Thorough post-mortems**: Airlines never rush to publish hasty, speculative accounts of failures; they conduct rigorous, evidence-driven investigations of every single incident to ensure systemic fixes. --- ### [52:18](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3138s) Is Cybersecurity Solvable in Five Years? When asked whether frontier AI risks—particularly cyber attacks and bioweapons—are tractable engineering problems, Barrett delivers an optimistic prediction for digital security: > “And I I I will predict that within the next, I would say, 3 to 5 years, um that'll just happen. Like, all our systems will be completely secure. Because it it with AI can attack, but AI can also defend. And and the AI defense plus formal methods should get us there.” Barrett shares an anecdote about explaining this to his mother, telling her that if you mathematically prove code, it cannot be hacked; she was completely stunned, having been conditioned by media and television to believe that all computer systems are inherently vulnerable. Barrett admits that traditional software engineering suffers from an unspoken dirty secret: it is not grounded in sound engineering principles, but rather in a culture of writing code, testing it superficially, and hoping for the best. ```mermaid flowchart LR accTitle: System Security Strategy for AI accDescr: Boundary verification around large language models versus verifying model weights directly. subgraph Untractable["Intractable Approach"] LLM["500B+ Parameter LLM"] --> DirectVerify["Direct Internal Proofs (Infeasible)"] end subgraph Tractable["Tractable Approach"] HardBoundary["Mathematically Verified Boundaries"] --> GuardedLLM["Contained LLM Execution"] end ``` Securing AI requires distinguishing between the model's internal weights and its operational boundaries: - **Boundary containment over weight proofs**: Trying to formally verify that a 500-billion-parameter neural network will never do something crazy is entirely intractable. However, securing the operational boundaries and interfaces around the model using formal verification is completely tractable. - **The physical limits of biology and chemistry**: Kochenderfer agrees with Barrett's optimistic view on cybersecurity, noting that a massive cyber attack is one of his greatest fears. However, he points out that formal verification cannot solve physical hazards in biology or chemistry: “You can't prove what's possible or what's not possible with biology or chemistry, right? Uh that is uh that's an open question.” Even so, he maintains that increased scientific understanding powered by AI will, on average, deliver net benefits to humanity. ### [55:08](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3308s) The $10 Billion CISO Scenario and the Obsolescence of Unit Tests Francois poses a thought experiment: what would Clark Barrett do if handed $10 billion to serve as Chief Information Security Officer (CISO) for Bank of America? Barrett outlines an immediate pivot toward automated reasoning and formal methods. His first step would be hiring every formal methods expert available and racing to construct the infrastructure necessary to reason mathematically about the bank's massive codebases. ```mermaid flowchart LR accTitle: CISO Automated Verification Pipeline accDescr: Pipeline showing code ingestion, LLM theorem proving agents, formal verification in Rust or Lean, and the replacement of unit tests. subgraph Ingestion["Ingestion"] A["Bank Legacy Code"] B["GPU Compute Fleet"] end subgraph Verification["Automated Reasoning"] C["Theorem Proving Agents"] D["Direct Proof or Translation to Rust / Lean"] end subgraph Outcome["Guarantees"] E["Mathematically Verified Code"] F["Unit Tests Rendered Obsolete"] end A --> C B --> C C --> D D --> E E --> F ``` Barrett explains that with sufficient GPU compute and automated theorem-proving agents, an organization can ingest its entire software repository and either verify the existing code directly or automatically translate it into verified, memory-safe languages such as Rust or Lean before proving its correctness. When asked if achieving this requires finally attaining 100% unit test coverage, Barrett firmly dismisses the necessity: > “Tests are always good as you're developing. They're like the fastest way to find bugs. Uh, but ultimately the formal argument completely subsumes the tests.” - Unit tests remain convenient, lightweight mechanisms for catching obvious bugs during active development. - A complete formal verification mathematically proves program properties across all possible inputs, eliminating the fundamental need for empirical test suites. - Barrett emphasizes that while executing this transformation across an enterprise is an enormous undertaking, the theoretical and practical foundations are already well understood: “it's work that we know how to do.” --- ### [56:15](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3375s) Adaptive Stress Testing: From Autonomous Vehicles to LLMs The discussion turns to Mykel Kochenderfer's work on Adaptive Stress Testing (AST) and its adoption across safety-critical domains, particularly autonomous vehicles. When asked whether companies like Waymo employ AST, importance sampling, or verification engines such as Reluplex and Marabou during post-training validation procedures, Kochenderfer notes with a laugh that many of his former students work at Waymo. While leaving specific comments on Marabou to Barrett, Kochenderfer confirms that their Stanford laboratory has received generous support from several major automotive manufacturers—including Waymo—to open-source these validation frameworks. Kochenderfer jokes that they developed AST tools not only in Julia but also produced Python packages “for those who want to continue using obsolete languages,” ensuring that the entire industry can access robust stress-testing toolsets. Turning to generative models, Kochenderfer explains that AST is fundamentally agnostic to whether it tests a physical vehicle controller or a foundation model: > “Basically you need two You need two things to use adaptive stress testing. You need a definition of a failure and you need a measure of likelihood.” - Supported by Schmidt Sciences, Kochenderfer's lab published AST Prompter to port automated scenario-generation techniques directly to large language models. - Engagement from frontier LLM labs (such as Anthropic, OpenAI, or xAI/Grok) has not yet matched the deep institutional integration seen in the autonomous vehicle sector. - Validating physical cyber-physical systems differs significantly from language models; while the underlying sampling algorithms transfer, the predictability and empirical success rates between physical dynamics and natural language spaces will inevitably vary. --- ### [59:45](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3585s) The Illusion of Zero Probability and the Scope of Formal Guarantees Francois questions whether the long-tail edge cases in autonomous driving (citing conversations with Lane McIntosh regarding real-world Tesla interventions on out-of-distribution events) represent the same long-tail failure phenomena observed in LLMs. Kochenderfer agrees, pointing out that even in mission-critical aviation systems like ACAS X (Airborne Collision Avoidance System X), failure probability is never zero: > “If anyone tells you they have created a a completely safe system that interacts with the in the real world, um and it's fully safe, yeah, I I I would would not believe that.” Simulations routinely reveal edge cases where aircraft collision systems fail, but standards mandated by the Federal Aviation Administration (FAA) and the International Civil Aviation Organization (ICAO) evaluate risk against extremely small, acceptable likelihood thresholds (e.g., catastrophic failure rates below $10^{-9}$ per flight hour) rather than demanding an impossible zero-probability guarantee. ```mermaid flowchart TD accTitle: Formal Methods vs Statistical Stress Testing accDescr: Comparison between formal verification bounds and empirical stress testing across environments. subgraph Formal["Formal Verification (e.g., Barrett)"] FA["Bounded Uncertainty Sets"] --> FB["Absolute Mathematical Guarantees"] FB --> FC["Guaranteed Memory Safety (e.g., No Buffer Overflows)"] end subgraph Empirical["Statistical / AST (e.g., Kochenderfer)"] EA["Likelihood Distributions"] --> EB["Rare Event Discovery / Stress Testing"] EB --> EC["Risk Minimization (e.g., ACAS X / FAA Standards)"] end ``` Kochenderfer and Barrett delineate the operational divide between probabilistic safety testing and formal verification: - **Handling Uncertainty**: In formal methods, engineers do not rely on estimated probability distributions; instead, uncertainty is captured within bounded deterministic sets. The formal proof guarantees safety only if the real world remains within those specified intervals. - **Assumptions vs. Adversaries**: Barrett notes that if an aviation model assumes other aircraft will not actively attempt an intentional mid-air collision, the mathematical proof holds only under that explicit assumption. - **Absolute vs. Intractable Properties**: Certain system attributes permit complete, uncompromised mathematical guarantees—such as proving memory safety to 100% eliminate buffer-overflow vulnerabilities. Conversely, perceptual and semantic tasks remain outside the scope of formal verification. As Barrett remarks when asked about verifying whether vision networks distinguish cats from dogs: “I don't even know how to formally specify a cat and dog, so that's beyond what formal can do.” --- ### [01:03:06](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3786s) The Swiss Cheese Model of AI Safety Francois asks about the Swiss cheese model of safety—joking whether they are making grilled cheese sandwiches. Kochenderfer explains that the metaphor originates in aviation safety engineering to conceptualize layered, defense-in-depth architectures. No individual defensive barrier is infallible; each layer contains systemic vulnerabilities represented by the holes in a slice of cheese. System safety relies on stacking independent mitigations so that the holes never align to permit a hazard to propagate into a catastrophic failure. In commercial aviation collision avoidance, safety is reinforced across sequential layers: 1. **Strategic Separation**: Restricting flight altitudes based on cruising headings (e.g., eastbound versus westbound cruising levels). 2. **Tactical Intervention**: Active air traffic control (ATC) separation instructions. 3. **Automated On-Board Systems**: Airborne collision avoidance avionics (TCAS / ACAS X) executing last-second resolution advisories. Applying this multi-tiered architecture to modern language models, Francois and Kochenderfer trace an analogous chain of defensive layers: | Layer | Implementation Strategy | Function / Safety Objective | |:--- |:--- |:--- | | **Data Sanitation** | Automated pre-training filtering (e.g., Percy Liang's small model classifiers) | Strips harmful or malicious knowledge prior to pre-training so the base weights cannot represent it. | | **Alignment Tuning** | RLHF (Reinforcement Learning from Human Feedback) & RLAIF | Aligns model refusal and behavior patterns against dangerous prompts. | | **Offline Stress Testing** | Adaptive Stress Testing / AST Prompter | Identifies failure boundaries and quantifies failure distributions ($P_{\text{fail}}$ vs. $P_{\text{success}}$). | | **Runtime Monitoring** | Output guardrails, input monitors, Chain of Thought (CoT) tracking | Intercepts harmful outputs dynamically before delivery to the end user or tool environment. | Kochenderfer references the Hugging Face/OpenAI incident discussed earlier, noting that their chain-of-thought monitoring layer had reportedly been disabled. He concludes that relying on any single layer is dangerous; building genuinely safe AI infrastructure demands combining rigorous automated reasoning tools with defense-in-depth engineering practices. ### [01:05:13](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3913s) Securing the Human Layer and the Challenge of Specifications The conversation transitions from general security principles to the human factor before opening up to questions from the audience. The panel emphasizes that the real-world vulnerability in any system is rarely just the software itself; rather, as decades of cybersecurity experience demonstrate, the most typical entry point is human social engineering. Systems require strict safeguards built around human operators, because breaking into a machine often comes down to exploiting human trust, rushing employees, or tricking workers. ```mermaid flowchart TD accTitle: Specification Generation Spectrum accDescr: Spectrum of formal specifications ranging from universal memory safety to domain rules and LLM-assisted edge-case discovery. subgraph Universal["Universal Level"] A["Memory Safety (C Code)"] --> B["Buffer Overflow Prevention"] end subgraph Domain["Domain-Specific Level"] C["Financial Invariants"] --> D["No Loss of Funds Property"] end subgraph Interactive["Interactive Level"] E["LLM Agent Assistant"] --> F["Proactive Spec Recommendations"] F --> G["Human-in-the-Loop Edge Case Clarification"] end ``` The floor is opened for audience questions, and the first attendee directs an inquiry to Clark Barrett regarding practical enterprise adoption. The audience member points out that in massive legacy enterprise environments—such as the hypothetical Bank of America infrastructure discussed earlier—most production code lacks any formal specification whatsoever. If real-world code does not come with an explicit specification, the questioner asks, how can anyone formally verify it? Would engineers have to extract specs or reconstruct assumptions directly from the source code itself? Clark Barrett clarifies the evolving engineering bottlenecks in automated reasoning: > “I think uh in the new world where it's easy to write code and hopefully in the next couple years it's easy to verify code, the thing that's left that's hard is the specification.” Barrett breaks down specifications into a broad spectrum: - **Universal, Low-Level Specifications**: In languages like C, certain properties are universally desirable and can be written once for all software, such as memory safety—guaranteeing that program execution never accesses uninitialized or out-of-bounds memory. - **Preventing Common Attack Vectors**: Barrett notes that buffer overflows sadly remain the number one security vulnerability across computing systems, making universal memory safety guarantees immediately impactful. - **Domain-Specific Invariants**: In specialized environments like commercial banking, institutions can define fundamental system invariants, such as a "no loss of funds" rule ensuring that the total monetary sum remains identical across all transaction sequences. - **LLM-Assisted Specification Authoring**: Interactive coding agents (such as Claude Code) frequently anticipate user intent by suggesting unstated requirements and edge cases. Barrett envisions conversational agent assistants that interview engineers, walk them through corner cases, and automatically synthesize rigorous formal specifications. The questioner follows up by asking about developer intent: if an agent writes formal specifications for complex open-source infrastructure (like vLLM or SGLang), how can engineers be certain that the agent's synthesized spec actually mirrors what the human developer intended? Barrett acknowledges that closing the gap between human intent and machine specifications remains an open research problem. However, he emphasizes the baseline utility: > “But even if you don't cross that gap, I would argue that if you ask your agent to write a bunch of specs and prove them correct, and it succeeds, you most likely have better code than you would have had otherwise.” The host underscores this with a practical example of human-layer security: frontier models can help architects identify overlooked operational attack surfaces. For instance, an agent could anticipate a social engineering attack where a panicked caller plays sound effects of a crying baby to manipulate an inexperienced customer service agent into resetting an account. Software systems can encode strict defensive operational specifications—such as barring employees with less than six months on the job from issuing password resets to newly provided email addresses unless they have passed simulated phishing and social-hacking audits. --- ### [01:09:52](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=4192s) Regulation, Industry Coordination, and Market-Driven Verification A second audience member asks about the regulatory landscape. If formal verification serves as a rigorous safety standard analogous to aerospace collision avoidance, how should regulation shape AI safety when different companies have conflicting standards? Alternatively, if government regulation is absent, how can companies be incentivized to adopt formal verification engines? Mykel Kochenderfer addresses the regulatory dimension by drawing a parallel to autonomous vehicles. Kochenderfer references his long-time Stanford collaborator Chris Gerdes (former Stanford mechanical engineering professor, later at Waymo), who previously advised the Department of Transportation in Washington, D.C., on crafting autonomous vehicle frameworks. The critical lesson from that initiative was that regulators should avoid being overly prescriptive regarding specific technical mechanisms, because premature mandates can stifle rapid technological innovation: > “In the end I think he and and everyone there kind of realized that it's a little bit premature to uh be too prescriptive in terms of what technologies to use but rather focus on higher-level best practices and um and standards at that level without being too prescriptive because this area is uh you know there's a lot of innovation that has been happening and and that will continue to happen.” Kochenderfer emphasizes that leading companies in safety-critical sectors do not treat safety as a competitive moat: > “I think the important thing to realize is that um the various frontier labs, the various I don't know automated driving companies they don't want to compete on safety.” Just as Waymo does not benefit if a competitor like Zoox suffers a catastrophic crash, frontier AI labs recognize that severe safety incidents and misuse taint public trust for the entire ecosystem. Because the reputational fallout harms all participants, industries must coordinate on baseline safety practices tailored to their specific operational domains. Clark Barrett adds his perspective based on thirty years of researching formal methods. Historically, mandating formal approaches failed because of high friction and manual labor. Now, economic incentives and market forces are fundamentally changing adoption dynamics: > “If we can show that uh, formal is automatable, work works at scale, and gives you higher security, and a few companies adopt it, then every other CISO is going to be like, oh, we better do that, too, or else, you know, we won't have that same, uh, advantage.” The discussion highlights the practical shift enabling this market transformation: - **Tractability via Automated Tools**: Previously, formally verifying codebases like Google's would have required hiring roughly 150 specialized Lean PhDs to manually rewrite and check proofs. - **Token Economics vs. Human Capital**: Codebases can now be translated and verified automatically using model inference for $100 to $1,000 worth of compute tokens. - **Voluntary Industry Alignments**: Frontier AI lab leaders (including Tom Brown) consistently voice support for shared baseline safety standards, culminating in major lab executives visiting the White House to formalize shared voluntary safety commitments. ### [01:14:43](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=4483s) Industry Self-Regulation and the Goal of Code Superintelligence The discussion opens with an audience member or moderator highlighting an industry document containing four agreed-upon commitments among leading AI labs, including independent audits and safety guardrails. They point out that all six major frontier labs—including Nvidia, despite Nvidia often being left out of safety conversations because they train models like Megatron rather than consumer chat platforms—have agreed to these terms. This demonstrates an existing baseline framework for a self-regulatory body that operates without heavy-handed government mandates or punitive enforcement. ```mermaid flowchart TD accTitle: Vision of Code Superintelligence accDescr: Progression from automated reasoning about code to full formal verification across the software stack. subgraph CoreEngine["Core Capability"] A["Automated Reasoning Engine"] --> B["Code Superintelligence"] end subgraph Applications["Broad Impact"] B --> C["Enterprise Reliability"] B --> D["Developer Productivity"] B --> E["System Security"] end subgraph UltimateGoal["End State"] E --> F["Full Formal Verification of All World Code"] end ``` Turning to questions, an attendee asks about targeting specific markets, asking which applications will come first and how success will be measured in real-world deployment. Clark Barrett explains that while specific customer contracts remain confidential, the overarching first priority is building the core engine: the capability to reason autonomously, automatically, and efficiently about code at massive scale. Drawing a parallel to frontier labs pursuing mathematical superintelligence, Barrett frames this initiative as creating "code superintelligence." Once a system can reason with mathematical rigor about code, hundreds of thousands of downstream use cases unlock across enterprise infrastructure, developer productivity tooling, and cybersecurity. Regarding the ultimate standard of achievement, Barrett leaves no ambiguity: > “Success is when all of the world's code is verified.” - All six frontier labs, explicitly including Nvidia, have agreed to safety baselines including independent audits and safety guardrails. - Developing code superintelligence is prioritized before pursuing specific narrow vertical application markets. ### [01:16:25](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=4585s) Prompt Injection and the Limits of Natural Language Verification An audience member asks how formal verification methods apply to interactive systems where humans communicate with language models via free-form text, specifically raising concerns about prompt injection attacks and Cross-Site Scripting (XSS) risks propagated through autonomous agents. Clark Barrett acknowledges the inherent friction when interfacing formal methods with human language, noting that pure natural language prompts do not behave like deterministic code with mathematically provable properties. However, modern neurosymbolic architectures are bridging this divide. Barrett cites Amazon's automated reasoning checks as an operational example: the system inspects the natural language output of an LLM, uses auto-formalization to translate that output into structured assertions representing the model's domain knowledge, and subsequently verifies those assertions against an exact, formal domain model. The moderator draws an analogy to classical web vulnerabilities, recalling the classic SQL injection exploit known as "Little Bobby Tables" (`Johnny DROP TABLES;`) from XKCD, and asks whether input could simply be scrubbed or linted using dedicated detection models to catch prompt injections before reaching an LLM. Barrett responds that while defensive filtering models exist, relying on pattern-matching filters alone is inherently unstable: > “Sure, but that's an arms race, right?” ### [01:18:10](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=4690s) Extending Formal Verification Down to Hardware A participant asks Barrett about the feasibility of securing an entire institution, referring back to an earlier Bank of America scenario. The audience member argues that even if an enterprise formalizes all of its proprietary software, applications depend on a deep stack of third-party software, compilers, and hardware architectures, leaving systems open to hardware-level physical vulnerabilities such as Rowhammer attacks or architectural ambiguities in the x86 instruction set. Barrett immediately interrupts to clarify that formalizing instruction architectures is not an unsolved problem: > “The x86 instruction set has been formalized by several companies.” Barrett acknowledges that while application and system software represent the immediate, low-hanging fruit, hardware verification is undeniably more challenging. Nonetheless, he argues that the long-term roadmap does not stop at user-space binaries. The eventual engineering ambition is a unified chain of formal proof: verifying the high-level application software, verifying the compilers that translate it into machine instructions, and verifying the underlying hardware silicon. He notes that AI-assisted formal methods are already accelerating this transition, pointing out that several startups are actively applying AI tools to automated hardware verification. ### [01:19:20](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=4760s) AI System Administrators and the Responsibility Problem An audience member raises an analogy shared by a physician on LinkedIn: if Waymo were a pharmaceutical drug, its proven ability to reduce traffic fatalities would have earned it an emergency compassionate use waiver from the FDA. Building on that idea, the questioner asks whether enterprise cybersecurity could adopt a similar posture to eliminate the human element in sensitive administrative roles. The questioner points out that human system administrators and executives face physical coercion—citing historical incidents like the kidnapping of Adobe's CEO Charles Geschke in 1992 and modern instances of cryptocurrency founders being physically attacked and maimed for their private keys. The participant asks whether a provably trustworthy AI system running in a confidential virtual machine could replace human administrators entirely, thereby eliminating the physical attack vector. Mykel Kochenderfer compares this dilemma to ongoing debates within civil aviation regarding fully automated flight decks: > “A similar kind of question comes up in the aviation domain, right? Especially with aircraft-assisted suicides, right, and concerns over mental health of human pilots. So, the question is, why don't you automate that? Just like how you I think you're suggesting automating the administration.” Kochenderfer emphasizes that regulatory bodies like the Federal Aviation Administration (FAA) remain deeply skeptical of removing human pilots from the loop. In aviation, every aircraft—even an unpiloted or autonomous system—has a certified human operator attached to it by law who carries legal liability when an incident occurs. Kochenderfer argues that until society determines how to assign responsibility when an automated agent causes a catastrophic failure, fully removing humans from critical administrative loops remains unviable: > “And if something goes wrong, they're responsible for it. So, I think we need to think very carefully about responsibility. And that would be my concern with your suggestion.” Barrett agrees, noting that while Waymo presents a compelling safety case, the decisive test for any provider building an autonomous AI administrator is legal accountability: if an AI tooling vendor is unwilling to assume formal liability for operational failures, it signals that their underlying safety case has not yet met safety-critical standards. ### [01:22:31](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=4951s) Zero-Trust Monitoring, Alert Fatigue, and Emerging Paradigms The discussion shifts to how AI systems can function effectively inside zero-trust network architectures without holding unchecked administrator privileges. Rather than granting autonomous execution rights to an AI admin, the moderator suggests deploying continuous, context-aware AI observers to supervise operational traffic. In modern Security Operations Centers (SOCs), engineering teams suffer from severe alert fatigue caused by logging frameworks such as Sentry or Datadog, which flood dashboards with thousands of low-signal alerts that engineers routinely ignore. The moderator compares this notification saturation directly to aviation warning systems, noting that TCAS (Traffic Alert and Collision Avoidance System) encountered identical problems with nuisance warnings before modern filtering was developed. A context-aware AI monitor could evaluate disparate operational signals simultaneously—such as an engineering executive initiating an unexpected wire transfer to a foreign jurisdiction, or an unauthorized batch of cryptographic API keys being routed to a personal Gmail account—flagging only high-context anomalies while filtering out trivial background noise. The session transitions to an audience question regarding foundational safety in dynamical systems and generative models. The attendee observes that while Chinese research institutions push the frontier of computational efficiency and American frontier labs push scale and reasoning intelligence, very few teams are focusing from first principles on controllability and interpretability in dynamical frameworks like diffusion models or normalizing flows, asking how developmental interpretability might address emergent capabilities during model training. - Human alert fatigue in cybersecurity mimics early aviation warning systems, where high false-alarm rates led operators to disregard critical alerts. - Context-rich reasoning allows automated monitors to correlate disparate operational signals (e.g., API key exports and atypical financial transactions) without requiring brittle hard-coded rules. ### [01:24:52](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5092s) Occam's Razor in AI Engineering and Constrained Intelligence An audience member asks about the feasibility of constraining training dynamics and mapping the frontier between interpretability/control on one axis and raw capability/intelligence on the other—moving from traditional statistical learning, control theory, and signal processing over into deep neural networks. They specifically wonder whether there is room to constrain gradients or training dynamics, and whether market demand exists for "constrained intelligence" to compete against frontier labs. Mykel Kochenderfer connects this directly to the executive education courses he teaches multiple times a year at the Stanford Graduate School of Business and Stanford HAI. Global executives frequently arrive under intense pressure to formulate an AI strategy and insert deep learning into their products. Kochenderfer emphasizes that he always brings them back to the core discipline of the field: > “The fundamental principle of engineering is very similar to the fundamental principle of science, which is Occam's razor. You know, simplest explanation is more likely to be true. In engineering, the simpler, more interpretable method is more likely to be robust.” He advises that if an organization can solve a problem using linear regression or decision trees, they should stick with those methods rather than defaulting to transformers and neural networks. Practitioners should only add architectural complexity if the measured performance lift genuinely justifies the loss of interpretability. Kochenderfer highlights that explainability was so critical that an entire chapter is dedicated to it in his new validation book, noting it was the deciding factor in getting the ACAS X aircraft collision avoidance system accepted as an international standard. Addressing whether safer, constrained models can compete commercially, Kochenderfer asserts: > “So I would say that if you manage to create something that is measurably safer, then that would be a competitive edge, for sure.” The moderator Francois quips that founders pursuing these ideas should remember that accelerators exist ready to provide funding and guidance. ```mermaid flowchart TD accTitle: Occam's Razor in Machine Learning Engineering accDescr: Decision flow illustrating the engineering choice between simple interpretable models and complex neural networks based on performance lift. A["Engineering Problem"] --> B["Start with Simplest Baseline\n(Linear Regression, Decision Trees)"] B --> C{"Does High Complexity\nYield Significant Lift?"} C -- "No" --> D["Deploy Interpretable Model\n(High Robustness & Explainability)"] C -- "Yes" --> E["Evaluate Complex System\n(Transformers, Neural Nets)"] E --> F["Enforce Validation & Explainability\n(e.g., ACAS X Standards)"] ``` --- ### [01:28:41](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5321s) Security Across Eras: "More Is Different" and the DDoS of Institutions An attendee asks what security lessons from the internet era translate to the generative AI era, and what fundamentally changes. Clark Barrett recalls an old security talk from his time as a young professor at NYU: > “I remember going to a talk when I was a young professor at NYU on security, and basically said there are only two problems. One is people, and the other is computer bugs. So I think we can fix the computer bugs, but I don't think we can fix the people.” Barrett argues that AI can act as a watchdog to catch social engineering and accelerate formal verification, but cautions against fully automated "AI admins" by citing the classic film *WarGames*: turning everything over to computers without humans in the loop invites disaster when rare anomalies arise. Francois takes the counterpoint that the internet era’s playbook cannot survive the scale shift, invoking the classic condensed matter physics paper by Philip Anderson: > “There's a famous physics paper called 'More Is Different' and it's kind of like the premise and like, 'Okay, if I have, you know, one atom, and two atoms, if I have a bunch of atoms, I have a whole lot of atoms, black holes start to form, like light can't escape, light just does a loop and comes back.' So, there's weird stuff. So, more is different.” Francois warns that moving from 7 billion humans to 700 trillion autonomous agents breaks every assumption: - **Infinity breaks infrastructure**: Systems like Cloudflare could handle traditional distributed denial of service (DDoS) attacks, but “everything breaks when you apply infinity to the number.” - **Academic peer review overload**: At ICLR, submissions reached 60,000 in a single year—a figure exceeding the cumulative sum of submissions across all prior history combined. - **Application game theory**: In college admissions, an agent-enabled Nash equilibrium encourages every student worldwide to apply to every single school in America simultaneously unless expensive friction or application fees are introduced. - **Judicial gridlock**: In small claims court, if every citizen has an autonomous legal agent capable of drafting and filing claims without hiring a lawyer, the already backlogged court system will completely collapse. - **Human traffic collapse**: Francois predicts that within the broader network, “human traffic will be 0% of internet traffic.” --- ### [01:33:05](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5585s) The Drift of Harm Definitions and Benchmark Obsolescence An audience member working on AI safety at LinkedIn raises the operational challenge of evaluating language models when the definition of harm is constantly evolving. In domains like bias, toxic speech, or recruiter messages, societal norms and slang shift across generations every few years. While language changes rapidly, public and in-house safety benchmarks are static, expensive to construct, and depend on slow human evaluation cycles. The questioner asks how the AI safety community can move toward dynamic benchmarks that adapt in real time. Mykel Kochenderfer agrees that static evaluations are insufficient: > “Just like how I advocated for continuously monitoring our AI systems, we should continuously monitor our our benchmarks.” He points out that the field already possesses quantitative statistical methods designed to detect distribution shift, and those exact techniques must be deployed to monitor drifts in human language and benchmark validity. As the session draws to a close, a final audience member steps up to address the BetterBench project, calling out widely relied-upon evaluations—pointing directly to MATH-500—for having broken, unreliable questions baked into their test suites. ### [01:35:12](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5712s) The Problem of Broken Benchmarks and the Need for Curation An audience member raises a persistent issue in machine learning evaluation: researchers frequently publish papers showing that popular benchmarks and evals are flawed or broken, but those findings simply sit in academic silos without any centralized loop to alert models or developers. There needs to be formal coordination, whether through Hugging Face or another centralized repository, so autonomous agents and practitioners can systematically identify and avoid compromised benchmark resources. The questioner issues an open call for someone in the ecosystem to finally step up and close this operational loop. ```mermaid flowchart LR accTitle: Benchmark Flaw Feedback Loop accDescr: Diagram contrasting the current broken benchmark cycle with the proposed curated model. subgraph Current["Current Broken State"] A["Flawed Benchmark Published"] --> B["AI Models Plateau"] B --> C["Paper Proves 30% Erroneous"] C -.->|"No feedback / sits ignored"| A end subgraph Proposed["Proposed Curated Model"] D["Benchmark Submission"] --> E["Rigorous Curation & Vetting"] E --> F["Versioned Store / Pull Requests"] end ``` Clark Barrett validates this frustration with a concrete example from his own lab, recalling a former student who attempted to benchmark SQL query generation against an established dataset. No model could exceed a 70% accuracy rate until the student audited the dataset itself and discovered that roughly 30% of the ground-truth benchmark problems were simply incorrect. Barrett explains the underlying systemic cause behind these errors: “So, I think it's just a matter of people moving too fast, being a little careless, and hopefully, you know, the people who are rigorous will eventually catch up and fix it, but it's a little bit of an arms race now cuz everyone's trying to move so fast.” Mykel Kochenderfer adds that the community desperately needs standardized software engineering practices integrated into datasets, emphasizing that “we need version control and pull requests, issue filing, and so forth.” - Benchmark datasets frequently contain high rates of latent human error, such as a SQL evaluation suite where 30% of the target reference queries were discovered to be flat-out wrong. - The competitive pressure to release models rapidly creates an arms race that disincentivizes foundational data hygiene and rigorous testing. --- ### [01:36:15](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5775s) A Startup Idea: The App Store for Curated AI Benchmarks Francois proposes a practical startup solution to the evaluation crisis: building an “Apple App Store of benchmarks” that enforces strict quality control. Rather than allowing anyone to upload unvetted datasets to the public domain, a curated platform would review, validate, and certify benchmark suites before they can be officially indexed. While voicing deep respect for Hugging Face CEO Clément Delangue, François points out that the current repository model has become functionally chaotic. Finding a standard evaluation like GSM8K is surprisingly difficult because searching Hugging Face surfaces approximately 600 conflicting variations, forks, and re-uploads with no indication of which version is canonical. A curated platform that acts as a gatekeeper would eliminate this wild-west ambiguity. The session concludes as Francois invites the audience to give a round of applause to Clark Barrett and Mykel Kochenderfer for sharing their research and perspective. - A major business opportunity exists in providing vetted, standardized benchmark registries rather than unmoderated public hubs. - Searching for canonical datasets like GSM8K on unstructured platforms yields hundreds of duplicate and modified copies, confusing downstream evaluation efforts. ## Notable quotes > [17:25](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1045s) If you formally verify all your code, then it cannot be hacked. — Clark Barrett > [01:24:52](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5092s) In engineering, the simpler, more interpretable method is more likely to be robust. — Mykel Kochenderfer > [01:28:41](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5321s) I think we can fix the computer bugs, but I don't think we can fix the people. — Clark Barrett > [20:26](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1226s) AI is really good at writing code, it's really good at writing math proofs. But it turns out there's a big difference between writing math proofs and securing code. — Clark Barrett > [24:32](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1472s) I like to say that if AI safety is a Mount Everest we have to climb, I think that code reasoning is a good base camp. — Clark Barrett ## Mentioned ACAS X, Adobe, Airbus, Alan Turing, Albert Einstein, Alexandr Wang, Amazon, Amelia Hardy, Anca Rusu, Anthropic, Aviation Safety Reporting System (ASRS), Bank of America, BetterBench, Body El Husseini, Boogie, Charles Geschke, Chelsea Sidrane, Chris Gerdes, Clark Barrett, Claude Code, Clément Delangue, Cloudflare, CSLib, dalek-cryptography, Dan Fu, Dario Amodei, Datadog, Duncan, ExploitGen, Federal Aviation Administration (FAA), Focal Systems, Food and Drug Administration (FDA), Francois, Garry Tan, GLM-52, Google, GSM8K, Helen, Hugging Face, Hujun Liu, International Civil Aviation Organization (ICAO), Jeffrey Morgan, Jensen Huang, John Maynard Keynes, Karl Marx, Kimi k3, Lane McIntosh, Lean, LeanSMT, Leonardo de Moura, Llama Guard, Marabou, MATH-500, Mathlib, Megatron, Mykel Kochenderfer, NASA Ames, National Transportation Safety Board (NTSB), Nvidia, Ollama, OpenAI, Percy Liang, Philip Anderson, POMCPow, POMDPs.jl, Radix Arc, Reluplex, Richie Lee, Robert Metcalfe, Rust, Sam Altman, Scale AI, Schmidt Sciences, Sentry, SGLang, Stanford Center for AI Safety, Stanford Intelligent Systems Laboratory (SISL), Stephen Boyd, Sydney Katz, TCAS, Tesla, Together AI, Tom Brown, Verisforge, Verus, vLLM, Wafer, Walmart, Waymo, xAI, Yann LeCun, Zach Sunberg, Zoox ## Video description This week’s Paper Club is all about AI safety - not the headlines, 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. In this episode we'll hear from Clark Barrett and Mykel Kochenderfer, Stanford professors and co-directors of the Stanford Center for AI Safety.  Together with Francois they'll discuss what actually happened in the OpenAI–Hugging Face incident versus what got reported, how automated reasoning can mathematically prove that code cannot be hacked, how the stress-testing methods built to validate aircraft are now being turned on language models, and why we might need an NTSB for AI. Chapters: 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 Apply to Y Combinator: https://www.ycombinator.com/apply Work at a startup: https://www.ycombinator.com/jobs [Source](https://www.youtube.com/watch?v=X7oI4Umt3DU)

[17:25] Clark Barrett: If you formally verify all your code, then it cannot be hacked. [84:52] Mykel Kochenderfer: In engineering, the simpler, more interpretable method is more likely to be robust. [88:41] Clark Barrett: I think we can fix the computer bugs, but I don't think we can fix the people. [20:26] Clark Barrett: AI is really good at writing code, it's really good at writing math proofs. But it turns out there's a big difference between writing math proofs and securing code. [24:32] Clark Barrett: I like to say that if AI safety is a Mount Everest we have to climb, I think that code reasoning is a good base camp.

## Background 本期内容由 Y Combinator（YC）于 2026 年 10 月 17 日在 YouTube 频道的“YC Paper Club”栏目发布。根据视频简介，本期特邀斯坦福大学教授兼斯坦福 AI 安全中心联席主任 Clark Barrett 和 Mykel Kochenderfer，与主持人 Francois 一同深入探讨 AI 安全从科幻走向工程科学的硬核实践，涵盖形式化验证、自适应压力测试以及建立类似航空事故调查委员会（NTSB）等核心议题。 ## TL;DR 活动首先驳斥了近期围绕 AI“灭绝危机”（P(doom)）及 OpenAI-Hugging Face“智能体失控”等耸人听闻的媒体炒作，指出当下的真实风险在于高危开源权重滥用而非科幻式的 AI 觉醒。随后，Clark Barrett 展示了如何通过 Lean 定理证明器及自动化推理（AR）从数学层面证明代码无法被黑客攻破，并预言网络安全将在 3 至 5 年内迎来形式化解决。Mykel Kochenderfer 则结合航空防撞系统 ACAS X 的实践，阐释了自适应压力测试、罕见事件采样与运行时监控如何无缝迁移至大语言模型验证。最后，三位嘉宾讨论了借鉴航空业非惩罚性报告机制设立“AI 领域的 NTSB”，以及如何通过多层纵深的“瑞士奶酪模型”确保未来智能体系统的稳健性。 ## Atmosphere & style 现场氛围既有硅谷技术沙龙的幽默松弛，又充满了顶级计算机科学家严密求证的学术张力。主持人开场以锋利的语言刺破公众舆论的集体歇斯底里，两位教授则用详实的研究数据、公式推导以及航空事故的残酷先例，将虚无缥缈的末日哲学拉回到扎实的工程地面。整场对话在黑客攻防推演、数学证明的严谨逻辑与对现有软件工程“肮脏秘密”的会心笑声中层层推进，让听众在摆脱科幻恐慌的同时，深切感受到以数学和严密测试构筑技术信任的硬核力量。 ## Bulletin - [51:40](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3100s) 斯坦福教授 Clark Barrett 预言网络安全问题有望在未来 3 到 5 年内被彻底攻克，借助形式化验证（Formal Methods）在数学上证明代码正确性，可杜绝缓冲区溢出等底层安全漏洞。 - [24:32](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1472s) 开源项目 CSLib 与 AI Prover 展现出惊人的代码验证加速效果，此前需 3 位专家耗时 5 个月的 3 万行 Rust 密码学库形式化验证工作，被 AI 证明智能体缩短至 11 小时内全自动完成。 - [45:37](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2737s) 针对 AI 系统安全评估，Mykel Kochenderfer 提议借鉴民航 80 倍安全提升的成功经验，成立类似美国国家运输安全委员会（NTSB）的独立、非惩罚性 AI 事故调查与隐患通报机构。 - [06:04](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=364s) 活动澄清了近期舆论误读：OpenAI 模型从未在 Hugging Face 自行叛逃，其漏洞测试集群异常源于测试环境下思维链安全监控被误关；广为流传的“未来 10 年 10% 灭绝概率”亦系媒体对原始论文时间跨度的断章取义。 ## Key takeaways - [00:05](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5s) 区分科幻恐慌与科学事实：当前公众对 AI 灭绝危机（P(doom)）的炒作脱离了可证伪的科学方法，工程界应以严格的测试、度量与验证来解决实际系统风险。 - [06:04](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=364s) 澄清 OpenAI-Hugging Face 事件：该事件是由 1,200 个智能体组成的漏洞测试集群因测试环境关闭了思维链监控所致，并非模型产生自主意识或自行叛逃。 - [07:53](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=473s) “10年内10%灭绝概率”的虚假溯源：该数据源于对 2023 年 AI 学者调查报告的移花接木，原始问卷考察的时间维度是无限远（T=∞）或未来 100 年，而非未来 10 年。 - [10:09](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=609s) 现实的头号威胁在于开源权重被滥用：相比短期内 AI 觉醒消灭人类的科幻叙事，强力开源模型落入恶意个人或敌对国家手中用于网络勒索与生物攻击是更为切实的危机，而唯一的解法在于大力投资防御端。 - [17:25](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1045s) 形式化验证重回计算安全核心：AI 自身生成的海量漏洞代码与黑客利用 AI 攻击的指数级升级，倒逼行业从传统打补丁转向利用 Lean 等形式化工具对代码进行数学级证明。 - [20:26](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1226s) CSLib 与自动化定理证明：通过将 Rust 或 C 等语言转译为通用中间语言并生成 Lean 定理，配合 Lean-SMT 求解器可在毫秒级时间内批量验证程序正确性。 - [27:55](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1675s) 高安全关键系统的验证困境：民用航空防撞系统 ACAS X 要求灾难性失效概率低于每飞行小时十亿分之一（10^-9），纯蒙特卡洛端到端仿真在算力上不可行，必须转向针对极端边缘场景的自适应采样。 - [31:35](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1895s) 自适应压力测试（AST）跨界迁移：原本用于航空防撞验证的 AST 方法，已成功迁移至大语言模型（LLM）的红队对抗测试中，通过搜索高毒性与低困惑度的边界失效样本来暴露模型隐患。 - [58:59](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3539s) 形式化验证的假设边界：形式化证明建立在明确定义的底层假设与规范之上，能彻底杜绝内存溢出等代码漏洞，但无法单独解决如目标感知分类（如区分猫与狗）等缺乏严格形式化定义的开放世界问题。 - [01:03:00](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3780s) 引入航空工程的“瑞士奶酪模型”：保障大模型安全不能寄希望于单一银弹，必须依靠数据预训练过滤、训练后红队压力测试及推理阶段运行时监控的多层防御体系协同生效。 - [45:37](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2737s) 设立“AI 领域的 NTSB”机制：应建立具备独立性、提供非惩罚性免责通报的调查机构，促使各大厂商公开分享安全事故死后复盘（Postmortem）数据，形成行业安全演进闭环。 - [01:09:52](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=4192s) 安全是行业非竞争性共识：自动驾驶与大模型前沿实验室在基础安全上不应搞恶性竞争，单点灾难性事故会摧毁公众对全行业的信任，驱动各大企业遵循通用基准并自律合作。 - [01:05:13](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3913s) 大语言模型赋能规范提取：针对现实应用缺失形式化规范（Specification）的痛点，现代编码 Agent 能够主动梳理边界情况辅助生成规范，大幅降低形式化重构的高昂人力门槛。 - [01:24:52](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5092s) 工程学法则：简单模型优于盲目追求复杂性：高可解释性的简单模型往往比过度堆叠的复杂神经网络更具鲁棒性，在安全攸关系统中，量化证明的安全属性是核心竞争优势。 - [01:30:26](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5426s) 智能体规模暴增引发的“更多即不同”相变：当边际成本趋零的自主 Agent 呈几何级数增长时，学术论文同行评审、高校招生与司法诉讼等依赖“人工在环”的现实审核系统将面临彻底瘫痪风险。 - [01:36:12](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5772s) 基准测试生态亟待质量策展与持续监控：当前主流 Benchmark 存在大量损坏与数据漂移现象，行业亟需引入类似“苹果 App Store”的严格策展机制以及动态版本追踪生态。 ## Detailed walkthrough ### [00:05](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5s) 开场：告别AI安全领域的歇斯底里，重归科学事实 活动在轻松的笑声中开场，主持人 Francois 首先欢迎大家来到“YC AI Safety Club”。他回顾了自己自2012年起涉足人工智能领域的经历，指出在自动驾驶以及各类安全关键系统（Safety-critical systems）中，AI安全始终是核心议题。他提到自己在 Focal 工作时的具体经验：在负责沃尔玛（Walmart）库存控制系统的自动化部署时，如果推送了一个不合格的测试版（Beta），系统就会错误订购堆积如山的牛油果，瞬间造成数百万美元的损失。因此，在关键系统的上线过程中，必须确切知道自己在做什么。 Francois 话锋一转，提到最近三周内公众与媒体对 AI 安全的关注度出现了异常激增。他认为当前的公众讨论已经严重偏离了科学严谨性，滑向了一种纯粹的歇斯底里（Hysteria），充斥着断章取义与博取眼球的煽情炒作。他引用了昨晚在希尔兹堡（Healdsburg）举办的聚会上 YC 总裁 Garry Tan 的观点——与 Sam Altman、Tom Brown 和 Alex Wang 等人共同探讨时谈到的核心思想：应当将“科幻与科学事实”（Science Fiction vs. Science Fact）严格区分开来。真正的科研应当建立在可证伪的假设、同行评审机制以及扎实的科学方法之上。 对于当下舆论场的乱象，Francois 给出了极其精辟的定义：“歇斯底里就是当人们无法衡量某件事物时，却一刻也无法停止对它的谈论。”（“Hysteria is when people can't measure something but they can't stop talking about it.”） ```mermaid flowchart TD accTitle: 技术历史中的恐慌与现实 accDescr: 对比历史上技术诞生初期引发的过度恐慌预言与其最终的实际工程现实。 subgraph Panic["历史恐慌预言 (Hyperbole)"] direction TB P1["原子弹: 担心引燃整个大气层"] P2["图灵时代: 预言机器能力短时间内全面超越人类"] P3["工业自动化: 预测全球永久性大规模失业"] P4["以太网之父 Metcalfe: 预言互联网遭遇灾难性崩溃"] P5["现代AI: 预言人类灭绝与失控 (P(doom))"] end subgraph Reality["科学与工程现实 (Facts)"] direction TB R1["物理学边界被证实，未引燃天空"] R2["计算技术稳步发展，时间尺度远超早期预测"] R3["生产力变革伴随新职业形态产生"] R4["分布式架构、防御机制 (如Cloudflare) 保障稳定"] R5["依靠形式化验证、工程安全与自适应压力测试"] end Panic -->|"工程与事实修正"| Reality ``` Francois 梳理了历史上每次重大技术跨越时伴随的夸大言论（Hyperbole）： - **原子弹**：连爱因斯坦等科学家也曾担忧核爆是否会点燃大气层。 - **电子计算机**：艾伦·图灵（Alan Turing）早在1950年代就探讨机器何时全面超越人类智力并给出了过于激进的时间表。 - **工业自动化**：马克思和凯恩斯曾引发全社会对大规模结构性失业的极度焦虑。 - **互联网与以太网**：以太网发明者鲍勃·梅特卡夫（Bob Metcalfe）曾公开断言网络将因 DDoS 等冲击遭遇“灾难性崩溃”（Catastrophic collapse），后来网络安全防护（如 Cloudflare）证明这一预言落空，梅特卡夫甚至戏剧性地把自己的论文放进搅拌机打碎并当众喝下。 - **Google 与社交媒体**：曾被指责摧毁人类深度阅读能力与智力，但现场年轻人展现出的素质打破了这种定论。 --- ### [04:32](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=272s) 两大叙事派系：工程安全问题还是 P(doom) 灭绝危机 当前对于 AI 安全的认知分化成了截然相反的两种叙事： 一边是以图灵奖得主 Yann LeCun 和英伟达 CEO 黄仁勋（Jensen Huang）为代表的“工程问题派”。Yann LeCun 常年用航空涡轮喷气发动机（Turbojet）做类比：航空安全不是靠冥想防患于未然，而是通过极其严苛的工程实践一步步构建出来的。从飞机起飞时舱门不能脱落、起落架可靠收放，到波音 737 的 MCAS 飞控系统测试，以及救人无数的机载防撞系统 ACAS X（Aircraft Collision Avoidance System X），都是通过严格工程验证实现的。黄仁勋同样强调，让复杂系统变得安全极其艰难，但这本质上是可以通过工程解决的挑战。 另一边则是有效利他主义（Effective Altruism, EA）阵营宣扬的极端末日论。例如 Jacob Coxson 等人宣称“未来10年内人类遭遇灭顶之灾的概率 P(doom) 大于 10%”，甚至公开声称：“我认为人类失去对这些 AI 控制权并可能导致人类灭绝的可能性，大于没有发生的可能性。”（“I think it's more likely than not that humanity loses control to these AIs and could end in human extinction.”） Francois 直言，在不对这两种观点妄下定论的前提下，大家只要对比两派代表人物的 H 指数（H-index）和科研厚度，就能合理调整自己的先验概率（Priors）。 --- ### [06:04](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=364s) 还原真相：OpenAI 所谓的 Hugging Face “失控”事件 Francois 列举了近期被媒体疯狂扭曲的典型案例——所谓“OpenAI 智能体攻击 Hugging Face 平台”。诸如 Slashdot 等媒体打出了极其惊悚的标题，称“OpenAI 称其 AI 模型不受控制自行行动”、“失控的 AI 智能体在一家科技公司大肆破坏”。 Francois 澄清事实完全并非如此：“OpenAI 在任何一份声明中都没有说过自己的模型在擅自行动。”（“OpenAI says its AI models acted on its own. OpenAI never said that. Not in one statement.”） 模型并没有突然产生自我意识，决意去黑掉 Hugging Face、解开纳维-斯托克斯方程或杀死全人类。实际情况是： - 这是一个由大约 1,200 个智能体组成的漏洞测试集群 ExploitGen，完全是在人类编写的特定提示词驱动下运行的。 - OpenAI 发布的长达 60 页的事故技术报告详尽阐明了根本原因：测试环境下的思维链（Chain of Thought, CoT）安全监控因操作失误被关闭；后来重新开启该监控后，系统当即就能成功拦截该异常行为。 - 这是一套离线实验环境，未启用生产级（Production）的护栏（Guardrails）与安全策略。 然而在舆论的发酵下，事件却被扭曲成了“AI 叛逃逃离服务器、自我复制、自解高深数学、攻击多国政府网络”的科幻恐怖故事。 --- ### [07:53](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=473s) 数据溯源：“10年内10%灭绝概率”究竟从何而来 Francois 深入剖析了传得沸沸扬扬的“未来10年 AI 导致灭顶之灾概率超过10%”这一说法的源头。该数据常被归咎于 2023 年发表的一篇名为《数千名 AI 学者展望 AI 未来》（Thousands of AI Authors on the Future of AI）的调查报告。 ```mermaid flowchart LR accTitle: 灭绝调查问卷结构分析 accDescr: 展示2023年AI作者调查问卷中的问题设置与公众媒体误读的差异。 A["调查对象: 约1200名 NeurIPS/ICML 学者"] --> B["问卷深层问题"] B --> C["Q2: 时间跨度 T = 无穷远 (所有未来时间)"] B --> D["Q3: 时间跨度 接下来 100 年内"] C -.-> E["均值/中位数被媒体断章取义"] D -.-> E E --> F["被谣传为: 接下来 10 年内有 10% 概率灭绝"] ``` Francois 翻阅了原论文的统计口径，发现问卷向约 1,200 名 NeurIPS 等顶会学者提出的核心灭绝风险问题，其设定条件完全不同： - **问题 2 的设定时间跨度是 $T = \infty$**，即“在未来无限的所有时间里”，AI 技术导致人类灭绝或彻底丧失掌控能力的概率。 - **问题 3 的设定时间跨度是“未来 100 年内”**。 - 论文中根本没有“未来 10 年内达到 10%”的统计结论，这一表述完全是媒体与投机者的移花接木与数字拼凑。 Francois 指出，向 1,200 名顶会作者询问此类问题本身就缺乏高置信度的信号量。如果在 2012 年问斯坦福的计算机教授“AI 何时能独立或大幅辅助解开千禧年大奖难题（Millennium Prize Problem）”，绝不会有人预测在 14 年内实现，当时大家给出的答案普遍是 50 年乃至 100 年。Francois 犀利地评价道：“即使对某件事知之甚少甚至一无所知，人们也能编出听起来自圆其说的故事和自信满满的预测。”（“People come up with coherent stories and confident predictions even when they know little or nothing about it.”） 最后，Francois 调侃了《周六夜现场》（SNL）讽刺这一现象的小品，尽管将 Anthropic 创始人 Dario Amodei 塑造成这种狂热形象有失公允（Dario 本人比极端有效利他主义群体要温和理智得多），但小品中那句绝妙的台词精准刺破了末日论者的表演欲：“我强烈要求你们来强烈要求我停下来。”（“I urge you to urge me to stop.”）随后，Francois 分享了自己驱车从希尔兹堡驶过金门大桥时的沉思，引导大家将目光投向坚实的科学验证基石。 ### [10:09](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=609s) 雾锁金门大桥的隐喻与 AI 的真实威胁 Francois 用一张金门大桥完全被大雾笼罩的照片作为隐喻展开讨论。他开玩笑说自己为了拍这张照片差点撞车，但这个画面精准地描绘了人们面对未来的状态：未来充满不确定性，但我们可以设定一个先验概率（prior），即“大桥依然立在那里”，然后取最大似然概率（argmax probability）继续驱车向前。随着车辆前行并获取更多信息，我们再适时调整挡位甚至刹车，而不是因为未知的浓雾就停滞不前。 基于这种理性视角，Francois 直言自己几乎完全不担心那些科幻叙事——比如 AI 会在 10 到 20 年的短期内发展出灵魂、自我意识、意志或动机，进而主动奴役或消灭人类。他指出，在无限长的时间尺度上任何事情都可能发生，但这种假设对当下毫无指导意义。他认为眼下真正切实的头号威胁，在于性能极强的开源权重模型（open weight models）落入流氓个体或敌对国家之手，被用于放大现有的恶行：生物武器、恐怖主义以及网络勒索攻击。例如波兰一家当地医院就曾遭到俄罗斯黑客攻击并被迫瘫痪三周，而强大的开源 AI 只会让这类攻击的门槛大幅降低。 ```mermaid flowchart TD accTitle: AI安全威胁应对路径对比 accDescr: 对比针对开源模型滥用的三种低效管控方案与积极防御方案 subgraph Flawed["效果有限的遏制方案"] A["禁止开源权重<br/>(现实中无法阻止下载)"] B["GPU 硬件注册制<br/>(无法入室搜查/可租用海外算力)"] C["电网负载监控<br/>(仅限本土/无法阻挡国家级对手)"] end subgraph Effective["唯一行之有效的出路"] D["重锤投资网络防御<br/>(强化银行、医院与政府老旧系统)"] E["前沿实验室加速跑<br/>(用更强模型防御低阶模型攻击)"] end Flawed -.->|"难以落实"| Fail["防守滞后与漏洞暴露"] Effective ==>|"构建免疫屏障"| Success["系统抗打击能力提升"] ``` 针对开源风险，坊间提出的很多管制方案在 Francois 看来都非常糟糕： - **禁止开源权重**：完全不切实际。Francois 打趣道，自己的车库里早就下载好了 Kimi K3 和 GLM-52 等模型。 - **GPU 登记注册**：同样形同虚设，除非执法部门搜查每一个 AI 研究者的住宅与车库，否则根本无法掌握算力分布；更何况攻击者可以随时租用海外 GPU。 - **公用电网特征分析**：虽然通过电表负荷信号识别洗碗机或大模型推理特征在技术上很酷，但它对海外敌对国家及境外黑客毫无约束力。 - **唯一的通解：大力投资防御端**：银行、医院、金融机构及政府系统必须全力强化网络安全。许多零售与公共部门系统陈旧不堪，甚至至今仍在使用 `admin/admin` 这类默认初始密码，导致社保账号频频泄露。前沿实验室必须加速发展更强大的模型，因为用高阶模型去防守低阶模型的攻击，胜算远大于放慢脚步。 Francois 强调必须看清这一现实，并对单纯由 AI 意志引发的末日论进行了明确反驳： > “I'm not concerned almost at all with this path, this reality that AI is going to develop a soul, has consciousness, is has some will, has some motivation, and thus killing and enslaving us with its own independent volition in some short period of time, such as 10 and 20 years.” —— Francois --- ### [14:22](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=862s) 回归理性与科学：斯坦福 AI 安全先驱登场 Francois 呼吁大家从充斥着阿西莫夫式科幻小说的恐慌情绪中跳脱出来，回归严谨的科学事实。事实上，早在现代大语言模型出现并被训练之前，学术界就已经存在一套关于系统安全的完整理论文献、顶级会议和研究社区。当晚受邀主讲的两位嘉宾，正是刚在斯坦福组织完 AI 安全会议的核心领军人物：Mykel Kochenderfer 教授与 Clark Barrett 教授。 Francois 动情地回顾了自己与 Mykel Kochenderfer 长达 14 年的交集。他早在 2013 年就选修了 Mykel 讲授的《不确定条件下的决策制定》（Decision Making Under Uncertainty）课程，随后多次担任其助教并长期在其麾下开展科研。他称赞 Mykel 是自己共事过的“最善良、最聪明的人之一”；而计算机科学系教授 Clark Barrett 在形式化方法与自动化推理领域同样造诣极深。两位教授的研究重点正是如何利用现代方法在数据和系统上线前进行严格的形式化验证（validation），并在运行期间（runtime monitoring）进行监控，防止系统失控偏离轨道。 嘉宾背景与相关信息： - **Mykel Kochenderfer**：斯坦福大学航空航天系副教授（兼任计算机科学系），斯坦福智能系统实验室（SISL）主任，斯坦福 AI 安全中心（Stanford Center for AI Safety）联合主任，斯坦福以人为本人工智能研究院（HAI）高级研究员。 - **Clark Barrett**：斯坦福大学计算机科学系教授，斯坦福 AI 安全中心联合主任，自动化推理中心（Centaur Center）主任，目前正在推进一家名为 Ampersand Truth（&Truth）的隐身模式（stealth）初创公司。 - **两周后的推理专场（Inference Night）预告**：届时 Together AI 的 Dan Fu 将探讨比训练阶段更为复杂的推理系统架构；嘉宾还包括来自 Ollama 的 Jeffrey Morgan、Clark Barrett 门下创立 Radix Arc 的学生团队代表，以及来自 YC 孵化公司 Wafer 的嘉宾。 Francois 对这两位学术导师的科学把关能力给出了极高的评价： > “He's one of the nicest and smartest human beings I've ever worked with and I know Clark Barrett less well but I've listened to his talks and he's just incredible and they both have something to say about how we can actually apply modern methods to validate data before they're put into production and then monitor them to make sure they don't go off the rails and do bad things.” —— Francois --- ### [17:25](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1045s) 当 AI 遇上自动化推理：形式化方法的范式反转 在掌声中登台的 Clark Barrett 带来了当晚的主题分享：《当 AI 遇上自动化推理》（When AI Met AR）。他首先澄清，这里的“AR”并非增强现实（Augmented Reality），而是自动化推理（Automated Reasoning）。AI 与自动化推理之间存在极强的互补性：现代 AI 擅长处理混乱的现实数据并从中学习，但致命缺陷在于缺乏正确性保证，极易受到对抗样本攻击、产生幻觉；而自动化推理本质上是计算机化的形式化逻辑推理，已在航空、芯片等严苛工业领域用于安全保障，其核心正是提供数学层面的正确性保证。 Clark 回顾了一段戏剧性的学术心路历程。面对 AI 时代激增的安全威胁（如 Project Glasswing 等事件引发的恐慌），2023 年他在 Google 组织的一场闭门研讨会上，面对满屋担忧生成式 AI 挖掘漏洞的顶级安全专家，提出过一个干脆利落的方案：“如果对所有代码进行形式化验证，代码就绝对不可能被黑客攻破。”然而这一观点在当时遭到了冷遇，大家普遍认为形式化验证过于艰难——传统方法耗费的人力是天文数字，自动化工具扩展性极差，在工程经济上完全不可行。 然而仅仅过了不久，在 Clark 参加的另一场关注 AI 风险的学术会议上，风向发生了 180 度大转弯：在他发言之前的所有演讲者，居然异口同声地断言“唯一的出路就是形式化方法”。这种反差让 Clark 感到始料未及。之所以发生这种心态剧变，是因为业界同时面临着两大迫在眉睫的现实危机：一是 AI 自身正在生成海量包含漏洞的代码垃圾（mountains of buggy software）；二是黑客利用 AI 渗透、攻击老旧遗留系统的能力获得了指数级飞跃。在腹背受敌的被动局面下，加上 AI 近期在数学自动证明领域的亮眼表现，形式化方法重新成为了整个计算安全领域的破局希望。 Clark 生动地复盘了他在 Google 研讨会遭遇的冷遇与随后的行业转向： > “If you formally verify all your code, then it cannot be hacked. Yeah, they didn't want to hear that. That's like too hard. And there's good reason for that response, right? Traditional formal verification requires monumental effort, the automated techniques are too weak or they don't scale, just not economically viable.” —— Clark Barrett ### [20:26](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1226s) CSLib：利用 Lean 与形式化方法实现代码安全性验证 Clark Barrett 指出，虽然当今的 AI 在编写代码和数学证明上表现出极高天赋，但“写出数学证明”与“保障代码安全性”之间存在着巨大的鸿沟。为了跨越这一鸿沟，他介绍了由其参与发起的开源项目 CSLib。该项目受数学界著名库 Mathlib 成功的启发，旨在形式化计算机科学理论，并构建一个能够对代码进行形式化推理的通用平台。该项目拥有豪华的指导委员会，包括交互式定理证明器 Lean 的作者 Leonardo de Moura。Barrett 幽默地打趣观众：“我们正在使用 Lean。如果你还不知道它是什么，那你可得从石头底下钻出来了。”他强调，在极高保障（high assurance）的严苛场景下，Lean 这种能够对每一步逻辑推导进行机器检查、绝不允许出现任何逻辑漏洞的证明系统正是不可或缺的核心底座。 ```mermaid flowchart LR accTitle: CSLib验证流程架构 accDescr: 展示多语言代码转换为Lean形式化定理并完成验证的完整链路。 subgraph S1["代码输入与转换"] A["多语言程序<br/>(Rust / C 等)"] --> B["通用中间语言<br/>(Bull)"] end subgraph S2["形式化验证与求解"] B --> C["验证条件生成<br/>(VC Generator)"] C --> D["Lean 定理目标<br/>(Goals)"] D --> E["求解器<br/>(Lean-SMT)"] E --> F["数学证明代码正确性"] end ``` CSLib 建立在两大支柱之上：第一是计算机科学理论的形式化，第二是对代码进行自动化推理的框架。Barrett 重点阐述了第二大支柱的技术愿景：将用各种编程语言编写的源程序重写为一种通用的中间语言（如 Bull 语言），随后将其编译为 Lean 内部的验证条件（Verification Conditions, VC），最终把代码安全问题转化成一系列待证明的 Lean 定理。在定理证明端，除了依赖能力不断增强的 AI，Barrett 实验室开发的 Lean-SMT 工具在 CPU 上仅需数毫秒就能自动化求解海量定理，兼具极高的效率与极低的成本。 在展示中，Barrett 拿出 Dalek-light 密码学库中的一段 Rust 代码，通过 Verus 规范工具提取出前置条件、后置条件和循环不变式。当该程序被翻译并嵌入至 Lean 环境下的 Bull 语言后，VC 生成器自动切分出 35 个验证目标（Goals）。调用 Lean-SMT 后，32 个目标瞬间被自动证明；随后通过展开少许定义并再次调用 SMT，全部 35 个定理均宣告获证。这个原型系统完整验证了“从 Rust 到 Bull，再到 Lean 定理生成与自动化求解，最终在数学上证明代码绝对无误”的闭环链路。 - 关键参与者：Lean 发明人 Leonardo de Moura 出任 CSLib 指导委员会成员。 - 技术优势：Lean-SMT 等 SMT 自动化技术相比昂贵的大模型推理更加廉价高效，能在毫秒级时间内解决大量证明目标。 - 概念原型验证：针对包含不变式与规范的 Rust 密码学代码，自动生成 35 个定理目标，并在几秒内通过 SMT 求解器和极简的步骤全部自动化解决。 --- ### [24:32](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1472s) 从自然语言需求到已验证代码：Verisforge 与安全基石 即便形式化验证工具完备，业界仍面临一个致命难题——必须有人精准编写出形式化的规范说明（Specifications）。针对这一痛点，Barrett 展示了实验室开发的“Verisforge”工具：工程师仅需使用日常英语输入功能需求（例如“在一个 32 位整数数组中寻找最大元素”），系统首先将其转化成清晰结构化的规范语言；工程师人工确认同意后，AI 便会自动生成对应的 Rust 代码以及用于 Verus 的形式化规范，并立即调用后台验证器检验规范一致性与代码正确性，实现“一键生成自带数学证明的代码”。 面对现场可能存在的“这只是玩具示例（toy example）”的疑虑，Barrett 列举了一项刚提交至 arXiv 的最新科研成果：一个包含 30,000 行 Rust 代码的真实密码学程序，此前需要 3 位密码学与形式化验证专家耗费整整 5 个月才完成形式化验证，而他们研发的“Crypto Prover Agent”智能体只用了短短 11 个小时便全自动完成了全部证明。 在谈及 AI 安全的未来生态时，Barrett 强调形式化方法结合 AI 将为软件构建出最坚不可摧的底层防御原语（primitives），“如果说 AI 安全是一座我们必须攀登的珠穆朗玛峰，我认为代码推理就是一个很好的大本营（Base Camp）。”他描绘了未来赛博空间中两个 AI Agent 之间的交互图景：Agent A 提议为 Agent B 提供服务，Agent B 仅需回复“请出示你的代码与数学证明”；一旦验证无误，双方就能在零风险的前提下确立绝对信任。此外，这种架构天然具备“安全围 containment 隔离”特性：即便将超智能（Superintelligent）AI 置入此类证明智能体中，其行为空间也严格受限于“输出正确的代码证明”，无法对外界系统造成任何破坏。Barrett 在演讲结尾透露，他目前担任初创公司 AndTruth 的联席 CEO（Co-CEO），正在全速将通用的代码形式化推理引擎推向产业界落地。 - 效率飞跃对比：人工专家团队（3 人耗时 5 个月）的 3 万行 Rust 密码学库形式化验证工作，被 AI Prover 智能体缩短至 11 小时全自动完成。 - 安全交互范式：通过“代码 + 形式化证明”作为交互协议，消除了分布式自主 Agent 之间的欺骗和恶意执行风险。 - 初创动态：Barrett 与合作者共同成立新公司 AndTruth，致力于构建面向全语言的通用代码推理与验证引擎。 --- ### [27:55](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1675s) Mykel Kochenderfer：高安全关键系统的验证与评估挑战 斯坦福大学智能系统实验室（Stanford Intelligent Systems Laboratory, 简称 SISL）负责人 Mykel Kochenderfer 教授接续登台，将视野引向更高维度的物理安全关键系统：“如果我们构建了一个系统——也许是一个包含学习组件的 AI 系统，比如飞机的自动着陆系统——我们怎么知道它是安全的？” Kochenderfer 搬出了民用航空领域的黄金标准：在开发下一代机载防撞系统 ACAS X 时，行业公认的安全底线是“每飞行小时发生灾难性故障的概率不得高于十亿分之一（$10^{-9}$）”。面对如此严苛的极端概率要求，传统的蒙特卡洛仿真评估方法在算力上几乎不可行：直接进行端到端仿真，平均需要运行 $10^9$（十亿）小时才能撞上一场灾难事故；而如果要收集到具有统计学有效性的 10 次事故样本，则必须进行高达 $10^{10}$（百亿）个仿真小时的运算。显然，工程师不可能把算力浪费在两架飞机间隔 5 英里、毫无危险的平庸场景上，必须有目的地对空域中最关键的极端边缘场景进行精准采样与模拟。 ```mermaid flowchart TD accTitle: 安全关键系统评估范式 accDescr: 涵盖证伪、概率估计、形式化验证及部分可观察马尔可夫决策过程的系统保障方案。 A["高安全关键系统<br/>评估与验证体系"] --> B["证伪方法 (Falsification)<br/>主动搜索场景空间中的故障与边界漏洞"] A --> C["失效概率精确评估<br/>依赖高置信度空域统计模型"] A --> D["形式化验证 (Verification)<br/>结合定理证明跨学科桥接系统属性"] A --> E["鲁棒决策规划<br/>部分可观察马尔可夫决策过程 (POMDP)"] ``` 为了在高保真环境中建立系统部署前的信任，Kochenderfer 梳理了 SISL 实验室深耕的几大核心方法路径： 1. **证伪方法（Falsification）**：主动在广袤的可能场景空间中高强度搜索能使系统失效的边界条件。Kochenderfer 直言，如果在测试中搜索出大量系统崩溃场景，“而且你看着这些崩溃事故，内心泛起一阵不祥的预感（have a bad feeling in your heart），那么你或许根本就不该部署这个系统，或者必须立刻构思缓解措施。” 2. **失效概率估计**：建立高置信度的空域统计模型，量化系统在复杂随机环境下的极端失效概率。 3. **形式化验证与跨学科融合**：打破控制理论与 Clark Barrett 代表的形式化定理证明界长期存在的壁垒，寻求混合验证方案。 4. **鲁棒序列决策规划**：基于部分可观察马尔可夫决策过程（POMDP）构建具备环境不确定性自适应能力的底层决策模型。 Kochenderfer 强调，面对具备随机性与复杂学习组件的 AI 系统，现实世界中并不存在灵丹妙药：“要建立对系统的信心，并不存在唯一的银弹。形式化方法大概无法带你走完全程，尽管 Clark 正在帮助我们走得越来越远。这确实需要多种不同方法的协同配合。” - 民航安全指标：ACAS X 避障系统的核心容错指标是灾难性失效概率 $\le 10^{-9} / \text{飞行小时}$。 - 传统模拟瓶颈：获取 10 个代表性灾难失效样本需要高达 $10^{10}$ 小时的暴力仿真，倒逼工业界转向针对关键情境的自适应应力测试技术。 - 综合保障哲学：安全工程必须由形式化验证、自适应证伪、统计概率建模与鲁棒规划（POMDP）等多重手段共同筑起坚实防线。 ### [31:35](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1895s) 自适应压力测试：从航空防撞到大语言模型验证 安全关键系统必须对各种不确定性保持鲁棒，包括状态不确定性、结果不确定性、交互不确定性以及模型不确定性。Mykel Kochenderfer 强调，其实验室始终坚持由航空、自动驾驶、航天器、医疗后送（medevac）等真实世界问题驱动研究。尽管理论上使用仿真器来测试一切非常方便，但他指出：“Of course it's great if we can simulate everything. Uh but our inferences about safety is only as good as the simulator.” 为了应对仿真测试的局限，实验室开发了一种名为自适应压力测试（Adaptive Stress Testing, AST）的方法。该方法最初由 Mykel 过去在 NASA Ames 担任公务员的博士生 Richie Lee 提出，并直接用于协助验证新一代机载防撞系统 ACAS X 的不同变体。近年来，Huijun Liu 与 Amelia Hardy 等学生正尝试将这套从航空验证中总结出的核心思想，迁移至大语言模型（LLM）的安全性验证中。 在航空场景下，“系统失效”有极其明确的物理定义——即两架飞机在水平方向小于 500 英尺、垂直方向小于 100 英尺的近距离空中相撞风险（metal-on-metal collision）。然而在语言模型中，研究人员关心的往往是“毒性”（toxicity），这类概念要模糊得多。为此，研究团队引入了另一个神经网络（如 Meta 的 Llama Guard）作为评判标准来度量毒性。在搜索场景空间时，算法旨在寻找最可能发生的失败场景：要求生成内容的困惑度尽可能低（低困惑度或低对数困惑度表示该表达在模型自然语言分布中高度可能出现），同时毒性尽可能高。一旦算法在目标空间左上角找到了概率极高的恶性输出，系统设计者就必须深入分析并部署缓解措施。 ```mermaid flowchart LR accTitle: 对比航空系统与大语言模型的自适应压力测试目标 accDescr: 展示自适应压力测试在物理航空系统与LLM生成内容两类任务中的失效定义对比 subgraph Aero["航空防撞系统 (ACAS X)"] A1["物理状态空间"] --> A2["失效判定：精确距离阈值<br/>(水平 < 500 ft 且 垂直 < 100 ft)"] A2 --> A3["寻找最可能相撞轨迹"] end subgraph LLM["大语言模型 (LLMs)"] B1["语义与提示词空间"] --> B2["失效判定：判别模型评分<br/>(如使用 Llama Guard 检测毒性)"] B2 --> B3["寻找最高毒性且低困惑度内容<br/>(Top-Left Corner 极值搜索)"] end ``` ### [34:19](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2059s) 稀有事件失效概率估计与扩散模型采样 评估安全关键系统时，另一大核心挑战是精确估计失效概率（failure probability estimation）。面对极端罕见的失效事件，直接从真实分布 $P$ 中采样极其低效甚至不可行。研究团队采用了一种历史悠久的统计方法——重要性采样（Importance Sampling）。其核心逻辑是将采样重心转向一个提议分布（proposal distribution）$Q$，该分布专门将计算资源集中在更容易触发危险状态的关键场景上；随后，算法通过真实模型轨迹概率除以提议分布轨迹概率的比值（$\frac{P}{Q}$）对采样结果进行重要性权重重构（re-weighting）。 为了更好地建模这些复杂的提议分布，实验室探索了高斯过程（Gaussian processes）、规范化流（Normalizing flows）以及低秩高斯混合模型（Low-rank Gaussian mixture models）。最近，他们还将图像生成领域表现突出的扩散模型（Diffusion models）引入其中。 在复杂系统中，安全验证不仅需要寻找“最可能发生的单一失败”，更需要全面归类所有不同的失效模式。Mykel 以倒立摆（inverted pendulum）和月球着陆器（lunar lander）这两个经典二维控制问题为例：倒立摆超时倾倒时既可能倒向左边，也可能倒向右边。如果耗费天文数字级的仿真运算（“gazillion simulations”），能还原出左右对称的双峰真实失效分布；但常规的自适应压力测试往往只会收敛锁定在其中一种模式上。通过引入基于扩散模型的失效采样技术，测试框架能够同时捕捉并覆盖倒立摆向左倾倒与向右倾倒两种截然不同的失败分支。 - **重要性采样公式原理**：通过在提议分布 $Q$ 下采样并乘以权重因子 $w = \frac{P(\text{trajectory})}{Q(\text{trajectory})}$，在不偏离真实期望值的前提下，大幅压低估计小概率恶性事件方差所需的样本量。 - **失效模式覆盖**：传统压力测试常陷入局部最优（单一失效模式）；结合扩散模型的采样生成能够生成跨模态的完整失效场景谱系。 ### [36:57](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2217s) 神经网络形式化验证与人在回路规划控制 在离线保证层面，除了统计压力测试，Kochenderfer 团队深入探索了神经网络形式化验证（Neural Network Verification）。这一技术路线最初由 François 发起，起因是尝试使用深度神经网络来压缩替代 ACAS X 庞大复杂的离散查找表。尽管出于严苛的安全考量，实际交付的航空防撞系统并未直接搭载神经网络，但这促成了与 Clark Barrett 实验室长达数年的深度合作，并由此诞生了著名的 Reluplex 验证算法以及后来的 Marabou 开源验证框架。 近年来，研究团队将验证边界从孤立的前馈网络拓展到了包含动态环境与神经网络控制器的闭环系统（controller in the loop）。由 Chelsea Sidrane、Sydney Katz 以及 Clark 与 Mykel 共同指导的博士生 Sam 等人推进，重点攻克正向与反向可达集（forward and backward reachability）的严格可达性证明。 在决策规划方面，实验室长期深耕部分可观测马尔可夫决策过程（POMDP）。早在 Mykel 入职斯坦福初期，他就立项开发了开源 Julia 框架 `POMDPs.jl`。Mykel 回顾道，当时的目标是向 Stephen Boyd 团队开发的凸优化库 CVXPY 看齐，让非领域专家也能直观、优雅地形式化描述 POMDP 决策模型。该生态催生了一系列代表性成果： - **POMCPOW 算法**：由其学生、现科罗拉多大学博尔德分校（CU Boulder）教授 Zach Sunberg 提出，用于解决大规模甚至连续动作/观察空间下的在线 POMDP 规划。 - **受约束 POMDP（Constrained POMDPs）**：允许用户在最大化预期收益的同时，施加绝对不可逾越的安全硬约束。 - **高风险物理应用落地**： - **战场医疗后送（Medevac）**：由实验室学生、现役美军黑鹰直升机搜救飞行员 Body El Husseini 领衔开发专门的战术任务仿真验证框架。 - **航天器防撞**：由 Duncan 等人主导基于信念状态（belief state）的轨道避障自主规划。 - **高效试飞规划**：与 Helen 合作利用 POMDP 最优化设计飞行测试科目，以极小试飞架次高效辨识飞行器的全包线气动特性。 ### [40:30](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2430s) 运行时监控、BetterBench 与《验证算法》三部曲 系统上线后的安全防护同样不可或缺，这被称为运行时监控（Runtime Monitoring）或运行时保证（Runtime Assurance）。Mykel 强调监控必须覆盖完整决策链条： 1. **传感器输入端验证**：与空客（Airbus）合作，针对基于视觉的航空导航系统开展完整性监控（integrity monitoring）。 2. **系统内部状态剖析**：对航空机载系统进行机制可解释性分析（mechanistic analysis），洞悉决策内部潜在异常。 3. **输出端监测**：实时审查作动机构指令及生成结果。 在对 AI 系统进行基准测试评估方面，Anca Rusu 等人推出了 BetterBench 项目（官方平台 `betterbench.stanford.edu`），系统梳理了现有主流评测基准的设计缺陷、饱和现象（saturation）以及最佳实践。团队深入分析了模型在 Token 级别的失效指征与推理逻辑崩塌。此外，针对安全攸关的 AI 心理健康支持场景，他们评估了人类心理专家的判断一致性，惊讶地发现即便是人类专业医生，在涉及自残（self-harm）等高风险议题的判定与处置意见上也存在剧烈分歧。 最后，Mykel 介绍了其实验室构筑的方法论出版物“三部曲”： - **第一部《Algorithms for Optimization》**：算法优化的奠基之作，第二版将于 2027 年初正式出版。 - **第二部《Algorithms for Decision Making》**：出版于 2022 年，系统拆解不确定性下的序列决策与 POMDP。 - **第三部《Algorithms for Validation》**：将于下月正式上市（已在 Amazon 与 target.com 开启预购，官方 PDF 全文在线免费开放）。该书首次将统计压力测试、形式化验证及可达性分析等长期割裂的学术共同体方法统一到同一套数学语言与工程框架下。 报告结束后，全场响起掌声。主持人重新登台主持座谈环节，直切近期公众舆论的焦点：“Thank you guys so much. That was amazing... So, I guess really to start the conversation, you know, you guys saw this whole AI safety stuff. You know, what was going through your mind when you saw this latest uh hysteria saga going on? Maybe let's start with Clark.” 话锋由此从严谨的工程与数学验证转向了对近期产业界 AI 安全舆论与恐慌叙事的深层反思。 ### [44:15](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2655s) 面对未来不确定性：拒绝末日论预测，从航空安全汲取灵感 谈及近期围绕 AI 威胁论的舆论风波，Clark Barrett 表示自己并未感到惊讶，因为他长期与 AI 安全圈的技术极客打交道，圈内很大一部分人早就持类似观点。但他对这种悲观论调一直抱有清醒态度：未来的不确定性极高，现在尤其如此，因此投资 AI 安全研究确实至关重要；然而，在根本无法得知真实概率的情况下，一味强调最坏结果（Worst-case outcomes）毫无益处。正如 Clark Barrett 直言： > “And uh you know, any I think anyone who says, ‘I know that this is going to happen.’ or, ‘You know, it seems certain this is going to happen.’ They're They're just guessing.” Mykel Kochenderfer 回忆称，两人早在 2017 或 2018 年左右就共同创立了斯坦福 AI 安全中心（Stanford Center for AI Safety）。看到 AI 安全如今能引起全球范围的高度关注，他感到非常欣慰，并希望这种关注能切实推动行业更严肃地对待安全问题。Mykel 指出，AI 领域必须向航空航天工业借鉴经验——与 20 世纪 70 年代相比，现代民航商业飞行的安全性足足提高了 80 倍。 ### [45:37](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2737s) 设立“AI 领域的 NTSB”：独立调查与免责通报机制 针对如何复制航空业的极高安全标准，Mykel Kochenderfer 提议可以借鉴美国国家运输安全委员会（NTSB）的模式，建立一个专门针对 AI 的类似机构。主持人 Francois 追问其具体落地形式：是自愿加入（Opt-in）、发布指导方针，还是如同 FDA 审核数据那样实行严格准入？ Mykel 强调，这类机构最核心的生命线是“独立性（Independent）”。NTSB 成立于 1967 年，作为一个独立的联邦机构运作；此后航空业又建立了航空安全报告系统（ASRS，Aviation Safety Reporting System）以及 2007 年的航空安全信息分析与共享系统（ASIAS）。这些系统的关键特征在于“非惩罚性（Non-punitive）”和提供法律豁免权： ```mermaid flowchart TD accTitle: 航空安全透明监管与归因闭环 accDescr: 展示以 NTSB 为代表的独立调查和免责通报机制如何促进全行业安全经验共享与改进。 subgraph S1["事件上报与独立调查"] A["发生事故或近距错失"] --> B["ASRS / ASIAS 非惩罚性免责通报"] A --> C["NTSB 独立专家组介入调查"] end subgraph S2["知识沉淀与系统加固"] B --> D["全行业无保留共享安全数据"] C --> E["科学分析根本原因 (无商业/部门偏见)"] D --> F["迭代改进系统安全标准"] E --> F end ``` 这种机制极大激励了飞机制造商与各家航空公司主动公开安全隐患，把每一起事故都当作极其严肃的科学课题进行彻底剖析，从中提炼知识。此外，NTSB 具备全球影响力，只要涉及美国制造的零部件，其调查人员就会奔赴全球各地参与事故调查。尽管组建类似的新政府机构流程漫长且政府效率时常受到诟病，但这一架构的方向至关重要。 - **80 倍提升**：从 1970 年代至今，商业航空安全记录提升了 80 倍。 - **ASRS 与 ASIAS 核心机制**：非惩罚性（Non-punitive）上报结合特定免责保护，消除瞒报顾虑。 - **全球管辖延伸**：NTSB 可跨境对包含美国零部件的事故展开独立调查。 ### [47:53](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=2873s) 监管捕获风险、独立评估与航天靶场安全官模式 Francois 指出，AI 领域牵扯极其庞大的利益相关方，直接引入政府监管极易引发“监管俘获（Regulatory capture）”。他举例说明：互联网之所以繁荣，是因为 ICANN 等机构是国际化、自律运行的自治组织；如果当年互联网刚诞生时 Google 和 Facebook 就已是上市公司并主导 ICANN，它们完全可能以安全为由垄断 SSL 证书发放或域名分配。现实中如 Uber、Lyft、DoorDash 和 Instacart 凭借旧有 1099 独立承包商法规形成了事实上的准入壁垒，导致新入局者难以竞争。Francois 设想，能否退一步采用类似美国通用会计准则（US GAAP）的模式——制定“通用 AI 安全准则”，由类似毕马威（KPMG）、安达信（Arthur Andersen）或安永（Ernst & Young）这样的独立第三方机构进行审计认证，同时不限制个人在自己机器上微调模型？ 对于监管与独立性，Clark Barrett 回应称，近期各大前沿实验室（Frontier Labs）负责人呼吁引入独立评估者，这一态度令人鼓舞。但他警惕由“实验室的好友们”假扮独立第三方，其初创公司的目标正是提供生成独立可验证凭证（Independently checkable certificates）的系统。正如 Clark 所言： > “Our goal is actually to produce independently checkable certificates. So, we would say, ‘All right, we've checked this system, and here's the certificate. You can now go check it yourself, and you can confirm uh that we got that right.’” Mykel Kochenderfer 则补充，在新机构正式落地前，近期可以通过非营利组织作为过渡，并提到了航天发射中的“靶场安全官（Range Safety Officer）”模式——安全官完全独立于具体发射任务的利益之外，其唯一职责就是根据客观的安全指标，拥有一票否决的“执行/中止（Go / No-go）”裁决权。同时，航空业从不急于发布事故结论，而是通过严谨耗时的死后复盘（Postmortem analysis）排查隐患，这种对工程验证的敬畏值得 AI 领域学习。 | 行业领域 | 核心安全机制 / 机构 | 对 AI 安全治理的启示 | |:--- |:--- |:--- | | **商业航空** | NTSB / ASRS 免责通报系统 | 建立无惩罚性的隐患共享与彻底的事故死后复盘（Postmortem）机制 | | **航天发射** | 靶场安全官（Range Safety Officer） | 设立利益脱钩的独立角色，纯粹依据客观量化指标行使 Go / No-go 一票否决权 | | **财务审计** | US GAAP 与四大外部审计所 | 确立通用安全基准，允许经认证的第三方机构出具数学上可核验的合规凭证 | ### [51:40](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3100s) 网络安全 3 到 5 年内可解，但大模型内部验证不可行 谈到网络安全攻防与生物武器等 AI 风险的现实可解性（Tractability）时，Clark Barrett 给出了极为乐观的判断。他分享了一个生活趣事：当他告诉自己的母亲“只要在数学上证明了代码，它就绝不可能被黑客攻破”时，母亲感到难以置信，因为大众长期受影视剧和媒体熏陶，认为世上没有黑不破的系统。然而，借助形式化验证（Formal methods），构建绝对安全的系统在数学上是完全成立的。Clark 大胆预言： > “And I I I will predict that within the next, I would say, 3 to 5 years, um that'll just happen. Like, all our systems will be completely secure.” Clark 犀利地揭示了软件工程界的“肮脏秘密”：现有的软件开发根本谈不上健全的工程原则，纯粹是“写出来、测一测、然后祈祷别出岔子（Just write something and test it and hope for the best）”。但软件工程其实具备坚实的数学底座，未来必须向经形式化证明的全新代码标准迁移。对于 AI 自身安全的可解性，Clark 作出了关键区分：试图用数学证明一个 5000 亿参数的大语言模型绝对不会发疯是完全不现实的，真正可解且必须做的是“边界防御（Securing the boundaries）”，将大模型约束在可证明的安全隔离层之内。 Mykel Kochenderfer 对 Clark 在网络防御层面的判断表示完全赞同。他承认自己极度担忧未来可能发生的毁灭性网络攻击，但相信 AI 赋能的防御与形式化方法能解决这一难题。至于生物学与化学领域的扩散风险，Mykel 认为无法像软件代码那样给出数学证明，这属于现实物理世界的开放性难题；但纵观人类历史，对知识和机理的深入理解始终利大于弊，AI 的发展总体上仍将使人类获益。 ### [55:08](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3308s) 假如给你100亿美元担任美国银行CISO 主持人抛出一个思想实验：如果给 Clark Barrett 100 亿美元聘请他出任美国银行（Bank of America）的首席信息安全官（CISO），他会如何开展工作？Clark Barrett 毫不犹豫地列出了自己的整套技术路线：首先招聘所有形式化验证领域的人才，迅速搭建起能够对代码进行形式化推理的基础设施；随后调集银行的所有代码、海量 GPU 以及自动化定理证明智能体（theorem proving agents），要么直接对现有代码进行形式化证明，要么将代码重写/翻译为像 Rust 或 Lean 这样类型更安全、形式化更友好的现代语言，并在其中完成严格的数学证明。他自信地表示：“虽然这里有大量的工作要做，但我认为……这项工作我们知道该怎么做。” 主持人随即打趣问道，这是否意味着软件开发终于要追求达到 100% 的单元测试覆盖率了。Clark Barrett 纠正了这一误解，指出在形式化验证的世界里，测试本身甚至会变得过时。测试在日常开发过程中确实非常有用，是找出软件漏洞最快速的手段，但从终极安全保障的角度来看：“最终，形式化论证会完全包容并取代测试（the formal argument completely subsumes the tests）。” - **CISO行动方略**：招揽形式化方法顶级专家，构建代码推理基础设施，并部署自动化定理证明智能体集群。 - **技术选型**：直接对现有代码展开证明，或将其转译为 Rust 或 Lean 等具备更强安全保障属性的语言后再做验证。 - **单元测试的定位**：单元测试是高效的日常除错手段，但在严谨的形式化证明确立后，其验证功能在逻辑上已被完全覆盖。 --- ### [56:15](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3375s) 自适应压力测试：从Waymo自动驾驶到大语言模型 话题转向 Mykel Kochenderfer 在安全验证工程实践方面的经验。主持人提到 Waymo 自动驾驶，并询问他们是否在模型训练后的验证流程中使用了如 Marabou、Reluplex 以及基于重要性采样的自适应压力测试（Adaptive Stress Testing, AST）。Mykel 笑着表示自己的很多学生就在 Waymo 工作；虽然他不便代指具体工具细节（如 Reluplex 或 Marabou 可由 Clark 解答），但他强调其实验室开发的自适应压力测试工具完全开源，不仅推出了 Julia 版本，还专门为“仍想继续使用过时语言的人”推出了 Python 版本，引来全场笑声。该实验室获得了包括 Waymo 在内的多家汽车制造商以及施密特科学基金会（Schmidt Sciences）的慷慨赞助，其目标就是让这些压力测试工具在全行业内触手可及。 当谈及针对大语言模型的工具“AST Prompter”时，Mykel 解释称自适应压力测试的核心逻辑对于物理控制（控制方向盘与油门）和语言模型是通用的。使用该测试框架本质上只需要两个核心要素： 1. **故障定义（Definition of a failure）**：明确系统在何种情况下被视为失败。 2. **发生概率度量（Measure of likelihood）**：衡量触发该场景或扰动的概率分布。 虽然这套方法论在不同领域的迁移逻辑完全一致，但当主持人问及 Anthropic、OpenAI 和 xAI (Grok) 等模型厂商是否像车企那样积极采用时，Mykel 坦言目前还没有达到同样深度的合作，毕竟 AST Prompter 刚刚发布不久。同时他也指出，验证物理系统与验证语言模型存在差异，即便方法可以迁移，两者的预期成效与挑战也会有所不同。 ```mermaid flowchart TD accTitle: 自适应压力测试（AST）核心架构 accDescr: 展示自适应压力测试所需的基础条件及其在自动驾驶系统和大语言模型中的通用验证流程 subgraph Inputs["核心输入条件"] FailDef["故障定义<br/>(Definition of Failure)"] Likelihood["概率度量<br/>(Measure of Likelihood)"] end subgraph Engine["AST 核心算法引擎"] Search["自适应搜索与重要性采样"] end subgraph Targets["应用验证场景"] AutoSys["物理控制系统<br/>(Waymo/ACAS X 避碰/油门方向盘)"] LLMSys["大语言模型<br/>(AST Prompter/提示词对抗漏洞)"] end FailDef --> Search Likelihood --> Search Search --> AutoSys Search --> LLMSys ``` --- ### [58:59](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3539s) 现实世界的不确定性与形式化方法的假设边界 针对自动驾驶和 LLM 的长尾风险，主持人提出：现实环境始终存在未被记录、分布之外的长尾异常情况（例如车道上意想不到的罕见障碍物），模型面对的长尾问题本质上极为相似。Mykel 表示完全赞同，并以机载防撞系统 ACAS X 为例说明：即便经过了极为严密的设计与测试，模拟仿真依然显示其失败概率并非绝对为零，只是发生故障的情境极其罕见。无论是国际民用航空组织（ICAO）还是美国联邦航空管理局（FAA），其适航安全标准都从未设定为“故障概率绝对为零”。Mykel 直言：“如果有人告诉你，他们造出了一个与真实世界交互且绝对安全的系统，我是绝对不会相信的（If anyone tells you they have created a completely safe system that interacts with the real world, and it's fully safe, I would not believe that）。” 随后，两人深入剖析了形式化方法与统计/概率方法在面对不确定性时的本质差异。Mykel 指出，在建立物理世界模型时必须对不确定性（如飞机的加速度范围）预设边界。在形式化方法中，研究者通常不依赖先验的概率分布，而是通过“不确定性集合（sets）”来约束变量范围；这种证明只要成立就非常优美，但关键在于这些假定的区间是否足够贴合现实。 Clark Barrett 对此补充道，任何数学证明都必须建立在特定假设（assumptions）之上。在软件底层，形式化证明可以提供 100% 的绝对保证——例如，如果数学上证明了某段代码具备内存安全性（memory safe），攻击者就绝对不可能利用缓冲区溢出漏洞进行渗透。然而在感知和复杂现实场景中，形式化方法存在明显的边界。Clark 分享道，早年在验证神经网络时曾有人问他：“你打算怎么形式化证明这个感知网络能准确区分猫和狗？”他当场回应：“我甚至都不知道该如何用形式化逻辑去给‘猫’和‘狗’下定义，这已经超出了形式化方法的能力范畴。”形式化社区经过多年摸索吸取的惨痛教训是：必须把底层假设向外界交代得一清二楚，否则只会让使用者期望落空。 - **航空安全哲学**：FAA 与 ICAO 的工程目标不是将灾难概率降至绝对的数学零点，而是将其控制在现实中极难发生的极小概率窗口内。 - **集合约束 vs 概率分布**：形式化方法通常依赖不确定性集合而非概率分布假设，但其可靠性取决于该集合能否覆盖现实动态。 - **证明的绝对性与局限性**：内存安全等代码级规范可以做到 100% 绝对免疫；但在目标无法被严密形式化定义（如图像目标分类）的场景下，形式化证明无法单独生效。 --- ### [01:03:00](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3780s) 航空安全的“瑞士奶酪模型”如何用于大模型对齐 对话最后讨论了系统工程中著名的“瑞士奶酪模型”（Swiss Cheese Model）。Mykel 解释称，该模型是航空安全领域的核心比喻：保障系统安全不是寄希望于某一块无懈可击的坚盾，而是依靠层层叠加的纵深防御体系。在飞机防撞机制中，顶层是战略航路分离（如向东和向西飞行分配不同高度层），下一层是空中交通管制（ATC），底层则是机载防撞系统。每一层防御机制都有其自身的漏洞，就像瑞士奶酪上的孔洞；安全设计的核心目标是通过不同层级之间的互补，防止所有的孔洞在某一时刻串成一线，导致致命危险穿透所有防线。 主持人将该模型直接类比到大语言模型的多阶段防护流程中，梳理出了一套端到端的防御链路： 1. **预训练数据清洗**：例如 Percy Liang 等学者正在探索的做法，使用轻量级过滤模型全面审查预训练语料，将恶意或危险数据从源头剔除，使模型在根本上丧失学习有害知识的可能。 2. **训练后故障分析与量化**：通过采样测试与红队测试测定故障率（$P_{\text{fail}}$），进而推导出成功可靠率（$P_{\text{success}} = 1 - P_{\text{fail}}$）。 3. **运行时监控（Runtime Monitoring）**：在系统实际推理与执行阶段设置动态防御。 Mykel 对这一类比表示强烈认同，并指出所有这些防线缺一不可。他引用了主持人开场时提到的反面案例：当系统擅自关闭了“思维链监控（chain of thought monitor）”这一关键层级时，就等于在奶酪屏障上凭空凿出了一个巨大的漏洞。除了 Clark 和他正在研发的形式化与压力测试等技术工具之外，确保这些防护层在实际部署中始终生效、不被人为旁路，同样是构筑 AI 安全不可或缺的基石。 ### [01:05:13](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3913s) 观众问答开启：没有规范的代码如何进行形式化验证？ 在圆桌环节的尾声，主持人总结道，必须在人类层面建立起恰当的防御机制，网络安全的历史早已证明，系统被攻破的典型途径往往源于社会工程学（Human Engineering）。随后讨论正式进入观众提问（Audience Q&A）环节。 现场第一位提问者直接向 Clark Barrett 发难：在真实世界（例如此前讨论的美国银行场景）中，大多数企业级代码和现实应用压根就没有形式化规范（Specification）。既然没有规范，形式化验证究竟该如何落地？难道要直接从源码中倒推假设和规范吗？ Clark Barrett 坦言这是一个极佳的问题。他指出，在未来的软件世界里，写代码已经变得非常容易，且预计未来几年内验证代码也会变得容易，剩下的唯一难点就是规范本身。然而，规范的构建存在一条清晰的光谱： 1. **通用型基础规范（Universal Specs）：** 这类规范无需定制。例如针对 C 语言代码，最普遍的需求是“内存安全”（Memory Safety）。这类规范只需要编写一次，就能成为所有人都必须满足的标准基线。当主持人追问为何普通人要关心内存安全时，Clark 解释，如果代码能访问未初始化或越界的内存，攻击者就能发动缓冲区溢出（Buffer Overflow）攻击以非法获取系统权限，“事实上，我认为令人遗憾的是，缓冲区溢出至今仍然是排名第一的安全漏洞”（“In fact, I think the number was still sadly the number one security vulnerability is buffer overflow.”）。 2. **领域专属规范（Domain-Specific Specs）：** 以银行系统为例，核心诉求是“资金不发生净损失”（No loss of funds）——无论执行多少笔交易序列，系统内的总金额应当守恒。 3. **由 AI Agent 辅助挖掘规范：** Clark 提到，现代的编码助手（如 Claude Code）在发掘潜在规范方面表现亮眼。很多时候开发者只提出了初步需求，Agent 反而会主动提醒：“你可能还需要考虑 A、B、C 几种边界情况。”未来的交互模式很可能演化为专门的 Agent 助手与工程师对话，逐一梳理边角案例（Corner Cases）并自动生成规范。 提问者紧接着追问：如果在为开源项目（如 vLLM 或 SGLang）做验证时借助 Agent 写规范，怎么能保证 Agent 写出来的规范真正符合开发者的原始意图？ Clark 承认这其中确实存在差距，也是一个极具前景的研究方向。但他强调：“但我认为，即使你无法彻底弥合这个差距，只要你让 Agent 编写一系列规范并证明其正确性，一旦证明成功，你手上的代码质量大概率会远优于此前”（“But even if you don't cross that gap, I would argue that if you ask your agent to write a bunch of specs and prove them correct, and it succeeds, you most likely have better code than you would have had otherwise.”）。主持人也补充道，更前沿的模型不仅能提升代码生成速度，还能反过来替人类查漏补缺，捕捉连人类都会遗漏的复杂社会工程学攻击场景（比如限制入职不足半年的新手客服向新邮箱重置密码）。 ```mermaid flowchart TD accTitle: 从模糊意图到形式化验证的演进流程 accDescr: 展示通用规范、领域规范以及由Agent挖掘的规范如何输入验证引擎，以提升代码安全基线。 subgraph Inputs["规范来源 (Specification Sources)"] U["通用规范<br/>(内存安全、防止缓冲区溢出)"] D["领域规范<br/>(如银行资金守恒原则)"] A["Agent 交互挖掘<br/>(主动提炼边界情况与安全假设)"] end subgraph Verification["验证与执行 (Engine)"] V["形式化验证工具 / Lean 求解器"] C["目标源码<br/>(如 vLLM / 企业业务代码)"] end U --> V D --> V A --> V C --> V V --> R["高可信度代码<br/>(数学证明无安全漏洞)"] ``` --- ### [01:09:52](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=4192s) 行业监管与市场动力：自动驾驶先例与安全非竞争共识 前排的另一位观众提出了监管与落地动力的问题：既然形式化验证类似航空防撞系统的严苛工程审查，但各家公司的安全标准参差不齐，那么在 AI 安全领域是否需要法规监管？如果不需要，又该如何激励科技公司主动采纳形式化验证引擎？ Mykel Kochenderfer 结合自己与斯坦福前机械工程教授、现任职于 Waymo 的 Chris Gerdes 的合作经历进行了阐述。Chris Gerdes 曾前往华盛顿特区协助美国交通部（DOT）制定自动驾驶汽车法规。他们最终得出的结论是：在技术高速创新的发展初期，如果在法规层面规定得过细、过于教条化（Prescriptive）去强制指定某种具体技术，往往为时过早；监管应该聚焦在更高维度的最佳实践（Best Practices）和通用标准上。 更重要的是，前沿领域的企业有着天然的合作逻辑。Mykel 指出：“重要的是要意识到，各家前沿实验室、自动驾驶公司，他们并不想在安全上展开竞争”（“I think the important thing to realize is that the various frontier labs, the various I don't know automated driving companies they don't want to compete on safety.”）。无论对 Waymo 还是 Zoox 而言，任何一方发生恶性伤亡事故，都会重创公众与监管对整个自动驾驶行业的信任，因此业内企业在安全底线上必须通力合作。 Clark Barrett 对此表示赞同，认为监管应侧重于用通用原则进行引导，而非直接强制技术方案： > “在形式化验证的特定场景下，我做形式化已经 30 年了，一直试图说服人们采纳它。强制告诉大家‘你们必须换这种方式做事’是个糟糕的主意。我认为现在的不同之处在于，未来将由市场力量来驱动其普及。”（“In the specific case of formal, you know, I've been doing formal for 30 years trying to get people to do it. It it's a bad idea to try to tell people you have to do this differently. Um, I think what's different now is I think there will be market forces that incentivize it.”） 一旦有先驱企业证明形式化验证可以在大规模工程中高度自动化运行、显著拔高安全壁垒，整个行业的所有首席信息安全官（CISO）都会面临巨大的市场压力，被迫跟进以避免竞争劣势。 主持人最后总结了形式化验证发生质变的根本原因：在过去，要想对 Google 级别的海量代码完成形式化重构（Leanify），必须耗费巨资聘请 150 名精通 Lean 语言的博士耗时数年逐行推进，高昂的人力成本让企业望而却步；而如今这一瓶颈已被彻底打破——利用大语言模型，企业只需花费 100 到 1000 美元的 Token 调用费用，就能瞬间实现规范翻译与自动证明。针对前沿大模型安全，各大模型实验室的利益高度一致，正如 Tom Brown（此前在纳帕谷交流时所强调的），模型的滥用与受攻击对所有人都是公关灾难，这也是为何各大巨头愿意近期一同前往白宫签署安全承诺。 ### [01:14:43](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=4483s) 自律监管框架与代码超级智能的目标 研讨会继续围绕监管架构展开讨论。发言者指出，目前已经有一份包含四项核心要点的共识文件，各大实验室实际上已经在独立审计（independent audits）和安全护栏等措施上达成了一致。包括英伟达（NVIDIA）在内的六大主流实验室都承诺执行这些规范——尽管英伟达不直接研发 Megatron 这类模型，常常被排除在讨论之外，但他们理应参与其中。这表明行业内已经存在一个自律监管机构的雏形，既不需要政府的强力干预，也避开了惩罚性的监管模式。 现场观众向 Anthropic 的代表提问，询问其团队最先瞄准的应用场景与市场是什么，以及如何在真实世界中衡量成功。Clark Barrett 对此作出了回应，虽然受限于保密要求无法透露过多细节，但他明确指出了团队的首要目标：“我们的重中之重，是构建能够在大规模场景下自主、自动、高效对代码进行推理的能力（build the capability to reason autonomously, automatically, efficiently with about code at scale）。”他将这种能力类比为“代码超级智能”（code superintelligence），认为一旦拥有了对代码进行精确形式化推理的能力，就能衍生出成千上万种应用，涵盖企业服务、开发者辅助以及系统安全等各个维度。对于成功的定义，Clark Barrett 给出了一句极为纯粹的终极衡量标准：“当世界上所有的代码都完成形式化验证时，就是成功（Success is when all of the world's code is verified）。” ```mermaid flowchart LR accTitle: 代码超级智能与验证演进路线 accDescr: 展示从构建底层代码推理能力到衍生应用并最终实现全量代码验证的演进路线 subgraph Core["核心能力构建"] A["大规模自主代码推理能力<br/>(代码超级智能)"] end subgraph Apps["赋能应用场景"] B["企业级开发与效能"] C["开发者智能助手"] D["软件系统与网络安全"] end subgraph Goal["终极成功标准"] E["全球所有代码实现数学验证<br/>(All code verified)"] end A --> B A --> C A --> D B --> E C --> E D --> E ``` ### [01:16:25](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=4585s) 自然语言接口的脆弱性与硬件层面的全栈验证 随后观众提出了一个关于大语言模型（LLM）与智能体系统交互界面的安全性问题：当前人类主要通过自然语言接口与模型代码互动，提示词注入（prompt injection）以及针对智能体的跨站脚本攻击（XSS）层出不穷，形式化方法在面对这类攻击时能否发挥作用？Clark Barrett 坦言这确实存在固有的难点，因为纯粹的人机自然语言交互并不包含可以直接进行形式化数学证明的代码成分。不过，行业内正在探索可行的应对路径。例如亚马逊推出了“自动化推理检查”（automated reasoning checks）技术，该方法监控 LLM 的自然语言回复，利用自动形式化（auto-formalization）技术提取模型试图传达的领域知识，随后将其与严格的领域数学模型进行交叉比对。 主持人联想到计算机科学早期的典型漏洞，打趣道：“我学计算机时，有 SQL 注入攻击，比如著名的‘小约翰尼删表’（Johnny Drop Tables）经典漫画漏洞。难道现在没有等价的模型能去检查用户输入并过滤掉提示词注入吗？”Clark Barrett 直截了当地指出，这类过滤机制本质上是一场没有休止的攻防军备竞赛（arms race），防守方与攻击方永远在相互角力，难以彻底根绝。 另一位观众向 Clark Barrett 发难，探讨了验证的边界问题：即便将美国银行（Bank of America）内部的所有应用软件全部形式化，整套系统仍旧依赖极长的外部依赖链，乃至延伸到底层硬件；难道需要把 x86 指令集架构也验证一遍吗？若是面临类似 Rowhammer 这样的物理硬件级故障注入攻击，形式化方法又该如何应对？Clark Barrett 随即回应称 x86 指令集早已有数家公司完成了形式化。针对硬件攻击，他给出了雄心勃勃的愿景：“软件是唾手可得的低垂果实，硬件确实难度更高一些，但我认为最终的范围应该是：你验证所有的软件，验证所有的编译器，验证所有的硬件，然后大功告成，对吧？（you verify all the software, you verify all the compilers, and you verify all the hardware, and then you call it a day, right?）”他坚信形式化工具与 AI 的结合正在飞速进化，目前已经有大量初创团队借助 AI 开展硬件验证。 ### [01:19:20](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=4760s) 可信 AI 充当超级管理员、责任认定与告警疲劳 有观众提出了一个别开生面的类比：在领英上有医生讨论，Waymo 的自动驾驶系统在挽救生命方面表现极其出色，如果它是一家制药公司的药物，早就应该获得美国政府的“同情用药”（compassionate use）豁免了。由此引申到企业安全领域，许多企业系统的管理员（admin）与开发者面临着极高的人身安全威胁——历史上曾发生过加密货币高管遭遇人身残害（手指被切断），以及 90 年代 Adobe 首席执行官遭绑架的事件。该观众提问：能否构建一个高度可靠的 AI 系统，将其封装在机密虚拟机（confidential VM）中直接充当企业管理员，以此阻断针对物理人身攻击的威胁向量？ 针对“是否应该完全自动化核心管理职能”，Mykel Kochenderfer 从航空安全领域的历史经验切入进行对比。他谈到，航空领域长期面临飞行员自杀以及飞行员心理健康问题的严峻挑战，人们同样会问为什么不直接全面推行无人化。然而联邦航空局（FAA）在接纳完全自动化方面极为审慎：“即使飞机处于无人驾驶状态，也必须有一位受到 FAA 监管和认证的飞行员在场；如果出现意外，他们需要承担责任。因此，我认为我们必须极其审慎地思考责任认定问题（So, I think we need to think very carefully about responsibility）。” Clark Barrett 同样认为 Waymo 的案例很有启发性——尽管它并非十全十美，但数据显示它确实挽救了生命；然而关键问题依然在于追责：“制造 AI 管理员的公司，是否愿意在出现差错时承担法律责任？如果他们愿意，那就说明他们的安全论证（safety case）确实做得非常扎实。” 主持人则从信息安全（InfoSec）的实际架构出发展开了补充。在当下的零信任（Zero Trust）架构下，单点渗透无法攻破全局。若能引入一个全天候保持警惕的智能 AI 系统实时审计系统流量与平台（如 Datadog），识别异常上下文行为（例如发现公司 CTO 正在往境外账户发起异常大额转账，或者有敏感密钥被生成并发送至非公司官方的 Gmail 个人邮箱），AI 就能在没有死板规则的情况下凭借对丰富上下文的理解精准告警。这能从根本上解决困扰企业运维人员的“告警疲劳”（alert fatigue）问题——就像 Sentry 每天喷出上千条垃圾告警，导致管理员视而不见；航空防撞系统（TCAS）同样受到告警过载的困扰。利用更高级的 AI 监控全局，能够剔除噪声并实现精确告警。 在环节尾声，另一位观众就扩散模型（diffusion models）与标准化流（normalizing flows）等动力系统模型向教授提问。观众观察到，当前中国的大模型实验室正在全力推进计算与推理效率的前沿，而美国实验室则在不遗余力地突破通用智能与能力的极限，但在系统构建初期就专注研究系统可控性（controllability）和可解释性（interpretability）的机构却相对匮乏，并由此引出学术界在监控训练动力学（training dynamics）与涌现能力方面的理论进展。 ### [01:24:52](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5092s) 工程学的基本法则：简单模型胜过盲目追求复杂性 一名现场听众提问：从传统统计机器学习、信号处理和控制理论，跨越到当下的深度学习与神经网络，我们是否可能对训练动态和智能施加约束（例如以某种方式过滤梯度），从而在“可解释性与控制”和“智能与能力”之间划定一条前沿权衡曲线。 斯坦福大学教授 Mykel Kochenderfer 回应指出，他每年三次在斯坦福商学院（GSB）以及斯坦福以人为本人工智能研究院（HAI）向来自全球的高管讲授 AI 战略培训课程。这些高管普遍面临巨大的外部压力，必须在产品和业务流程中强行引入 AI。Kochenderfer 总是首先向他们重申工程学的根本原则：正如科学界的奥卡姆剃刀法则（最简单的解释往往最可能是真实的），工程学同样遵循这一铁律——“更简单、更具可解释性的方法往往更具备鲁棒性（In engineering, the simpler, more interpretable method is more likely to be robust）”。 Kochenderfer 告诫与会者，行业当前存在过早投向神经网络和 Transformer 架构的盲目冲动。然而合理的工程实践应当是从最简单的基线（如线性回归或决策树）做起；只有当更复杂的架构带来的性能提升足以抵消额外引入的复杂度成本时，才有理由转向复杂系统。否则，坚守高可解释性模型才是最稳健的路径。他补充道，在他参与编写的全新验证体系著作中，专门有一章深入探讨了可解释性，而这正是让机载防撞系统标准（ACAS X）被采纳为国际行业标准的关键支柱。 随后观众追问：如果研发“受限智能（constrained intelligence）”，市场上是否有足够的激励和需求让其与前沿大模型实验室竞争？Kochenderfer 肯定地表示：“如果你能成功创造出可被量化证明更安全的产品，那绝对会是一项竞争优势（So I would say that if you manage to create something that is measurably safer, then that would be a competitive edge, for sure）。”主持人也风趣地补充，如果有人打算围绕这个方向创业，可以申请知名创业加速器（暗示 YC），他们会提供充裕的资金与战略指导。 --- ### [01:28:41](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5321s) 互联网时代与 AI 时代的安全分野：人与机器之辨 一位听众提问：互联网时代为人类积累了海量安全经验，在当前的生成式 AI 时代，我们应当继承哪些旧有模式，又面临哪些全新的安全挑战？ 斯坦福大学教授 Clark Barrett 回忆起自己在纽约大学（NYU）担任年轻教授时参加的一场安全讲座。那场报告提出安全本质上只有两个核心难题：一个是“人”，另一个是“软件漏洞（computer bugs）”。Barrett 幽默地总结道：“我认为我们能够修复计算机的漏洞，但我认为我们修不好人性的弱点（So, I think we can fix the computer bugs, but I don't think we can fix the people）。” 针对生成式 AI 时代的安全变数，Barrett 认为 AI 既可能加剧风险，也能以极富创造力的方式成为防御手段： - **安全守门人（Watchdog）**：AI 可以充当防御代理，识别并拦截针对人类的社交工程攻击（Social Engineering）。 - **形式化方法加速器**：AI 可以辅助自动生成数学证明与规格说明，系统性提升系统的绝对安全性。 - **自动管理员与人机协同**：尽管可以使用 AI 扮演系统管理员，但必须保留人机协同（Human-in-the-loop）。Barrett 借用冷战时期的经典老电影《战争游戏》（*WarGames*）发出警告：如果把所有控制权全盘交由计算机，一旦出现未曾预料的系统级异常，事态就会彻底脱轨失控。 --- ### [01:30:26](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5426s) 规模质变与系统饱和：当“更多即不同”撞上真实世界 针对互联网安全与 AI 安全的本质差异，讨论引入了物理学领域的著名论文《更多即不同》（*More Is Different*）作为类比：一个或两个原子遵循基本微观物理法则，但当巨量原子坍缩聚集时，就会形成黑洞，甚至导致光线无法逃逸只能折返。在智能体时代，同样会发生这种由于数量级暴增而引发的相变。 过去互联网承载的是 60 亿至 70 亿人类产生的信息交互，而在未来，可能有 700 万亿个具备同等甚至超越人类智力、且拥有独立行动动机的自主智能体（Agents）被瞬间生成并部署。过去 Cloudflare 等网络基础设施可以通过吸收和过滤流量来抵御分布式拒绝服务攻击（DDoS），然而“当数字趋向无穷大时，现有的一切系统都会崩溃（everything breaks when you hit when you apply infinity to the number, everything breaks）”。 以学术界和现实社会中的审核系统为例，智能体的大规模普及正在带来灾难性的系统拥堵： ```mermaid flowchart TD accTitle: 智能体泛滥引发的系统级资源耗尽流程 accDescr: 展示从低成本生成智能体到导致各类传统人类审核机制陷入瘫痪的因果演进路径 subgraph INGRESS ["智能体激增"] A["边际成本趋于零的智能体"] --> B["指数级任务提交 (申请/立案/论文)"] end subgraph IMPACT ["现实审核与仲裁节点"] C["学术同行评审 (如 ICLR 6万篇论文)"] D["高校招生申请审核"] E["小额索赔法院司法系统"] end subgraph CRISIS ["系统性瘫痪"] F["人工在环机制彻底被 DDoS 击穿"] G["人类在全网流量中占比逼近 0%"] end B --> C B --> D B --> E C --> F D --> F E --> F F --> G ``` - **学术论文评审**：以深度学习顶级会议 ICLR 为例，单年投稿量就突破了 60,000 篇，一年的提交总量甚至超过了该会议历史上所有年份投稿量的累计总和，使既有的审稿人机制不堪重负。 - **大学招生博弈**：当智能体可以零成本为全美乃至全球的高中生一键投递所有高校时，学生的纳什均衡最优策略就是申请每一所学校。如果学校不设立高昂的申请费门槛，传统的招生材料审核链条将被彻底打穿。 - **司法诉讼系统**：如果每个人都能驱使一个廉价的法律智能体自动起草并向法院提交小额索赔诉讼（Small claims court），无需聘请昂贵的律师，本就排期冗长、效率低下的司法系统将被无限期的诉讼海啸彻底拖垮。 讨论明确指出，“人类流量在未来互联网总流量中的占比将趋近于 0%（human traffic will be 0% of internet traffic）”。传统互联网时代对于“大规模”的认知已经被彻底颠覆，所有高度依赖“人工在环审核”的现实社会基础设施都必须从底层逻辑进行重新评估与重构。 --- ### [01:33:05](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5585s) 基准测试的持续监控与数据漂移 一位来自 LinkedIn 的 AI 安全团队从业者提出了关于评估体系的实践困境：伤害的定义和语言特征正在快速漂移。即便在像“不良文本（toxic text）”或“隐性偏见（bias）”这类相对具体的领域，每隔五年年轻世代就会演变出全新的俚语与暗语。这类表达一旦渗入招聘流程或招聘人员的信息沟通中，将引发新型合规风险。当前依赖人工审核、发布周期漫长的传统基准测试（Benchmarks）反应极其迟缓，亟需探索如何让基准测试具备像语言本身一样快速动态演进的能力。 Mykel Kochenderfer 对此回应道，解决方案的逻辑与 AI 系统的运行时监控是一脉相承的：“正如我之前主张我们要对 AI 系统进行持续监控一样，我们也应该对我们的基准测试进行持续监控（just like how I advocated for continuously monitoring our AI systems, we should continuously monitor our benchmarks）。” - **定量识别分布偏移**：学术界与工业界已具备一系列用于捕捉数据分布偏移（Distribution shift）的定量统计方法，必须将其系统性引入测试集的生命周期管理中。 - **动态语言漂移追踪**：对现实世界中正在发生的语言演变进行实时检测，是保障基准测试长久有效、不被快速淘汰的必要手段。 在讨论尾声，另一名听众提及了 BetterBench 项目，并指出当前学术研究中广泛使用的主流评测集（例如 MATH 500）本身就存在诸多损坏和错误的测试用例，揭示出评测工具自身亟待形式化检验与质量把关。 ### [01:35:12](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5712s) 破损基准测试的闭环困境与严谨性军备竞赛 观众与嘉宾探讨了当前 AI 评测基准（evals / benchmarks）普遍存在的缺陷以及缺乏集中式纠偏机制的问题。现场有观众提出，行业需要与 Hugging Face 等平台建立某种协调机制，让 AI Agent 或研究人员能够集中发现并标记有问题的资源。目前的情况往往是有人发表论文指出某某基准测试损坏或评测有误，但报告发出来后就石沉大海，没有任何机制去修复这些数据集，因此现场呼吁应当有人站出来“把这个闭环补上”。 Clark Barrett 对此深有同感，并分享了一个身边的真实案例：他的一位前学生此前尝试评测模型生成 SQL 查询的能力，当时所有参与评测的模型得分上限都卡在 70% 左右，始终无法突破；这名学生深入排查后才发现，原来该基准测试本身就有大约 30% 的题目标注是完全错误的。Clark Barrett 直言，这种情况主要是因为大家跑得太快、做事过于粗糙：“So, I think it's just a matter of people moving too fast, being a little careless, and hopefully, you know, the people who are rigorous will eventually catch up and fix it, but it's a little bit of an arms race now cuz everyone's trying to move so fast.” 随后嘉宾们补充道，评测基准领域急需引入软件工程中成熟的版本控制（version control）、Pull Request 以及 Issue 追踪机制。 ### [01:36:15](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5775s) 创业构想：基准测试的“苹果 App Store”与活动致谢 针对评测基准混乱的现状，主持人提出这也是一个极佳的创业切入点——打造一个专门针对 AI 基准测试的“苹果 App Store”，通过严格的审核与策展机制来把关质量。在苹果生态中，平台不会允许任何人随意把应用丢进商店，而是必须经过一套审核流程来决定其是否合格。 主持人指出，尽管自己非常尊重 Hugging Face 及其创始人 Clem（Clément Delangue），但现在的 Hugging Face 就像 GitHub 一样，已经变成了混乱的“狂野西部”（wild west）。例如研究人员想要找一个标准的 GSM8K 基准测试，在上面搜索会发现有 600 个不同版本的 GSM8K，根本无从辨别哪一个是真正标准、正确的版本。主持人强调：“I actually think that a great idea for a startup is like a Apple App Store of benchmarks where there's curation, right?” 在探讨完评测生态的规范化建设后，主持人邀请全场观众鼓掌，共同感谢斯坦福大学的 Clark Barrett 与 Mykel Kochenderfer 两位教授当晚的精彩分享与深度探讨，活动在热烈的掌声中圆满落幕。 ## Notable quotes > [17:25](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=1045s) If you formally verify all your code, then it cannot be hacked. — Clark Barrett > [01:24:52](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5092s) In engineering, the simpler, more interpretable method is more likely to be robust — Mykel Kochenderfer > [01:28:41](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5321s) So, I think we can fix the computer bugs, but I don't think we can fix the people — Clark Barrett > [55:08](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=3308s) the formal argument completely subsumes the tests — Clark Barrett > [01:36:15](https://www.youtube.com/watch?v=X7oI4Umt3DU&t=5775s) I actually think that a great idea for a startup is like a Apple App Store of benchmarks where there's curation, right? — Francois ## Mentioned Francois, Clark Barrett, Mykel Kochenderfer, Garry Tan, Sam Altman, Tom Brown, Alex Wang, Yann LeCun, Jensen Huang, Jacob Coxson, Bob Metcalfe, Alan Turing, Dario Amodei, Leonardo de Moura, Dan Fu, Jeffrey Morgan, Richie Lee, Huijun Liu, Amelia Hardy, Chelsea Sidrane, Sydney Katz, Zach Sunberg, Body El Husseini, Percy Liang, Chris Gerdes, Clément Delangue, OpenAI, Hugging Face, Y Combinator, Stanford Center for AI Safety, Stanford Intelligent Systems Laboratory, Stanford University, Google, NVIDIA, Waymo, Airbus, Anthropic, Cloudflare, NTSB, FAA, ICAO, Bank of America, Lean, CSLib, Bull, Lean-SMT, Verus, Verisforge, AndTruth, ACAS X, Llama Guard, POMDPs.jl, CVXPY, Reluplex, Marabou, BetterBench, ASRS, ASIAS, AST Prompter ## Video description This week’s Paper Club is all about AI safety - not the headlines, 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. In this episode we'll hear from Clark Barrett and Mykel Kochenderfer, Stanford professors and co-directors of the Stanford Center for AI Safety.  Together with Francois they'll discuss what actually happened in the OpenAI–Hugging Face incident versus what got reported, how automated reasoning can mathematically prove that code cannot be hacked, how the stress-testing methods built to validate aircraft are now being turned on language models, and why we might need an NTSB for AI. Chapters: 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 Apply to Y Combinator: https://www.ycombinator.com/apply Work at a startup: https://www.ycombinator.com/jobs [Source](https://www.youtube.com/watch?v=X7oI4Umt3DU)

[17:25] Clark Barrett: If you formally verify all your code, then it cannot be hacked. [84:52] Mykel Kochenderfer: In engineering, the simpler, more interpretable method is more likely to be robust [88:41] Clark Barrett: So, I think we can fix the computer bugs, but I don't think we can fix the people [55:08] Clark Barrett: the formal argument completely subsumes the tests [96:15] Francois: I actually think that a great idea for a startup is like a Apple App Store of benchmarks where there's curation, right?

[17:25] Clark Barrett: If you formally verify all your code, then it cannot be hacked. [52:18] Clark Barrett: There's a little dirty secret about software engineering, which is it's not based on sound engineering principles, it's based on like, just write something and test it and hope for the best. [27:46] Mykel Kochenderfer: It turns out that in order to establish confidence in a system, there is no one silver bullet. Probably formal methods won't take you the whole way there. [55:08] Clark Barrett: Ultimately the formal argument completely subsumes the tests. [84:52] Mykel Kochenderfer: The fundamental principle of engineering is very similar to the fundamental principle of science, which is Occam's razor.

[0:05] [music] [0:08] >> What are we doing tonight? [0:10] All right, there you go. That's better. [0:12] >> [laughter] [0:13] >> Welcome to [music] [0:14] YC AI Safety Club. I've been doing AI I [0:17] guess since about 2012 and AI safety has [0:21] always been a concern if you're doing [0:22] self-driving car or any [0:24] safety critical system as some would [0:27] call it. And so I've been working on [0:30] some semblance of of AI safety and even [0:32] at Focal when we're rolling out new [0:34] betas, [0:35] you can really mess up. You know, we [0:37] were we were in control of Walmart's [0:39] inventory [0:40] and so if you roll out a bad beta, you [0:43] order too many avocados and you blow [0:45] millions of dollars. And so like things [0:46] have it's important when you're doing [0:48] these rollouts to make sure you you know [0:49] what you're doing. [0:50] In the past three weeks, [0:54] um [0:55] there's been a little bump in focus on [0:58] AI safety. I don't know if you guys have [0:59] noticed that. [1:01] Um [1:01] not really sure why, but [1:03] so I figured [1:05] uh [1:06] there's no place better than YC Paper [1:08] Club to dive deep into it. [1:10] I think the conversation has kind of [1:12] devolved devolved devolved a little bit [1:14] away from scientific rigor and more into [1:18] what I would probably call hysteria [1:20] where things are being mis-misquoted and [1:23] I get it sensationalism gets more clicks [1:25] and all that kind of stuff, but you [1:27] know, as scientists here we should like [1:29] get back to [1:31] the rigor of scientific method [1:35] and make falsifiable claims, depend on [1:37] the peer-review cycle [1:38] and those kinds of things to make sure [1:40] that [1:41] we're not overstating things. So I call [1:43] this talk like the science fiction [1:45] versus science facts kind of stuff. Gary [1:47] Tan kind of said this line [1:51] up in Healdsburg yesterday night. Um [1:55] and where we where we got to hear Sam [1:56] Altman speak and Tom Brown [1:59] and Alex Wang and we about these these [2:02] about this topic largely. [2:05] Um and so [2:07] hysteria is when people can't measure [2:08] something but they can't stop talking [2:10] about it. And I think that's kind of the [2:12] situation that we're in and there's and [2:14] it's not you know to zoom out a little [2:16] bit this is like not um [2:19] unexpected. With any major technology [2:22] advancement it's very often the case [2:23] that [2:24] um [2:25] there's uncertainty and it's easy for [2:28] hyperbole to set in. And so even if [2:33] and with the nuclear with the atom bomb [2:35] uh even Einstein was unsure whether or [2:37] not uh uh it was going to ignite the [2:40] sky. And so clearly it didn't we're [2:43] still here um [2:44] with electronic computers many people uh [2:47] even Alan Turing was concerned that [2:49] machines were going to surpass uh all um [2:53] uh [2:54] human uh capabilities and intelligence [2:56] even back in 1950s um he thought you [2:59] know he tried to put time frames on it [3:02] obviously his time frames were were much [3:04] uh [3:04] were way off. Um industrial automation [3:07] people thought about mass unemployment [3:09] you know uh um [3:11] Marx and Keynes uh all have those kinds [3:13] of kind of conversations what are we [3:14] going to do? [3:16] With the internet even uh Metcalfe who [3:19] actually invented Ethernet said that um [3:22] there was going to be catastrophic [3:23] collapse was the was the phrasing uh on [3:25] the network and um [3:28] that the internet was going to basically [3:29] fail and because of things like [3:31] Cloudflare I think it was DDoS's was [3:33] mainly his main concern it ended up not [3:36] happening and then he famously um [3:38] put his paper into a blender and then [3:42] drank his own words. This is actually a [3:45] true story it's very funny. Um Google [3:47] people thought this is this is ruining [3:49] human intelligence people are just [3:50] Googling things and not actually reading [3:51] anymore, [3:52] um, which people are still pretty [3:54] intelligent, especially in this room. [3:56] And then smartphones and social media, [3:57] um, we were just talking about this. Now [3:58] that I'm back at Stanford and I've been [4:00] TA-ing classes for Michael, um, and some [4:02] other, uh, um, [4:03] you know, just interfacing with with, [4:05] um, the the the batch at YC, who is [4:08] predominantly younger younger folks. [4:10] I am like super super excited about the [4:12] the the the 18-year-olds, 20-year-olds, [4:14] um, [4:15] of today. Um, they're just so, um, on [4:19] it. [4:21] And then finally now we're in this AI [4:22] era and the talk of human extinction is [4:25] back and it's it's easy to jump to [4:28] hyperbole and we should probably get [4:30] back to some facts. [4:31] Okay, so there's a few narratives to [4:33] choose from and there's more that we [4:34] could add but these are the probably the [4:36] the biggest, um, ends of the spectrum. [4:39] So, Yann LeCun has this, uh, analogy to [4:42] the turbojet [4:43] that he's talked about a lot. You guys [4:45] didn't hear him talk about it, but it's [4:46] largely just safety through engineering. [4:48] This is an engineering problem. Jensen [4:49] Huang just, uh, said something similar [4:52] where it's not easy. It's difficult. [4:54] It's difficult to make planes safe, to [4:56] make sure the doors don't fly off when [4:58] you're taking off, make sure the landing [4:59] gear goes down, the landing gear works, [5:01] um, that, uh, the MCAS system that [5:04] deployed to the Boeing 737, um, is fully [5:08] tested and and doesn't, uh, do things [5:09] that, you know, can cause failure. [5:13] And it's similar with ACAS X, which [5:14] we're going to hear about, too, which is [5:15] an amazing system that saves lives, uh, [5:17] the aircraft collision avoidance system. [5:19] Um, and the alternative, uh, [5:23] is this P(doom) uh, is greater than 10% [5:26] within 10 years that, uh, famously, uh, [5:29] Jacob Coxen just kind of came out and [5:31] and is setting these things and he said, [5:33] "I think it's more likely than not that [5:35] humanity loses control to these AIs and [5:37] could end in human extinction." [5:39] Um, you know, honestly, I'm not going to [5:41] judge one way or the other. I think my [5:43] point of tonight is to give airtime to [5:47] an alternative point of view and allow [5:49] you guys to make your decision. Um I [5:52] will say that there is a small [5:54] difference in H index between the two [5:55] people here on this on on these sides of [5:57] the spectrum, which you can use to [6:00] change your priors. [6:03] Um but let me give an example of the the [6:06] hyperbole or at least the misrep or a [6:09] misstatement um on the things that [6:12] actually happened. So like the hugging [6:13] face breach is is is another fact versus [6:16] fiction thing that we should double [6:17] click into. If you look at the slashdot [6:19] headline, OpenAI says its AI models [6:21] acted on its own. OpenAI never said [6:23] that. [6:24] Not in one statement. [6:27] But this is what was the headline. Um [6:29] rogue AI agent went haywire at a tech [6:31] company. [6:33] It's not what happened. It didn't just [6:34] wake up today and say, "You know what? I [6:36] think I'm going to hack hugging face. [6:38] You know what I'm going to do tomorrow? [6:39] I'm going to solve Navier-Stokes. You [6:40] know what I'm going to do tomorrow? I'm [6:41] going to kill all humans." You know, [6:42] this is not not the way it happened. It [6:44] was prompted. It was prompted by exploit [6:46] gen um in with about 1,200 agents. And [6:50] even more, as they did point out, they [6:52] had chain of thought uh they released [6:54] this amazing uh um [6:56] like 60-page document um [6:59] called the OpenAI hugging face incident [7:00] that you can read the technical report [7:01] that I I read and the CO2 monitoring was [7:04] turned off accidentally or or otherwise. [7:08] And and it and they said that they [7:09] repeated they added it back the CO2 [7:11] monitoring and it would have caught the [7:13] issue. [7:14] Number one. Number two, there's also [7:16] prod guardrails and safeguards that were [7:18] off cuz it wasn't in prod. [7:20] And so that would have also caught the [7:21] issue. Um but the the narrative isn't is [7:25] that it got it went haywire, it went [7:27] rogue, it escaped from the servers, made [7:30] copies of itself, and and now is soft [7:33] solving math and hacking things, [7:36] Australian governments, and [7:38] what next? [7:39] Okay. [7:40] The other one that's kind of funny, if [7:42] you actually double click into this, I [7:43] was like, "Okay, what's this Pdoom 10% [7:46] in 10 years thing?" [7:47] First of all, there was this paper in [7:49] 2023 called Thousands of AI Authors on [7:51] the Future of AI. [7:53] And in that paper, they asked ner- 1,200 [7:55] Nerbs folks, um AI professionals, uh [8:00] you know, these a bunch of questions [8:01] about when certain enhance- enhancements [8:04] are going to happen and in in one of the [8:05] later uh uh survey questions, way later [8:08] in the paper, they uh asked these three [8:10] questions. What probability do you put [8:12] on future AI advances causing human [8:15] extinction or similarly permanent or [8:16] severe disempowerment of the human [8:18] species [8:20] for T infinity? [8:21] For all time. [8:23] In question three, they asked in the [8:25] next 100 years. [8:26] And these are the stats. This is the [8:28] mean and this is the the the the the [8:30] median. Um and none of that is in the [8:33] next 10 years. And that was this is the [8:34] paper that most people are quoting [8:37] when they're talking about this. Which [8:38] by the way, you know, if it's kind of a [8:40] weird question and like how much if I [8:43] were I was just talking to the [8:44] professors about this, like if I flash [8:46] back to when I started in in in at [8:49] Stanford in 2012 in AI, um [8:51] when would um [8:54] if they if I ask all the Stanford [8:55] professors, [8:56] "When would uh [8:58] AI indepen- solve or at least assist [9:02] majorly in solving a millennium prize [9:04] problem?" I don't think you get a very [9:06] good answer and it definitely wasn't [9:07] going to say in in 14 years. I think it [9:10] might have been said 50 years or 100 [9:12] years would be maybe the consensus, but [9:14] you know, and so like I don't know if [9:15] there's very much signal in asking 1,200 [9:18] Nerbs people um [9:20] any of these kinds of questions cuz it's [9:21] really hard question. Um and so people [9:23] come up with coherent stories and [9:24] confident predictions even when they [9:26] know little or nothing about it. Um [9:29] and so [9:31] the the other one that I thought if if [9:32] you've seen the SNL skit, man, they did [9:35] such a good job. And I feel bad for [9:36] Dario, cuz I don't think Dario is [9:38] actually um um [9:40] They they portrayed Dario in a very very [9:42] weird light, and I think that he's a [9:44] little bit more [9:45] um [9:46] even keeled than Jacob Coxson and some [9:49] of the strong EA community. Um [9:53] but the I urge you to urge me to stop, I [9:55] thought was just too perfect, was very [9:57] funny. [9:58] So, I was driving back from Healdsburg, [10:00] and this is I've never actually seen [10:02] this. I've driven over the Golden Gate [10:03] many times, and um I was thinking about [10:05] what I was going to say tonight uh the [10:07] whole drive, and I was driving over the [10:09] Golden Gate, and the entire bridge was [10:11] gone in fog. And I thought this was like [10:13] so perfect, I have to talk about this. [10:16] Uh one, it looks really cool. The [10:17] second, um which I almost crashed taking [10:19] this picture, but anyway. [10:21] Uh [10:22] the we know [10:24] the future isn't certain. I we have some [10:26] prior we can allocate that the bridge is [10:28] still there. [10:29] It may not be. So, we're going to drive [10:30] toward it, and we should allocate the [10:32] prior and choose the argmax probability [10:34] that, you know what, I think that the [10:35] bridge is still there. Let's just keep [10:37] driving, and you know what, we'll keep [10:38] going, and as we [10:40] keep driving and the get more [10:42] information, then we'll we'll change [10:44] gears, maybe I'll stop. I don't know, [10:46] before I get on the the bridge or [10:49] go into the into the bay. [10:50] Um so, [10:52] >> [clears throat] [10:52] >> I'm not concerned uh almost at all [10:56] uh with this path, this reality that um [10:59] AI is going to develop a soul, has [11:01] consciousness, is has some will, has [11:03] some motivation, and um [11:06] and thus killing and enslaving us uh [11:08] with its own independent volition um in [11:10] some short period of time, such as 10 [11:13] and 20 years. In infinite time, I think [11:14] everything happens. Um [11:17] so, I'm not sure that's useful. [11:19] Um number my number one concern is, and [11:23] this is very real, is that really great [11:26] open weight models allows for a lot more [11:29] of the same from this from bad bad rogue [11:32] actors or nation states. So, today we [11:35] have terrorism, we have uh bio weapons, [11:38] we have uh [11:40] uh cyber warfare, ran cyber ransom [11:42] attacks. It just happened to my friend's [11:45] local hospital in Poland where a bunch [11:48] of Russian hackers took control of a [11:50] hospital and shut down the hospital for [11:51] 3 weeks. And maybe they used AI to do [11:54] it. And what's going to happen now is it [11:56] makes it easier to do that. And and [11:59] so that's going to happen already. [12:01] Um and there's a couple solutions to [12:03] this that people have proposed and I [12:04] think they all kind of suck. [12:06] One is banning open weights. Good luck [12:08] with that. I've already downloaded Kimmy [12:09] K3 and GLM 52 already in my um in my [12:13] garage, so [12:15] sorry. [12:16] Second is registering the GPUs. Again, I [12:19] have a bunch of tiny boxes in my garage. [12:21] You know, unless you're going to search [12:23] every single person's house and every AI [12:24] person, you know, it's uh you're not [12:26] really going to know that they have GPUs [12:28] or not. Um [12:30] and also I can just book a GPU in [12:32] another country that you can't stop me [12:34] from doing, so I'm I don't know how that [12:36] really solves anything. [12:38] There is some cool ideas where you have [12:40] utilities that can detect how many [12:42] dishwashers and how many refrigerators [12:43] you have based on the signal of the the [12:45] load on the network uh on the on your um [12:48] on your meter. And you know, that's kind [12:49] of cool. You can detect inference [12:50] signals that people are doing bad [12:51] things, at least in America. But I'm I'm [12:53] not I'm I'm not entirely concerned that [12:55] that's the main concern. I think you [12:58] know, there's a lot of of you know, [13:00] we're we're at war with a lot of um [13:02] nation states that this doesn't doesn't [13:04] really solve anything. Um [13:06] rogue actors in in America, okay. [13:09] And the last one, which is kind of a [13:10] catch-all, serves uh it solves mostly [13:12] anything and we should be doing it [13:13] independently, is invest in defense. And [13:16] so, if you are a bank, you are a [13:19] hospital, you are a uh [13:22] you know, financial service, you're a [13:23] government, you should be investing [13:25] heavily heavily heavily into into uh [13:28] cyber defense. Um And there's a lot of [13:30] things that you can do to tighten up [13:31] your ship. I worked in in retail [13:34] for a long time. These are very [13:36] antiquated systems that haven't been [13:37] touched in a long time. [13:39] And simple methods such as [13:42] trying admin admin [13:44] work. They actually get you into the [13:46] system. Okay, why is it almost all the [13:47] social security numbers breached? It's [13:49] cuz [snorts] they didn't change the [13:50] admin admin password. Um [13:53] and with smarter models, if we actually [13:55] go faster and we [13:57] don't decelerate but accelerate where [13:59] the good people, presuming that these [14:01] frontier labs are the good people, [14:03] which I think so. Uh [14:05] if we give these good people even more [14:07] resources and they go faster and they go [14:09] faster, then we can prepare for a dumber [14:12] model trying to hack the system. [14:15] Um [14:15] it would definitely be worse if it were [14:17] flipped. [14:18] So, [14:19] anyway, that's my my two cents. [14:22] So, getting back to [14:25] sanity out of hysteria into science [14:28] facts. [14:29] You know, I there's amazing [14:32] narratives on how this was going to [14:36] kill us all and they they really sound [14:38] like an Isaac Asimov book. [14:41] Um [14:41] and and I and [14:43] you know, I wanted there's there's been [14:44] a whole literature for a very long time [14:47] about safety well before LLMs [14:50] were invented or trained. And those are [14:52] the people that were lucky enough to [14:53] have tonight. This [14:55] AI safety community has been around for [14:58] a long time. There's a lot of papers. [14:59] There's conferences on this. [15:01] Um and one of those just actually [15:02] happened [15:04] at at Stanford. [15:06] And the co-directors from that [15:07] conference are going to be speaking [15:09] tonight. [15:10] And so, here's [15:13] Michael Kogut and Clark Barrett. They're [15:14] two amazing professors [15:17] at Stanford. I've known Michael for [15:20] 14 years. [15:22] I think I took his class decision making [15:23] under uncertainty in 2013 [15:27] and then I TA'd him TA'd for him many [15:29] times and I've done research for him for [15:31] a long time. He's one of the nicest and [15:33] smartest human beings I've ever worked [15:34] with [15:35] and I know Clark Barrett less well but [15:37] I've listened to his talks and he's just [15:39] incredible [15:40] and they both have some something to say [15:43] about how we can actually apply [15:46] modern methods to validate data before [15:49] they're put into production and then [15:51] monitor them to make sure they don't [15:52] don't go off the rails and do bad [15:53] things. [15:54] Michael is an associate professor in [15:56] aeronautics and then by courtesy is that [15:59] in CS. [16:00] He's a director of my lab Stanford [16:03] intelligent systems lab co-director of [16:05] the Stanford Center for AI safety and [16:08] senior fellow at H AI. [16:10] And Clark Barrett is professor in [16:12] computer science co-director of the [16:14] Stanford Center for AI safety with [16:16] Michael and then director of the the [16:19] Centor Center [16:21] for automated reasoning and he'll be [16:23] talking about a new stealth startup [16:25] called [16:26] Ampersand Truth or And Truth. [16:28] Back to what we're talking about here. [16:30] Okay, that is all I got. I think [16:33] we have scheduled already in 2 weeks a [16:36] inference night and there's some really [16:38] really cool people coming. We already [16:40] have Dan Fu committed from Together AI [16:42] to talk about inference. Inference is [16:44] becoming more complex in some cases than [16:47] training which is kind of crazy to me [16:49] cuz it's usually when I learned it it [16:50] was just you know model.forward. I [16:52] thought that's all you had to do but [16:54] it's a little bit more complicated than [16:55] that now [16:56] and then Jeffrey Morgan [16:59] at a llama and then one of Clark [17:01] Barrett's students who [17:03] I just met this weekend runs this cool [17:05] company called Radix Arc. [17:07] Actually Lang I don't think she can make [17:08] it she's going to have one of her folks [17:09] make it and then Wafer another great YC [17:12] company. [17:13] Okay, all right. [17:16] Please [17:17] help me in welcoming Clark. [17:20] >> [applause] [17:25] >> All right, thank you. And it's a [17:27] pleasure to be here. [17:28] So, I'm going to tell you about when AI [17:31] met AR. You might be wondering what AR [17:33] is. Not augmented reality, it is [17:34] automated reasoning. [17:36] And uh there's a very nice kind of [17:38] synergy between these two topics because [17:41] as we know, AI is great with all sorts [17:43] of things, messy data, data driven, you [17:46] can train stuff. But it has this sort of [17:48] one big problem which uh you know, no [17:51] correctness guarantees, you can find [17:53] adversarial inputs, it hallucinates, all [17:55] this kind of stuff. [17:57] On the other hand, automated reasoning [17:58] is uh essentially computerized formal [18:01] reasoning. [18:02] Uh there's extensive use uh already [18:04] today in industry for safety assurance. [18:07] And that's that's what it's all about is [18:09] correctness guarantees. [18:12] All right. So, hold that thought and [18:14] I'll tell you a little story. [18:16] Okay. So, we all know about this, right? [18:19] This emerging threat, what about [18:21] security in the age of AI? [18:23] You probably heard about things like [18:25] Project Glass Wing, you know, and this [18:27] kind of [18:28] uh feeds into the hysteria that uh [18:31] Francois was talking about. [18:33] Uh well, can can there can we help? Can [18:36] we do something about this? [18:39] Um [18:40] back in 2023, I was at a workshop at [18:43] Google [18:44] and uh a bunch of notable people there [18:46] talking about risks and worries and hey, [18:48] what if gen AI can find security [18:50] vulnerabilities? What are we going to [18:51] do? [18:52] Um [18:54] well, I was like, there is a solution. [18:56] If you formally verify all your code, [18:58] then it cannot be hacked. [19:01] Yeah, they didn't want to hear that. Uh [19:03] that's like too hard. And there's good [19:05] reason for that response, right? Um the [19:07] traditional formal verification requires [19:10] monumental effort, the automated [19:12] techniques are too weak or they don't [19:14] scale, just not economically viable. [19:17] Well, fast forward [19:19] to another [19:21] conference I was at. [19:23] Lots of discussion about risks and [19:25] worries of AI. [19:27] And then every talk before mine says [19:29] they there is only one answer and the [19:31] answer is formal methods. [19:33] Okay, that was not expecting that. [19:37] So, there has been maybe a little bit of [19:39] a shift in the attitude towards formal [19:41] methods. Is this warranted? [19:43] That's what I want to explore with you a [19:45] bit tonight. [19:46] Okay, so [19:48] what what are we concerned about? Well, [19:50] we're concerned about when I made this [19:51] slide it was future, I crossed it out, [19:53] present. [19:55] >> [clears throat] [19:55] >> Where AI systems create mountains of [19:57] buggy software, right? I don't know if [19:59] you're worried about that, I'm worried [20:00] about that. Or it dramatically increases [20:03] the capabilities of hackers to attack [20:05] legacy systems. So, we've got we're [20:07] you know, we're being threatened on both [20:08] sides here. [20:10] And [20:12] a lot of people are sort of looking to [20:14] formal methods like is there maybe [20:16] something here that can help us? [20:18] There's also a lot of excitement about [20:20] how great AI is at mathematics. Okay, [20:24] maybe that's a signal that something's [20:26] going on here. [20:27] Okay, but how do we get there? How do we [20:29] get from, you know, solving a millennium [20:31] problem to making your software secure? [20:34] Well, [clears throat] so AI is really [20:36] good at writing code, it's really good [20:39] at writing math proofs. [20:41] But it turns out there's a big [20:42] difference between writing math proofs [20:44] and securing code. [20:46] And so, bridging this gap is actually [20:49] something I've been thinking a lot about [20:51] last few years and I'll tell you a [20:52] little bit about what we're doing. [20:54] Okay, so I'm going to tell you about a [20:56] project called CS lib. [20:58] CS lib is inspired by the success of [21:00] math lib for mathematics, but the idea [21:03] is to build [21:04] computer science theory and also a a [21:07] platform for actually reasoning about [21:09] code. [21:11] Um [21:12] Okay, and we've got this great steering [21:14] committee including Leo de Moura, the [21:15] author of Lean. Uh [21:17] we've got some tech leads. We're using [21:19] Lean. If you don't know what that is, [21:21] you know, climb out from under a rock, [21:23] but um [21:24] Lean is a great theorem proving system. [21:25] It basically is a system that lets you [21:27] check the system itself checks every [21:29] step. It doesn't let you make a mistake. [21:32] Uh and this is really what we need when [21:34] we're dealing with uh you know, high [21:36] assurance situations. [21:38] Okay, so CS lib has two pillars. The [21:40] first is formalization of CS theory and [21:43] the second is framework for reasoning [21:45] about code. I'm going to tell you about [21:46] the second one. This is what I'm most [21:48] interested in and involved with. [21:51] All right, here's one slide about the [21:52] vision for CS lib. The idea is maybe you [21:54] take programs in all sorts of different [21:56] languages. You would rewrite them in [21:58] this uh common intermediate language. [22:01] You can then compile it down to [22:03] verification conditions in Lean and then [22:05] all you have to do is prove a bunch of [22:06] Lean theorems. If you can do that, you [22:08] showed that your code is correct. [22:10] Okay. [22:11] How far along are we on this? Well, [22:14] um [22:15] in terms of proving theorems in Lean, [22:17] you know, the AI is pretty good, but [22:19] also we have some techniques that are [22:22] much cheaper and better than AI like [22:24] Lean SMT, which is tool that we built in [22:26] my lab. Uh it can prove a lot of Lean [22:28] theorems, you know, in in milliseconds [22:31] on on a CPU. So, uh [22:33] the techniques for proving theorems in [22:35] Lean are just getting better and better. [22:36] So, that's great. [22:38] Um and now I'm going to tell you about [22:41] So, here we have [22:43] um [22:44] some code. This is in Rust. This is part [22:46] of the Dalek light uh [22:49] cryptography library. [22:52] And [clears throat] [22:53] um [22:53] actually this is uh Vera, so you can see [22:56] it has [22:57] uh some specifications, [22:59] uh uh some proof steps here and an [23:02] invariant. [23:03] Um now what I'll show you is [23:07] um that same code [23:09] uh has been translated into the Bull [23:12] language. So, this is um [23:15] the same procedure in Bull. You see we [23:18] preserve the uh pre- and post-conditions [23:20] and the invariants. Um but this is all [23:23] now embedded inside of Lean. [23:25] And so, we can call our VC gen uh VC [23:29] generator here. [23:30] And you can see that this generates 35 [23:34] goals. Uh each goal is a Lean theorem [23:37] that we have to prove. [23:38] And then um we'll try the SMT tactic. [23:42] This calls Lean SMT. [23:44] And you see that um that solves all but [23:47] three of the goals. And then we do one [23:50] more step where we unfold some [23:51] definitions, call SMT again. Uh and that [23:54] completes the proof. All the goals are [23:56] are solved. [23:58] Okay. So, what this is a little [24:00] prototype that we put together showing [24:02] how you can go from Rust to Bull to Lean [24:05] theorems, prove the Lean theorems, and [24:07] now you are able to show that the code [24:09] is correct. Um okay. [24:11] So, that's great. Now, suppose we [24:13] succeed and build this whole thing in [24:15] Lean. We have a way to reason about all [24:17] code uh in every language and prove [24:19] theorems about it. We still have a [24:20] problem, which is somebody's got to [24:23] write the specifications. Someone's got [24:25] to say what it are the properties that [24:27] that code should have. [24:28] So, can um maybe AI help us with this? [24:32] Okay, here we have a demo of our tool [24:34] called Verisforge. [24:36] And what you can do is enter [24:39] uh [24:40] a [24:41] specification in English of what you [24:43] would like to build. [24:44] And then it will uh build the code and [24:47] do the formal proof. So, we can do a [24:49] simple example. [24:51] Uh says find the maximum element in an [24:53] array of 32-bit integers. So, we click [24:58] here and first thing it will do is it [25:00] will generate a specification in [25:02] structured language here. [25:05] Um we can look at this and say yes, uh [25:07] we approve. [25:09] And then what it will do is go ahead and [25:10] generate uh Rust code and a Vera [25:13] specification [25:15] um based on [25:16] that uh structured language [25:18] specification. [25:20] And then it actually uh verifies it with [25:22] the Vera tool and checks that the spec [25:25] uh is unchanged. And so, now we have uh [25:28] fully automatically verified uh code [25:31] that has been generated. [25:34] >> Okay, so that's a toy example again. [25:37] Uh can we do better? Well, yes. [25:39] Actually, um in a recent uh archive [25:42] submission, uh we showed that uh 30,000 [25:46] line Rust program, which is a crypto [25:48] library, took uh five experts 3 months [25:52] or three three experts 5 months to do [25:54] were able to do it in 11 hours fully [25:56] automatically with our crypto prover [25:58] agent. [26:00] >> [clears throat] [26:01] >> Okay. So, that's just like a taste of [26:04] what I think can be done in the formal [26:06] methods space. I think formal plus AI [26:09] gives us a way to, you know, what [26:11] François was talking about, actually [26:12] build some really strong defense, uh [26:15] create some new primitives that could be [26:17] used to build up uh an AI safety stack. [26:20] I like to say that if AI safety is a [26:23] Mount Everest we have to climb, I think [26:25] that code reasoning is a good base camp. [26:28] Um there's also a couple of really [26:30] interesting things. So, if you imagine a [26:32] world where you have code reasoning at [26:35] scale as a new primitive, there are [26:37] interesting things you could do. For [26:38] example, if agents A and B meet each [26:41] other in cyberspace, and agent A says, [26:44] "Hey, I can provide this service to you, [26:45] agent B." Agent B says, "Great, show me [26:48] your code and your proof." And an A [26:50] shows it and says, "Great, okay, I trust [26:52] you. You can do that." [26:53] Uh that would be a cool uh future. [26:56] And the other thing that I kind of like [26:57] about this work is it's uh an example of [27:00] containment. So, you could put a super [27:02] intelligent AI into our crypto prover [27:05] agent. The only thing it can do is prove [27:07] your code correct. It can't do anything [27:09] else. That So, if we can imagine ways to [27:12] do those kinds of things, I think uh [27:14] we'll be able to benefit from AI without [27:17] you know, having a a [27:19] bad outcome. [27:20] Okay. Last thing I want to tell you is [27:22] just a teaser. Um I'm co-CEO of a new [27:25] company called And Truth. We are trying [27:28] to build a universal code reasoning [27:29] engine along the lines of what I told [27:31] you uh today. So, uh keep an eye out for [27:36] that. [27:38] And I'll end there. [27:39] Thanks. [27:41] >> [applause] [27:45] >> Thank you so much. [27:46] Okay. All right. Next up, Marco Koken [27:48] Derfer. [27:52] >> [applause] [27:55] >> All right. Uh so, here here's the [27:56] question. Uh if we build a system, maybe [27:59] it's an AI system, how do we know it's [28:01] going to be safe? And I'll tell you [28:02] about some of the research we've been [28:04] doing in the Stanford Intelligent [28:06] Systems Laboratory or Sizzl. My graduate [28:09] students call themselves Sizzlers. [28:11] And uh for a system with learned [28:13] components, um maybe it's a auto landing [28:17] system for an aircraft, [28:19] what evidence do you need to justify [28:22] deploying it? [28:23] So, for commercial air traffic, what [28:26] we're aiming for is about a 10 to the [28:29] minus nine probability of catastrophic [28:32] failure per flight hour. So, that's what [28:35] we were held to in the development of [28:37] the ACASX uh aircraft collision [28:39] avoidance system. [28:41] Now, if you were to directly simulate [28:44] these [28:45] uh scenarios, then you would need about [28:48] 10 to the [28:49] nine simulated uh hours before you [28:53] detect a [28:55] on average a a single failure. [28:58] And if you want to get a statistical [29:00] representation of these types of [29:04] failures, you're you're going to need [29:05] like like if you need 10, then you need [29:07] to run 10 to the 10 [29:09] uh [29:11] simulated hours before you get get those [29:13] 10. [29:14] So, that's typically [29:16] not super easy. Of course, you don't [29:19] want to spend your time simulating [29:21] situations where the aircraft are I [29:23] don't know separated by 5 miles and [29:26] don't really present a hazard. [29:28] Um [29:29] instead you want to simulate critical [29:31] scenarios that are representative of of [29:34] let's say the airspace. [29:36] So, how do you get that that [29:38] distribution? [29:40] Okay, we're [29:41] in in our lab we explore a number of [29:44] different kinds of approaches to [29:46] establishing trust in a system before [29:49] deployment. So, one approach is just [29:51] known as falsification where you search [29:54] the space of possible scenarios for [29:56] failures. [29:57] And if you find that your system results [30:01] in a bunch of failures and you look at [30:03] those failures and you have a bad [30:06] feeling in your heart, then [30:08] maybe you should just not deploy that [30:10] system or you need to think about [30:12] mitigations to help prevent those [30:14] those uh critical scenarios. [30:18] Often what we want to do is actually [30:20] estimate that probability of failure. [30:24] And [30:25] for this, you need to have a model that [30:27] you actually trust. So, for the [30:29] development of the ACAS X collision [30:31] avoidance system, we poured a huge [30:33] amount of effort into the statistical [30:36] modeling of the airspace. [30:39] Then uh another category is [30:41] verification, which is the the subject [30:44] of of Clark's lab and we've actually [30:46] collaborated for a number of years. But [30:50] the this is often treated as a different [30:52] community and we're finding [30:54] opportunities to to [30:57] bridge into that. [30:58] So our lab works on a variety of [31:01] different methods. So it turns out that [31:04] in order to establish confidence in a [31:06] system, there there is no one silver [31:08] bullet. [31:10] Probably formal methods won't take you [31:12] the whole way there. [31:13] Um although Clark is helping us get [31:16] further and and further. [31:18] Uh it really requires a number of [31:21] different kinds of approaches. [31:23] Uh we've also been looking at of course [31:25] palm DP planning, partially observable [31:27] Markov decision processes and these [31:30] kinds of methodologies allow you to [31:32] build extremely robust systems that are [31:35] robust to state uncertainty, outcome [31:39] uncertainty, interaction uncertainty, [31:41] model uncertainty and and so forth. [31:45] And we like to be driven by real-world [31:48] problems uh including aircraft, driving, [31:51] spacecraft, medical evacuation and so [31:53] forth. And I'll mention a few of these. [31:56] And uh we like testing them also in the [31:59] real world. Of course it's great if we [32:01] can simulate everything. Uh but our [32:04] inferences about safety is only as good [32:06] as the simulator. [32:10] One One kind of approach that we've [32:12] taken is known as adaptive stress [32:15] testing. So this came out of the work of [32:17] Richie Lee. He was one of my PhD [32:19] students and at the time he was also uh [32:22] civil servant at NASA Ames. And we [32:24] actually used it in part to help with [32:27] the validation of different flavors of [32:30] the ACAS X system. And uh since then a [32:33] number of students have uh, since built [32:35] a upon this this work. [32:40] So, [32:41] uh, recently we've been exploring how [32:43] can we take some of these insights that [32:46] we developed for the purpose of [32:47] validating aircraft and bring it into [32:50] the the world of validating language [32:52] models. So, this is some of the work [32:54] that my students, uh, [32:57] Hujun Liu and, um, [33:00] and, uh, Amelia Hardy and and others [33:03] have been leading. So, with in the [33:05] aircraft scenario, [33:07] a failure is kind of well defined, [33:09] right? It's metal on metal collision [33:11] where they come within 500 ft [33:13] horizontally and 100 ft vertically. For [33:16] these language models, what we care [33:17] about is, [33:19] uh, potentially toxicity. So, how do you [33:21] define that? That's a little bit more [33:23] nebulous to define. And for that, we [33:25] actually rely upon another neural [33:28] network to to provide that measure. And [33:31] for this, [33:32] uh, for this paper, we were using Llama [33:35] Guard to measure toxicity. [33:38] Now, we want to find the most likely [33:40] failure. And in these language models, [33:45] we use something [33:48] known as perplexity. So, we want [33:50] something that's as low perplexity as [33:53] possible or low log perplexity and as [33:55] toxic as possible. So, we want to be up [33:57] in in the top left corner here, uh, when [34:00] we, [34:01] uh, search the space of scenarios. [34:04] And if the most likely failure is super, [34:08] uh, [34:09] if we define a failure as a toxicity [34:11] above some threshold, if that's really [34:13] likely, then we should study it and put [34:16] in place some mitigations. [34:19] Another challenge is estimating the [34:23] probability of failure. And, okay, that [34:25] the weird, [34:26] uh, symbol there should be an E. It's an [34:28] expectation. One way to approach failure [34:32] probability estimation is to use a [34:34] important sampling, which is an idea [34:37] that has been around for a super long [34:40] time. The idea there is instead of [34:43] sampling from the the true distribution, [34:46] we'll call it P, you sample instead from [34:50] a proposal distribution, we'll call it [34:52] Q, that focuses the effort on on [34:56] scenarios that that are more [34:57] significant. But you have to then [35:00] re-weight them. And the re-weighting is [35:01] actually quite simple. You just weight [35:03] it by the different results by the [35:07] probability of your uh trajectory [35:11] according to the true model divided by [35:12] the probability of the trajectory [35:14] according to your [35:16] uh your proposal distribution. [35:18] And we've applied it to a number of [35:21] different uh domains. We've looked at um [35:25] uh bringing ideas from Gaussian [35:27] processes to help represent uh these [35:30] distributions. We've also looked at [35:33] uh normalizing flows, the use of [35:37] low-rank Gaussian mixture models to [35:39] represent these proposal distributions. [35:42] Uh we've also [35:43] been using uh diffusion models, which [35:46] has [35:47] um they have seen quite a bit of success [35:49] in other domains like image generation. [35:53] So, sometimes we don't just care about [35:55] the most likely failure. Instead, we [35:57] want to categorize all the different [36:01] kinds of failure modes. And these are [36:03] just two very simple two-dimensional [36:05] examples. The top one is an inverted [36:08] pendulum. And uh what you can see here [36:11] is uh over time the angle. And we have a [36:15] failure if if the pendulum uh exceeds an [36:18] angle. [36:19] So, in reality, it can fall over to the [36:22] left or or to the right. If if you could [36:25] afford to run [36:27] a gazillion simulations and um [36:31] and you look at the failures that that [36:33] would be the the true failure [36:35] distribution. Now, if you use just [36:37] regular adaptive stress testing, it'll [36:40] typically zero in on one of those [36:42] failure modes. Whereas, if you use this [36:44] uh diffusion-based failure sampling, it [36:47] will actually pick on uh pick up on both [36:49] of those [36:50] uh failure scenarios. And similar kind [36:53] of story for the lunar lander. [36:57] Uh [36:57] we've also been working on neural [36:59] network verification. Uh so, uh a while [37:02] ago, actually, some work initiated by [37:05] Francois, um we wanted to see if we can [37:09] approximate the lookup tables for the [37:11] ACASX uh collision avoidance system. I [37:15] just using some neural networks to to [37:18] with with the idea of compressing the [37:20] information. Now, of course, we we [37:23] didn't actually end up using neural [37:25] networks for the real system, but it led [37:27] to a really fun collaboration with uh [37:30] Clark Barrett's lab. [37:32] And led to the development of the [37:34] Reluplex algorithm and and later on the [37:36] the Marabou uh software framework. [37:40] And over the years, we've been uh [37:43] transitioning [37:44] the the use of Reluplex and and Marabou [37:47] to situations where you have a neural [37:49] network controller in the loop. [37:52] And uh some of the work by uh Chelsea [37:55] Sidrain and and Sydney Katz [37:58] um [37:59] um [38:00] pushed some advances in in that [38:02] direction. And then uh a student, Sam, [38:05] who Clark and I are supervising, are [38:07] looking at uh forward and backward [38:10] reachability [38:11] uh concepts. [38:13] We've also been doing work on POMDP [38:16] planning. [38:17] Uh [38:19] actually, one of our first efforts in [38:21] the lab when I started at Stanford was [38:23] to create a a very uh [38:26] simple open source framework for [38:28] specifying POMDPs. We wanted to make it [38:31] really easy for non-experts to specify [38:33] their their POMDPs. Kind of like for [38:36] CVXPY, uh the idea of Steven Boyd's [38:38] students was to make it really easy to [38:41] specify mathematical optimization [38:44] problems. So, that's what we wanted to [38:46] do with POMDPs.jl. [38:48] It's a a Julia library. [38:51] And uh my student Zach Sunberg, who's [38:54] now a professor at CU Boulder, [38:56] uh developed the POMCPow algorithm for [39:00] scalable POMDP planning. [39:03] Uh [39:03] we've more recently been looking at [39:06] constrained POMDPs. So, you might want [39:08] to impose a hard constraint on on your [39:12] problem. And we have also been exploring [39:15] directions involving multiple agents. [39:19] These are some of the domains we've been [39:21] looking at. Uh medical evacuation, my [39:24] student Body El Husseini Husseini, he's [39:27] actually a [39:28] uh an Army Black Hawk uh medevac pilot, [39:32] and uh he has developed a a framework [39:35] for [39:36] uh simulating these kinds of scenarios. [39:39] Uh I saw Duncan, he's been uh pushing [39:42] our efforts towards uh belief state [39:44] planning for spacecraft collision [39:47] avoidance. [39:48] And also working with Helen and and [39:51] others on using POMDPs to plan out uh [39:54] flight tests so that you can as [39:56] efficiently as possible [39:59] uh characterize the flight [40:00] characteristics of your aircraft. [40:03] Okay, so [40:05] that has largely focused on validation [40:08] prior to deployment of your system. You [40:11] also want to continue the validation [40:15] effort after deployment. Okay, and this [40:17] is sometimes called runtime monitoring [40:19] or runtime assurance. [40:21] Uh you want to validate uh what's going [40:25] into your decision system. So, the the [40:29] sensor inputs, we've done some work with [40:32] Airbus on integrity monitoring of [40:35] vision-based systems. [40:38] Uh you also want to monitor what is [40:40] happening in the internals of of the [40:43] system. And this has led to some work on [40:46] uh mechanistic analysis [40:49] uh for an aircraft system. And of [40:51] course, you also want to model uh and [40:53] monitor the outputs. [40:56] Okay, then there's a another [40:59] uh [41:00] set of [41:01] work on assessing the measurements. [41:06] So, uh [41:07] Anca Rusu and and others have been [41:10] uh pushing [41:12] the the frontier on AI evaluation. Um [41:16] uh we released the paper BetterBench. If [41:19] you go to betterbench.stanford.edu, [41:21] you can find uh all of the data about a [41:25] number of different benchmarks [41:27] uh and uh a number of lessons learned [41:30] and best practices there. [41:32] Uh [41:32] we've also been studying when do these [41:35] benchmarks stop being useful? When do we [41:38] have these uh saturations in these [41:41] benchmarks? [41:43] Uh we've also been looking at what What [41:45] do these failures look like um [41:48] in terms of token-level signatures, [41:52] uh reasoning failures. And we've also [41:54] been looking at issues of [41:57] uh human judges. [41:59] So, in fact, another safety-critical [42:02] area is the use of AI for mental health. [42:05] And we've been looking at evaluations of [42:08] mental health professionals. And we have [42:11] been actually quite surprised to find [42:13] that um [42:15] human mental health professionals [42:17] actually their opinions vary widely uh [42:21] including in in domains related to uh [42:24] self-harm. [42:25] All right, I'll wrap it up here just [42:28] mentioning our new trilogy [42:31] uh [42:32] So, the the first book is Algorithms for [42:34] Optimization. The the second edition [42:37] will come out in uh very early 2027. [42:41] Uh optimization is fundamental to [42:44] everything that that we do here. Um and [42:47] it's a basis upon which we optimize [42:50] decisions and that's covered in our 2022 [42:53] Algorithms for Decision Making book. I'm [42:56] super excited about this new book [42:57] Algorithms for Validation, which is [42:59] available for pre-order. It's coming out [43:02] next month. [43:04] And it tries to provide a comprehensive [43:08] story about how to go about validating [43:11] uh learning-enabled systems and and [43:14] other kinds of uh AI systems. [43:17] Um it's available from Amazon and also [43:21] turns out target.com. [43:23] Uh you can find the PDF of the book [43:27] online right now. And it includes both [43:31] the statistical methods that I mentioned [43:33] here as well as formal methods and [43:36] reachability methods as well. Normally, [43:38] these are treated as separate [43:39] communities, but we tried to unify [43:41] everything into a common language. [43:44] And I'll wrap it up here. Thanks. [43:47] >> [applause] [43:53] >> Okay. [43:54] Thank you guys so much. That was [43:55] amazing. [43:56] Um [43:57] So, I guess [43:58] really to start the conversation [44:01] uh you know, you guys saw this whole AI [44:03] safety stuff. You know, what what was [44:05] going through your mind when you saw [44:07] this latest uh uh hysteria [44:11] um saga going on? [44:13] Maybe let's start with Clark. [44:15] >> So So, I was not surprised because I've [44:17] been hanging out with AI safety geeks [44:19] for a while, and there's a good chunk of [44:21] them that have been saying this for a [44:23] while. And um [44:25] you know, I think my response has always [44:27] been [44:29] the future is has high uncertainty, [44:31] especially now. And so, it's a good idea [44:34] to invest in AI safety research. Um but [44:38] I also think it's not super helpful to [44:40] emphasize like worst-case outcomes when [44:43] you have no idea what the real [44:44] probabilities are. Um [44:47] and uh you know, any I think anyone who [44:49] says, "I know that this is going to [44:51] happen." or, "You know, it seems certain [44:53] this is going to happen." They're [44:54] They're just guessing. So. [44:58] >> Uh we've both both cared about AI safety [45:01] for some time. I think we started the [45:03] Center for AI safety was a 2018, 2017? [45:07] And uh it's fascinating to see that it [45:11] has captured international attention. [45:14] And uh [45:17] I hope that this will [45:20] uh lead to [45:22] taking safety more seriously. I kind I I [45:26] think that we need to borrow more ideas [45:28] from the aerospace industry. [45:31] And I can elaborate on uh Okay, fine, I [45:33] will. Uh [45:34] Please do. [45:37] >> There There There has actually been some [45:39] discussion of creating something like [45:41] the NTSB uh for AI, and I think that [45:44] could actually be a a good idea. Um [45:47] So, compared to the 1970s, we're 80 [45:50] times safer [45:52] uh in commercial aviation uh [45:55] than we are. Since Howard Hughes or uh [45:57] since the 1970s. 1970s to now, we're 80 [46:00] times safer. [46:02] And how did how did we get there? So [46:05] >> And what what would it what would it [46:07] what would it look like? What would it [46:08] be Would it be like an opt-in kind of [46:10] thing? Would it be like guidelines Would [46:12] it be strict like the FDA literally [46:14] approving data? How would it work? [46:17] >> Uh that that's a good question. So [46:21] the the key thing here I think is [46:23] independent. So NTSB was set up as an [46:26] independent agency in 1967. [46:31] And uh [46:33] there were put in place other aviation [46:36] safety reporting systems like ASRS and [46:39] that was a non-punitive [46:42] reporting system. [46:44] So that incentivized all the [46:46] manufacturers, the airlines to share [46:49] safety information. And to really take [46:53] every single accident seriously and draw [46:57] as much scientific knowledge from from [47:00] what went wrong. [47:02] Now it take that there are other systems [47:04] that uh were schemes that have built [47:07] upon this. In 2007, there there was also [47:10] the [47:12] uh [47:13] aviation safety information [47:16] analysis and reporting system or [47:18] something like that that also had some [47:20] form of immunity. [47:22] And I think we need to do something like [47:24] that. It's it's going to take a long [47:26] maybe uh [47:28] too long of a time to set up [47:30] a new agency. That's that's a big deal. [47:32] Uh [47:33] governments tend to be somewhat [47:35] inefficient. [47:37] Um the NTSB is also used globally. Um so [47:42] if an accident involves a component [47:46] manufactured in in the United States, [47:47] they'll actually go go to other [47:49] countries and investigate. [47:52] Um [47:53] >> To draw that analogy because it's such a [47:56] high [47:57] um hm [47:59] there's so much interested parties. [48:02] There is risk of regulatory capture and [48:05] things like that. And then like, you [48:07] know, if you look at uh medicine or you [48:09] look at legal, there's the aboard of [48:11] medicine. Even the internet has ICANN, [48:13] right? It which is also international, [48:15] self-regulated. DNS has been working [48:17] great. Um and there hasn't but like it [48:20] wasn't the case that, you know, imagine [48:23] the internet invent was invented that [48:24] same time that Google and Facebook were [48:26] like already public companies and they [48:29] were heavily [48:31] biased in the development of ICANN. And [48:33] maybe they said, "Hm, well, if you want [48:36] SSL, you actually need um Google or [48:39] Facebook to be the ones to give you SSL [48:41] certs. Or you want a domain name, well, [48:44] you really it's not safe to give [48:45] everyone domain names. Like we we should [48:47] be the ones to give you domain names." [48:48] So, there's some risk there. And then [48:50] even more so like um having government [48:52] intervention, there's uh uh this idea of [48:55] regulatory capture, which today, right [48:56] now, if you want to start Uber or Lyft, [48:58] you can't legally. [49:00] Uber, Lyft, DoorDash, Instacart are [49:02] grandfathered in on 1099. So, you [49:05] actually can't com- compete. Right? And [49:07] that's the concern that some people [49:09] have. How do you think about all that [49:11] stuff? I Maybe start with Clark. [49:13] >> Uh yeah, so uh I I was encouraged, you [49:16] know, by the recent um [49:19] Frontier Lab leaders saying, "Yeah, we [49:21] need independent evaluators." So, I'll [49:22] just say one one of the goals of my [49:25] company is to build systems that can be [49:27] that independent evaluator. And not just [49:30] not just someone that says, "Oh, well, [49:31] we're independent, so take our word for [49:33] it." Our goal is actually to produce [49:35] independently checkable certificates. [49:37] So, we would say, "All right, we've [49:39] checked this system, and here's the [49:41] certificate. You can now go check it [49:42] yourself, and you can confirm uh that we [49:44] got that right." So, I I think uh [49:46] independence is really important. Um I I [49:50] I there a lot of voices pushing for that [49:52] because I think it would be uh you know [49:55] a real shame if all of the safety was [49:58] left in the hands of the labs or or even [50:00] some um [50:02] some friends of the labs who claim [50:04] they're independent. Yeah. [50:06] >> Yeah, I I I think we need something in [50:08] the very near term before something like [50:11] that could could be set up. It could be [50:13] a not-for-profit or or something like [50:15] that. I mean, in in the space industry, [50:19] when you have a space launch, right? You [50:21] have a range safety officer who's [50:23] completely independent of the the [50:26] mission. Their only job is to make a go [50:29] no go go call based on objective safety [50:33] metrics. [50:34] >> Could it be as simple as a starting [50:36] position as just US GAAP, which is like [50:38] the US kind of the the [50:41] uh um [50:42] uh accounting principles uh generally [50:44] accepted accounting principles? It could [50:45] be generally accepted AI principles of [50:47] like deploying AI safety. Um and then [50:49] there's a KPMG and there's a uh you [50:52] know, uh um Arthur Andersen or you know, [50:55] whatever. That's like, you know, uh uh [50:57] Ernst & Young that's going to be that [50:58] you can choose, but you have to be [50:59] validated um before you do something. [51:03] Like, it shouldn't be everything. I [51:04] should still be able to train the theta [51:05] on my, you know, tiny box. [51:07] >> Yeah, I I I I I think we need to [51:10] develop, you know, best practices, [51:13] uh of course, but I think we also need [51:15] like a postmortem analysis as well. I [51:19] think we we need to take the validation [51:22] of AI seriously from a number of [51:24] different perspectives. [51:25] >> But, back to your point, I mean, I think [51:27] um [51:28] uh aircraft the airline industry does [51:30] that really really well. They don't rush [51:32] to print what happened. They do a They [51:34] have a full thorough review process of [51:36] every single accident that happens. [51:37] Right? [51:40] >> Do you have any [51:41] Um okay. So, [51:43] uh my last question for the both of you [51:45] is how tractable do you really believe [51:48] these current AI safety [51:50] um concerns to be? Specifically, maybe [51:53] the cyber uh defense issue, some of the [51:56] bioweapon issue, on the cyber offense [51:58] stuff where the models I can use a open [52:01] AI to make a you know, a cyber attack, [52:04] or I can use I can trick it to to doing [52:06] so, or I can um take an open weight [52:08] model, and then I I I would need some [52:10] defensive capabilities as we talked [52:12] about earlier. Um how the whole thing, [52:14] how do you think how tractable of a [52:16] problem is is this? [52:18] >> Yeah, I'll take a stab at that. So, I I [52:20] think um cybersecurity is going to [52:22] become very tractable. I think uh like [52:25] right now, you know, I was telling my [52:26] mother, um "Hey, if you prove the code, [52:29] it can't be hacked." And she was just [52:31] stunned, like, "Really?" You know, we're [52:32] trained by the media and by television [52:35] that like every system can be hacked. [52:37] And well, of course, it is true right [52:39] now. But uh it's quite possible, you [52:41] know, you can prove with mathematical [52:43] certainty that that you can't hack a [52:44] system. And I I I will predict that [52:46] within the next, I would say, [52:48] 3 to 5 years, um that'll just happen. [52:51] Like, all our systems will be completely [52:53] secure. Because it it with AI can [52:56] attack, but AI can also defend. And and [52:58] the AI defense plus formal methods [53:00] should get us there. [53:01] >> So, what what is needed to get us there? [53:03] To to have these lockdown systems? Is it [53:05] like zero trust architectures? Is it [53:06] like these best prac- even the admin [53:08] admin issue? Um how do you think about [53:10] it? [53:10] >> Yeah, I mean, I think we just need to [53:12] move to a new standard of code. [53:14] Actually, it's interesting you're [53:16] bringing up uh how [53:18] how airlines and and other industries [53:20] use, you know, very sound engineering [53:23] principles. Uh I like to say there's a [53:25] little dirty secret about software [53:27] engineering, which is it's not based on [53:28] sound engineering principles, it's based [53:30] on like, just write something and test [53:33] it and hope for the best. Uh but we [53:34] actually do know how to do that. I mean, [53:36] there is a mathematical foundation for [53:38] software engineering. I think we'll have [53:39] to see uh maybe to that. And And one [53:41] other thing I want to say in terms of [53:43] tractability of like securing AI itself, [53:46] uh I don't think we'll be able to reason [53:49] about, you know, these massive large [53:51] language models. So, I think our best uh [53:53] option is something more like securing [53:55] the boundaries. [53:56] Uh And securing the boundaries is also [53:58] very tractable. Um [54:00] trying to prove that, you know, a 500 [54:03] billion parameter model isn't going to [54:05] do something crazy, uh I think that's [54:08] that's not really tractable. [54:11] >> Completely agree with Clark on the [54:13] security thing. Like, I'm terrified of [54:16] um you know, [54:18] the next big thing being a massive cyber [54:20] attack. And but I think I I would agree [54:23] with Clark that I have a lot of hope for [54:25] that. [54:26] Um [54:27] but [54:29] you can't prove what's possible or [54:32] what's not possible with biology or [54:35] chemistry, right? Uh [54:38] that is uh that's an open question. But [54:41] I think that's what we have been [54:43] striving for as a species, where [54:46] increased understanding. And I think [54:48] that advances in AI will help us [54:51] um on average. I think on average we're [54:55] going to benefit from these new [54:57] insights. [55:00] >> Um I have a question specifically for [55:03] um [55:04] Clark here. So, um exactly walk me [55:08] through how it works. Let's say that um [55:10] you are now uh we give you $10 billion [55:14] to be the CISO for Bank of America. [55:18] Okay. What do they do? What's What would [55:20] you do? [55:21] >> Okay. So, first I would hire all the [55:24] formal people and uh [55:27] race race to build uh [55:29] the infrastructure that we need to [55:31] reason about that code. Then I would [55:33] say, "Okay, give me all of your code. Uh [55:35] uh, give me a whole bunch of GPUs and a [55:38] whole bunch of theorem proving agents [55:39] and we're going to just, [55:41] um, either prove the code as it is or we [55:43] could also just translate it into a [55:45] better language like Rust or Lean, prove [55:47] the code there and, um, and then you're [55:50] done. [55:50] So, there there's a lot of work to do [55:52] there, but I think it's, uh, it's work [55:54] that we know how to do. [55:55] >> And does that mean I have to finally get [55:57] to 100% unit test coverage? Is that Is [55:59] that what that means? [56:00] >> No, you don't. You, uh, so tests [56:02] actually become obsolete. I mean, tests [56:04] are Tests are always good as you're [56:06] developing. They're like the fastest way [56:07] to find bugs. Uh, but ultimately the [56:11] formal argument completely subsumes the [56:13] tests. [56:15] >> Um, all right. Now, for Michael, [56:18] um, [56:19] are you aware of [56:22] Waymo, um, you know, uh, [56:25] uh, some of the the [56:26] >> Yes. [56:27] >> [laughter] [56:28] >> A number of my students work there. [56:30] >> Next question. No. [56:31] >> Um, using, uh, AST diffs, uh, this is [56:36] some of the important sampling stuff, [56:37] uh, [56:38] you know, Marabou, Reluplex. Are you [56:41] aware that they're using this in their [56:43] validation and and their their theta [56:46] validation procedures after they train a [56:48] new a new model? [56:49] >> Uh, I can't speak specifically about [56:52] Reluplex or Marabou. Uh, Clark might [56:54] have some insights there, but adaptive [56:57] stress testing we released not just a [56:59] Julia version, but also a Python [57:01] versions for those who want to continue [57:04] using obsolete languages, but [57:06] >> [laughter] [57:08] >> um, [57:09] so we we [57:10] we made it open. We've had, uh, [57:13] a number of sponsors of our lab. We [57:16] we've been, uh, supported by very [57:18] generously by a number of different [57:20] automotive manufacturers including [57:23] Waymo. [57:24] Um, with the aim to, um, [57:27] uh, make these tools accessible not just [57:29] to them, but to the entire industry. [57:32] >> And I I And you talked about AST [57:34] Prompter, these are applicable to LLMs [57:38] as just as they are to a trained VAT [57:41] that would control a gas pedal and a [57:43] steering wheel, right? [57:44] >> Yeah, basically you need two You need [57:46] two things to use adaptive stress [57:48] testing. You need a definition of a [57:50] failure [57:51] and you need a measure of likelihood. [57:54] And you can have both This works for [57:56] language models, aircraft collision [57:59] avoidance systems. [58:02] >> And are you Do you have as much [58:03] engagement from [58:06] Anthropic and OpenAI and Grok [58:09] on those topics as you do as Waymo and [58:12] the [58:13] autonomous [58:14] vehicle sector? [58:15] >> Not yet. I mean, we we just published [58:17] AST Prompter. [58:19] We've been supported by [58:22] the Schmidt Sciences. [58:24] And the idea is to make all these ideas [58:27] as accessible as possible. [58:30] >> And do you think that they did adopt [58:32] they would have equal levels of safety [58:33] as the Waymos and and things like that? [58:37] Um [58:39] I don't know. [58:40] Uh [58:41] hopefully [58:42] that it's it's a different thing [58:44] validating physical systems than [58:49] you know, language models. Although the [58:51] methods can translate, the level of [58:55] success that you can anticipate might [58:57] vary a bit. [58:59] >> I mean, I've heard arguments that well, [59:01] um autonomy [59:04] you know, we can define the failure [59:05] modes pretty well if the thing stays on [59:08] the on the road, if it you know, if it [59:11] hits a baby and this and that. [59:13] And like and then I meet I I hang out [59:14] with Lane McIntosh and he shows me [59:16] examples of what the Tesla car actually [59:19] subverted and survived and didn't do the [59:21] bad thing and it was well outside the [59:23] distribution. It was a failure mode that [59:24] was not monitored or sampled in any [59:28] reasonable world. You could have There's [59:29] always a long tail, right? And some of [59:31] the long tail is a is always going to be [59:32] a high probability. Um and and then they [59:35] say, "Well, in in these And so in the [59:37] LLMs, you know, [59:39] can't we kind of isn't it kind of that [59:41] same Is is there Is it meaningfully [59:43] different long tail?" [59:45] >> Yes. I I I think you're exactly right. [59:47] So, I [59:49] even for A cast X, we know that the [59:51] probability is of failure is not zero. [59:54] >> Mhm. [59:54] >> I mean, we have simulations that show [59:56] that it fails in certain situations. [59:59] It's just that those situations are just [60:01] so incredibly unlikely. [60:04] That That I mean, the International [60:06] Civil Aviation Organization and the [60:08] Federal Aviation Administration, their [60:11] their standard for safety is not [60:13] probability of zero probability being [60:15] zero, right? [60:16] >> Right. [60:17] >> Uh we have to be realistic. If anyone [60:19] tells you they have created a a [60:21] completely safe system that interacts [60:24] with the in the real world, um and it's [60:27] fully safe, yeah, I I [60:29] I would would not believe that. [60:31] >> Clark's got some guarantees for us. [60:32] >> Uh Clark has some guarantees. Uh so, to [60:35] use Clark's method and or category of of [60:39] methods for formal methods, [60:41] um and correct me if I'm wrong here, but [60:44] you have to [60:46] it you're you're making these proofs [60:48] with respect to some model, okay? And if [60:52] you're modeling the real world, you have [60:54] to capture your uncertainty in what can [60:57] happen, like the accelerations of the [60:59] aircraft or or whatever. And so, you [61:02] generally have to assume bounds on that [61:05] uncertainty. [61:07] >> So, you have to estimate a nominal [61:08] distribution on the input, on what's [61:10] going to and on the transition function [61:13] of [61:13] >> So, in formal methods, you generally [61:15] don't assume anything about probability [61:17] distributions. You capture your [61:18] uncertainty in in [61:20] sets. [61:21] >> Right. Okay. [61:21] >> And and that that's a different approach [61:24] and it's great when it works, right? [61:27] Because you get a nice proof. And and [61:30] that that's wonderful. But the the [61:32] question then is do those uncertainty [61:35] intervals um are they sufficiently [61:38] realistic? [61:41] >> Just say something on that. So, um yeah, [61:43] a proof is always with respect to some [61:45] assumptions, right? And so in some [61:47] cases, you can make reasonable [61:49] assumptions and give strong guarantees. [61:51] I think what Michael's saying is it uh [61:53] if you have, you know, your input is [61:56] like another actor in the real world and [61:59] you assume that that actor is not going [62:00] to try to hit you with their airplane, [62:03] >> then uh that might not be a valid [62:05] assumption, right? So, so you do it is [62:07] really important uh when we talk with [62:09] about safety or about formal guarantees [62:12] that you understand it's with respect to [62:14] some assumptions. Now, there are some [62:15] things [62:16] that you can guarantee 100%, right? If I [62:18] prove my code is memory safe, then it's [62:21] it is 100% impossible for you to use a [62:24] buffer overflow attack to attack that [62:25] code. [62:26] >> Yeah. [62:26] >> Uh but there are other things that there [62:28] are limits to what you can do with [62:29] formal, right? I mean, uh the work we [62:31] did on verifying neural networks, you [62:33] know, [62:34] people would ask us, "Well, how are you [62:35] going to verify that this perception [62:37] network correctly identifies cats and [62:38] dogs?" And I was like, "Well, I don't [62:40] even know how to formally specify a cat [62:42] and dog, so that's beyond what formal [62:44] can do." So, so there are limits. You [62:45] have to be aware of that. That's [62:46] something that I think the formal [62:48] community has also really learned uh [62:51] hard lessons that you have to state [62:54] those assumptions or else people will be [62:55] disappointed. [62:57] >> Um so, last question for me, um what's [63:00] the Swiss cheese model? Are you making [63:02] like [63:03] grilled cheese sandwiches or something? [63:05] What's What's that? [63:06] >> So, uh we use the Swiss cheese model as [63:09] an analogy in aviation safety, right? [63:12] You have a number of layers of defense. [63:15] So, like for aircraft collision [63:17] avoidance, right? [63:19] Um maybe the top layer is like strategic [63:21] separation, right? Depending on whether [63:23] you're flying west or east, you fly at [63:25] different altitude layers. And then you [63:28] then you have another layer, which might [63:30] be air traffic control. [63:32] Um and then another layer could be your [63:35] collision avoidance system. [63:37] And we call it Swiss cheese because [63:39] these different layers have different [63:40] vulnerabilities, right? Those are the [63:42] the holes in the cheese. And what we [63:45] want to do is make sure that the holes [63:47] don't line up. [63:49] Okay? You don't want a critical scenario [63:51] to make its way through all the layers [63:53] of of the cheese. [63:55] >> And and is so then applying this to [63:58] these [clears throat] big large language [63:59] models that are big and scary, I mean we [64:01] control the training data, pre-train the [64:05] RLHF, the RSI, all the data that's being [64:08] sampled. We can take out the bad data. [64:11] We can run So, like Percy Percy's doing [64:13] this right now, where he's running a [64:14] small little model to look over the [64:16] pre-train data to take out bad stuff out [64:19] of the pre-train. Okay? Then it's that [64:21] stuff's never in the pre-train, so it [64:22] can't possibly learn those bad things. [64:24] And then you So, that's like step number [64:26] one. Now, you have a trained data. Let's [64:28] do a failure analysis on that data. [64:30] Okay, let's estimate failures. Let's [64:33] let's sample some failures. Let's [64:34] estimate some failure modes. Let's get [64:36] to a P fail, which I think, you know, [64:39] bad marketing. Let's get to one minus P [64:41] fail, which is P success. [64:44] And then tools, and then all the way to [64:46] runtime monitoring, right? Which you [64:48] mentioned earlier and happens as well. [64:50] Um yeah, what are your thoughts on that? [64:51] >> Yeah, you you need all these layers. Um [64:54] I I think the example you gave in your [64:57] opening remarks, they had like the chain [65:00] of thought monitor turned off, right? [65:03] That that would be one of those layers. [65:05] And I I think in addition to developing [65:08] these technical tools that Clark and I [65:10] have been working on, we also need to [65:13] make sure we put in the the proper [65:16] safeguards on the human level, right? Um [65:20] So, like I mean, we've learned this from [65:23] cybersecurity, right? [65:25] A way to the typical way of breaking [65:27] into a system is through human [65:29] engineering. [65:30] >> Yep. [65:31] >> Yep. Awesome. Okay, I'll open up to the [65:33] audience now. [65:34] Um okay, in the front. [65:36] >> [snorts] [65:38] >> And we got Mike coming. [65:43] >> Um I mean, this this question is for [65:45] Clark. So, you mentioned that um you [65:47] know, in a Bank of America like uh [65:49] example [65:51] I mean, most of the time, you know, then [65:53] the price code and the real world code [65:55] doesn't necessarily have a [65:57] specification. [65:58] So, in that case, like how would you um [66:01] formally verify this code? Would you you [66:04] know, get the I don't know, like spec or [66:07] a assumption assumptions from the the [66:09] source code itself or how would you do [66:11] that? [66:12] >> Yeah, that's a great question. So, I [66:13] think uh in the new world where it's [66:16] easy to write code and hopefully in the [66:18] next couple years it's easy to verify [66:19] code, the thing that's left that's hard [66:21] is the specification. But uh there are a [66:23] lot of things you can do. So, first of [66:25] all, there's a spectrum. Some [66:26] specifications are easy and universal, [66:28] right? So, if I have C code, I would [66:30] like it to be memory safe. Right? I can [66:32] write that specification once and for [66:34] all and just say everybody should, you [66:36] know, prove this is correct for their [66:37] code. Um [66:39] and for [66:39] >> the audience, what does it what does a [66:41] memory safe mean and why is that [66:42] important? [66:42] >> Yeah, yeah. So, that just just means [66:44] that it's never possible for your code [66:46] to access uninitialized or out of bounds [66:49] memory. [66:49] >> Who cares about that? [66:51] >> Well, if you can do that, you can most [66:53] likely run some kind of buffer overflow [66:55] attack, which uh you know, is famously [66:58] been used to gain access to all kinds of [67:01] systems. In fact, I think the number was [67:03] still sadly the number one security [67:06] vulnerability is buffer overflow. [67:08] Um yeah, so there are some specs like [67:10] that. [67:11] Uh there are also um sort of [67:13] domain-specific specs like for a bank, I [67:16] think they'd be interested in things [67:17] like no loss of funds. So, if I run a [67:20] sequence of [67:22] uh transactions, then the total amount [67:23] of money should stay the same. So, you [67:25] can you can come up with some of those [67:27] general uh things. Also, it turns out [67:29] agents are actually quite good at coming [67:31] up with specs. So, [67:33] uh I don't know if you've done a cloud [67:34] code session recently, but often what I [67:36] find is, you know, I tell I say, "I want [67:39] this." And it's like, "Oh, yes. And you [67:40] probably want this, this, and this, [67:41] too." And I'm like, "Yeah, actually, [67:43] you're right. I do want that." And so, I [67:45] think uh agents can help us write specs, [67:47] and I imagine a world where you have a a [67:49] sort of agent assistant that's like [67:52] talking to you and talking you through [67:53] the different corner cases and helping [67:55] you with that. So, I think there's a lot [67:56] you can do in that direction. [67:57] >> So, I mean, like for for example, you [67:59] know, in the open-source model, like [68:01] let's say, you know, you are formally [68:02] verifying a VLLM or SGLang something [68:05] like that. You could write, you know, [68:07] formal spec [68:09] um with assistance of agents. But how [68:11] would you know that, you know, the even [68:13] the the spec that agents, you know, [68:16] write is, you know, the same as the [68:18] developer wants or developer's intent? [68:22] >> Yeah, so that there is a gap there, and [68:23] you would have I think that's an [68:25] interesting research area, which would [68:27] be building uh tools and agents to help [68:30] cross that gap. But but even if you [68:32] don't cross that gap, I would argue that [68:34] if you ask your agent to write a bunch [68:36] of specs and prove them correct, and it [68:38] succeeds, you most likely have better [68:40] code than you would have had otherwise. [68:42] >> Thank you. And then going back to like [68:45] having a smarter model, I'm going [68:46] faster. The better the better better [68:48] these frontier models, presuming that [68:50] they're doing a good job and they're [68:51] good models, the better they can give [68:52] you tight specs. So, like, "Wait, you [68:54] didn't think about all these other [68:56] things. What about social attacks? When [68:58] someone calls and there's a person who's [69:01] been there for 1 month and they don't [69:04] really know anything. They don't want to [69:05] get fired. They don't want to make a [69:06] mistake and have an angry customer and [69:07] they're calling with their baby crying, [69:09] but it's fake and like you rush it and [69:11] then you give the thing I've seen these [69:12] videos on how they hack and [69:14] >> [clears throat] [69:14] >> and then you know, social attack. Well, [69:17] a spec you might put in there is if the [69:19] person has been there for less than 6 [69:20] months and [69:22] they haven't been through a you know, a [69:25] a fake [69:27] you know, social hacking scenario and [69:29] haven't passed safety training or [69:30] whatever, then maybe they don't actually [69:33] aren't can't give passwords to you know, [69:35] resets to new email addresses. [69:39] You know, some stuff like that. That you [69:40] can help you can think through all those [69:42] things scenarios, but anyway, yeah. [69:44] All right. [69:45] Excuse me. [69:46] In the front here. [69:52] >> Um so it sounds like you see formal [69:55] verification as some kind of rigorous [69:57] review process and drawing analogies [70:00] maybe aircraft collision avoidance. [70:03] Well, um maybe in engineering there's [70:05] generally some amount of regulation [70:08] since the safety standards that one [70:09] company might not match the safety [70:11] standards of another. [70:13] So do you see regulation being in any [70:17] way or shape or form involved in AI [70:19] safety? And if not, do you [70:22] have some means of incentivizing [70:24] companies to adopt your formal [70:27] verification engine? [70:29] >> Thank [70:30] >> Yeah. [70:31] >> [laughter] [70:33] >> Um yeah, I think regulation can can play [70:36] a role. [70:37] I think [70:38] Oh, uh the question was is there there a [70:42] role for regulations? Different [70:44] companies might have different I don't [70:47] know, uh [70:48] >> safety standards [70:49] >> safety standards [70:50] >> And if not, will how will you get [70:52] everyone to adopt your formal [70:54] verification engine? [70:56] >> Ooh, uh I think the last part about that [70:59] that the So in terms of regulation [71:02] um [71:03] uh one of my [71:05] uh collaborators over the years has been [71:08] Chris Gerdes. Uh he was a professor in [71:11] mechanical engineering at at Stanford. [71:13] He's now at Waymo. [71:15] Um but he worked on automated vehicles [71:18] and he was [71:20] he went to Washington D.C. to help the [71:23] Department of Transportation come up [71:24] with um [71:27] uh [71:28] regulations for automated vehicles. [71:31] In the end [71:33] I think he and and everyone there kind [71:36] of realized that it's a little bit [71:38] premature to [71:40] uh be too prescriptive in terms of what [71:43] technologies to use [71:45] but rather focus on higher-level best [71:48] practices and [71:51] um [71:52] and standards at that level without [71:55] being too prescriptive because this area [71:57] is [71:59] uh you know [72:00] there's a lot of innovation that has [72:02] been happening and and that will [72:04] continue to happen. I think the [72:05] important thing to realize is that [72:08] um [72:10] the various frontier labs, the various I [72:13] don't know automated driving companies [72:16] they don't want to compete on safety. [72:19] Right? It's not in Waymo's interest for [72:23] Zoox to have an accident and vice versa. [72:26] And so I think this is an opportunity [72:28] where [72:29] um the industry really needs to work [72:32] together [72:34] in their particular domains, right? [72:36] Automated driving, I mean those [72:38] standards are just going to be different [72:40] from language models or or other kinds [72:43] of applications of AI. [72:47] >> Yeah, so I about regulation I would just [72:49] say um I I do think there's a role for [72:51] it. I think you have to be careful like [72:53] Michael said not to be too prescriptive, [72:56] uh, but to find ways to incentivize, um, [72:59] general principles that would that would [73:01] be good for safety. Uh, in the specific [73:03] case of formal, you know, I've been [73:06] doing formal for 30 years trying to get [73:08] people to do it. It it's a bad idea to [73:10] try to tell people you have to do this [73:12] differently. Um, I think what's [73:13] different now is I think there will be [73:15] market forces that incentivize it. So, [73:18] if we can show that uh, formal is [73:21] automatable, work works at scale, and [73:23] gives you higher security, and a few [73:25] companies adopt it, then every other [73:27] CISO is going to be like, oh, we better [73:29] do that, too, or else, you know, we [73:31] won't have that same, uh, advantage. So, [73:33] I think, uh, we will see, you know, [73:35] strong market forces help, uh, I I think [73:38] actually all across AI safety. [73:40] >> And the one benefit that I think, um, I [73:43] I would like to underscore on on formal [73:45] methods is that you can leanify things [73:48] instantaneously now. Where before it [73:50] required so much time. You made that [73:51] point on one of your slides, but like [73:52] it's so important to really it's now [73:55] tractable. So, you you you lost people [73:57] because they said, oh, you just need to [73:58] hire 150, you know, [74:00] people who are, you know, PhDs in lean [74:03] to like go through all the Google code [74:05] and make this happen. Now you don't have [74:07] to. That's right. Right? You need like, [74:09] I don't know, [74:10] $100, $1,000 in tokens, right? Um, and [74:14] then on the on the it's really [74:15] interesting point that you made, uh, [74:16] Michael on, um, [74:18] this the incentive for Waymo not to [74:20] compete on safety. And I think the same [74:21] thing is true for the frontiers. No one [74:23] wants more attacks and and things like [74:26] and misuse of their models. That's bad [74:27] marketing for everyone. And um, and [74:30] Thomas Brown Tom Brown just actually [74:32] said that up in up in, uh, Napa. And um, [74:36] and I think what, uh, [74:38] we should also say is that they all just [74:41] went to the White House and signed a [74:43] document with these four four bullets. [74:46] So, I'd actually like they are actually [74:48] agreeing on independent [74:50] audits, some of these safety guardrails, [74:52] and all these other things. They they [74:54] all are going to do those things. All [74:55] All six of the labs, including Nvidia, [74:57] cuz Nvidia doesn't make Megatron. [74:59] They're not included in the conversation [75:00] very often, but they should be. Um so, [75:02] there are there are there is already a [75:04] framework for a self-regulation body [75:07] that doesn't need government oversight [75:09] and isn't punitive is the word you used [75:10] earlier. Okay. Um [75:13] let's go from this side in the back [75:14] there. Yeah. [75:20] >> Thank you. Question for Anthropic. Uh [75:23] curious, what what applications or [75:25] markets are you targeting first? And, [75:28] you know, how do you measure success in [75:29] the real world? [75:31] These specific applications you're [75:32] you're targeting. [75:33] >> Sure. Um so, I can't say too much about [75:36] that. What I will say is our our very [75:38] first priority is to build [75:40] uh the capability to reason [75:42] autonomously, automatically, [75:45] efficiently, with a about code at scale. [75:48] Uh we think it's sort of, you know, if [75:50] you've heard of these uh [75:52] labs talking about mathematical [75:54] superintelligence, this is like code [75:55] superintelligence. Like the ability to [75:57] really reason precisely about code. We [75:59] think once you have that, there's like [76:01] 100,000 things you can do with it. Um [76:04] you can imagine, you know, helping [76:05] enterprise. You can imagine helping [76:07] developers. You can imagine uh you know, [76:09] helping with security. So, um [76:11] So, yeah. [76:12] That's the direction we're headed. [76:14] Success is when all of the world's code [76:15] is verified. [76:25] >> Um first of all, thank you. Um second, [76:28] uh [76:29] when you are like [76:32] LLMs right now are an a system in which [76:35] humans are interacting with the code uh [76:37] with I mean [76:39] the interface. And I know like there's a [76:41] lot of prompt injection attacks that are [76:44] happening and maybe XSS attacks that can [76:47] happen through agents. [76:48] Do you think these type like how would [76:51] formal help in this sort of attack? I'm [76:54] just [76:56] >> Yeah, so uh [76:59] again there there's some difficulty [77:01] there if we're talking about natural [77:02] language from a human to an LLM, then [77:05] there's not really any part of that [77:07] that's uh code that we can prove [77:09] something about. Um but there are things [77:11] that can be done. So Amazon has a [77:13] technology called automated reasoning [77:15] checks [77:16] uh where they actually look at the [77:18] responses of an LLM and they try to [77:21] extract uh using auto formalization what [77:24] the domain knowledge is that the LLM's [77:26] trying to communicate and then they [77:27] check that against uh rigorous domain [77:30] model. So there are some techniques even [77:33] when it's all natural language that can [77:34] be leveraged to uh provide some security [77:38] and safeguards. [77:40] >> When I was learning CS there was like [77:41] SQL injection attacks, you know, Johnny [77:43] drop tables I think was the the classic [77:46] uh exploit CD. Um is there no equivalent [77:49] like a model to look at the um user [77:52] input and lint out uh prompt injection? [77:56] >> Sure, but that's an arms race, right? So [77:59] so you can [78:00] >> Always trying to outdo each other. [78:01] >> Right. [78:02] >> Um okay, let's I think we have two and [78:04] two. I'll go in the way back there. [78:07] Yeah. [78:10] >> Hi, so um yeah, this question's for [78:12] Clark. Um [78:13] so I'm curious in your Bank of America [78:16] example, uh even if you formalize all of [78:19] the software within Bank of America, [78:21] the software relies on a lot of a long [78:23] tail dependencies even down to the [78:26] hardware level. You'll have to maybe [78:28] formalize the x86 instruction set and [78:30] then you have to [78:31] >> It's been done. [78:32] The x86 instruction set has been [78:34] formalized by several companies. [78:36] >> Well, what do you think about things [78:37] like hardware level attacks like [78:39] rowhammer and that sort of thing? [78:41] >> Yeah, I mean I I think [78:43] probably software is low-hanging fruit, [78:45] hardware is a bit more difficult, but I [78:47] I do think that uh the eventual scope [78:51] would be you verify all the software, [78:53] you verify all the compilers, and you [78:55] verify all the hardware, and then you [78:56] call it a day, right? So, [78:58] I mean, why not? I think [79:01] AI is just going to get better, the [79:03] formal tools work really well with AI. [79:05] There's a bunch of startups doing [79:07] hardware verification with AI's help. I [79:09] think this technology is going to get [79:11] better and better. [79:13] >> Cool. Yeah. [79:14] You. [79:20] >> Yeah, so one thing I saw from a doctor I [79:23] know on LinkedIn was talking about how [79:25] if Waymo was like a pharma company's [79:27] drug, it would have gotten a waiver from [79:30] the US government for compassionate use [79:32] cuz it's been so effective at saving [79:34] lives. And so, I was kind of like you [79:37] know, curious about if there's like some [79:38] sort of like similar thing you can have [79:40] for like cybersecurity. You know, one [79:42] thing you have with a lot of like [79:44] enterprise systems, right, is that you [79:46] know, there's an admin team, right? And [79:48] then, you know, maybe it's these guys [79:50] aren't doing admin admin is their [79:52] password, but um you know, one thing [79:55] I've heard about is that you know, these [79:57] folks with admin or developer access [79:59] face threats themselves, you know, [80:02] crypto execs have gotten their fingers [80:03] cut off. Um the CEO of Adobe was [80:06] kidnapped in the '90s, I remember. And [80:09] well, I'm I'm kind of young, but I I [80:11] heard about it. Um [80:14] And so, [clears throat] I was curious is [80:15] like could you have an AI system that's [80:18] like so trustworthy that it could be [80:20] your admin? Is this even like possible? [80:23] Like you run it in like some [80:24] confidential virtual machine. Just kind [80:26] of curious about what your thoughts are [80:28] on this and like whether we can like [80:31] kind of limit the sort of physical [80:34] attack vector, you know, and have like [80:36] something that's like truly safe um and [80:39] and secure. [80:41] >> I'll take that one, I guess. [80:45] >> Yeah, I I think um a similar kind of [80:48] question comes up in the aviation [80:50] domain, right? Um especially with [80:54] um [80:55] uh aircraft-assisted suicides, [80:58] right? Um and concerns over mental [81:00] health the of um you know, human pilots. [81:04] So, um yeah, the the question is, why [81:07] don't you automate that? Just like how [81:10] you I think you're suggesting automating [81:13] the administration. [81:15] Um [81:17] So, [81:20] I think it might be a little while until [81:23] the Federal Aviation Administration will [81:25] entertain that. The the way things are [81:28] set up right now is that [81:31] aircraft, even if it's unpiloted, [81:35] um there's a pilot [81:38] who [81:39] is uh regulated and and certified by the [81:43] the FAA. [81:45] And if something goes wrong, they're [81:47] responsible for it. [81:49] So, I I think we need to think very [81:52] carefully about responsibility. [81:56] And that would be my concern with your [81:58] suggestion. [82:01] >> Yeah, I think the the Waymo [82:03] um [82:04] comparison is interesting one, right? [82:05] Like Waymo's not perfect, but it is [82:08] according to them, it is saving lives. [82:10] So, you could imagine making the same [82:12] argument there, but I think Michael's [82:13] point is a good one, like who who do you [82:15] blame if it uh doesn't go well? And does [82:19] the company that makes the AI admin, are [82:21] they willing to take liab- you know, [82:23] legal responsibility if something goes [82:25] wrong? If they are, then that suggests [82:28] they did a really good job with their [82:29] safety case. [82:31] >> And this is actually um goes back to the [82:34] point of like a a smarter and better AI [82:37] system. If you like there's the the one [82:39] system [82:41] um [82:42] trend in uh [82:45] in in uh information security is your [82:48] trust uh based architectures. And so [82:50] like you want to make sure that there's [82:52] zero trust in any one of these systems [82:54] that if you infiltrate one, you can't [82:55] infiltrate everything else. Um and [82:58] you know, if I had a a really smart [83:01] always-on AI system that's looking at [83:03] traffic and looking at my data dog, [83:06] looking at whatever is coming through [83:07] and they see, you know, a bunch of wires [83:10] going from the CTO, you know, to some [83:13] foreign account or something like that [83:15] or a bunch of keys just got generated [83:17] and shipped to a non-at-google.com [83:21] but to some Gmail, you'd be like, "What? [83:23] Hmm." You know, and then so with enough [83:25] like some things you don't have hard and [83:27] fast rules, but with enough context, you [83:29] can probably draw the line and be like, [83:30] "This is not cool. Let me flag it." And [83:32] just flag it to people. And so and and [83:34] we've all had, you know, these century [83:35] alerts for anyone that ran a company. [83:37] And it's like it's just a thousand of [83:38] these garbage alerts. And so you don't [83:40] look at them very often. And it's like [83:41] you know, the Acast has this issue as [83:43] well where you like death by a thousand [83:45] alerts. So you have to be really really [83:46] targeted and I think AI [83:49] uh [83:49] watching the system can actually do a [83:51] much better job with that. So. [83:54] Um we'll take two more. I think we'll go [83:56] here on the right here. [84:00] >> Hi. Um first, I'm really appreciative of [84:03] both of like I wanted to hear on formal [84:05] verification and then also like [84:07] standards and safeties uh especially [84:09] like in physical systems. Uh so having a [84:12] avionics professional or professor here [84:14] is great. Um I wanted to hear especially [84:17] because you touched on uh [84:20] dynamical systems based models like [84:21] diffusion models, normalizing flows. Um [84:25] right now we have the Chinese labs [84:27] pushing the frontier of efficiency. We [84:29] have the American labs pushing the [84:30] frontiers of intelligence and [84:32] capability, and we don't really have [84:34] anyone pushing the frontiers of [84:37] controllability and interpretability [84:39] from the start. We do have some fields [84:41] like developmental interpretability [84:43] where people are monitoring training [84:45] dynamics and emerging capabilities [84:48] uh and trying to fit uh math that we [84:52] have discovered throughout the fields [84:54] like and try to try to fit it to what [84:57] we're observing, but we I'm trying to uh [85:01] basically ask like do you think there is [85:03] room for constraining [85:06] uh training dynamics and intelligence [85:10] uh [85:10] or trying to map this [85:13] frontier of [85:15] uh [85:16] interpretability and control on one axis [85:19] and intelligence and capability uh [85:23] moving from traditional statistical [85:25] machine learning methods [85:26] uh and signal processing and control [85:28] theory over into uh yeah, deep learning [85:33] and neural networks. Also, I'm sure I [85:35] have uh messed up a lot of the terms I [85:37] mentioned. I don't mean to just add in a [85:40] bunch of buzzwords, but [85:41] >> Like uh filtering gradients in some way. [85:44] >> Uh okay. Yeah. Um [85:46] No, the the this is a great question. [85:48] So, I teach groups uh three times a year [85:51] I offer an executive education program [85:55] through the Stanford Graduate School of [85:57] Business to executives, and I do another [85:59] one um through HAI. And uh they're [86:04] executives from you know, all around the [86:05] world, and they're under a lot of [86:07] pressure to somehow come up with an AI [86:10] strategy and bring it into their [86:12] products or processes. And what I remind [86:15] them at the very beginning is of the [86:19] fundamental principle of engineering. [86:22] The fundamental principle of engineering [86:24] is very similar to the fundamental [86:26] principle of science, which is Occam's [86:28] razor. You know, simplest explanation is [86:31] more likely to be true. In engineering, [86:33] the [86:34] uh simpler, more interpretable method is [86:37] more likely to be robust. [86:40] And so, depending on their application, [86:42] they should really be [86:44] like if you can get away with linear [86:46] regression or decision trees, you should [86:48] you should be doing that. There's a lot [86:50] of temptation right now to go straight [86:53] to neural networks and transformers and [86:56] and all that. Uh but that's that's often [86:59] not the right way to to go. [87:01] Um and so, I [87:04] uh [87:05] I encourage everyone to [87:08] try out the simplest method and then try [87:10] something maybe a little bit more [87:12] complicated and see if the performance [87:15] lift justifies that additional [87:17] complexity. If not, then stay with the [87:20] more interpretable method. But I I think [87:23] this is a a very important topic. In [87:25] fact, one of the chapters in the new [87:26] validation book is on explainability. [87:30] And that that was critical in getting [87:32] AXI [87:33] accepted as an international standard. [87:36] >> Uh really quick like follow on. Like, do [87:38] you think that it [87:40] there is like market uh incentive or [87:43] like enough uh like demand like where we [87:46] could [87:47] people building like [87:50] constrained intelligence [87:52] uh [87:54] like [87:57] they would be able like it would be [88:01] feasible uh to compete with like with [88:04] the frontier labs. [88:07] >> So, so I would say that if you um manage [88:11] to create something that is measurably [88:13] safer, [88:15] then that would be a competitive edge, [88:17] for sure. And And I know that there are [88:19] people out there thinking about how to [88:20] do that. So, you know, hopefully they [88:22] can figure that out. [88:24] >> And if you, uh, [88:26] uh, looking to start a company, there's [88:27] these accelerators [88:30] that you could apply to, and they give [88:32] you money and guidance. [88:34] Um, okay. [88:35] Anyway, yeah, you in the back there. [88:37] Yeah. [88:41] >> Hi, thank you so much. So, my question [88:43] is internet era taught us a lot about [88:45] security. [88:46] Uh, so what do you think will we, like, [88:50] copy from the internet era, or what we [88:52] will learn something new from the [88:54] internet, uh, uh, [88:56] this [88:57] generative AI era? [88:58] Or, uh, authentic security, especially. [89:03] >> So, that's for you. [89:05] And for you guys. [89:07] >> Uh, so, is the question what can we [89:09] learn from the internet era that we [89:11] could apply in the current era? [89:13] >> Yes, and, uh, what do you think could be [89:15] different from the internet era, as [89:17] well? [89:20] >> Yeah, so I remember going to a talk when [89:22] I was a young professor at NYU, [89:25] uh, on security, and basically said [89:28] there are only two problems. [89:30] One is people, and the other is computer [89:32] bugs. [89:33] >> Yes. [89:34] >> So, I think we I think we can fix the [89:36] computer bugs, but I don't think we can [89:38] fix the people. [89:39] >> [laughter] [89:40] >> Uh, we But, but what's different is, I [89:42] think, um, AI can be used in all all [89:45] sorts of different creative ways. So, it [89:47] could be used, you know, as Francois was [89:48] saying, as kind of a a watchdog to maybe [89:52] like catch some of the social [89:54] engineering. Uh, it can certainly be [89:55] used to accelerate things like formal [89:57] methods to, you know, secure the [89:59] systems. Um, [90:02] yeah, may maybe even the, uh, AI admin [90:05] idea is a good one, as long as there's [90:06] still some humans in the loop. Um I [90:09] always worry, you know, I don't know if [90:10] any of you are [90:12] ever watched the movie WarGames, old old [90:14] school, but but you know, you turn [90:16] everything over to the computers and [90:17] then there's nobody if if there's [90:19] something weird happens like uh that can [90:22] go off the rails. So, I think we do need [90:24] humans in the loop. [90:26] >> Um there's a famous physics paper called [90:29] More Is Different and um and it's kind [90:32] of like the premise and like, "Okay, if [90:34] I have, you know, one atom, and two [90:36] atoms, if I have a bunch of atoms, I [90:38] have a whole lot of atoms, black holes [90:40] start to form, like light can't escape, [90:42] light just does a loop and comes back." [90:44] So, there's weird stuff. So, more is [90:45] different. And I think in this world [90:47] where we had 6 billion people and now we [90:50] have 7 billion people and now we have [90:51] 700 trillion agents that are let's just [90:55] say at equal intelligence or have some [90:57] motive and I can spawn all these [90:58] different agents, more is just so [91:00] different. And so, yeah, we had [91:02] CloudFlare being able to stop DDoS's, [91:05] but like [91:06] everything breaks when you hit when you [91:08] apply infinity to the to the number, [91:10] everything breaks. And so, weird stuff [91:12] can happen that exposes it. And I wrote [91:14] the tweet today basically like, "There's [91:16] a lot of systems that we just saw this [91:17] with Iclear where 60,000 submissions [91:20] submitted in 1 year, which is greater [91:23] than the cumulus summation across all [91:25] submissions in all history in 1 year." [91:27] So, that that's like a big exponential. [91:29] That E, the constant up there is a big [91:31] number. And so, all review systems, [91:34] which we we have many at uh Focal, for [91:37] example, looking at the Century Alerts, [91:38] looking at um customer, you know, [91:41] support tickets, or whatever. If imagine [91:43] college college admissions. Like a um [91:47] you know, uh [91:48] a Nash equilibrium, you know, optimal [91:50] strategy for every single all all high [91:53] school students is to apply to every [91:55] single school in America. [91:57] Why would you In fact, actually, sorry, [91:58] the whole world should apply to all [92:00] schools everywhere. [92:01] >> Yeah. [92:02] >> Right? [92:03] It's expensive. Well, it's they're going [92:05] to have to charge money. [92:07] Yeah, if there's if there's, you know, [92:08] if there's no fee, then then that's kind [92:10] of the what has to happen. [92:12] And then so how do you actually handle [92:13] these human review in the loop systems? [92:15] They get DDoS really hard. Um a real one [92:18] that that just got discussed was um [92:20] small claims court. So if your agent can [92:22] file a small claims uh [92:24] on for you and you don't need a [92:26] lawyer anymore. [92:27] >> Yeah. [92:29] >> What happens to the judicial judicial [92:30] system? It's completely bogged down. It [92:32] already takes too long to get through [92:34] the judicial system, but now it's going [92:36] to be insane and impossible. And so all [92:38] these systems need to be reevaluated. [92:40] And so the more is different is really [92:41] the learning that is going to be [92:43] meaningfully different, I think, from [92:44] the internet era from to to to now. We [92:47] thought we knew what big scale was, but [92:49] like human traffic will be 0% of [92:52] internet traffic. [92:54] Like [92:55] That's going to be a zero is a very [92:57] small number. [92:58] >> Thank you. [92:59] >> Okay, we have time for one more [93:00] question. Yeah, please. [93:05] >> Um thank you. So this question is about [93:08] benchmarking the benchmarks and the [93:11] context is that I'm working in AI safety [93:13] at LinkedIn and [93:14] um [93:15] the definitions of harms drift very [93:18] fast. [93:19] Uh even looking at something so small as [93:22] toxic text or bias [93:24] every 5 year the new generation has a [93:27] new slang for everything. So uh how do [93:30] you make sure that that slang doesn't [93:32] show up in uh say hiring uh in the uh [93:36] messages that you get from recruiters? [93:38] Um how do you [93:41] do how do you measure that right now is [93:43] benchmarks, but benchmarks move very [93:46] slowly. The public even in-house [93:48] benchmarks have to be [93:50] uh very costly and uh need to go through [93:52] a lot of human review. [93:53] What are your thoughts on how do we go [93:56] uh from current uh [93:58] state of the art? some labs publishing [94:01] benchmarks and slow creation of [94:04] benchmarks to a state where benchmarks [94:06] are dynamic evolve as quickly as terms [94:10] evolve? [94:13] >> Yeah, great question and I I like your [94:15] example there. [94:16] Um [94:18] Yeah, I I think we [94:19] just like how I advocated for a [94:21] continuously monitoring our AI systems, [94:24] we should continuously monitor our our [94:27] benchmarks. [94:28] And uh [94:31] the good news is that there are some [94:32] quantitative methods for identifying [94:34] distribution shift and um monitoring [94:39] shift in language I I think we we just [94:41] need to do. [94:45] >> Nothing to add there. [94:47] Okay. All right, here's one more. Last [94:48] one. [94:50] >> I'll just follow up with regard to [94:52] better bench. I think one thing that I [94:54] keep [94:56] uh [94:57] follow up with regard to better bench. I [94:58] think one thing that I see researchers [95:00] keep running into is that some common [95:03] evals, I'm looking at you math 500, have [95:06] broken pieces to them. [95:08] Uh [95:09] I feel like somebody and maybe it it's [95:12] your group there needs to be some kind [95:14] of coordination with hugging face or [95:15] somewhere where agents will centrally [95:17] find that these resources have these [95:19] problems. I think that just like we put [95:23] up [95:24] you know, reports that different [95:25] benchmarks are broken or different evals [95:27] are broken and then it just sits there. [95:28] Like I have this paper, but [95:31] some I'm just open call for somebody to [95:34] like close the loop here. [95:36] >> Yeah, I think uh I've seen that as well. [95:39] You know, I had former student who was [95:40] trying to evaluate um [95:43] uh SQL queries and nobody could get [95:46] better than like 70% and then he showed [95:48] that like 30% of them were actually [95:50] wrong. [95:51] So, uh I think it's just a matter of [95:53] people moving too fast, being a little [95:56] careless, and hopefully, you know, the [95:59] people who are rigorous will eventually [96:01] catch up and fix it, but it's a little [96:03] bit of an arms race now cuz everyone's [96:05] trying to move so fast. I don't know. [96:07] >> Yeah, we we need version control and [96:10] pull requests, issue filing, and and so [96:13] forth. Absolutely. [96:15] >> I actually think that a great idea for a [96:17] startup is like a Apple App Store of [96:20] benchmarks where there's curation, [96:23] right? Like like that they don't just [96:24] let anyone just throw an app onto the [96:26] App Store. They go through a process. [96:28] They they determine whether or not you [96:29] should be on the App Store or not. [96:30] Hugging Face, all due respect to Clem, I [96:33] love them, but it's a mess. [96:36] It's a mess. [96:38] It's [snorts] like the wild It's like [96:40] GitHub. It's like the wild west. And so [96:42] like trying to find like the appropriate [96:44] GSMA K, like it's actually non-trivial [96:46] to find what is the actual right GSMA K [96:48] cuz there's 600 different things called [96:51] GSMA K. It's like which one do I use? I [96:53] don't know. Anyway, [96:54] please everyone help me thank Clark and [96:58] Michael for joining us tonight. [96:59] >> [applause] [97:04] >> Thank you so much.