Courtesy: towardsdatascience.com
AI comes of age
After several decades of disappointment, effective artificial intelligence (AI) systems emerged in the late 1990s and early 2000s, with the emergence of Bayes-theorem-based methods, combined with steadily advancing computer technology.
One notable milestone came in March 2016, when a computer program named “AlphaGo,” developed by researchers at DeepMind, a subsidiary of Alphabet (Google’s parent company), defeated champion Go master Lee Se-dol, an achievement that many observers had not expected to occur for decades. Then in October 2017, Deep Mind researchers announced a new program, AlphaGo Zero, which was programmed only with the rules of Go and a simple reward function and then instructed to play games against itself. After just three days of training (4.9 million training games), the AlphaGo Zero program had advanced to the point that it defeated the earlier Alpha Go program 100 games to zero.
AI and machine-learning methods are now being used in Apple’s Siri and Amazon’s Alexa voice recognition systems, in Facebook’s facial recognition API, in Apple’s 3-D facial recognition hardware and software, and in Tesla’s “autopilot” facility. See also these earlier Math Scholar blogs: Blog A and Blog B, from which some of the material below was taken.
Computer discovery and proofs of mathematical theorems
Since the earliest days of AI, researchers have wondered whether these programs would ever be able to do serious mathematical research. In fact, computer programs that discover new mathematical identities and theorems are already a staple of the field known as experimental mathematics. A typical scenario is that a computer program, typically employing high precision computation software with an integer relation algorithm such as PSLQ, numerically discovers a previously unknown identity and confirms it to some compelling level of precision, such as 1000 or 10,000 digits. However, such programs typically offer only scant assistance as to why the result holds, so rigorous proofs must be done the old-fashioned human way.
So what about computers actually proving theorems?
Actually, this is also old hat at this point in time. Perhaps the best example is Thomas Hales’ 2003 proof of the Kepler conjecture, namely the assertion that the simple scheme of stacking oranges typically seen in a supermarket has the highest possible average density for any possible arrangement. Hales’ original proof met with some controversy, since it involved a computation documented by 250 pages of notes and three Gbyte of computer code and data. So Hales and his colleagues began entering the entire proof into a computer proof-checking program. In 2014 this process was completed and the proof was certified.
In November 2019, researchers at Google’s research center in Mountain View, California, published results for a new AI theorem-proving program. This program works with the HOL-Light theorem prover, which was used in Hales’ proof of the Kepler conjecture, and can prove, essentially unaided by humans, many basic theorems of mathematics. They have provided their tool in an open-source release, so that other mathematicians and computer scientists can experiment with it.
The Google AI system was trained on a set of 10,200 theorems that the researchers had gleaned from several sources, including many sub-theorems of Hales’ proof of the Kepler conjecture. Most of these theorems were in the area of linear algebra, real analysis and complex analysis, but the Google researchers emphasize that their approach is very broadly applicable. In the initial release, their software was able to prove 5919, or 58% of the training set. When they applied their software to a set of 3217 new theorems that it had not yet seen, it succeeded in proving 1251, or 38.9%.
For additional details see the Google authors’ technical paper, and a New Scientist article by Leah Crane.
New result: AI program discovers counterexamples to graph theory conjectures
In a remarkable new development, Adam Zsolt Wagner of Tel Aviv University in Israel employed an AI approach to search for counterexamples to a set of long-standing conjectures in graph theory. In each case, these conjectures were thought to be true, but no one had been able to produce a proof.
For each problem, Wagner’s approach was to devise a measure of how close a given specific construction is to a disproof. Wagner then coded a neural network program to create random constructions and evaluate them according to the measure.
As is common with other neural network research efforts, Wagner’s program advanced step-by-step, discarding low-scoring constructions and replacing them with additional random examples, proceeding over many steps to steadily improve the top-scoring constructions. In the majority of cases, Wagner’s program was unable to find a counterexample construction (perhaps because the conjecture in question may actually be true?). But in five cases the program was successful in discovering a construction that disproved the conjecture.
These were rather modest computations — Wagner ran his program on his five-year-old laptop, which required between two and 48 hours run time to discover the successful counterexamples. Wagner notes that the discovered disproof examples were mostly rather counterintuitive: “I would never have come up with these constructions by myself even if you gave me hundreds of years.”
For additional details see this New Scientist report.
How close are we to fully automatic mathematical reasoning?
Present-day computerized theorem provers are typically categorized as automated theorem provers (ATPs), which use computationally intensive methods to search for a proof; and interactive theorem provers, which rely on an interplay with humans — verifying the correctness of an argument and checking proofs for logical errors. Researchers in the field, however, acknowledge that both types of software are still a far cry from a completely independent computer-based mathematical reasoning system.
For one thing, these tools have been met with cold shoulders by many present-day mathematicians, in part because they require considerable study and practice to become proficient in using them, and in part because of a general distaste for the notion of automating mathematical thought.
But some mathematicians are embracing these tools. Kevin Buzzard of Imperial College London, for example, has begun to focus his research on computerized theorem provers. But he acknowledges, “Computers have done amazing calculations for us, but they have never solved a hard problem on their own. … Until they do, mathematicians aren’t going to be buying into this stuff.”
Emily Riehl, of Johns Hopkins University, teaches students to write mathematical proofs using a computerized tool. She reports that these tools help students to rigorously formulate their ideas. Even for her own research, she says that “using a proof assistant has changed the way I think about writing proofs.”
Vladimir Voevodsky of Princeton University, after finding an error in one of his own published results, was an ardent advocate of using computers to check proofs, until his death in 2017.
Timothy Gowers of Cambridge, who won the Fields Medal in 1998, goes even further, saying that major mathematical journals should prepare for the day when the authors of all submitted papers must first certify that their results have been verified by a computerized proof checker.
Josef Urban of the Czech Institute of Informatics, Robotics and Cybernetics believes that a combination of computerized theorem provers and machine learning tools is required to produce human-like mathematical research capabilities. In July 2020 his group reported on some new mathematical conjectures generated by a neural network that was trained on millions of theorems and proofs. The network proposed more than 50,000 new formulas, but, as they acknowledged, many of these were duplicates: “It seems that we are not yet capable of proving the more interesting conjectures.”
A research team led by Christian Szegedy of Google Research sees automated theorem provers as a subset of the field of natural language processing, and plans to capitalize on recent advances in the field to demonstrate solid mathematical reasoning. He and other researchers have proposed a “skip-tree” task scheme that exhibits suprisingly strong mathematical reasoning capabilities. Out of thousands of generated conjectures, about 13% were both provable and new, in the sense of not merely being duplicates of other theorems in the database.
For additional examples and discussion of recent research in this area, see this Quanta Magazine article by Stephen Ornes.
What does the future hold?
So where is all this heading? With regards to computer mathematics, Timothy Gowers predicts that computers will be able to outperform human mathematicians by 2099. He says that this may lead to a brief golden age, when mathematicians still dominate in original thinking and computer programs focus on technical details, “but I think it will last a very short time,” given that there is no reason that computers cannot eventually become proficient at the more creative aspects of mathematical research as well.
Some mathematicians are already envisioning how this software can be used in day-to-day research. Jeremy Avigad of Carnegie Mellon University sees it this way:
You get the maximum of precision and correctness all really spelled out, but you don’t have to do the work of filling in the details. … Maybe offloading some things that we used to do by hand frees us up for looking for new concepts and asking new questions.
One implication of all this is that mathematical training, both for mathematics majors and other students, must aggressively incorporate computer technology and teach computer methods for mathematical analysis and research, at all levels of study. Topics for prospective mathematicians should include a solid background in computer science (programming, data structures and algorithms), together with statistics, numerical analysis, machine learning and training in the usage of at least one symbolic computing computing tool such as Mathematica, Maple or Sage.
Mathematical research is hardly the only field that may be revolutionized by advanced computation. Indeed, intelligent computers are destined to transform virtually every aspect and occupation of modern civilization. Thus our modern society must find a way to accommodate this technology, and to deal respectfully with the many people whose lives will be impacted. This will be no picnic, but neither need it be all gloom and doom. The eventual outcome depends on choices we make now.