Weryfikacja formalna pomaga ratować demokrację (i sterować rakietami)
SpaceVote to nowy międzynarodowy projekt badawczy, realizowany przez Instytut Podstaw Informatyki PAN, SpaceForest z o.o. i Uniwersytet Luksemburski. Celem jest wykorzystanie najnowszych osiągnięć weryfikacji probabilistycznej do analizy tak różnorodnych zjawisk, jak wpływanie na wyborców podczas głosowania i manewrowanie prostą rakietą bezzałogową.
W ciągu ostatnich 30 lat świat przekształcił się w globalną, gęsto połączoną wioskę. Dotyczy to w pierwszym rzędzie usług i systemów IT, które obsługują skomplikowaną sieć użytkowników, rozproszonych na dużym obszarze geograficznym i pochodzących z różnych kontekstów kulturowych. Co więcej, usługi IT są tworzone przez ludzi i dla ludzi. W konsekwencji, analiza tych systemów musi brać pod uwagę czynnik ludzki i społeczny - co jest ogromnym wyzwaniem, gdyż ludzkie zachowania notorycznie wymykają się próbom formalnego, matematycznego opisu.
Procedury wyborcze są świetnym przykładem takich usług. Są niezwykle ważne dla społeczeństwa, a równocześnie z trudem poddają się formalnej weryfikacji. Tymczasem społeczeństwa demokratyczne stoją w obliczu poważnych zagrożeń. Oszustwa wyborcze, manipulowanie wyborcami, fake news i dezinformacja są wykorzystywane do zmiany wyników wyborów, a jeśli to się nie uda - do podważania tych wyników. SpaceVote to trzeci już z rzędu projekt, w którym łączymy techniki weryfikacji formalnej, teorii gier i logiki matematycznej, by lepiej oceniać i zapobiegać zagrożeniom dla demokracji.
W projekcie SpaceVote pokażemy również, że te same algorytmy mogą być wykorzystane w szerokiej palecie zastosowań, w szczególności do lepszej syntezy strategii dla prostych autonomicznych rakiet, poruszających się w niepewnym środowisku.
Projekt SpaceVote otrzymał finansowanie w ramach XI konkursu POLLUX Narodowego Centrum Badań i Rozwoju realizowanego w ramach programu CORE 2022, program luksemburskiej agencji Fonds National de la Recherche (FNR). W ramach konkursu POLLUX finansowane są bilateralne, polsko-luksemburskie projekty badawcze.
Instytut Podstaw Informatyki Polskiej Akademii Nauk jest jednym z wiodących badawczych centrów informatycznych w kraju. W Instytucie prowadzone są badania dotyczące uczenia maszynowego, wnioskowania statystycznego i teorii informacji, modelowania różnicowego i probabilistycznych modeli języka naturalnego. Wypracowywane są i rozwijane metody do analizy i modelowania wielkich zbiorów danych medycznych, dotyczących przede wszystkim chorób cywilizacyjnych (nowotwory i cukrzyca typu 2). Odrębnym istotnym tematem badawczym jest inżynieria pozyskiwania wiedzy z różnych źródeł, w tym pochodzących z wyszukiwarek internetowych. Kolejnym tematem badań są systemy wieloagentowe, ich specyfikacja i formalna weryfikacja obejmujące m.in. modelowanie i weryfikacja rzeczywistych procedur wyborczych i protokołów elektronicznego głosowania. Od lat prowadzone są także prace z zakresu lingwistyki komputerowej, w tym badania dotyczące formalnego opisu języka naturalnego, a także realizowane są krajowe i międzynarodowe projekty mające na celu budowę narzędzi i zasobów pozwalających na automatyczne przetwarzanie tekstów.
SpaceForest (Gdynia) jest małym, prężnym przedsiębiorstwem R&D, specjalizującym się w zastosowaniach kosmicznych. SpaceForest rozwija i komercjalizuje innowacyjne rozwiązania w dziedzinie technik mikrofalowych, sztucznej inteligencji, zaawansowanej elektronice i technologiach rakietowych. Firma opracowuje i wdraża technologie dla systemów kosmicznych, autonomiczne rozwiązania w zakresie śledzenia i komunikacji dla pojazdów powietrznych oraz prowadzi eksperymenty na pokładzie samodzielnie opracowanych rakiet eksperymentalnych. Współpraca z ESA (Europejską Agencją Kosmiczną) doprowadziła do opracowania niskoszumowych generatorów wysokiej częstotliwości, półprzewodnikowych wzmacniaczy mocy oraz budowy środowiska testowego systemu zbierania danych dla misji JUICE (Jupiter Icy Moons Explorer) ESA. SpaceForest będzie reprezentowany przez dr. habil. Jerzego J. Michalskiego, jej dyrektora ds. badań i rozwoju oraz członka Sekcji Mikrofalowej Polskiej Akademii Nauk.