Doing theoretical research that ignores practicalities is sometimes turns out to be valuable in practice. It can open a door to something you assumed to be impossible; or save a lot of wasted effort on a plan that turns out to have an impossible sub-problem.
A concrete example of first category might be something like quantum error correcting codes. Prior to that theoretical work, a lot of people thought that quantum computers were not worth pursuing because noise and decoherence would be an insurmountable problem. Quantum fault tolerance theorems did nothing to help solve the very tough practical problems of building a quantum computer, but it did show people that it might be worth pursuing—and here we are 20 years later closing in on practical quantum computers.
I think source code based decision theory might have something of this flavour. It doesn’t address all those practical issues such as how one machine comes to trust that another machine’s source code is what it says. That might indeed scupper the whole thing. But it does clarify where the theoretical boundaries of the problem are.
You might have thought “well, two machines could co-operate if they had identical source code, but that’s too restrictive to be practical”. But it turns out that you don’t need identical source code if you have the source code and can prove things about it. Then you might have though “ok, but those proofs will never work because of non-termination and self-reference” … and it turns out that that is wrong too.
Theoretical work like this could inform you about what you could hope to achieve if you could solve the practical issues; and conversely what problems are going to come up that you are absolutely going to have to solve.
But it might not be a useful line of thinking? Is it possible for lesswrong/AI Risk community to talk about the two universes at the same time? To be concrete I mean the universe where very formal models are useful for AI development and the other where the only practical solutions are adhoc and contextual.
Just as AIXI seems to have been discarded for not being naturalistic enough (Hoorah) you might want to entertain the idea that software based decision theories aren’t naturalistic enough.
This feels like a weird objection to me and I’m having some difficulty expressing why. Yes, it’s better to use lines of thinking that are more likely to produce results, but it feels like a fully general counterargument because all lines of thinking might not produce results. If we want to move past the results of the past, we have to actually explore, and that necessarily involves some dead ends. And Kyre’s argument is why I would say that research direction isn’t an obvious dead end.
Is it possible for lesswrong/AI Risk community to talk about the two universes at the same time?
MIRI currently has two research agendas, which seem to me like trying to do both at the same time. (I don’t think it lines up quite with the division you’re discussing; for example, my suspicion is that improved naturalism mostly comes out of the agent foundations agenda.)
I don’t think I want to make it fully general. I want to contrast between two schools of thinking, both of which are hard to get out of with only the tools of that school.
At what point do you put down the formal proof tools? You might prove that a statement is unprovable, but you may not do it may just hang around like P vs NP forever. Or you might prove a statement is unprovable within a system and then just switch to a different system (adding oracles and what not). What is your stopping condition?
Same with Empiricism. You will never show that empircism isn’t a useful method of gaining knowledge for a specific goal using just experiments, just that a single line of experimentation is unfruitful.
You can prove that certain lines of empiricism are likely to be unfruitful (things like trying to create infinite free energy) based on other axioms that hold up empirically. Similarly if an empirical approach is being productive you can use that to constrain the formal proofs you attempt.
This is something I would like to have said a long time ago. I’m not sure how relevant it is to current MIRI research. How much of it is actually writing programs?
Doing theoretical research that ignores practicalities is sometimes turns out to be valuable in practice. It can open a door to something you assumed to be impossible; or save a lot of wasted effort on a plan that turns out to have an impossible sub-problem.
A concrete example of first category might be something like quantum error correcting codes. Prior to that theoretical work, a lot of people thought that quantum computers were not worth pursuing because noise and decoherence would be an insurmountable problem. Quantum fault tolerance theorems did nothing to help solve the very tough practical problems of building a quantum computer, but it did show people that it might be worth pursuing—and here we are 20 years later closing in on practical quantum computers.
I think source code based decision theory might have something of this flavour. It doesn’t address all those practical issues such as how one machine comes to trust that another machine’s source code is what it says. That might indeed scupper the whole thing. But it does clarify where the theoretical boundaries of the problem are.
You might have thought “well, two machines could co-operate if they had identical source code, but that’s too restrictive to be practical”. But it turns out that you don’t need identical source code if you have the source code and can prove things about it. Then you might have though “ok, but those proofs will never work because of non-termination and self-reference” … and it turns out that that is wrong too.
Theoretical work like this could inform you about what you could hope to achieve if you could solve the practical issues; and conversely what problems are going to come up that you are absolutely going to have to solve.
But it might not be a useful line of thinking? Is it possible for lesswrong/AI Risk community to talk about the two universes at the same time? To be concrete I mean the universe where very formal models are useful for AI development and the other where the only practical solutions are adhoc and contextual.
Just as AIXI seems to have been discarded for not being naturalistic enough (Hoorah) you might want to entertain the idea that software based decision theories aren’t naturalistic enough.
This feels like a weird objection to me and I’m having some difficulty expressing why. Yes, it’s better to use lines of thinking that are more likely to produce results, but it feels like a fully general counterargument because all lines of thinking might not produce results. If we want to move past the results of the past, we have to actually explore, and that necessarily involves some dead ends. And Kyre’s argument is why I would say that research direction isn’t an obvious dead end.
MIRI currently has two research agendas, which seem to me like trying to do both at the same time. (I don’t think it lines up quite with the division you’re discussing; for example, my suspicion is that improved naturalism mostly comes out of the agent foundations agenda.)
I don’t think I want to make it fully general. I want to contrast between two schools of thinking, both of which are hard to get out of with only the tools of that school.
At what point do you put down the formal proof tools? You might prove that a statement is unprovable, but you may not do it may just hang around like P vs NP forever. Or you might prove a statement is unprovable within a system and then just switch to a different system (adding oracles and what not). What is your stopping condition?
Same with Empiricism. You will never show that empircism isn’t a useful method of gaining knowledge for a specific goal using just experiments, just that a single line of experimentation is unfruitful.
You can prove that certain lines of empiricism are likely to be unfruitful (things like trying to create infinite free energy) based on other axioms that hold up empirically. Similarly if an empirical approach is being productive you can use that to constrain the formal proofs you attempt.
This is something I would like to have said a long time ago. I’m not sure how relevant it is to current MIRI research. How much of it is actually writing programs?