Skupina računalniških znanstvenikov z Univerze v Massachusetts Amherst je razvila inovativno metodo Baldur, ki izkorišča moč velikih jezikovnih modelov (LLM) za samodejno generiranje dokazov za preprečevanje napak in preverjanje kode. S kombiniranjem te prebojne tehnike s naprednim orodjem Thor so dosegli izjemno učinkovitostno stopnjo skoraj 66%. Raziskava ekipe je bila nagrajena z nagrado za odličen članek na skupnem evropsko-ameriškem simpoziju o programski inženiringu in osnovah programskega inženirstva.
Napake v programski opremi so postale vsakdanji problem v našem vsakdanjem življenju, pri čemer se težave gibljejo od manjših motečih težav, kot so težave z oblikovanjem in sesutja, do resnih varnostnih kršitev ali okvar kritičnih sistemov, kot so raziskovanje vesolja ali medicinski pripomočki. Običajne metode preverjanja programske opreme vključujejo ročno preverjanje kode ali zagon kode z uporabo pričakovanih rezultatov, vendar so te metode nagnjene k človeškim napakam in zahtevajo veliko časa pri kompleksnih sistemih.
Alternativna tehnika, imenovana strojno preverjanje, vključuje generiranje matematičnih dokazov za prikaz, da koda deluje kot je bilo načrtovano. Vendar je ročno ustvarjanje teh dokazov dolgotrajno in specializirano opravilo, ki zahteva veliko časa in strokovnosti. Vodja raziskave Emily First pojasnjuje, da so ti dokazi pogosto daljši od same programske kode.
Da bi se soočili s tem izzivom, je ekipa preučila potencial velikih jezikovnih modelov, kot je ChatGPT, za avtomatsko generiranje dokazov. Veliki jezikovni modeli so postali vse močnejši in lahko razumejo kompleksna okolja, kar jih naredi primernega za pomoč pri preprečevanju napak in preverjanju kode. Z integracijo metode Baldur z orodjem Thor so raziskovalci dosegli impresivno učinkovitostno stopnjo skoraj 66%.
Kombinacija obdelave naravnega jezika in umetne inteligence omogoča generiranje natančnih in zanesljivih dokazov, kar pomembno zmanjšuje možnost človeških napak. Ta tehnološki napredek obeta veliko v svetu programskega inženirstva, saj pripomore k izboljšanju kakovosti in zanesljivosti programske opreme. Ko tehnologija še naprej napreduje, lahko izkoriščanje strojnega preverjanja, ki ga poganja umetna inteligenca, postane standardna praksa za zagotavljanje programske opreme brez napak z zmanjšanim tveganjem kritičnih napak.