UMass Amherst Team Advances in Quest for Bug-Free Software
Summary
– 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. This new method, called Baldur, leverages the artificial intelligence power of Large Language Models (LLMs), and, when combined with the state-of-the-art tool Thor, yields unprecedented efficacy of nearly 66%. "We have unfortunately come to expect that our software is buggy, despite the fact that it is everywhere and we all use it every day," says Yuriy Brun, professor in the Manning College of Information and Computer Sciences at UMass Amherst and the papers senior author. If, for instance, you expect your word-processing software to break the line every time you press the "return" key, but it instead outputs a question mark, then you know something in the code is wrong. "These proofs can be many times longer than the software code itself," says Emily First, the papers lead author who completed this research as part of her doctoral dissertation at UMass Amherst.