Kinda. The current approach is more like “Pretend you’re trying to solve a much easier version of the problem, e.g. where you have a ton of computing power and you’re trying to maximize diamond instead of hard-to-describe values. What parts of the problem would you still not know how to solve? Try to figure out how to solve those first.”
(1) If we manage to (a) generate a theory of advanced agents under many simplifying assumptions, and then (b) generate a theory of bounded rational agents under far fewer simplifying assumptions, and then (c) figure out how to make highly reliable practical generally intelligent systems, all before anyone else gets remotely close to AGI, then we might consider teching up towards designing AI systems ourselves. I currently find this scenario unlikely.
(2) We’re currently far enough away from knowing what the actual architectures will look like that I don’t think it’s useful to try to build AI components intended for use in an actual AGI at this juncture.
(3) I think that making theorem provers easier to use is an important task and a worthy goal. I’m not optimistic about attempts to merge natural language with Martin-Lof type theory. If you’re interested in improving theorem-proving tools in ways that might make it easier to design safe reflective systems in the future, I’d point you more towards trying to implement (e.g.) Marcello’s Waterfall in a dependently typed language (which may well involve occasionally patching the language, at this stage).
Kinda. The current approach is more like “Pretend you’re trying to solve a much easier version of the problem, e.g. where you have a ton of computing power and you’re trying to maximize diamond instead of hard-to-describe values. What parts of the problem would you still not know how to solve? Try to figure out how to solve those first.”
(1) If we manage to (a) generate a theory of advanced agents under many simplifying assumptions, and then (b) generate a theory of bounded rational agents under far fewer simplifying assumptions, and then (c) figure out how to make highly reliable practical generally intelligent systems, all before anyone else gets remotely close to AGI, then we might consider teching up towards designing AI systems ourselves. I currently find this scenario unlikely.
(2) We’re currently far enough away from knowing what the actual architectures will look like that I don’t think it’s useful to try to build AI components intended for use in an actual AGI at this juncture.
(3) I think that making theorem provers easier to use is an important task and a worthy goal. I’m not optimistic about attempts to merge natural language with Martin-Lof type theory. If you’re interested in improving theorem-proving tools in ways that might make it easier to design safe reflective systems in the future, I’d point you more towards trying to implement (e.g.) Marcello’s Waterfall in a dependently typed language (which may well involve occasionally patching the language, at this stage).