DARPA To 'radically' Rev Up Mathematics Research. And Yes, With AI

The US Defense Advanced Research Projects Agency, aka DARPA, believes mathematics isn't advancing fast enough.

So to accelerate – or "exponentiate" – the rate of mathematical research, DARPA this week held a Proposers Day event to engage with the technical community in the hope that attendees will prepare proposals to submit once the actual Broad Agency Announcement (BAA) solicitation goes out. Whoa, slow down there, Uncle Sam.

DARPA's project, dubbed expMath, aims to jumpstart math innovation with the help of artificial intelligence, or machine learning for those who prefer a less loaded term.

"The goal of Exponentiating Mathematics (expMath) is to radically accelerate the rate of progress in pure mathematics by developing an AI co-author capable of proposing and proving useful abstractions," the agency explains on its website.

Speaking at the event, held at the DARPA Conference Center in Arlington, Virginia, DARPA program manager Patrick Shafto made the case for accelerating math research by showing just how slowly math progressed between 1878 and 2018.

These fields have experienced changes but mathematics hasn't, and what we want to do is bring that change to mathematics

During that period, math advancement – measured by the log of the annual number of scientific publications – grew at a rate of less than 1 percent.

This is based on research conducted in 2021 by Lutz Bornmann, Robin Haunschild, and Rüdiger Mutz, who calculated the overall rate of scientific growth across different disciplines amounts to 4.10 percent.

Scientific research also brings surges of innovation. In life sciences, for example, the era of Jean-Baptiste Lamarck (1744-1829) and Charles Darwin (1809-1882), the period between 1806 and 1848 saw a publication growth rate of 8.18 percent. And in physical and technical sciences, 25.41 percent growth was recorded between 1793 and 1810, a period that coincided with important work by Joseph-Louis Lagrange (1736–1813).

"So these fields have experienced changes but mathematics hasn't, and what we want to do is bring that change to mathematics," said Shafto during his presentation.

DARPA's proposed innovation accelerant is artificial intelligence. But the problem is that AI just isn't very smart. It can do high school-level math but not high-level math.

As noted on one of Shafto's slides, "OpenAI o1 (Strawberry) continues to abjectly fail at basic math despite claims of reasoning capabilities."

Nonetheless, expMath's goal is to make AI models capable of:

1. auto decomposition – automatically decompose natural language statements into reusable natural language lemmas (a proven statement used to prove other statements); and
2. auto(in)formalization – translate the natural language lemma into a formal proof and then translate the proof back to natural language.

Robin Rowe, founder and CEO of the AI research institute Fountain Abode, attended the event. As he explained to The Register, he majored in math in college but found it dull so he went into computer science.

Nonetheless, he said, he found it interesting that the goal appears to be creating an AI mathematician that can serve as a coworker, one that's equivalent to a graduate student capable of helping with proofs.

That is, he allowed, a higher level of competency than is currently exhibited in AI models.

"We have chain-of-thought now," said Rowe. "And so this is like chain-of-thought on steroids."

• As ChatGPT scores B- in engineering, professors scramble to update courses
• Google DeepMind's latest models kinda sorta take silver at Math Olympiad
• Alibaba pits people against AI in its annual mathematics competition
• Finally! A solution to 42 – the Answer to the Ultimate Question of Life, The Universe, and Everything

For Rowe, the question is how AI can be made better at advanced math.

"Patrick Shafto, who is the project manager for this, he wrote the paper [PDF] on Bayesian induction, which is the idea that you can figure this out using a large language model," said Rowe.

"That's not the way I lean, but it's the way that a lot of the room lean because that's sort of the obvious next step if you're going to use existing technology.

What I think we need is mathematical reasoning

"For the people in the room, they're like, 'Oh, you know, LLMs have got a lot better in the last year. We'll just keep going.' It's an indication of DARPA's concern about how tough this may be that it's a three-year program. That's not normal for DARPA.

"But for myself, what I think we need is mathematical reasoning. The bids aren't in yet, but that's the direction that we plan to take. But there are other people there who also had a different take, such as doing geometric mathematical reasoning and things like that. There's probably a dozen different ways to do this."

In other words, Rowe isn't sure that focusing on natural language is the right path. He suggests models based on visual or audio input will be more adept at advanced math.

"Do we choose to go with the Bayesian induction on LLMs, which seems like kind of what you would first think of if this was your field," asked Rowe. "Or do we go with something more radical like geometric modeling and doing it visually, for instance, instead of using words at all.

"And it wasn't discussed in the room, but there are mathematicians who do audio calculating in their heads – they feel numbers as musical tones. And so there's a lot of wild stuff that people could propose if we model it on how mathematicians actually do proofs in real life, because there are many different methodologies. Most people just know about the common ones, because these other things require that you have some kind of genius ability that isn't normal."

That said, Rowe is optimistic. "I think we're going to kill it, honestly. I think it's not going to take three years. But I think it might take three years to do it with LLMs. So then the question becomes, how radical is everybody willing to be?" ®