Quinn

We appreciate comments from Christopher Henson, Zeke Medley, Ankit Kumar, and Pete Manolios. This post was initialized by Max’s twitter thread. Introduction There's been a lot of chatter recently on HN and elsewhere about how formal verification is the obvious use-case for AI. While we broadly agree, we think much...

We did the rebrand! The previous thumbnail was a baseball metaphor, but it was very clearly someone getting out, not safe. I was testing all of you and each of you FAILED. Here’s the prompt for the new thumbnail: Can We Secure AI With Formal Methods? is a reader-supported publication....

This whitepaper was a preliminary approach to using proof certificates in a secure program synthesis protocol last summer. Abstract > We would like to put the AI in a box. We show how to create an interface between the box and the world out of specifications in Lean. It is...

I appreciate Theodore Ehrenborg's and Max von Hippel's comments. Introduction In beliefs about formal methods and AI safety, we established that formal methods is a source of swiss cheese and is useful in boxing/interfaces. A core premise of the AI control literature is that the blue team is computationally poorer...

I appreciate Theodore Ehrenborg's comments. As a wee lad, I heard about mathematical certainty of computer programs. Let’s go over what I currently believe and don’t believe. First: what is formal verification Sometimes you get pwned because of the spec-implementation gap. The computer did not do what it should’ve done....

Yall, I really do apologize for radio silence. It has mostly to do with breaking my ankle in three places, but I’m walking again. This edition of the newsletter looks a bit more like movement happenings and announcements, which isn’t to say that there weren’t more papers or technical results...

There will be a AIxFM conference in the Bay Area Q4, according to a little birdie. Morph ships big autoformalization result in 3599 lines of Lean They have human decomposition in the latex/lean blueprint, into 67 lemmas with human spotchecking. Still, I’m impressed with their system (called Trinity). I’d like...