I’ve been hearing vague claims that automated theorem provers are able to, or will soon be able to prove things about complex software such as AIs.

Max Tegmark and Steve Omohundro have now published a paper, Provably Safe Systems : The Only Path To Controllable AGI, which convinces me that this is a plausible strategy to help with AI safety.

Context: looking for an alternative to a pause on AI development.

There’s some popular desire for software decisions to be explainable when used for decisions such as whether to grant someone a loan. That desire is not sufficient reason for possibly crippling AI progress. But in combination with other concerns about AI, it seems promising.

Much of this popular desire likely comes from people who have been (or expect to be) denied loans, and who want to scapegoat someone or something to avoid admitting that they look unsafe to lend to because they’ve made poor decisions. I normally want to avoid regulations that are supported by such motives.

Yet an explainability requirement shows some promise at reducing the risks from rogue AIs.

I’m wondering how selection effects will influence the first serious attempt by an AGI to take over the world.

My question here is inspired by thoughts about people who say AGI couldn’t conquer the world because it will depend on humans to provide electricity, semiconductors, etc.