AI Safety Fact vs. Fiction | YC Paper Club

This YC Paper Club session treats AI safety as an engineering discipline with its own methods rather than a debate about doom. The host, Francois, opens by arguing that recent coverage has drifted into hysteria, but most of the hour belongs to Clark Barrett and Mykel Kochenderfer, Stanford professors who co-direct the Stanford Center for AI Safety, explaining how evidence that a system is safe is actually produced.

Barrett works on automated reasoning: instead of testing code and hoping, you prove it meets a formal specification, and a proof checker such as Lean confirms every step. He describes CSLib, a project to build a Lean-based framework for reasoning about programs written in different languages, and demonstrates tools that turn an English description into a structured specification, then generate Rust code and verify it. He presents formal methods combined with AI as a strong defense against AI-assisted hacking and predicts that within three to five years systems will be completely secure, which is his forecast rather than a result. He is also explicit about limits. A proof holds only under its assumptions; some properties can be guaranteed outright, such as memory safety ruling out buffer-overflow attacks, but others, like whether a vision model correctly tells cats from dogs, cannot even be written down formally. He does not think proving the behavior of a very large language model is tractable, so he would secure the boundaries around it instead.

Kochenderfer brings the aviation approach. The ACAS X aircraft collision-avoidance system was held to about one catastrophic failure per billion flight hours, a rate too rare to confirm by simulating flights at random. His lab instead uses methods such as adaptive stress testing, which searches for the most likely ways a system fails, and importance sampling, which concentrates simulation on risky scenarios and reweights the results to estimate the true failure probability. His students have applied the stress-testing approach to language models, using a classifier to flag toxic output as the failure; he says the method needs only a definition of failure and a measure of likelihood. He adds monitoring after deployment and work on judging benchmarks, and cautions that while the methods transfer from physical systems, the level of success may vary.

Both speakers end in the same place. Kochenderfer says he would not believe anyone who claims a fully safe system that interacts with the real world, and describes aviation's Swiss cheese model, in which several imperfect layers of defense are arranged so their weaknesses do not line up. Both also favor independent oversight, with Kochenderfer suggesting an independent body like the NTSB for AI, backed by the kind of non-punitive safety reporting aviation uses, and Barrett describing evaluators that issue certificates others can check for themselves.