Mapping Civilization's Resilience Gaps w/ Dr. Evan Miyazono

Yeah.

The starting focus was to take.

to compliment Davidad's approach of what is the world we want to build toward with safeguarded AI, where we have evidence-backed quantitative safety margins with AI systems backed by formal methods, He was building for a future that could exist and trying to work backwards to today.

And the idea of Atlas was to start from today and work into the future, what things would have to be true in order for safeguarded AI to be very successful.

And the biggest hypothesis that seemed untested at the time was If Safeguard AI works, then there are a lot of people who have gotten very good at doing formal methods because that was kind of a prerequisite in the tech tree for Safeguard AI.

And that wasn't the technology side of it.

It was really the user willingness and understanding of why formal methods was useful and Maybe this is

a great time then to give me a lesson on why formal methods is useful, just to make sure, because I totally know it really, really well.

But, you know, just in case.

Evan did explain things, but as is the case when you're asked to explain a highly technical concept off the cuff, it was a bit windy and there was a tangent or two.

So here's the streamlined version.

Formal methods are a family of mathematical tools which allow us to reason about how correct a system is.

Formal verification is essentially an application of these tools to check whether a given program is correct.

Before getting into formal verification, I think it's helpful to first establish the three translation points where things can go wrong on the road from having an intention in your head to having the thing in the real world.

Let's say I want a naturally lit place to work in my home.

This is the intent, or the thing in my head.

After thinking about it a bit, I hire some contractors and I tell them I want a two meter by three meter window on my south facing wall.

In providing these instructions, I've translated my intent to a specification.

The contractors get to work and some indeterminate amount of time later, I have a window.

They have translated my specification into an implementation.

Finally, I can begin working next to my new window, translating the implementation into what actually happens in the world or reality.

As I said earlier, each of these translation points represents a place where things could go wrong.

Formal verification closes the gap between specification and implementation by introducing a mathematical proof, which demonstrates based on some fundamental model of the underlying hardware or programming language that you're working with, that it must meet all the characteristics in your specification always.

So if I had some sort of formal verification in this case, I would be able to say with extreme confidence that there was a 2 meter by 3 meter window on my south facing wall.

However, this doesn't address the gap between my intent and what I asked for.