Is there a simple explanation how set theory, mathematical logic etc. can be used for alignment problem? From reading this post I got an impression that it is very important for the research in MIRI, or, at least, was important in 2013. Maybe I simply don’t know what the author means by this subjects. When I hear this, I am thinking about Gödel theorem, axiomatic of set theory and such stuff, and I can’t imagine how is it related to the alignment. It would be nice to read something where it is explained. Thank you!
See section 2 of this Agent Foundations research program and citations for discussion of the problems of logical uncertainty, logical counterfactuals, and the Löbian obstacle. Or you can read this friendly overview. Gödel-Löb provability logic has been used here.
I don’t know of any application of set theory to agent foundations research. (Like large cardinals, forcing, etc.)
Thank you!
Mathematics is essentially the art/science of making some statements about some kinds of values, and proving those statements. You need some working definition of “value”, “statement” and “proof”.
Set theory is a possible approach to define values, because you can use sets to emulate things like numbers, graphs, functions, etc. Logic is about making statements. Gödel theorem is related to proofs. If you want to teach a computer to do math, you probably want to work with these.
How is math related to alignment? Well, most things about alignment we don’t know how to solve yet—like, how to actually extract the human values. But assuming we solve this problem one day, we will probably also want the AI to reason correctly. That involves some math, for example using the Bayesian theorem. Should the AI try to improve itself, it better be good at reasoning about code and algorithms, which involves more math. And it may need to be good at reasoning about math itself.
This is not a 100% proof that at some moment the set theory will be needed (perhaps the AI can avoid this part of math, or can rediscover it on its own using some other parts of math), but given that it plays an important role in math today, and that math in general will be needed, it seems like a good idea for the AI researcher to know it.
(This is just my guess, I am not involved with MIRI.)
Thank you, but it is again like to say: “oh, to solve physics problem you need calculus. Calculus uses real numbers. The most elegant way to introduce real numbers is from rational numbers from natural numbers via Peano axiomatics. So let’s make physicists study Peano axiomatic, set theory and formal logic”.
In any area of math, you need some set theory and logic—but usually in the amount that can be covered in one-two pages.
It’s just generally useful math background. Things like set theory, logic, category theory, etc. are the modern building blocks of mathematical modeling. I don’t think there’s anything specific about at theory and alignment that’s important, only that you can’t get very far in things directly relevant to alignment, like decision theory, without a good baseline of set theory knowledge.
Thank you, but I would say it is too general answer. For example, suppose your problem is to figure out planet motion. You need calculus, that’s clear. So, according to this logic, you would first need to look at the building blocks. Introduce natural numbers using Peano axioms, then study their properties, then introduce rational, and only then construct real numbers. And this is fun, I really enjoyed it. But does it help to solve the initial problem? Not at all. You can just introduce real numbers immediately. Or, if you care only about solving mechanics problems, you can work with the “intuitive” calculus of infinitesimals, like Newton himself did. It is not mathematically strict, but you will solve everything you need.
So, when you study other areas of math (like probability theory, for example), you need some knowledge of set theory, that’s right. But this set theory is not something profound, which has to be studied separately. It will be introduced in a couple of pages. I don’t know much about the decision theory, does it use more?