Deepmind's AlphaCode, OpenAI's theorem-prover, and the road ahead... [A rambling discussion of some of my thoughts on this]
By starspawn0
I've seen a few people write some skeptical takes on what Deepmind has accomplished with AlphaCode (none yet about OpenAI), and I just can't fathom how they could see the accomplishment as not being stunningly impressive. Take a look again at the program that AlphaCode wrote to solve the "string matching problem":
https://deepmind.com/blog/article/Compe ... -AlphaCode
You'd have to be a complete idiot to think that it's just a matter of translation (of text into code analogous to translating French into English), like run-of-the-mill programming assistant-type problems (that Codex solves). And even if the solutions generated are correct only 1% of the time, and AlphaCode has to filter out 99% of bad solutions, that's still stunning. Just think of how many ways you can go wrong in coming up with a solution like that -- any little mistaken variable name, pop or append, syntax error, etc. and the show's over.
Now, this doesn't mean that in the next couple months the system will be at or above the 99 percentile in these competitions like AlphaGo was; but I could see it reaching the 75th percentile or even 90th percentile if a larger language model is used and an inner-monologue procedure added to increase its "reasoning power". This would be a great feat of engineering!
The reason I am hesitant it will go above 90th percentile all that soon is that some of these programming competition problems involve geometric insight, which would require some additional training (large training dataset). For example, consider a simple problem like, "Write a program that takes a set of points (x,y) as input, and then finds a triangle with vertices equal to those points, and that encloses the greatest number of points from the set." To solve a problem like that you need to know that triangles have 3 vertices, and you need to have a way of determining whether a point lies inside or outside the triangle. This latter step is something a human could invent if they didn't know a procedure (a triangle is the intersection of 3 half-planes, determined by the 3 sides; and it's easy to check which side of a half-plane a point is on); but a computer might struggle, unless it has absorbed enough mathematical tricks.
And there may be other domains of knowledge like this that would give a human a huge advantage on certain types of problems.
As to what it will mean when computers can routinely beat the top humans in programming competitions and also win at IMO and Putnam-type competitions, I don't think it will immediately translate into radical scientific breakthroughs directly (but maybe indirectly). To make such breakthroughs you still need to do a lot of experiments, and also build several more generations of tools to carry them out. Imagine the ancient Greeks trying to develop deep theories of particle physics without access to CERN-level accelerators, and without even calculators...
A lot of the great theories in math are admired because they are so general. However, being general means that they probably are not going to say very much about specific instances. Then there is a lot of math that just verifies the things we already believed were true. Mathematicians usually already know when certain big conjectures are true or not; they're just looking for an airtight proof. And, finally, there are "important" results that only hold "out at infinity", when the parameters used are beyond any you will see in the real world -- e.g. maybe a factoring algorithm that only runs quickly when the numbers have a million digits.
Years ago, I had a conversation with a neuroscientist and mathematician named Carina Curto:
http://www.personal.psu.edu/cpc16/
Before she did neuroscience work she worked on String Theory, and her current work involves a lot of applications of topology to understanding memory and neuro-dynamics. Anyways, she said something that stuck with me. She said that what really transfers from math to the real world is the definitions. Mathematicians are good at coming up with good definitions and objects, like "homotopy", "homology", and "cohomology", that then can be woven into algorithms that do data analysis. However, because the real world is so messy, it's usually going to be the case that the deepest results on these concepts won't get that helpful. Maybe an algorithm that gives you some rough, statistical measure of topological invariants will help you; but the deeper algorithms a mathematician hopes would prove the true power of math will remain ever elusive.
Well, that's not quite true. If we're talking about the universe at the scale of particle physics, where there are lots of deep symmetries and where the world seems "crystalline", the deep math can help. Or, if we're talking about domains invented by humans -- such as cryptology -- then, again, deep math may help. But if we're talking about biology, biochemistry, stock market behavior, weather, and so on, then much dumber math will probably do just as good as the fancier variety in solving problems. No need to find a global solution to the Navier-Stokes equations, just build a neural net to simulate the behavior of fluids, for example.
What really would unlock the power of mathematics, then, as far as direct impacts go, would be more computing power -- since those dumber algorithms could be applied to much larger datasets. And if we ever get attacked by a superintelligent AI, it probably will quickly realize that a smarter way to solve the problems leading to our annihilation than "deep theory" will just involve acquiring more and more compute.
That said, what I see as the main application to science and engineering, of writing code and proving theorems at an expert level, is more indirect. It will eventually enable us to automate a lot of programming labor. So, instead of taking years for whole teams of people to write very complex code, we could instead have it written in a matter of weeks or at worst a small number of months using next-generation programming assistants (similar to Codex, only a lot better). And we could also have it verified for correctness, though automated theorem-proving tools.
What this would do is reduce the perceived risk of engaging in any particular line of research. Take, for example, anti-aging. Suppose you had some idea about how to find anti-aging supplements by doing textual analysis on medical texts. Without a programming assistant it may take a long time to code that up. And if you're wrong, then all that time will have been wasted. Thus, you might not even bother, unless you are certain it will work. But if you could just tell a programming assistant your idea, and it could code it up and check for you, then the risk will be almost zero.
Now think about what that would mean if you extend that to every time someone has an idea that they think might work, but are afraid will eat up their time if it doesn't. The number of important advances will probably skyrocket, but only indirectly due to next-gen programming assistants.