Szoftverhibák megelőzése
A Massachusetts Amherst-i Egyetem informatikusokból álló kutatócsoportja nemrégiben jelentette be, hogy új módszert dolgozott ki, amellyel megelőzhetők a szoftverhibák, és ellenőrizhető, hogy az alapjául szolgáló kód helyes-e. A Baldur nevű új módszer az LLM-ek mesterséges intelligencia erejét használja ki, és a Thor eszközzel kombinálva közel 66%-os hatékonyságot eredményez.
A szoftverhibák napjainkban mélyreható hatással vannak a társadalomra. A bosszantó, de jelentéktelen hibáktól kezdve, amelyek akkor bukkannak fel, amikor dolgozni próbálunk, vagy összeomlanak a filmnéző alkalmazásaink, amikor pihenni próbálunk, egészen a sebezhetőségekig, amelyek az orvosi eszközöket támadhatóvá teszik, vagy amelyek lehetővé teszik a hackerek számára, hogy személyes adatokat lopjanak, több milliárd dolláros kárt okozva a gazdasági növekedésben – írta Jurij Brun, az UMass Amherst-i Manning College of Information and Computer Sciences professzora és a tanulmány vezető szerzője.
Baldur felépítése több hónapot vett igénybe. A munka a Google-lal együttműködésben készült, és jelentős mennyiségű korábbi kutatásra épült. Először, akinek a csapata a Google-nál végezte a munkáját, a Minervát, egy nagy természetes nyelvű szövegkorpuszon betanított LLM-et használt, majd 118 GB matematikai tudományos dolgozaton és matematikai kifejezéseket tartalmazó weboldalakon finomhangolta. Ezután tovább finomhangolta az LLM-et egy Isabelle/HOL nevű nyelven, amelyen a matematikai bizonyításokat írják. Baldur ezután egy teljes bizonyítást generált, és a teorémafuttatóval együttműködve ellenőrizte annak munkáját. Amikor a tételpróba hibát észlelt, a bizonyítást, valamint a hibára vonatkozó információkat visszatáplálta az LLM-be, hogy az tanulhasson a hibájából, és új, remélhetőleg hibamentes bizonyítást generálhasson.
Ez a folyamat figyelemre méltó pontosságnövekedést eredményez. A bizonyítások automatikus generálására szolgáló eszköz a Thor nevet kapta, amely az idő 57%-ában képes bizonyításokat generálni. Ha Baldurt (Thor testvére az északi mitológia szerint) Thorral párosítjuk, akkor ők ketten az esetek 65,7%-ában képesek bizonyításokat generálni.