Kliknąłeś w wilka brawo !

Czasem błąd w algorytmie ujawnia się szybko, niekiedy zaś dopiero po bardzo długim czasie. Jak znaleźć ten zakres, w którym program może się „wykrzaczyć”? Za rozwiązanie tego problemu dla modelu VASS nagrodzono zespół z polskimi informatykami.

Polsko-niemiecko-brytyjski zespół informatyków otrzymał nagrodę za najlepszą pracę w ramach 50. edycji konferencji International Colloquium on Automata, Languages and Programming (ICALP) 2023. Konferencja ICALP jest podzielona na dwie ścieżki: algorytmiczną i logiczną. Ta praca jest ze ścieżki logicznej. ICALP to jedna z dwóch najważniejszych konferencji logicznych w informatyce teoretycznej.

Wspomniany artykuł (preprint został przesłany do serwisu Arxiv ) dotyczy wykrywania błędów w algorytmach.

„Nasze rozwiązanie wyjaśnia, jak dobry może być algorytm dotyczący tzw. problemu pokrywalności dla modelu VASS - zarówno jak szybko może działać i ile czasu musi wymagać, żeby działał poprawnie”, opisuje w rozmowie z portalem PAP Nauka w Polsce jeden z autorów dr Filip Mazowiecki z Uniwersytetu Warszawskiego. „Jeśli pisze się programy, to chciałoby się sprawdzać automatycznie, czy w wyniku ich działania może dojść do jakiegoś błędu. W ramach działu informatyki, którym się zajmuję - weryfikacji formalnej - zajmuję się modelami, które wykrywają różne rodzaje błędów”, tłumaczy naukowiec.

Badaczom po pierwsze chodziło o to, żeby pokazać, kiedy może najszybciej dojść do błędu przy wykonywaniu danego algorytmu. A z drugiej strony - pokazać, ile maksymalnie kroków trzeba wykonać, żeby mieć pewność, że dalej wszystko pójdzie już bezbłędnie. Czyli chodziło o to, by dowiedzieć się, ile ma najkrótsza i najdłuższa droga do błędu.

Na warsztat wzięli tzw. model VASS. Jakiego typu problemów dotyczy ten algorytm? Przypuśćmy, że mamy 5 współrzędnych, każda z nich opisuje liczbę osób w danym pomieszczeniu: mamy salon, łazienkę, kuchnię, przedpokój i sypialnię. W kolejnych krokach różne osoby wchodzą do mieszkania i poruszają się po pomieszczeniach (to tzw. tranzycje) według określonych zasad (to właśnie VASS). Np. do mieszkania można wejść tylko przez przedpokój, z kuchni można przejść do salonu, ale nie do sypialni itp. Jest pewna liczba przejść między pomieszczeniami. Problem pokrywalności polega na tym, że chcemy wykryć tranzycję, która jest zgodna z regułami, ale niepożądana - jest błędem. Takim błędem może być np. sytuacja, w której dwie osoby (albo więcej) znajdą się jednocześnie w łazience (a w innych pomieszczeniach - wszystko jedno). Początkiem drogi, którą badali naukowcy byłoby więc wejście pierwszej osoby do mieszkania, a końcem drogi - wejście osoby do zajętej łazienki. „Sprawdzamy więc, ile ruchów musi minąć, zanim będzie pewność, że najszybciej może dojść do błędu. I jak daleko od startu może się znaleźć niepożądana sytuacja” - tłumaczy informatyk z UW.

To oczywiście uproszczony przykład, ale algorytmy działające zgodnie z podobnymi regułami mogą się przydawać np. przy okazji rozdzielania zadań między komputery czy procesory. Można sobie wyobrazić, że błąd wystąpi, jeśli dwa komputery jednocześnie będą chciały wykonać jedno zadanie. Dobrze więc umieć przewidzieć czy może dojść do takiej sytuacji i kiedy. „A może być ogromna liczba kroków, kiedy jeszcze nie dojdzie do błędu, ale on cały czas jest możliwy”, mówi Filip Mazowiecki.

Już w l. 70. XX wieku badano złożoność algorytmu VASS, jeśli chodzi o pamięć, a więc jaką minimalnie pamięcią komputera trzeba dysponować, aby rozwiązać problem. Polsko-niemiecki zespół badawczy pokazał, jaka jest złożoność tego algorytmu, jeśli chodzi o czas.

Pytany o możliwe zastosowania tej pracy, Filip Mazowiecki zaznacza, że jest to wynik teoretyczny. „Weryfikacja formalna powinna z założenia dawać odpowiedzi na pytania dlaczego coś działa, a dlaczego nie, gdzie są błędy. Jeśli chodzi o takie zagadnienia jak machine learning - to czasem się słyszy, że te algorytmy działają, ale nikt nie wie dlaczego i czy są tam błędy. I rzeczywiście - one działają szybko, bo są niedokładne. Problem przy stosowaniu formalnych metod weryfikacji jest taki, że to spowalnia liczenie”, mówi. Ale są i obszary, gdzie taka dokładność i bezbłędność jest konieczna. Podsumowuje, że może badania z tego obszaru nie służą bezpośrednio do rozwiązywania problemów, z którymi mierzy się ludzkość, jednak nie każda praca ma temu służyć. Tu akurat jest to raczej kwestia estetyki.

Autorami nagrodzonej pracy są: Marvin Künnemannem (RPTU Kaiserslautern-Landau, Niemcy), Filip Mazowiecki (Uniwersytet Warszawski, Polska), Lia Schütze (Max Planck Institute for Software Systems, Niemcy) Henry Sinclaire-Banks (University of Warwick, Anglia) oraz Karol Węgrzycki z (Saarland University, Niemcy, wcześniej robił doktorat na Uniwersytecie Warszawskim).