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. A to jedna z dwóch najważniejszych konferencji logicznych w informatyce teoretycznej.

Praca (https://arxiv.org/abs/2305.01581) 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 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. Filip Mazowiecki tłumaczy, 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. A zespół z Polski i Niemiec pokazał, jaka jest złożoność tego algorytmu, jeśli chodzi o czas.

Praca ma pięciu współautorów, z dwóch środowisk matematyków - logików i algorytmików (a więc reprezentują dwie ścieżki ICALP). Wykorzystując pomysły z obu obszarów matematyki badacze znaleźli rozwiązanie problemu. "Z badaniami na pograniczu obszarów bywa różnie - albo nikt ich nie zrozumie i trafiają do śmietnika, albo są doceniane za innowacyjność" - uśmiecha się Filip Mazowiecki.

W tym przypadku praca znalazła uznanie. "Chyba po prostu wyszło nam to bardzo zgrabnie. Dla osób, które siedzą w temacie, problem jest dość naturalny i nie jest trudny do zrozumienia, a przedstawienie rozwiązania jest klarowne i ładne" - komentuje badacz.

Pytany o możliwe zastosowania tej pracy, naukowiec 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 naukowiec. Ale są i obszary, gdzie taka dokładność i bezbłędność jest konieczna.

"Mój doktorant, który też zajmował się weryfikacją formalną, odszedł do korporacji i implementuje zagadnienia związane z takimi zagadnieniami" - zwraca uwagę Filip Mazowiecki.

Podsumowuje, że może badania z tego obszaru nie służą bezpośrednio do rozwiązywania problemów, z którymi mierzy się ludzkość. Ale nie każda praca ma temu służyć. Tu akurat jest to raczej kwestia estetyki. "Naszą pracę można porównać do pisania książek. Kierujemy jednak nasze prace nie do masowej publiczności, ale do zupełnie innej grupy docelowej" - porównuje informatyk.

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).