Peter Sarnak on “The AlphaZero Test” for Mathematics
Peter Sarnak
Communicated by Notices Executive Editor Siobhan Roberts
I’m an old-fashioned number theorist. I don’t use artificial intelligence devices myself. But I’m spoiled because I’ve had a lot of students who are very capable — both these days with AI, and in the past with programming and running any technology that’s useful. I learned to program in Fortran when I was young, but that’s not what anybody’s using anymore. So, I appeal to my students and work with them.
When Jacob Tsimerman came along as my PhD student, it was clear from the very start that he was a superb mathematician, a superb talent. It was more a matter of guiding him. I was involved in training him in the old-fashioned way.
I know Jacob is very excited about AI. I ignored it for a while. But then I asked him, “Why are you so excited?” He said, “It’s solving these math competitions, the International Mathematical Olympiad competitions.” I suggested, “Well, maybe that says more about the math competitions than it does about AI.” His response: “What level does the AI need to perform at before you take it seriously? What would it need to do? When would you change your mind?” And since I take Jacob very seriously, I took note. It’s certainly a relevant question. Many of us mathematicians have our heads in the sand, ignoring AI, hoping it goes away.
Peter Sarnak and Jacob Tsimerman.
After that discussion with Jacob, I had a discussion with Akshay Venkatesh at the Institute. He is thinking similarly about AI. With those two influences, I really started thinking about it. I go to seminars. I invite people to talk about it. When I have the opportunity, I talk about it myself.
Last year in India I had the pleasure of being part of the awards ceremony for the winners of the Infosys Prize, and they asked me to give a speech. The title of my talk was “Number Theory Pure and Applied,” and I also philosophized about AI and its impact on mathematics. Drawing from my remarks on that occasion, here’s my position:
Calculations and computation have always been central to the development of number theory. The question of whether and how the recent explosion in statistical machine learning will impact number theory, or more generally pure mathematics in say the next 50 years, is one that working mathematicians are beginning to and should be addressing.
My perspective is that of a mathematician and chess player — I was a semi-professional chess player before I became a mathematician. I played from the age of 10 to 16, non-stop every day for six years, and I continued to play until I was about 24. At the beginning, I learned the theories of the famous old-world chess champions — Lasker, Alekhine, Botvinnik. They invented theories about what you do in different positions that blew me away. I was in awe.
When I encountered abstract math, I found it to be a different level of intellectual achievement, a different level of awe. And I still feel that that’s true of the great discoveries in math.
AlphaZero and AlphaGo, the AI game-playing machines from DeepMind, arrived on the scene about ten years ago. I was extremely impressed. They permanently changed chess and Go. With AlphaZero, the word “zero” is very important. It starts from zero. It doesn’t go to a database. It’s self-teaching. If that starts happening in mathematics, it will be a major change.
Taking a closer look at the chess playing machines may offer some insight as to how the trajectory of machines doing mathematics will evolve. Notably, while chess is finite and has artificial rules, it is too large to be analyzed by brute force. The strongest chess programs are Stockfish and AlphaZero and their derivatives. AlphaZero is stronger than Stockfish; both programs beat humans handily.
Stockfish is programmed according to chess theory, and it is an extension of chess master play. It calculates faster and deeper, never makes shallow tactical mistakes, and it accesses large databases of recorded games. Critically, because Stockfish is based upon and explained by chess theory, its play can be understood by strong players.
AlphaZero, on the other hand, makes no use of chess theory or databases. Instead, it generates a database by playing against itself many times and uses statistical machine learning to improve its guess for the best move in any position. It is better at guessing than any human or any other machine, and as such, it has passed some statistical complexity threshold special to the game of chess and its size. AlphaZero offers no understandable — to a human — explanation for its guesses. Nonetheless, some masters say that they can get understanding and inspiration by using AlphaZero’s descendants.
In parallel, we have machines doing mathematics.
The idea of theorem-proving machines presents itself as soon as one formalizes mathematics with axioms and rules of deduction — the theorems being the statements that can be derived by a finite number of deductions.
But there are fundamental differences to chess.
First, the universe of mathematics is infinite. You have to either find a proof or not find a proof, and there will be statements that you can’t decide one way or another — philosophically that is extremely important. And that already tells you that we’re talking about a different universe to something like chess, or the world for that matter.
Secondly, the rules are “god given,” at least if one starts with whole numbers and their arithmetic.
Thirdly, the theory is undecidable (per Kurt Gödel). That is, there are statements, and even interesting ones (per Paul Cohen), whose truth or falsity cannot be decided within the formal framework.
By a theorem-proving machine I mean a device that has the axioms and rules of deduction and that accepts as input a statement that it is supposed to prove or disprove. We give it some time to “think,” after which it either comes back with a formally correct answer or it says that it does not know. Or it could even come back with “this statement is independent of the given axioms!”
Where do we stand today as far as theorem proving machines? Perhaps at the stage that chess was in the 1950’s with the arrival of the modern computer. There are effective formal programs that can check correctness of proofs and can do so interactively. There is a laborious global effort by mathematicians to formally check and record advanced mathematical theories into these systems. These projects should be complete and running efficiently long before our 50-year timeline, and they will be available to our theorem prover to use.
At the center of my speculation is what I call The AlphaZero Test: The theorem prover has no access to any outside data or theory, and we input the statement of, say, the Ramanujan ConjectureFootnote1 in the form that Srinivas Ramanujan formulated it (which is explicit and elementary), and we ask the theorem prover to decide if it is true or false.
I postulate that it will fail the test, and that it will similarly fail with most of our theorems whose present-day proofs make use of abstraction, conceptualization and the development of a body of theorems that we call mathematical theories. These theories are what allow mathematicians to understand and communicate ideas and proofs and also to internalize why various statements are true.
The proofs, if written out from scratch, would be quite long. So, I am postulating that the threshold which was passed by AlphaZero for chess will fail for mathematics. That is, the process of generating proofs toward a goal via self-correcting guesses using statistical machine learning (of course completely different technology will no doubt be available in 50 years) will recover few of the theorems of our theories.
If the postulate is wrong, the impact on mathematics would be dramatic since we would be in the position of knowing that statements of great interest to us are true (proven!) but not understanding why. Since understanding is such an integral part of doing mathematics, we will have to rethink what mathematics is.
To continue, we assume the postulate is correct and call the theorems that our prover can prove “elementary statistical.” The point of our discussion is to allow our proving device to access any information that might be useful for its learning and correction. If we were to input the statement of the Ramanujan Conjecture, it will answer yes instantly and refer to the database of mathematics, where by then it will have been formally checked and recorded. In this way, at any point in time we have a body of mathematical theorems and theories, and the question is, “What further statements can our statistical theorem prover deduce?”
Again, I postulate — and here I know that many mathematicians will disagree — that this class will be limited. In ordinary mathematical terminology, the problems for which it will have success are ones that are already in the ballpark of our current theories — “the elementary statistical derivatives of the theories.” Indeed, these are the problems that most of us try to solve, most of the time. The proving device will expedite the determination and understanding of what these are and serve as an assistant in resolving them.
As such these theorem provers will be an important tool for mathematicians. I imagine it being something like Stockfish is for competitive chess players. In any case, whether this class is limited, or more expansive, mathematical theory will be its basis. Of course, the theory, its formulation and execution, will evolve naturally with these developments. I expect that mathematicians of my generation would still know it as mathematics if we were to see and smell it!
Peter Sarnak is the Eugene Higgins Professor of Mathematics at Princeton University, and a professor emeritus at the Institute for Advanced Study in Princeton. His email address is [email protected]
Article DOI: 10.1090/noti3373
Credits
Figure 1 photo is courtesy of Jacob Tsimerman.