AI Safety Fact vs. Fiction | YC Paper Club

The event opens with François Bonneau arguing that recent AI safety discourse has devolved from scientific rigor into sensationalism and hysteria. He provides historical context showing that major technological breakthroughs—from nuclear weapons to the internet—have consistently generated unfounded catastrophic predictions. Bonneau discusses the Hugging Face incident as a case study of media misrepresentation, noting that headlines claiming AI acted autonomously were factually incorrect; the incident involved prompted agents with monitoring systems that were simply disabled. He also examines the '10% P(doom) in 10 years' statistic, revealing it originated from a survey asking about extinction risks over 100 years, not a decade, demonstrating how misquotation propagates through the discourse.

Clark Barrett presents automated reasoning (AR) as a complement to AI capabilities. He explains how formal verification can provide correctness guarantees that AI alone cannot achieve. Barrett describes CS lib, a project inspired by mathematical libraries, designed to formalize computer science theory and build frameworks for reasoning about code. He demonstrates a prototype showing how Rust code can be translated to the Bool language, embedded in Lean (a theorem proving system), and automatically verified. Barrett presents Verisforge, a tool that accepts English specifications and generates formally verified code. He highlights that a 30,000-line Rust cryptography library took five experts three months to verify manually but only eleven hours with their automated crypto prover agent. Barrett emphasizes that code reasoning provides containment capabilities—a superintelligent AI could be restricted to only proving code correctness, preventing it from performing other actions.

Michael Kogut discusses validation methodologies developed for safety-critical systems like aircraft collision avoidance. He explains that commercial aviation targets a 10^-9 probability of catastrophic failure per flight hour, requiring enormous simulation efforts to validate. Kogut introduces adaptive stress testing, a technique developed with NASA to identify failure scenarios efficiently rather than exhaustively simulating all possibilities. He describes how these methods are being applied to language models, using perplexity as a likelihood measure and separate neural networks to evaluate toxicity. Kogut discusses importance sampling for failure probability estimation and diffusion models for capturing multiple failure modes. He emphasizes that no single method provides complete safety assurance; instead, a layered 'Swiss cheese model' of defenses is necessary, with each layer having different vulnerabilities that must not align.

The discussion addresses regulatory approaches, with both speakers cautious about prescriptive regulations but supportive of industry collaboration on standards. They reference the aviation industry's evolution to 80 times safer operations since the 1970s through independent agencies like the NTSB and non-punitive reporting systems. Kogut proposes applying similar models to AI through centralized benchmarking and independent evaluation frameworks. Barrett and Kogut discuss how formal methods have become more tractable with AI assistance, potentially automating specifications and proofs that previously required extensive manual effort. They acknowledge limitations: formal methods work best for well-defined specifications and cannot verify properties like whether a neural network correctly identifies cats. The speakers emphasize human elements remain critical, particularly in social engineering vulnerabilities, and that humans must remain in the loop for accountability.

The event concludes with audience questions addressing practical implementation challenges, including how to specify requirements for existing legacy code, how to handle upstream dependencies and hardware vulnerabilities, and how to maintain dynamic benchmarks as language and harm definitions evolve. The speakers advocate for market-driven adoption of safety practices, arguing that companies adopting formal verification and rigorous validation will gain competitive advantages, incentivizing industry-wide adoption without heavy-handed mandates.