Can AI-Generated Proofs Bring Bug-Free Software One Step Closer?

The University of Massachusetts Amherst has an announcement. A team of computer scientists 'recently announced a new method for automatically generating whole proofs that can be used to prevent software bugs and verify that the underlying code is correct.' It leverages the AI power of Large Language Models, and the new method, called Baldur, 'yields unprecedented efficacy of nearly 66%.'

The idea behind the machine-checking technique was 'to generate a mathematical proof showing that the code does what it is expected to do,' according to the announcement, 'and then use a theorem prover to make sure that the proof is also correct.

But manually writing these proofs is incredibly time-consuming and requires extensive expertise. 'These proofs can be many times longer than the software code itself,' says Emily First, the paper's lead author who completed this research as part of her doctoral dissertation at UMass Amherst... First, whose team performed its work at Google, used Minerva, an LLM trained on a large corpus of natural-language text, and then fine-tuned it on 118GB of mathematical scientific papers and webpages containing mathematical expressions. Next, she further fine-tuned the LLM on a language, called Isabelle/HOL, in which the mathematical proofs are written. Baldur then generated an entire proof and worked in tandem with the theorem prover to check its work. When the theorem prover caught an error, it fed the proof, as well as information about the error, back into the LLM, so that it can learn from its mistake and generate a new and hopefully error-free proof.

This process yields a remarkable increase in accuracy. The state-of-the-art tool for automatically generating proofs is called Thor, which can generate proofs 57% of the time. When Baldur (Thor's brother, according to Norse mythology) is paired with Thor, the two can generate proofs 65.7% of the time. Though there is still a large degree of error, Baldur is by far the most effective and efficient way yet devised to verify software correctness, and as the capabilities of AI are increasingly extended and refined, so should Baldur's effectiveness grow.
In addition to First and Brun, the team includes Markus Rabe, who was employed by Google at the time, and Talia Ringer, an assistant professor at the University of Illinois — Urbana Champaign. This work was performed at Google and supported by the Defense Advanced Research Projects Agency and the National Science Foundation.

Read more of this story at Slashdot.