Cyber Defence: After reinventing maths, can AI fix software bugs?

Cade Metz

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 had bedevilled the world's smartest humans for decades. In the following weeks, further findings stunned leading mathematicians and raised questions about the future of a field long viewed as the pinnacle of human achievement.

But the implications extend well beyond academia. Using similar techniques, Silicon Valley is now building AI systems that aim to eliminate dangerous flaws, or "bugs", in the world's software. Just as AI can prove a maths problem, it can, at least in theory, prove an application bug-free. This effort, which scientists call "software verification", is vital as the internet faces its biggest cybersecurity threat in decades. Now that leading AI systems can hack into software by identifying and exploiting its flaws with stunning speed, the world needs a new breed of AI that can remove them.

Truth, a new Palo Alto startup, is among the companies building this technology. Like the startups Axiom and Logical Intelligence and labs such as Anthropic and OpenAI, it hopes to verify the world's software using a specialised programming language called Lean, the tool that lets AI solve million-dollar maths problems.

"It is possible to do something that was not possible before," said Clark Barrett, a Stanford University professor and co-founder and co-chief executive of &Truth. "You've seen what has happened in mathematics — proving these massive open conjectures. We can apply the same formal methods to verifying software."

Bugs arise when applications do things they were not designed to do. An application might write too much into system memory, so that it spills over and corrupts other data. Attackers can use such bugs to hack their way in. Verification aims to prevent such mistakes at a logical level, by formally proving that an application behaves only as designed, much as mathematicians prove maths problems — one logical step at a time. Experts can verify software by hand, but it takes years. &Truth and others are building AI systems that could do so in hours or days.

Lean was invented more than a decade ago by Microsoft researcher Leonardo de Moura as a tool for human programmers. Now AI can use it to write its own maths proofs. Through trial and error, a technique called "reinforcement learning", an AI system can learn to write better Lean code and ultimately prove problems that have flummoxed top mathematicians.

The trouble is that training AI for code verification is significantly harder, and the software is much messier than maths, whose rules have been well established for centuries. To verify an application, someone must first lay down formal specifications defining how it should behave. Only then can an AI system write Lean code that verifies this behaviour.

Even then, applications may behave in unexpected ways that let hackers in. Designers cannot anticipate everything that will go wrong once real people start using the application.

The New York Times