Artificial intelligence can write a poem in the style of Walt Whitman, provide dating advice and suggest the best way to cook an artichoke. But when it comes to mathematics, large language models like OpenAI’s ChatGPT have sometimes stumbled over basic problems. Some see this as an inherent limitation of the technology, especially when it comes to complex reasoning.
A new initiative from the Defense Advanced Research Projects Agency (Darpa) seeks to account for that shortfall by enlisting researchers in finding ways to conduct high-level mathematics research with an AI “co-author”. The goal of the new grant-making programme, Exponentiating Mathematics, is to speed up the pace of progress in pure (as opposed to applied) maths — and, in doing so, to turn AI into a superlative mathematician.
“Mathematics is this great test bed for what is right now the key pain point for AI systems,” said Patrick Shafto, a mathematician and computer scientist from Rutgers University, US, who now serves as a programme manager in Darpa’s information innovation office, known as I20. “So if we overcome that, potentially, it would unleash much more powerful AI.” He added, “There’s huge potential benefit to the community of mathematicians and to society at large.”
Shafto spoke from his office at Darpa’s headquarters, an anonymous building in northern Virginia, US, whose facade of bluish glass gives little indication that it houses one of the most unusual agencies in the federal government.
“By improving mathematics, we’re also understanding how AI works better,” said Alondra Nelson, who served as a top science adviser in President Joe Biden’s administration and is a faculty member at the Institute for Advanced Study in Princeton, New Jersey, US. “So I think it’s kind of a virtuous cycle of understanding.” She suggested that, down the road, maths-adept AI could enhance cryptography and aid in space exploration.
Started after World War II to compete with the Soviet Union in the space race, Darpa is most famous for fostering the research that led to the creation of Arpanet, the precursor to the Internet we use today. Darpa later funded the research that gave rise to drones and Apple’s digital assistant, Siri. But it is also responsible for the development of Agent Orange, the potent defoliant used to devastating effect during the Vietnam War.
“I’m sure this isn’t 100 per cent innocent,” Andrew Granville, a mathematician at the University of Montreal, Canada, said of Darpa’s maths initiative, although he emphasised that he was only speculating about eventual outcomes. Darpa is, after all, part of the Pentagon, even if it has traditionally operated with enviable independence. The US military is rapidly incorporating AI into its operations, with the aim of not losing out to China and its People’s Liberation Army or to Russia, which has been testing out new technologies on the battlefield in Ukraine.
A surfer and skateboarder in his free time, Shafto, 49, sat in a sparse conference room one recent afternoon, imagining a future when AI would be as good at solving multistep problems as it is at trying to glean meaning from huge troves of texts, which it does through the use of probability theory.
“There are great mathematicians who work on age-old problems,” Shafto said. “That’s not the kind of thing that I’m particularly interested in.” Instead, he wanted the discipline to move more quickly by using AI to save time.
“Problems in mathematics take decades, or centuries sometimes, to solve,” he said in a recent presentation at Darpa’s headquarters on the Exponentiating Mathematics project, which was accepting applications till mid-July. He then shared a slide showing that, in terms of the number of papers published, maths had stagnated during the last century while life and technical sciences had exploded. In case the point wasn’t clear, the slide’s heading drove it home: “Math is sloooowwww.”
The kind of pure maths Shafto wants to accelerate tends to be “sloooowwww” because it is not seeking numerical solutions to concrete problems, the way applied mathematics does. Instead, pure maths is the heady domain of visionary theoreticians who make audacious observations about how the world works, which are promptly scrutinised (and sometimes torn apart) by their peers.
“Proof is king,” Granville said.
Maths proofs consist of multiple building blocks called lemmas, minor theorems employed to prove bigger ones. Whether each Jenga tower of lemmas can maintain integrity in the face of intense scrutiny is precisely what makes pure maths such a “long and laborious process”, acknowledged Bryna R. Kra, a mathematician at Northwestern University, US. “All of maths builds on previous maths, so you can’t really prove new things if you don’t understand how to prove the old things,” she said. “To be a research mathematician, the current practice is that you go through every step, you prove every single detail.”
Lean, a software-based proof assistant, can speed up the process, but Granville said it was “annoying, because it has its own protocols and language”, requiring programming expertise. “We need to have a much better way of communication,” he added.
Could artificial intelligence save the day? That’s the hope, according to Shafto. An AI model that could reliably check proofs would save enormous amounts
of time, freeing mathematicians to be more creative.
NYTNS
