In September, OpenAI announced that its new artificial intelligence technology needed less than a week to solve the Navier-Stokes problem, a mathematical puzzle that bedeviled the world’s smartest humans for decades. In the weeks that followed, the company released a deluge of additional findings that stunned leading mathematicians and raised new questions about the future of an academic field that has long been viewed as the pinnacle of human achievement.
But the implications of A.I.’s newfound mathematical skills extend well beyond academic research. Using similar techniques, Silicon Valley is now building A.I. systems that aim to eliminate the dangerous flaws, or “bugs,” in the world’s computer software. Just as an A.I. system can prove a math problem, it can prove that a software application is bug-free — at least in theory.
This sweeping effort to guarantee the integrity of computer software, which scientists call “software verification,” is vitally important as the internet faces its biggest cybersecurity threat in decades. Now that the leading A.I. systems can hack into computer software, by identifying and exploiting its flaws with stunning speed, the world needs a new breed of A.I. that can remove these flaws.
&Truth, a new start-up based in Palo Alto, Calif., is among the many companies working to build this kind of technology. Much like the Silicon Valley start-ups Axiom and Logical Intelligence and leading A.I. labs like Anthropic and OpenAI, &Truth hopes to verify the world’s software using a specialized computer programming language called Lean, the same tool that allows A.I. technologies to solve million-dollar math problems.
“It is possible to do something that was not possible before,” said Clark Barrett, a Stanford University professor who is among the founders of &Truth and its co-chief executive. “You’ve seen what has happened in mathematics — proving these massive open conjectures. We can apply the same formal methods to verifying software.”
Software bugs arise when applications do things they were not designed to do. An application might store information in the wrong database or write too much information into system memory, so that it spills into the wrong memory register and corrupts other data. Malicious attackers can use these bugs to hack their way into the application.
Software verification is an effort to prevent such mistakes at a logical level. The aim is to formally prove that an application behaves only as it was designed to behave, much in the way that mathematicians prove math problems — one logical step at a time.
Experienced engineers can verify software by hand, but this requires years of work. Now, companies like &Truth are working to build A.I. systems that can verify software in a matter of hours or days, which would finally provide a practical way of ensuring the integrity of computer software.
Lean, the coding language these efforts revolve around, was invented more than a decade ago by a Microsoft researcher named Leonardo de Moura. He designed the language as a tool for human programmers, but now that A.I. technologies can generate their own computer code, they too can use Lean to write their own math proofs. Through extreme trial and error — a technique called “reinforcement learning” — an A.I. system can learn to write better Lean code and, ultimately, prove math problems that have flummoxed top mathematicians for decades.
Companies like &Truth aim to eliminate buggy software using similar techniques. The trouble is that training A.I. systems for code verification is significantly more difficult than training them for math.
Part of the problem is that software code is much messier than math. The rules of math are well established — and have been for centuries. To verify the integrity of a software application, someone must first lay down a set of formal specifications that define how the application is supposed to behave. Only then can an A.I. system write Lean code that verifies this behavior.
Even then, applications may behave in unexpected and unwanted ways that allow malicious hackers into the system. An application’s designers cannot anticipate everything that will go wrong once they roll the application into the real world and real people start to use it.
“How do you know that your assumptions are correct?” said Will Wilson, chief executive of Antithesis, a company that tests computer code for bugs and security holes. “At some point, code comes into contact with messy reality.”
At this point, companies like &Truth are a long way from ensuring that all software is bug-free. But at a moment when A.I.-enabled hacking is threatening online security like never before, any bit of progress helps.
“There is an urgency that was increasingly palpable beginning at the end of last year,” said Chris Hsu, &Truth’s co-founder and co-chief executive. “This security problem is a defining problem of our time.”
The post After Reinventing Mathematics, Can A.I. Eradicate Computer Bugs? appeared first on New York Times.
