Shades of WOPR. "This is a game nobody can win..."
Shades of WOPR. "This is a game nobody can win..."
And, when the legal moves are replaced with the moves of other games (like Go for which it was actually written, or Shogi), it did exactly the same thing. Redevelop millennia of human knowledge and go beyond, all within 8 hours of compute.
Makes you wonder what will happen when instead of the rules of chess, you put in the axioms of logic and natural numbers. And give it 8 months of compute.
(The operations the TPU can run are far simpler than what supercomputers can do, but just for the sake of comparison, the current top supercomputer in the world can do 1.25×10^17 floating point operations per second)
But it's not really misleading at all. The ability to produce massive amount of power and product is the pinnacle of our society. The fact is we can make thousand, if not millions or even billions of TPUs if we desired, and it is a relatively easy engineering problem at that. And that these things may solve all kinds of problems mankind has had for millennia in hours should be a wakeup call to a future that will be hard to predict.
Humans take 9 months to gestate, no amount of parallelism will speed that up, after that it takes 18 years for them not to be completely stupid all the time attempting to hammer an education in them. Even after that it takes more years to become a specialist.
How do you score this computation? What's your goal? There's no checkmate here.
Maybe give it a list of problems of varying degree of hardness, and tell it to either prove or disprove as many as possible?
For example, give it a number and tell it to factor it into the prime factors. The score might be the solution with the smallest time or storage requirements. Or maybe find a way to generate a hash where the last n digits are zero.
I also remember a RadioLab episode where they talked about electronic theorem solvers and they would do something like show it a video of a double pendulum and it would come up with equations to model the behavior of that system.
If you're talking about formal proofs or maths, I'm not sure how this would apply in general as the branching factor for each 'move' in a proof is efficiently infinite. It would be interesting to see it applied to more constrained proof domains though.