A team of computer scientists led by the University of Massachusetts Amherst 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.
The effects of buggy software can range anywhere from the annoying-glitchy formatting or sudden crashes-to potentially catastrophic security breaches or the precision software used for space exploration or controlling healthcare devices.
Of course, there have been methods for checking software for as long as it has existed.
One popular method is the simplest: you have a human being go through the code, line by line, manually verifying that there are no errors.
Or you can run the code and check it against what you expect it to do.
The problem with both methods is that they are prone to human error, and checking against every possible glitch is extraordinarily time-consuming, expensive, and infeasible for anything but trivial systems.
A much more thorough but harder method is to generate a mathematical proof showing that the code does what it is expected to do and then use a theorem prover to ensure the proof is also correct.
Manually writing these proofs is incredibly time-consuming and requires extensive expertise.
With the rise of LLMs, of which ChatGPT is the most famous example, a possible solution is to try to generate such proofs automatically.
The work was done as a collaboration with Google, and built on top of a significant amount of prior research.
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 tool for automatically generating proofs is called Thor, which can generate proofs 57% of the time.
When Baldur 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.
This Cyber News was published on www.helpnetsecurity.com. Publication date: Wed, 10 Jan 2024 04:13:05 +0000