The way the type (A→O)→A corresponds loosely to the “type of agency” (if you kinda squint at the arrow symbol and play fast-and-loose) is that it suggests a machine that eats a description of how actions (A) leads to outcome (O), and produces from that description an action.
Consider stating an alignment property for on elements f of this type. What sort of thing must it say?
Perhaps you wish to say “when f is fed the actual description of the world, it selects the best possible action”. Congratulations, f in fact exists, it is called argmax. This does not help you.
Perhaps you instead wish to say “when f is fed the actual description of the world, it selects an action that gets at least 0.5 utility, after consuming only 1^15 units of compute” or whatever. Now, set aside the fact that you won’t find such a function with your theorem-prover AI before somebody else has ended the world (understanding intelligence well enough to build one that you can prove that theorem about, is pro’lly harder than whatever else people are deploying AGIs towards), and set aside also the fact that you’re leaving a lot of utility on the table; even if that worked, you’re still screwed.
Why are you still screwed? Because the resulting function has the property “if we feed in a correct description of which actions have which utilities, then the optimizer selects an action with high utility”. But an enormous chunk of the hard work is in the creation of that description!
For one thing, while our world may have a simple mathematical description (a la “it’s some quantum fields doing some quantum fielding”), we don’t yet have the true name of our universe yet. For another thing, even if we did, the level of description that an optimizer works with, likely needs to be much coarser than this. For a third thing, even if we had a good coarse-grain description of the world, calculating the consequences that follow from a given action is hard. For a fourth thing, evaluating the goodness of the resulting outcome is hard.
If you can do all those things, then congrats!, you’ve solved alignment (and a good chunk of capabilities). All that’s left is the thing that can operate your description and search through it for high-ranked actions (a remaining capabilities problem).
This isn’t intended to be an argument that there does not exist any logical sentence such that a proof of it would save our skins. I’m trying to say something more like: by the time you can write down the sorts of sentences people usually seem to hope for, you’ve probably solved alignment, and can describe how to build an aligned cognitive system directly, without needing to postulate the indirection where you train up some other system to prove your theorem.
For this reason, I have little hope in sentences of the form “here is an aligned AGI”, on account of how once you can say “aligned” in math, you’re mostly done and probably don’t need the intermediate. Maybe there’s some separate, much simpler theorem that we could prove and save our skins—I doubt we’ll find one, but maybe there’s some simple mathematical question at the heart of some pivotal action, such that a proof one way or the other would suddenly allow humans to… <??? something pivotal, I don’t know, I don’t expect such a thing, don’t ask me>. But nobody’s come up with one that I’ve heard of. And nobody seems close. And nobody even seems to be really trying all that hard. Like, you don’t hear of people talking about their compelling theory of why a given mathematical conjecture is all that stands between humans and <???>, and them banging out the details of their formalization which they expect to only take one more year. Which is, y’know, what it would sound like if they were going to succeed at banging their thing out in five years, and have the pivotal act happen in 15. So, I’m not holding my breath.
Thanks, this helps a lot. The point about a lot of the work being in the mapping from actions to utilities is well-taken.
This line of thinking was from a vague intuition that it ought to be possible to do what evolution and gradient descent can’t, but do it faster than argmax, and have it be not-impossibly-complicated. But sounds like the way I was thinking about that was not productive though; thanks.
The way the type (A→O)→A corresponds loosely to the “type of agency” (if you kinda squint at the arrow symbol and play fast-and-loose) is that it suggests a machine that eats a description of how actions (A) leads to outcome (O), and produces from that description an action.
Consider stating an alignment property for on elements f of this type. What sort of thing must it say?
Perhaps you wish to say “when f is fed the actual description of the world, it selects the best possible action”. Congratulations, f in fact exists, it is called argmax. This does not help you.
Perhaps you instead wish to say “when f is fed the actual description of the world, it selects an action that gets at least 0.5 utility, after consuming only 1^15 units of compute” or whatever. Now, set aside the fact that you won’t find such a function with your theorem-prover AI before somebody else has ended the world (understanding intelligence well enough to build one that you can prove that theorem about, is pro’lly harder than whatever else people are deploying AGIs towards), and set aside also the fact that you’re leaving a lot of utility on the table; even if that worked, you’re still screwed.
Why are you still screwed? Because the resulting function has the property “if we feed in a correct description of which actions have which utilities, then the optimizer selects an action with high utility”. But an enormous chunk of the hard work is in the creation of that description!
For one thing, while our world may have a simple mathematical description (a la “it’s some quantum fields doing some quantum fielding”), we don’t yet have the true name of our universe yet. For another thing, even if we did, the level of description that an optimizer works with, likely needs to be much coarser than this. For a third thing, even if we had a good coarse-grain description of the world, calculating the consequences that follow from a given action is hard. For a fourth thing, evaluating the goodness of the resulting outcome is hard.
If you can do all those things, then congrats!, you’ve solved alignment (and a good chunk of capabilities). All that’s left is the thing that can operate your description and search through it for high-ranked actions (a remaining capabilities problem).
This isn’t intended to be an argument that there does not exist any logical sentence such that a proof of it would save our skins. I’m trying to say something more like: by the time you can write down the sorts of sentences people usually seem to hope for, you’ve probably solved alignment, and can describe how to build an aligned cognitive system directly, without needing to postulate the indirection where you train up some other system to prove your theorem.
For this reason, I have little hope in sentences of the form “here is an aligned AGI”, on account of how once you can say “aligned” in math, you’re mostly done and probably don’t need the intermediate. Maybe there’s some separate, much simpler theorem that we could prove and save our skins—I doubt we’ll find one, but maybe there’s some simple mathematical question at the heart of some pivotal action, such that a proof one way or the other would suddenly allow humans to… <??? something pivotal, I don’t know, I don’t expect such a thing, don’t ask me>. But nobody’s come up with one that I’ve heard of. And nobody seems close. And nobody even seems to be really trying all that hard. Like, you don’t hear of people talking about their compelling theory of why a given mathematical conjecture is all that stands between humans and <???>, and them banging out the details of their formalization which they expect to only take one more year. Which is, y’know, what it would sound like if they were going to succeed at banging their thing out in five years, and have the pivotal act happen in 15. So, I’m not holding my breath.
Thanks, this helps a lot. The point about a lot of the work being in the mapping from actions to utilities is well-taken.
This line of thinking was from a vague intuition that it ought to be possible to do what evolution and gradient descent can’t, but do it faster than argmax, and have it be not-impossibly-complicated. But sounds like the way I was thinking about that was not productive though; thanks.