Similar to V_V’s comment. I’m only a layman, but I don’t understand one of the first steps.
The paper appears to jump straight into the logic, justifying itself (pardon the pun) by a statement about the intricacies of formal systems proving things about other formal systems.
Can you explain how and why all AI systems correspond to formal systems—what precisely you mean by ‘formal system’?
(Btw, I have in fact read GEB, but I am still unable to confidently define a formal system.)
Or a better question might be “Why does this need to be possible within the realms of formal logic to be doable at the level of code/AI? There are many general problems intractable as part of pure maths, yet many numerical methods exist to solve particular instantiations. Why must this be doable at the level of pure logic?”
Good question as well! I should add motivation to the notes on this point.
Basically, we study deterministic mathematical objects within formal systems because these cases are easier for us to analyze and prove theorems about; it’s an example of looking first under the streetlight before meandering farther into the darkness. Hopefully this way we’ll notice many phenomena that still hold when we add randomness, bounded computations, and other realistic limitations.
And indeed, plenty of the topics in MIRI research do hold up when you make them messier. Many of the topics in formal systems can handle random variables just as easily as deterministic facts. There’s a version of Löb’s Theorem for bounded-length proof searches, and tracing it through shows that Löbian cooperation and other phenomena behave the same there as in the unbounded case (for sufficiently large choices of the bounds). Using quantum random variables to evaluate logical counterfactuals doesn’t solve implementing UDT, it just collapses it into CDT; so we still need to study logical counterfactuals. And so on.
Also, when I say “formal system” you can usually substitute in “Peano Arithmetic” or “Peano Arithmetic plus some extra axioms”.
Right! So you’re trying to get ahold of the idea of an intelligent computational agent, in clear formalisms, and trying to solve the basic issues that arise there. And often, the issues you discover at the fundamental mathematical level work their way through to the highly applied level.
That makes sense. I feel like this is the most direct answer to the question
… are you curious why MIRI does so much with mathematical logic, and why people on Less Wrong keep referring to Löb’s Theorem?
Similar to V_V’s comment. I’m only a layman, but I don’t understand one of the first steps.
The paper appears to jump straight into the logic, justifying itself (pardon the pun) by a statement about the intricacies of formal systems proving things about other formal systems.
Can you explain how and why all AI systems correspond to formal systems—what precisely you mean by ‘formal system’?
(Btw, I have in fact read GEB, but I am still unable to confidently define a formal system.)
Or a better question might be “Why does this need to be possible within the realms of formal logic to be doable at the level of code/AI? There are many general problems intractable as part of pure maths, yet many numerical methods exist to solve particular instantiations. Why must this be doable at the level of pure logic?”
Good question as well! I should add motivation to the notes on this point.
Basically, we study deterministic mathematical objects within formal systems because these cases are easier for us to analyze and prove theorems about; it’s an example of looking first under the streetlight before meandering farther into the darkness. Hopefully this way we’ll notice many phenomena that still hold when we add randomness, bounded computations, and other realistic limitations.
And indeed, plenty of the topics in MIRI research do hold up when you make them messier. Many of the topics in formal systems can handle random variables just as easily as deterministic facts. There’s a version of Löb’s Theorem for bounded-length proof searches, and tracing it through shows that Löbian cooperation and other phenomena behave the same there as in the unbounded case (for sufficiently large choices of the bounds). Using quantum random variables to evaluate logical counterfactuals doesn’t solve implementing UDT, it just collapses it into CDT; so we still need to study logical counterfactuals. And so on.
Also, when I say “formal system” you can usually substitute in “Peano Arithmetic” or “Peano Arithmetic plus some extra axioms”.
Right! So you’re trying to get ahold of the idea of an intelligent computational agent, in clear formalisms, and trying to solve the basic issues that arise there. And often, the issues you discover at the fundamental mathematical level work their way through to the highly applied level.
That makes sense. I feel like this is the most direct answer to the question
Thanks! I’ll try and work that into the introduction.