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?
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?