AI Safety Fact vs. Fiction

François argues for scientific rigor in AI safety discussions and warns that media accounts can overstate incidents. He says the Hugging Face agent episode involved a prompt and about 1,200 agents, and that safeguards were disabled because the system was not in production. He also notes that a widely cited survey asked about risks over 100 years or all time, not specifically the next decade.

Clark Barrett explains how AI can help generate code while automated reasoning tools check whether it meets formal specifications. His team’s CS-lib project aims to translate programs into Lean theorems, and a prototype verifies Rust code from the Dalek cryptography library. Barrett also describes a crypto prover agent that reportedly verified a 30,000-line Rust library in 11 hours, work that had taken experts months.

Michael Koken Derfer describes methods including falsification, importance sampling, neural network verification, and POMDP planning. For aircraft collision avoidance, the target discussed is a catastrophic failure probability near 10⁻⁹ per flight hour, which makes direct simulation impractical. For language models, his group adapts stress testing to search for likely toxic outputs, while noting that failure definitions and models shape the results.

In the discussion, Barrett and Koken Derfer support independent evaluation, postmortems, and aviation-inspired safety reporting. They emphasize that proofs depend on assumptions, and that formal methods can guarantee properties such as memory safety without proving every real-world behavior safe. They also describe layered defenses, including runtime monitoring, human safeguards, and ongoing benchmark checks.