HackTalk: Quinn Dougherty (Forall R&D)

​HackTalk: Quinn Dougherty (Forall R&D)

​Pre-hackathon talk for the Secure Program Synthesis Hackathon, May 22-24 online. Free and open. Recording available after.

​If you want a concrete list of where formal methods could buy something real in the ML stack right now, Quinn has one. The talk is built around Tractable: a catalog of 17 formal-methods opportunities across the ML training and inference stack, working from the premise that we should treat ML infrastructure with the same seriousness we treat airplanes.

​Quinn Dougherty runs Forall R&D and the Beneficial AI Foundation. He co-organizes the SPS Fellowship with Atlas Computing and chairs the technical committee for this hackathon. He's the author of FVSpec, Lean 4 benchmarks for formal verification of code, both ARIA-funded. Previously at QURI.

​Topics: Tractable problems in AI security via formal methods, where Lean 4 benchmarks fit in, and the open problems that map onto this hackathon's four tracks.

​Format: 15-25 min talk + ~15 min Q&A. Zoom, livestreamed and recorded.

​Co-organized by Apart Research and Atlas Computing.