Pretty interesting. You’re still constrained by your ability to specify solutions, so you can’t immediately solve cold fusion or FTL (you’d need to manually write and debug an accurate-enough physics simulator first). Truly, no computing system can free you from the burden of clarifying your ideas. But this constraint does leave some scope for miracles, and I want to talk about one technique in particular: program search.
Program Search
Program search is a very powerful, but dangerous and ethically dubious, way to exploit unbounded compute. Start with a set of test cases, then generate all programs of length less than 100 megabytes (or whatever) and return the shortest, fastest one that passes all the test cases. Both constraints are important: “shortest” prevents the optimizer from returning a hash table that memorizes all possible inputs, and “fastest” prevents it from relying on the unusual nature of the oracle universe (note that you will need a perfect emulator in order to find out which program is fastest, since wall-clock time measurements in the oracle’s universe might be ineffective or misleading). In a narrow sense, this is the perfect compiler: you tell it what kind of program you want, and it gives you exactly what you asked for.
Risks
There are some practical dangers. In Python or C, for example, the space of all programs includes programs which can corrupt or mislead your test harness. The ideal language for this task has no runtime flexibility or ambiguity whatsoever; Haskell might work. But that still leaves you at the mercy of God’s Haskell implementation: we can assume that He introduced no new bugs, but He might have faithfully replicated an existing bug in the reference Haskell compiler, which your enumeration will surely find. This is unlikely to cause serious problems (at least at first), but it means you have to cross-check the output of whatever program the oracle finds for you.
More insidiously, some the programs that we run during the search might instantiate conscious minds, or otherwise be morally relevant. If that seems unlikely, ask yourself: are you totally sure it’s impossible to simulate a suffering human brain in 100 megs of Haskell? This risk can be limited somewhat, for example by running the programs in order from smallest to largest, but is hard to rule out entirely.
Applications
If you’re willing to put up with all that, the benefits are enormous. All ML applications can be optimized this way: just find the program that scores above some threshold on your metric, given your other constraints (if you have a lot of data you might be able to use the best-scoring program, but in small-data regimes the smallest, fastest program might still just be a hash table. Maybe score your programs by how much simpler than the training data they are?).
With a little more work, it should be possible to—almost—solve all of mathematics: to create an oracle which, given a formal system, can tell you whether any given statement can proved within that system and, if so, whether it can be proved true or false (or both)...that is, for proofs up to some ridiculous but finite length. I think you will have to invent your own proof language for this; the existing ones are all designed around complexity limitations that don’t apply to you. Make sure your language isn’t Turing complete, to limit the risk of moral catastrophe. Once you have that, you can just generate all possible proofs and then check whether the one you want is present or not.
Simulation
Up until now we’ve been limited by our ability to specify the solution we want. We can write test cases and generate a program which fulfills them, but it won’t do anything we didn’t explicitly ask for. We can find the ideal classifier for a set of images, but we first have to find those images out in the real world somewhere, and the power of our classifier is bounded by the number of images we can find.
If we can specify precise rules for a simulation, and a goal within that simulation, most of that constraint disappears. For example, to find the strongest Go-playing program, we can instantiate all possible Go-playing programs and have them compete until there’s an unambiguous winner; we don’t need any game records from human players. The same trick works for everything simulatable: Starcraft, Magic: the Gathering, piloting fighter jets, you name it. If you don’t want to use the oracle to directly generate a strong AI, you can instead develop accurate-enough simulations of the real-world, and then use the oracle to develop effective agents within those simulations.
Endgame
Ultimately the idea would be to develop a computer model of the laws physics that’s as correct and complete as our computer model of the rules of Go, so that you can finally develop nanofactories, anti-aging drugs, and things like that. I don’t see how to do it, but it’s the only prize worth playing for. At this point it becomes very important to be able prove the Friendliness of every candidate program; use the math oracle you built earlier to develop a framework for that before moving forward.
With a little more work, it should be possible to—almost—solve all of mathematics: to create an oracle which, given a formal system, can tell you whether any given statement can proved within that system
...with a proof of length L or less.
Aside from the issue of the given statement, what can’t be proved?
Problems whose answers are independent of the framework you are using (The continuum hypothesis). [1]
Undecidable problems. [2]
Things which probably can’t be proved:
Things which are false, like 2+2=3. (For a given framework which meets certain requirements, it is not possible to prove that there isn’t a contradiction—within that framework.) [3]
The continuum hypothesis was advanced by Georg Cantor in 1878, and establishing its truth or falsehood is the first of Hilbert’s 23 problems presented in 1900. The answer to this problem is independent of ZFC, so that either the continuum hypothesis or its negation can be added as an axiom to ZFC set theory, with the resulting theory being consistent if and only if ZFC is consistent.
In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is proved to be impossible to construct an algorithm that always leads to a correct yes-or-no answer. The halting problem is an example: it can be proven that there is no algorithm that correctly determines whether arbitrary programs eventually halt when run.
the halting problem is undecidable over Turing machines. It is one of the first cases of decision problems proven to be unsolvable. This proof is significant to practical computing efforts, defining a class of applications which no programming invention can possibly perform perfectly.
Problems whose answers are independent of the framework you are using (The continuum hypothesis). [1]
Undecidable problems. [2]
These are pretty much the same thing. The continuum hypothesis is a case where you have a single formal system in mind ( ZFC ) and have proved that the continuum hypothesis is independent of the axioms.
In the case of the halting problem, you just have a couple of extra quantifiers. For all formal systems that don’t prove a contradiction, there exists a Turing machine, such that whether the Turing machine halts or not can’t be proved from the axioms of the formal system. (Technically, the formal system needs to be R.E., which means that there is a computer program that can tell if an arbitrary string is an axiom. )
If you’re using the oracle to generate moves directly then you don’t need an agent, yeah. But that won’t always work: you can generate the complete Starcraft state space and find the optimal reply for each state, but you can’t run that program in our universe (it’s too big) and you can’t use the oracle to generate SC moves in real time (it’s too slow).
If you don’t mind, I might try playing around with some of the ideas you mentioned in future write-ups here; there’s a lot of interesting theoretical questions that could be explored along those lines.
Pretty interesting. You’re still constrained by your ability to specify solutions, so you can’t immediately solve cold fusion or FTL (you’d need to manually write and debug an accurate-enough physics simulator first). Truly, no computing system can free you from the burden of clarifying your ideas. But this constraint does leave some scope for miracles, and I want to talk about one technique in particular: program search.
Program Search
Program search is a very powerful, but dangerous and ethically dubious, way to exploit unbounded compute. Start with a set of test cases, then generate all programs of length less than 100 megabytes (or whatever) and return the shortest, fastest one that passes all the test cases. Both constraints are important: “shortest” prevents the optimizer from returning a hash table that memorizes all possible inputs, and “fastest” prevents it from relying on the unusual nature of the oracle universe (note that you will need a perfect emulator in order to find out which program is fastest, since wall-clock time measurements in the oracle’s universe might be ineffective or misleading). In a narrow sense, this is the perfect compiler: you tell it what kind of program you want, and it gives you exactly what you asked for.
Risks
There are some practical dangers. In Python or C, for example, the space of all programs includes programs which can corrupt or mislead your test harness. The ideal language for this task has no runtime flexibility or ambiguity whatsoever; Haskell might work. But that still leaves you at the mercy of God’s Haskell implementation: we can assume that He introduced no new bugs, but He might have faithfully replicated an existing bug in the reference Haskell compiler, which your enumeration will surely find. This is unlikely to cause serious problems (at least at first), but it means you have to cross-check the output of whatever program the oracle finds for you.
More insidiously, some the programs that we run during the search might instantiate conscious minds, or otherwise be morally relevant. If that seems unlikely, ask yourself: are you totally sure it’s impossible to simulate a suffering human brain in 100 megs of Haskell? This risk can be limited somewhat, for example by running the programs in order from smallest to largest, but is hard to rule out entirely.
Applications
If you’re willing to put up with all that, the benefits are enormous. All ML applications can be optimized this way: just find the program that scores above some threshold on your metric, given your other constraints (if you have a lot of data you might be able to use the best-scoring program, but in small-data regimes the smallest, fastest program might still just be a hash table. Maybe score your programs by how much simpler than the training data they are?).
With a little more work, it should be possible to—almost—solve all of mathematics: to create an oracle which, given a formal system, can tell you whether any given statement can proved within that system and, if so, whether it can be proved true or false (or both)...that is, for proofs up to some ridiculous but finite length. I think you will have to invent your own proof language for this; the existing ones are all designed around complexity limitations that don’t apply to you. Make sure your language isn’t Turing complete, to limit the risk of moral catastrophe. Once you have that, you can just generate all possible proofs and then check whether the one you want is present or not.
Simulation
Up until now we’ve been limited by our ability to specify the solution we want. We can write test cases and generate a program which fulfills them, but it won’t do anything we didn’t explicitly ask for. We can find the ideal classifier for a set of images, but we first have to find those images out in the real world somewhere, and the power of our classifier is bounded by the number of images we can find.
If we can specify precise rules for a simulation, and a goal within that simulation, most of that constraint disappears. For example, to find the strongest Go-playing program, we can instantiate all possible Go-playing programs and have them compete until there’s an unambiguous winner; we don’t need any game records from human players. The same trick works for everything simulatable: Starcraft, Magic: the Gathering, piloting fighter jets, you name it. If you don’t want to use the oracle to directly generate a strong AI, you can instead develop accurate-enough simulations of the real-world, and then use the oracle to develop effective agents within those simulations.
Endgame
Ultimately the idea would be to develop a computer model of the laws physics that’s as correct and complete as our computer model of the rules of Go, so that you can finally develop nanofactories, anti-aging drugs, and things like that. I don’t see how to do it, but it’s the only prize worth playing for. At this point it becomes very important to be able prove the Friendliness of every candidate program; use the math oracle you built earlier to develop a framework for that before moving forward.
...with a proof of length L or less.
Aside from the issue of the given statement, what can’t be proved?
Problems whose answers are independent of the framework you are using (The continuum hypothesis). [1]
Undecidable problems. [2]
Things which probably can’t be proved:
Things which are false, like 2+2=3. (For a given framework which meets certain requirements, it is not possible to prove that there isn’t a contradiction—within that framework.) [3]
Footnotes
[1]
From https://en.wikipedia.org/wiki/Continuum_hypothesis:
[2]
https://en.wikipedia.org/wiki/Undecidable_problem
https://en.wikipedia.org/wiki/Halting_problem:
[3]
https://en.wikipedia.org/wiki/Kurt_G%C3%B6del#Incompleteness_theorem
These are pretty much the same thing. The continuum hypothesis is a case where you have a single formal system in mind ( ZFC ) and have proved that the continuum hypothesis is independent of the axioms.
In the case of the halting problem, you just have a couple of extra quantifiers. For all formal systems that don’t prove a contradiction, there exists a Turing machine, such that whether the Turing machine halts or not can’t be proved from the axioms of the formal system. (Technically, the formal system needs to be R.E., which means that there is a computer program that can tell if an arbitrary string is an axiom. )
I don’t think there’s any reason to create the agents for those games, since you can just brute force solve for the optimal play.
If you’re using the oracle to generate moves directly then you don’t need an agent, yeah. But that won’t always work: you can generate the complete Starcraft state space and find the optimal reply for each state, but you can’t run that program in our universe (it’s too big) and you can’t use the oracle to generate SC moves in real time (it’s too slow).
Good point!
Thanks for the fascinating response!
If you don’t mind, I might try playing around with some of the ideas you mentioned in future write-ups here; there’s a lot of interesting theoretical questions that could be explored along those lines.
Sure, go ahead.