Tým počítačových vědců z University of Massachusetts Amherst vyvinul inovativní metodu nazvanou Baldur, která využívá sílu velkých jazykových modelů (LLM) k automatickému generování důkazů pro prevenci chyb a ověřování kódu. Tato průlomová technika, ve spojení s pokročilým nástrojem Thor, dosáhla dosud nevídané účinnosti téměř 66 %. Výzkum týmu byl oceněn Cenou za vynikající práci na ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering.
Chybový software se stal běžným problémem v našem každodenním životě, přičemž se jedná o problémy od drobných nepříjemností, jako jsou formátovací chyby a pády, až po vážné bezpečnostní narušení nebo poruchy v kritických systémech jako je průzkum vesmíru nebo zdravotnická zařízení. Tradiční metody kontroly softwaru zahrnují ruční ověřování kódu nebo spuštění kódu s očekávanými výsledky, ale tyto přístupy jsou náchylné k lidským chybám a jsou časově náročné pro složité systémy.
Alternativní technika, nazvaná strojová kontrola, zahrnuje generování matematických důkazů, které demonstují, že kód funguje podle zamýšleného účelu. Ruční vytváření těchto důkazů je však pracný a specializovaný úkol, který vyžaduje značný čas a odbornost. Emily First, hlavní autorka výzkumu, vysvětluje, že tyto důkazy často mohou být delší než samotný kód softwaru.
Pro řešení tohoto problému tým zkoumal potenciál velkých jazykových modelů, jako je ChatGPT, k automatickému generování důkazů. Velké jazykové modely se stávají stále výkonnějšími a dokáží rozumět složitým kontextům, což je činí vhodnými pro asistenci při prevenci chyb a ověřování kódu. Integrací metody Baldur s nástrojem Thor dosáhli výzkumníci úctyhodné účinnosti téměř 66 %.
Kombinace zpracování přirozeného jazyka a umělé inteligence umožňuje generování přesných a spolehlivých důkazů, což výrazně snižuje potenciální riziko lidských chyb. Tento pokrok slibuje velké možnosti v oblasti softwarového inženýrství a pomáhá zvyšovat kvalitu a spolehlivost softwarových systémů. S postupujícím vývojem technologií by využití strojové kontroly řízené umělou inteligencí mohlo stát běžnou praxí pro zajištění bezchybného softwaru s nižším rizikem kritických poruch.
The source of the article is from the blog be3.sk