Strona w trakcie przygotowywania - przepraszamy za niedogodności

Uporządkowana struktura głównych obszarów tematycznych będących przedmiotem naszych badań oraz szczegółowe charakterystyki projektów – wraz z ich listą – obejmują kontekst, cele, zakres techniczny i zastosowania. Strona pełni funkcję informacyjną oraz orientacyjną, prezentując zarówno kierunki naszych prac, jak i aktualnie rozwijane inicjatywy badawcze i projektowe.

Zachęcamy do współpracy, która może obejmować różne formy zaangażowania: od zwykłego uczestnictwa w projektach i realizacji eksperymentów, przez przygotowanie prac dyplomowych inżynierskich i magisterskich, aż po – w przypadku osób o zacięciu naukowym – współautorstwo publikacji, rozwijanie wyników badawczych oraz działania prowadzące do uzyskania wyższych stopni naukowych.

Obszar tematyczny

Słowa kluczowe: Large Language Models, Generative AI, Reasoning, Context Understanding, Agentic AI, Multimodal Processing, Explainability

Generatywna Sztuczna Inteligencja, a w szczególności duże modele językowe (LLM), zmienia sposób projektowania systemów informatycznych. Modele te potrafią rozumieć język naturalny, generować treści, interpretować kontekst, analizować dane oraz wspierać podejmowanie decyzji. Wprowadzają nową jakość w obszarach takich jak programowanie, modelowanie, analiza procesów, interakcja człowiek–komputer czy inteligentne środowiska.

LLM są „game changerem”, ponieważ:

• działają uniwersalnie — mogą analizować, streszczać, projektować i generować,
• rozumieją opisy zadań i potrafią tworzyć formalne artefakty (kod, modele, reguły),
• łączą dane symboliczne i opisowe, umożliwiając semantyczną interpretację kontekstu,
• umożliwiają tworzenie agentów potrafiących samodzielnie planować działania,
• działają multimodalnie (tekst, obraz, dane), co otwiera nowe zastosowania.

Jednocześnie obszar ten wiąże się z wyzwaniami: kontrolą jakości generacji, stabilnością wyników, interpretowalnością, bezpieczeństwem, halucynacjami oraz potrzebą integrowania modeli z klasycznymi narzędziami analitycznymi i weryfikacyjnymi. To czyni tę dziedzinę intensywnie rozwijaną i badawczo bardzo atrakcyjną.

LLM stają się fundamentem nowych platform obliczeniowych, środowisk developerskich, narzędzi analitycznych i systemów agentowych. Ich skuteczne wykorzystanie wymaga zrozumienia ich możliwości, ograniczeń oraz metod łączenia ich z klasycznymi technikami inżynierii oprogramowania.

Przykładowe tematy projektowe:

Słowa kluczowe: Kreatywność, Myślenie Dywergencyjne, Testy Alternatywnych Zastosowań (AUT), Generative AI, Human-AI Interaction, Oryginalność

Projekt bada fundamentalne różnice w naturze i przejawach kreatywności pomiędzy ludźmi a dużymi modelami językowymi (LLM). Kreatywność jest często uznawana za unikalną cechę ludzką; w obliczu możliwości LLM do generowania nowych, złożonych i czasem zaskakujących treści, konieczne staje się systematyczne zbadanie, jak generatywna AI realizuje proces twórczy.

Metodologia: Zostanie opracowany zestaw zadań kreatywnych (np. Test Alternatywnych Zastosowań - generowanie nietypowych zastosowań dla prostych przedmiotów; zadania z Twórczego Rozwiązywania Problemów - generowanie nowych pomysłów, wariantów rozwiązań, nietypowych interpretacji). Zadania te będą wykonywane przez dwie grupy: uczestników ludzkich oraz różne warianty modeli LLM (np. z różnymi technikami promptowania lub „temperaturą”).

Oceniane aspekty kreatywności (zgodnie ze standardami psychometrycznymi):

• Oryginalność (Novelty): Rzadkość występowania pomysłu.

• Różnorodność (Fluency): Liczba wygenerowanych pomysłów.

• Elastyczność (Flexibility): Liczba różnych kategorii, do których należą pomysły.

• Użyteczność (Usefulness/Elaboration): Praktyczność i poziom rozwinięcia pomysłu.

• Odwaga Poznawcza: Skłonność do generowania ryzykownych, ale potencjalnie przełomowych idei.

Cel Projektu: Zrozumienie, w jakich obszarach (np. szybkość, różnorodność) modele generatywne przewyższają ludzi, a w jakich (np. oryginalność, głęboka interpretacja kontekstu) ludzie nadal zachowują przewagę. Projekt ma na celu wizualizację profilu kreatywności obu stron.

Materiały:

• Large language models show both individual and collective creativity comparable to humans
• Divergent Creativity in Humans and Large Language Models

Słowa kluczowe: Formal Logic, Dedukcja, Reasoning, Explainable AI (XAI), Semantic Interoperability, Halucynacje

Projekt bada innowacyjne podejście do wnioskowania, łącząc elastyczność i kreatywność Dużych Modeli Językowych (LLM) z precyzją i weryfikowalnością klasycznych silników wnioskujących (np. systemy reguł, Solvery, bazy danych grafów logicznych).

Celem jest stworzenie systemu, w którym LLM pełni funkcję Interpretera Języka Naturalnego (tłumacząc zapytania na formalne reguły) oraz Generatywnego Proponującego (tworząc wstępne hipotezy). Następnie, klasyczny silnik dedukcyjny przejmuje rolę Weryfikatora i Finalnego Wnioskującego, gwarantując logiczną spójność i poprawność wyniku.

Projekt wymaga implementacji technik konwersji języka naturalnego na formalne reguły oraz ewaluacji, w jaki sposób model hybrydowy poprawia weryfikowalność i ogranicza halucynacje w zadaniach wymagających ścisłej logiki.

Materiały:

• Towards Data-And Knowledge-Driven AI: A Survey on Neuro-Symbolic Computing
• Neuro-symbolic artificial intelligence: a survey

Słowa kluczowe: Retrieval-Augmented Generation (RAG), Context Understanding, Data Quality, Prompt Engineering, Halucynacje, Faithfulness

Halucynacje (generowanie nieprawdziwych, ale brzmiących wiarygodnie informacji) są kluczowym wyzwaniem w zastosowaniach LLM opartych na wiedzy. Projekt skupia się na stworzeniu zaawansowanego frameworku RAG, który ma na celu minimalizację halucynacji i zwiększenie weryfikowalności odpowiedzi w oparciu o zaufaną bazę wiedzy.

Innowacja polega na udoskonaleniu trzech kluczowych etapów RAG:

• Pobieranie Kontekstu: Eksperymentowanie z zaawansowanymi strategiami pobierania (np. Multi-Hop RAG, Re-ranking).

• Generacja: Optymalizacja promptów, aby wymagały od LLM cytowania źródła dla każdego faktu.

• Autoweryfikacja (Self-Correction/Critique): Opracowanie drugiego etapu, w którym model krytycznie ocenia swoją własną odpowiedź w kontekście pobranych dokumentów, identyfikując i korygując potencjalne halucynacje.

Efektem jest implementacja architektury RAG oraz ewaluacja wskaźników Faithfulness (wierność źródłu) i Answer Relevance (trafność odpowiedzi).

Materiały:

• A Survey on Hallucination in Large Language Models: Principles, Taxonomy, Challenges, and Open Questions

Słowa kluczowe: Safety, Security, Responsible AI, Guardrails, Prompt Injection, Jailbreaking, Content Moderation

LLM wdrożone w środowiskach produkcyjnych wymagają silnych mechanizmów bezpieczeństwa, zwanych Guardrails (Bariery Ochronne), które kontrolują zarówno intencję użytkownika (wejście), jak i treść generowaną przez model (wyjście).

Projekt polega na zaprojektowaniu i zaimplementowaniu modułu Guardrails, który chroni system przed:

• Prompt Injection/Jailbreaking: Złośliwymi instrukcjami mającymi na celu złamanie wewnętrznych reguł LLM.

• Generowaniem Szarej Strefy (Harmful Content): Uzyskaniem toksycznych, nieetycznych lub poufnych informacji.

Moduł ten działa jako pośrednik między użytkownikiem a LLM, wykorzystując techniki takie jak klasyfikatory semantyczne do walidacji intencji oraz Output Filtering do sprawdzania zgodności wygenerowanej odpowiedzi z polityką bezpieczeństwa.

Oczekiwany rezultat to gotowy moduł Guardrails, który jest testowany pod kątem odporności na ataki i skuteczności w zapobieganiu niepożądanym treściom.

Materiały:

• A survey on large language model (LLM) security and privacy: The Good, The Bad, and The Ugly

Obszar tematyczny

Słowa kluczowe: Multi-Agent Systems, Agentic AI, LLM-driven Agents, AutoGen, LangGraph, Generative AI, Context-Aware Agents, Proactive Systems

Systemy agentowe (MAS) umożliwiają budowę rozproszonych, autonomicznych i współpracujących komponentów, które wspólnie realizują złożone zadania. Wraz z pojawieniem się nowoczesnych modeli językowych (LLM), klasyczne podejście do MAS ewoluuje: zamiast sztywnych reguł i wbudowanych planów, agenci zyskują zdolność semantycznego rozumienia sytuacji, generowania planów, analizowania kontekstu oraz elastycznego reagowania na zmiany w środowisku.

W architekturach MAS wzbogaconych o GenAI, LLM pełni rolę adaptacyjnego „umysłu” agenta. Dzięki temu agent potrafi:

• interpretować kontekst na podstawie opisów tekstowych, danych IoT i informacji środowiskowych,
• planować działania i przewidywać konsekwencje decyzji,
• komunikować się z innymi agentami w języku naturalnym,
• negocjować role, priorytety i strategie,
• uczyć się nowych zadań bez przebudowy kodu,
• działać proaktywnie i adaptacyjnie w dynamicznym środowisku.

Współczesne platformy takie jak AutoGen, CrewAI czy LangGraph pozwalają tworzyć środowiska, w których wiele agentów LLM współpracuje, dzieli się wiedzą, koordynuje zadania i prowadzi rozmowy w celu osiągnięcia celu. Połączenie MAS+LLM otwiera nowe możliwości w systemach inteligentnych, symulacjach, inteligentnych miastach, przemyśle, bezpieczeństwie i logistyce.

W podejściu hybrydowym agenci mogą działać jednocześnie na dwóch poziomach: * operacyjnym – realizując działania w środowisku (percepcja → interpretacja → decyzja), * strategicznym – gdzie LLM wspiera rozumowanie, generację planów, wykrywanie anomalii i wyjaśnialność działań.

Systemy te stają się szczególnie wartościowe tam, gdzie potrzebna jest współpraca wielu jednostek (fizycznych lub programowych), dynamiczne reagowanie na kontekst oraz zdolność do przetwarzania informacji nieustrukturyzowanych. To obszar niezwykle aktualny, intensywnie rozwijany badawczo i oferujący ogromny potencjał projektowy.

Przykładowe tematy projektowe:

Materiały:

• Libelium White Paper - 50 IoT Real Case Studies

Opis projektu: Celem jest stworzenie środowiska logistycznego (miasto, kampus lub sieć transportowa), w którym agenci reprezentują pojazdy, magazyny, punkty odbioru i centra planowania. Wersja klasyczna bazuje na regułach i prostych heurystykach, natomiast wersja GenAI wykorzystuje LLM do planowania tras, priorytetów i negocjacji między agentami.

Zakres:

• generowanie dynamicznych zdarzeń (opóźnienia, korki, awarie),
• agenci negocjują zadania i priorytety,
• LLM interpretuje kontekst logistyczny i generuje plany w języku naturalnym,
• symulacja umożliwia porównanie obu wersji systemu.

Hipoteza badawcza: MAS+LLM podejmuje trafniejsze i bardziej kontekstowe decyzje logistyczne, redukując liczbę przejazdów, konfliktów i opóźnień.

Metryki:

• efektywność tras (km/pojazd),
• zbieżność decyzji z rekomendacją eksperta,
• liczba działań wykonanych proaktywnie.

Opis projektu: Projekt polega na stworzeniu systemu monitorowania stanu pacjentów, w którym agenci odpowiadają za czujniki (tętno, saturacja, temperatura), pacjentów oraz jednostki reagujące. Wersja MAS klasyczna opiera się na progach alarmowych, podczas gdy wersja MAS+LLM interpretuje sytuację opisowo (np. „pacjent po ćwiczeniach rehabilitacyjnych”, „po podaniu leków występuje spodziewany wzrost tętna”).

Zakres:

• symulacja danych biometrycznych i zdarzeń medycznych,
• wykrywanie anomalii i alarmów,
• interpretacja opisowa przez LLM (uzasadnienia, wyjaśnienia),
• porównanie trafności decyzji i liczby fałszywych alarmów.

Hipoteza badawcza: MAS+LLM redukuje fałszywe alerty i generuje bardziej kontekstowe decyzje medyczne.

Metryki:

• FP rate (fałszywe alarmy),
• trafność decyzji (zgodność z ekspertem),
• czas reakcji,
• czytelność wyjaśnień (ocena 1–5).

Słowa kluczowe: Smart Animal Farming, Offspring Care, Animal Tracking, Toxic Gas Levels, Hydroponics, LLM Condition Monitoring, Predictive Health

Opis projektu: Celem jest stworzenie agentowego systemu do kompleksowej opieki nad zwierzętami hodowlanymi i roślinami (w przypadku hydroponiki) w celu maksymalizacji ich zdrowia i wydajności. Agenci reprezentują czujniki monitorujące nowo narodzone potomstwo (Offspring Care), czujniki gazów toksycznych (związanych z wydzielinami zwierząt), urządzenia śledzące zwierzęta (Animal Tracking) oraz systemy kontroli hydroponiki.

Wersja klasyczna alarmuje przy chorobie. Wersja MAS+LLM działa jako Doradca Weterynaryjny i Produkcyjny, interpretując złożony kontekst w celu proaktywnego zapobiegania problemom i optymalizacji.

Zakres:

• Symulacja danych: wahania warunków w budynkach inwentarskich (wentylacja, gazy), dane o lokalizacji zwierząt (pastwiska, stajnie) i warunki hydroponiczne.

• LLM interpretuje wzorce: „Pojedynczy wzrost amoniaku w sektorze A jest alarmujący, ale brak oznak chorobowych u potomstwa sugeruje problem z wentylacją, a nie epidemię”.

• LLM generuje spersonalizowane plany opieki i hodowli (np. zmiana diety, optymalizacja mikroklimatu dla konkretnej grupy zwierząt).

• Porównanie wpływu interwencji LLM na zdrowie stada i efektywność upraw.

Hipoteza badawcza: MAS z LLM-Doradcą redukuje śmiertelność (szczególnie wśród potomstwa) i poprawia wydajność produkcji (zarówno zwierzęcej, jak i hydroponicznej) poprzez proaktywne i kontekstowe interwencje.

Metryki:

• Wskaźnik śmiertelności/zachorowalności w grupie eksperymentalnej.

• Procent zoptymalizowanej produkcji (np. większa efektywność upraw hydroponicznych).

• Trafność i szybkość diagnostyki proaktywnej (wykrycie problemu przed wystąpieniem objawów klinicznych).

Obszar tematyczny

Słowa kluczowe: Intelligent Environments, Ambient Intelligence, Context-Aware Systems, IoT, Pervasive Computing, Smart Environments

Systemy i środowiska inteligentne (Intelligent Environments, Ambient Intelligence, pervasive / ubiquitous computing) to jedna z najbardziej dynamicznych i przyszłościowych dziedzin informatyki. Ich celem jest tworzenie przestrzeni – budynków, miast, szlaków górskich, lasów, stref przemysłowych – które same rozumieją sytuację, reagują na zmiany i wspierają użytkowników w sposób dyskretny, proaktywny i kontekstowy.

To informatyka „zanurzona w otoczeniu”: tysiące czujników, urządzeń IoT, systemów komunikacji i modułów obliczeniowych pracuje w tle, integrując się w inteligentną warstwę wspomagającą ludzi. W takich środowiskach system *nie tylko zbiera dane*, ale potrafi:

• analizować kontekst (np. warunki pogodowe, zachowania użytkowników, zagrożenia),
• przewidywać sytuacje (np. powstawanie zagrożeń),
• podejmować decyzje w czasie rzeczywistym),
• działać w sposób rozproszony, autonomiczny i skalowalny.

Dziedzina ta jest atrakcyjna ponieważ łączy technologie przyszłości: IoT, sztuczną inteligencję, agentowość, stream processing, systemy czasu rzeczywistego, analizę danych kontekstowych, a dodatkowo oferuje realne scenariusze zastosowań, takie jak:

• inteligentne wsparcie ratownictwa w górach,
• monitoring i przewidywanie zagrożeń w lasach,
• inteligentne miasta wspierające działania patrolowe,
• inteligentne budynki, domy, sieci transportowe i obiekty przemysłowe.

Nowoczesne inteligentne środowiska są dziś coraz bardziej wzmacniane przez agentów sterowanych GenAI/LLM, którzy potrafią rozumieć kontekst semantycznie, przewidywać zachowania oraz współpracować ze sobą jak zespoły ludzkie.

Jest to obszar pełen wyzwań – od danych środowiskowych wysokiej zmienności, przez budowę cykli życia kontekstu i algorytmów proaktywnego wnioskowania, po tworzenie systemów odpornych i skalowalnych. Jednocześnie daje on szerokie możliwości tworzenia innowacyjnych projektów o znaczeniu praktycznym.

Przykładowe tematy projektowe:

Rozwijamy zintegrowany system, którego celem jest bieżące monitorowanie środowiska górskiego oraz wspieranie działań ratowniczych poprzez analizę danych kontekstowych, ocenę ryzyka i generowanie alertów w czasie zbliżonym do rzeczywistego. Pracujemy jednocześnie nad dwoma komplementarnymi elementami: inteligentnym systemem wspierającym oraz symulatorem środowiska górskiego, które razem tworzą spójny ekosystem informacyjny.

System wspierający przetwarza zróżnicowane strumienie danych, obejmujące m.in. lokalizacje turystów i zwierząt, odczyty stacji pogodowych, zgłoszenia zagrożeń lawinowych oraz sygnały z infrastruktury telekomunikacyjnej. Integrujemy te dane w jednolity model sytuacyjny, stosując podejścia logiczne, probabilistyczne i maszynowe w celu wykrywania anomalii, oceny poziomów zagrożeń i formułowania zaleceń operacyjnych. Tworzymy architekturę mikrousługową o niskiej latencji, umożliwiającą skalowalne przetwarzanie informacji przestrzenno-czasowych.

Równolegle rozwijamy symulator środowiska górskiego, który odwzorowuje złożone zjawiska naturalne i behawioralne. Modelujemy dynamiczne warunki pogodowe, ewolucję pokrywy śnieżnej, zagrożenia lawinowe, ruch turystyczny, migracje zwierząt oraz ich wzajemne oddziaływania. Symulator stanowi środowisko eksperymentalne, pozwalające wytwarzać syntetyczne dane, badać scenariusze skrajne, testować algorytmy wykrywania zagrożeń i kalibrować moduły decyzyjne systemu wspierającego.

Połączenie perspektywy operacyjnej i symulacyjnej umożliwia analizę zachowań i zagrożeń w rzeczywistych i hipotetycznych warunkach, tworząc podstawy do budowy inteligentnych środowisk górskich zdolnych do proaktywnego działania. To podejście sprzyja rozwijaniu metod przetwarzania kontekstu, tworzeniu usług ambient-aware oraz opracowywaniu narzędzi zwiększających bezpieczeństwo i skuteczność działań ratowniczych.

Materiały własne:
Artykuł w *Information Sciences* (Ambient-aware continuous aid for mountain rescue activities)
Informacje medialne

Rozwijamy kontekstowy system monitorowania lasów, którego celem jest wczesne wykrywanie zagrożeń pożarowych oraz wspieranie operacji ochrony przeciwpożarowej. Wykorzystujemy gęstą sieć czujników środowiskowych, analizę strumieni danych i inteligentne mechanizmy decyzyjne, tworząc rozwiązanie zdolne do ciągłej oceny sytuacji oraz szybkiej, automatycznej reakcji na zmieniające się warunki.

System przetwarza dane o temperaturze, wilgotności, dynamice wiatru, koncentracji gazów i pyłów, integrując je w wielowymiarowy model kontekstu. Na tej podstawie określamy poziomy zagrożeń, identyfikujemy wczesne symptomy pożarów oraz klasyfikujemy ich stadium. Architektura opiera się na rozproszonych agentach odpowiedzialnych za zbieranie danych, analizę zagrożeń, planowanie działań oraz alokację zasobów.

Wprowadzamy także mechanizmy negocjacji automatycznej, w których agenci reprezentujący różne jednostki strażackie uzgadniają sposób podziału zasobów i wybór sektorów interwencji. Wykorzystujemy modele teorii gier – m.in. strategie kooperacyjne, równowagi negocjacyjne i preferencyjne modele alokacji – aby umożliwić podejmowanie decyzji zgodnych z globalnym celem minimalizacji ryzyka i strat. W połączeniu z uczeniem ze wzmocnieniem pozwala to dynamicznie dostosowywać strategie reagowania do rozwoju sytuacji i dostępności brygad.

Symulator środowiska leśnego umożliwia analizę różnych scenariuszy, od powolnych zarzewi po szybkie pożary frontowe. Odtwarzamy modele rozprzestrzeniania ognia, interakcje warstw środowiskowych, wpływ wiatru i ukształtowania terenu, a także zachowania agentów decyzyjnych. Symulator stanowi środowisko eksperymentalne do testowania algorytmów wykrywania zagrożeń, strategii podziału zasobów oraz skuteczności negocjacji opartych na teorii gier.

Projekt integruje przetwarzanie kontekstu, systemy wieloagentowe, modelowanie środowiskowe i negocjacje strategiczne, tworząc nowoczesną platformę badawczą dla inteligentnych systemów ochrony przeciwpożarowej.

Materiały własne:

• Artykuł na konferencji ISD 2024 (System For Monitoring Forests with Context-Aware Capabilities)

Rozwijamy kontekstowy system wspierający interwencje policyjne, w którym inteligentne moduły smart-gun, urządzenia mobilne oraz systemy nawigacyjne tworzą spójne środowisko przetwarzania danych. Broń służbowa jest traktowana jako sensor kontekstu, inicjujący procesy decyzyjne w systemie — w momencie nieplanowanego oddania strzału system automatycznie analizuje sytuację i wyszukuje patrole zdolne do udzielenia wsparcia.

System działa w ramach wieloagentowej architektury (MAS), obejmującej m.in. centrum zarządzania (MC), patrole policyjne (PP), agentów broni (Gn), agentów nawigacji (Nv), agentów komunikacyjnych (X) oraz agentów reprezentujących służby wspierające (np. ambulanse, drony). Każdy agent przetwarza wybrane zmienne kontekstowe, związane z czasem, lokalizacją, typem zdarzenia, stanem patrolu oraz relacjami przestrzennymi w mieście. Kontekst jest modelowany z użyciem kategorii oraz operacyjnych relacji przetwarzania (R6), co pozwala na kontrolowanie przepływu i transformacji danych w cyklu: akwizycja – modelowanie – przechowywanie – wnioskowanie – działanie.

Kluczowym elementem systemu jest mechanizm wyboru patroli wsparcia dla interwencji o podwyższonym ryzyku. Wykorzystujemy do tego zadanie ważonego MaxSAT, w którym zmienne odpowiadają m.in. stanowi patrolu, położeniu geograficznemu, charakterystyce dzielnicy oraz odległości od miejsca zdarzenia. Wagi odzwierciedlają priorytety operacyjne: preferowane są patrole w stanie obserwacji, z bezpieczniejszych dzielnic oraz znajdujące się relatywnie blisko zdarzenia, przy jednoczesnym uwzględnieniu dostępności zasobów. Rozwiązanie zadania MaxSAT generuje listę jednostek wsparcia, zapewniając kompromis między szybkością reakcji, bezpieczeństwem a efektywnym wykorzystaniem sił.

Całość jest testowana w symulatorze miejskiego środowiska, który odtwarza układ ulic, podział na dzielnice o różnym poziomie bezpieczeństwa, generuje interwencje oraz incydenty z użyciem broni. Symulacja pozwala analizować obciążenie patroli, dynamikę zdarzeń, czasy reakcji oraz jakość decyzji alokacyjnych. Wyniki potwierdzają możliwość zastosowania proponowanego podejścia w inteligentnych środowiskach miejskich, w których kontekst, dane przestrzenno-czasowe i architektura wieloagentowa wspólnie wspierają automatyzację i orkiestrację decyzji w systemach bezpieczeństwa publicznego.

Materiały własne:

• Artykuł na konferencji ISD 2022 (Police Interventions as a Context-aware System. A Case of a Contextual Data Modelling)

Rozwijamy wielomodułowy, kontekstowy asystent turysty, którego celem jest automatyczne generowanie spersonalizowanych planów zwiedzania miast i regionów. System integruje wiele źródeł danych o preferencjach użytkownika, uwzględnia aktualny kontekst środowiskowy (pogoda, dostępność atrakcji, godziny otwarcia) i tworzy optymalne trasy zwiedzania, dostosowane do ograniczeń czasowych i logistycznych.

Budujemy rozwiązanie, które łączy NLP i analizę sentymentu, modele klasyfikacji preferencji, moduły rekomendacyjne POI, oraz heurystyczną optymalizację tras (VRPTW), generując wielodniowe, spójne i dynamicznie aktualizowane itineraria. System przetwarza dane z chatbotów, mediów społecznościowych, dokumentów tekstowych oraz kwestionariuszy, tworząc wektorowy profil zainteresowań i priorytetów turysty.

W warstwie rekomendacyjnej wykorzystujemy semantyczne dopasowanie opisów atrakcji do profilu użytkownika, Bayesowskie metody oceny jakości POI (Wilson score), a także real-time filtering zależny od pogody, dostępności i kontekstu lokalnego. Kolejne etapy obejmują klastrowanie dzienne (K-Means) oraz budowę tras z użyciem algorytmów Christofidesa, 2-opt, A\*, z uwzględnieniem okien czasowych i długości przejść.

Tworzymy rozwiązanie, które ma zastosowanie w inteligentnych miastach, systemach informacji turystycznej, aplikacjach mobilnych, a także jako komponent wirtualnych biur turystycznych. Projekt obejmuje również rozwój interfejsu mapowego (Leaflet / OpenStreetMap) i integracji z usługami transportu publicznego.

Materiały własne:

• Artykuł na konferencji PACIS 2025 (Context-aware Intelligent Tourist Assistant)

Rozwijamy system generowania syntetycznych trajektorii mobilności turystów, który umożliwia modelowanie zachowań odwiedzających w dowolnym mieście – także tam, gdzie rzeczywiste dane telekomunikacyjne są niedostępne z powodów prawnych lub kosztowych. Wykorzystujemy profile behawioralne, informacje geograficzne (GIS), rekomendacje POI oraz reguły opisujące preferencje i ograniczenia użytkowników, tworząc realistyczne i powtarzalne modele ruchu.

Model łączy komponenty odpowiedzialne za wybór punktów POI, planowanie sekwencji odwiedzin, konstrukcję tras opartych o dane OSM lub usługi routingu oraz generowanie pełnych trajektorii czasoprzestrzennych. System pozwala definiować ograniczenia *what–when–where*, testować scenariusze typu „co-jeśli” oraz badać zakłócenia mobilności, takie jak zamknięcia obiektów, zmiany organizacji ruchu czy ograniczenia transportowe.

Generator może tworzyć dane na dowolną skalę, z kontrolą poziomu realizmu poprzez integrację preferencji turystów, okien czasowych, dostępności obiektów oraz różnych profili wizyt (kulturalnych, rekreacyjnych, mieszanych). Ważnym elementem jest także generowanie narracji tekstowych, które zwiększają interpretowalność danych i pozwalają na jakościową ocenę zachowań.

Projekt wspiera rozwój inteligentnych środowisk miejskich, dostarczając syntetycznych danych mobilności nieosiągalnych w tradycyjny sposób. Umożliwia testowanie systemów smart-city, budowę modeli predykcyjnych, badanie przepływów turystycznych oraz symulowanie sytuacji nietypowych lub kryzysowych.

Materiały własne:

• Artykuł na konferencji ICCS 2021 (Profile-Driven Synthetic Trajectories Generation to Enhance Smart System Solutions)

Obszar tematyczny

Słowa kluczowe: Process Mining, Workflow Discovery, Event Logs, Process Optimization, Data-Driven Analysis, Temporal Logic, Automated Reasoning, Explainability, LLM Support

Workflow Mining (Process Mining) to dziedzina, która analizuje rzeczywiste zachowanie systemów i użytkowników na podstawie danych rejestrowanych w event logach. To podejście wyjątkowe, bo zamiast opierać się na deklaracjach, dokumentach czy intuicji — wykorzystuje fakty: kto, kiedy, gdzie i jak wykonał określoną czynność. Takie logi są dzisiaj generowane przez niemal wszystko: systemy ERP, aplikacje mobilne, urządzenia IoT, systemy przemysłowe, platformy usługowe i procesy administracyjne. To sprawia, że event logi są jednym z najbogatszych i najbardziej wiarygodnych źródeł informacji o działaniu współczesnych organizacji i systemów.

Dzięki algorytmom odkrywania procesów możliwe jest automatyczne tworzenie modeli workflow, które pokazują faktyczny przebieg pracy: sekwencje działań, rozgałęzienia, współbieżność, powtórzenia, wyjątki i nietypowe przypadki. Tak powstałe modele służą do:

• analizowania efektywności i identyfikowania wąskich gardeł,
• znajdowania niezgodności z procedurami (compliance checking),
• optymalizacji i automatyzacji procesów,
• monitorowania poprawności systemów software'owych,
• analiz predykcyjnych i detekcji anomalii.

Process Mining ma kluczowe znaczenie w przemyśle, administracji, finansach, ochronie zdrowia, logistyce i produkcji — wszędzie tam, gdzie złożone procesy generują duże ilości danych operacyjnych.

Coraz częściej łączy się też Process Mining z metodami formalnej weryfikacji oraz nowoczesnymi technikami wyjaśnialności (np. Shapley values), aby zrozumieć, które elementy procesu wpływają na poprawność, bezpieczeństwo lub zgodność z regułami. Dodatkowym kierunkiem rozwoju jest wspomaganie analizy przez LLM, które potrafią interpretować struktury workflow, podpowiadać wzorce optymalizacyjne i generować opisy procesów w języku naturalnym.

To obszar szybko rosnący, bardzo praktyczny, a jednocześnie badawczo nowatorski — idealny do budowy narzędzi, eksperymentów, prac dyplomowych i projektów wykorzystujących dane o realnym działaniu systemów.

Przykładowe tematy projektowe:

Słowa kluczowe: Process Mining, Workflow Discovery, Event Logs, Temporal Logic, Automated Reasoning, Formal Methods, LLM-supported Analysis

Event logi to jedno z najbogatszych i najbardziej wiarygodnych źródeł wiedzy o tym, jak naprawdę działają systemy. Zawierają szczegółowe zapisy zdarzeń wykonywanych przez użytkowników, usługi, aplikacje, urządzenia IoT i systemy biznesowe. Dzięki temu pozwalają odkrywać procesy nie na podstawie dokumentów czy założeń, ale na podstawie faktycznego działania.

W projekcie opracowujemy podejście łączące techniki Process Mining z logiką temporalną i automatycznym wnioskowaniem. Celem jest wydobywanie z event logów formalnych reguł opisujących zachowanie procesów: zależności czasowych, kolejności działań, sytuacji wyjątkowych oraz wzorców przepływu pracy. Takie reguły mogą następnie służyć do analizy poprawności, optymalizacji oraz wykrywania niezgodności w procesach.

Tworzone rozwiązanie wykorzystuje:

• algorytmy odkrywania procesów (np. Inductive Miner),
• identyfikację typowych wzorców zachowań (sekwencje, rozgałęzienia, współbieżność, pętle),
• generowanie formuł logiki temporalnej opisujących te zależności,
• automatyczną weryfikację reguł z wykorzystaniem theorem provers,
• możliwość interpretacji i podpowiedzi wspieranych przez LLM.

Takie podejście pozwala przejść od surowych danych operacyjnych do formalnych specyfikacji procesu, które mogą być wykorzystane w optymalizacji, audycie, analizie wydajności oraz monitorowaniu zgodności.

Projekt jest atrakcyjny dla osób zainteresowanych analizą danych, logiką, formalną weryfikacją, automatyzacją oraz praktycznym zastosowaniem Process Mining w biznesie i systemach informatycznych.

Materiały własne: Artykuł na konferencji ASE 2024 (Automatic Generation of Logical Specifications for Behavioural Models)

Słowa kluczowe: Process Mining, Workflow Analysis, Temporal Logic, Shapley Values, Explainability, Automated Reasoning, Formal Verification

Współczesne systemy generują ogromne ilości event logów, na podstawie których można automatycznie odkrywać złożone, hierarchiczne modele workflow. Problem pojawia się wtedy, gdy takie modele rosną do setek lub tysięcy elementów — trudno zrozumieć, *dlaczego* dany proces spełnia (lub narusza) właściwości logiczne, które elementy są kluczowe dla poprawności, a które nie mają żadnego wpływu lub wręcz są szkodliwe.

Projekt rozwija narzędzie łączące Process Mining, logikę temporalną oraz Shapley Values z teorii gier kooperacyjnych, aby tworzyć wyjaśnialne analizy workflow. Model procesu odkryty z event logów (np. metodą Inductive Miner) tłumaczony jest automatycznie na zestaw formuł logiki temporalnej. Te specyfikacje poddawane są weryfikacji z wykorzystaniem theorem proverów (np. Vampire, E), aby ocenić takie własności jak:

• spójność (satisfiability),
• możliwość postępu (liveness),
• bezpieczeństwo (safety).

Następnie, dzięki Shapley Values, projekt umożliwia określenie, które elementy workflow:

• są krytyczne — bez nich proces traci poprawność,
• są neutralne,
• są zbędne lub szkodliwe, obniżając jakość lub bezpieczeństwo modelu.

Ta forma wyjaśnialności pozwala zobaczyć, *dlaczego* model zachowuje się tak, jak pokazują wyniki weryfikacji — zamiast jedynie otrzymać odpowiedź „spełnia/nie spełnia” bez kontekstu. To szczególnie cenne w audytach, compliance, optymalizacji procesów oraz diagnozowaniu dużych workflow pochodzących z przemysłu i administracji.

Projekt ma również wymiar eksperymentalny — analizowane są różne metody przybliżania Shapley Values (Monte Carlo vs. Random Subset Sampling), ich stabilność, koszt obliczeniowy i interpretowalność. To otwiera drogę do tworzenia narzędzi developerskich wspierających praktyków process mining.

Obszar tematyczny

Słowa kluczowe: model-driven software engineering, formal methods, AI-IDE, logical verification, automated code generation, technical debt analysis, LLM support, explainability

Modele oprogramowania i formalna weryfikacja stanowią podstawę budowy systemów, które są spójne, bezpieczne i możliwe do logicznego uzasadnienia. Pozwalają przechodzić od wymagań i opisów zachowania do precyzyjnych modeli, które można analizować, transformować oraz automatycznie przekształcać w działające komponenty oprogramowania.

Współczesne środowiska inżynierii oprogramowania coraz częściej wykorzystują zintegrowane narzędzia AI-IDE, łączące generatywną sztuczną inteligencję z technikami analizy i weryfikacji formalnej. Dzięki temu możliwe jest:

• automatyczne tworzenie i uzupełnianie modeli behawioralnych (diagramy aktywności, maszyny stanów),
• dedukcyjna analiza semantyczna i wykrywanie niespójności,
• automatyczna identyfikacja i kategoryzacja długu technicznego,
• zapewnienie śladowalności i wyjaśnialności na bazie logicznych reprezentacji,
• projektowanie systemów zgodnie z zasadami correctness-by-construction.

Dług techniczny oznacza ukryte koszty wynikające z uproszczonych decyzji projektowych lub implementacyjnych, które przyspieszają powstawanie systemu, ale później wymagają dodatkowej pracy, refaktoryzacji lub modyfikacji. Modele formalne i automatyczne analizy pozwalają ten dług _wykrywać, mierzyć i skutecznie redukować_.

Obszar obejmuje wykorzystanie różnorodnych środowisk developerskich i akademickich IDE wspieranych przez LLM, edytory modeli, logiki temporalne, narzędzia SMT/ATP oraz mechanizmy przekształceń modeli. Umożliwia to budowę inteligentnych, wyjaśnialnych i weryfikowalnych środowisk programistycznych, wspierających cały cykl życia oprogramowania.

Przykładowe tematy projektowe:

Słowa kluczowe: LLM-assisted modelling, Requirements Engineering, UML, Formal Verification, Deductive Reasoning, AI-IDE

Słowa kluczowe: LLM-assisted modelling, Requirements Engineering, UML, AI-IDE, formal analysis, smart modelling

Projekt dotyczy tworzenia nowoczesnego środowiska, w którym inteligentne modele językowe (LLM) pomagają w budowaniu i analizowaniu wymagań systemowych. Celem jest wsparcie procesu projektowego tak, aby szybciej powstawały spójne, logiczne i dobrze ustrukturyzowane modele opisujące działanie przyszłego systemu.

Pracujemy nad rozwiązaniem, które potrafi przetwarzać opisy w języku naturalnym i na ich podstawie automatycznie tworzyć pierwsze wersje diagramów behawioralnych UML. System podpowiada brakujące elementy, wykrywa niespójności oraz wskazuje miejsca wymagające doprecyzowania. Dzięki temu modelowanie staje się bardziej intuicyjne, a przy tym precyzyjne.

W projekcie łączymy zalety generatywnej AI z elementami formalnej analizy, która pozwala sprawdzić poprawność logiki modelu i wczesne wychwytywanie potencjalnych błędów projektowych. Takie połączenie umożliwia budowę środowiska typu inteligentne IDE, wspierającego użytkownika na każdym kroku – od analizy wymagań, przez tworzenie modeli, aż po generowanie fragmentów kodu zgodnych z zaproponowaną strukturą.

Projekt jest atrakcyjny dla osób zainteresowanych połączeniem AI, modelowania UML, praktycznej inżynierii oprogramowania oraz nowoczesnych narzędzi wspierających projektantów systemów.

Materiały własne:
Artykuł na konferencji FSE 2025 (RE-oriented Model Development with LLM Support and Deduction-based Verification)

Słowa kluczowe: state machines, behavioural modelling, logical square of opposition, formal reasoning, automated modelling, LLM support

Projekt IDE SQUARE dotyczy nowoczesnego podejścia do modelowania maszyn stanowych, w którym proces projektowania wspierany jest zarówno przez struktury logiki formalnej, jak i inteligentne podpowiedzi generowane przez modele językowe (LLM). Celem jest ułatwienie tworzenia poprawnych, przejrzystych i logicznie spójnych modeli, które stanowią podstawę wielu systemów informatycznych — od aplikacji mobilnych po złożone systemy cyber-fizyczne.

Kluczowym elementem projektu jest wykorzystanie kwadratu logicznego jako narzędzia porządkującego analizę dziedziny. Pozwala on w sposób uporządkowany identyfikować stany, relacje między nimi (sprzeczność, przeciwieństwo, subalternacja), a także wykrywać sytuacje, które trudno zauważyć przy klasycznej analizie tekstowych wymagań. Dzięki temu powstają modele bardziej precyzyjne i wolne od ukrytych niespójności.

W projekcie rozwijamy również elementy automatyzacji, takie jak:

• generowanie propozycji stanów i atrybutów na podstawie opisu w języku naturalnym,
• podpowiedzi przejść i zdarzeń wykrytych przez LLM,
• wstępna analiza niespójności na bazie struktur logicznych,
• automatyczna budowa szkieletów kodu powiązanego z maszyną stanów.

Takie połączenie klasycznego modelowania z inteligentnym wsparciem tworzy podstawy inteligentnego IDE, które pomaga w projektowaniu systemów lepiej, szybciej i bardziej świadomie. Projekt jest atrakcyjny dla osób zainteresowanych logiką, AI, modelowaniem zachowań systemów oraz praktycznym wykorzystaniem narzędzi programistycznych wspomaganych przez sztuczną inteligencję.

Materiały własne:
Artykuł na konferencji ASE 2024 (Logical square-driven and state-oriented generation of behavioural models)

Słowa kluczowe: theorem provers, automated reasoning, logical benchmarks, formal verification, model checking, AI-assisted verification

Projekt dotyczy stworzenia nowoczesnego i elastycznego systemu do porównywania wydajności theorem proverów – narzędzi stosowanych w automatycznym wnioskowaniu i formalnej weryfikacji. Celem jest zbudowanie środowiska, które potrafi generować różnorodne formuły logiczne, konwertować je do formatów wymaganych przez różne provery, a następnie badać ich zachowanie pod kątem czasu, pamięci oraz poprawności wyniku.

Tworzymy połączony zestaw dwóch narzędzi:

• Generatora – który buduje formuły w logice pierwszego rzędu FOL, od prostych struktur po złożone konstrukcje obejmujące bezpieczeństwo, żywotność, kwantyfikatory, wzorce probabilistyczne i zależności inspirowane kwadratem logicznym.
• Testera – który uruchamia wybrane provery (np. Vampire, E, Z3, CVC5, SPASS, Prover9, InKreSAT), mierzy ich wydajność i zapisuje wyniki w czytelnych formatach.

System pozwala badać m.in.:

• wpływ wielkości formuły na czas i pamięć,
• różne długości klauzul i ich rozkłady (np. Poissona),
• proporcje safety/liveness,
• stopień powiązań między klauzulami,
• głębokość zagnieżdżenia kwantyfikatorów,
• wpływ operatorów, polaryzacji literałów i redundancji,
• formuły o strukturach inspirowanych kwadratem logicznym.

Projekt daje możliwość pracy z logiką, generowaniem danych, tworzeniem narzędzi developerskich oraz analizą eksperymentalną. Powstaje praktyczne środowisko benchmarkowe, które można wykorzystywać w badaniach, projektach inżynierskich oraz testowaniu rozwiązań formalnych.

Materiały własne:
* Artykuł na konferencji EASE 2025 (Re-evaluation of Logical Specification in Behavioural Verification)

Projekt koncentruje się na opracowaniu i eksperymentalnym zbadaniu możliwości dużych modeli językowych (LLM) w automatycznym wspieraniu poszczególnych aktywności cyklu życia oprogramowania (Software Development Life Cycle). Celem jest zrozumienie, w jakim zakresie nowoczesne modele – takie jak GPT-4.1, Claude 3.5 Sonnet czy Llama 3.1 – mogą realnie wspomagać inżynierów w zadaniach analitycznych, projektowych, implementacyjnych i testowych.

Ideą projektu jest stworzenie wieloaspektowego benchmarku obejmującego zadania reprezentujące kluczowe obszary SDLC oraz porównanie jakości odpowiedzi różnych modeli. Pozwoli to ocenić ich przydatność, ograniczenia oraz potencjalne ryzyka związane z wykorzystaniem w procesach inżynierii oprogramowania.

Możliwe kierunki realizacji obejmują:

* Analiza wymagań – wykrywanie niejednoznaczności, doprecyzowanie funkcjonalności, generowanie user stories i kryteriów akceptacji.

* Modelowanie i architektura – tworzenie opisów architektury, dekompozycja modułów, analiza API i rekomendacje wzorców projektowych.

* Generowanie i refaktoring kodu – implementacja funkcji na podstawie opisu, poprawa jakości kodu, wykrywanie błędów oraz uzasadnianie zmian.

* Projektowanie testów – tworzenie przypadków testowych (w tym brzegowych), generowanie testów jednostkowych i analiza zgłoszonych błędów.

* Wsparcie DevOps / CI-CD – analiza konfiguracji pipeline, wykrywanie problemów w YAML, dobre praktyki bezpieczeństwa i interpretacja logów.

* Metodyka oceny jakości – opracowanie jednolitego systemu scoringu (0–3), zastosowanie testów automatycznych do kodu oraz ewaluacja odpowiedzi za pomocą LLM-sędziego.

Projekt pozwala zrozumieć, które obszary cyklu życia są najbardziej podatne na automatyzację z wykorzystaniem AI, a gdzie modele językowe wykazują istotne ograniczenia. Może obejmować implementację benchmarku SDLC-LLM, porównanie modeli, analizę błędów oraz propozycje rekomendacji i dobrych praktyk wykorzystania LLM w projektach informatycznych.

Projekt dotyczy stworzenia systemu eksperckiego wspomaganego przez duży model językowy (LLM), którego zadaniem jest analiza wymagań projektowych oraz rekomendowanie optymalnej architektury systemu IT. Rozwiązanie adresuje realny problem w branży: nietrafione decyzje architektoniczne — wynikające z braku doświadczenia lub presji czasu — prowadzą do niskiej wydajności, problemów ze skalowalnością i rosnącego długu technicznego.

System działa jako interaktywny agent architektoniczny, który na podstawie opisu projektu sugeruje odpowiednie podejścia, takie jak architektura monolityczna, mikroserwisowa, event-driven lub serverless. Oprócz rekomendacji struktury systemu agent generuje także uzasadnienia, wzorce projektowe oraz reprezentacje modelowe, np. w PlantUML lub Structurizr.

Projekt obejmuje:

• klasyfikację wymagań funkcjonalnych i niefunkcjonalnych,
• mapowanie wymagań na decyzje architektoniczne,
• projekt i implementację zestawu promptów,
• budowę agenta rekomendującego architekturę na podstawie dialogu,
• generowanie i wizualizację struktury systemu,
• analizę porównawczą wyników LLM z decyzjami architektów w rzeczywistych projektach,
• ocenę jakości rekomendacji, ryzyk i kompromisów architektonicznych.

W ramach pracy przewidziana jest eksperymentalna ewaluacja pokazująca, czy rekomendacje oparte na LLM mogą konkurować z klasycznym procesem projektowym, a także jaką rolę mogą pełnić modele generatywne jako wsparcie dla architektów systemowych.

Efektem końcowym jest prototyp inteligentnego narzędzia wspierającego architekta IT oraz ocena jego przydatności w rozwiązywaniu realnych problemów projektowych.

Projekt dotyczy opracowania zaawansowanego systemu, który łączy narzędzia formalnej analizy bezpieczeństwa smart kontraktów (np. Slither, Mythril, Echidna) z dużymi modelami językowymi (LLM). Celem jest stworzenie mechanizmu umożliwiającego iteracyjną refaktoryzację i samonaprawę kodu Solidity – system analizuje kontrakt, wykrywa podatności, generuje poprawki przy użyciu LLM, a następnie ponownie ocenia ich skuteczność w kolejnych cyklach.

Praca rozwiązuje realny problem bezpieczeństwa w ekosystemie blockchain: błędy takie jak reentrancy, overflow, niepoprawna obsługa uprawnień czy błędne konstrukcje logiczne prowadzą do strat finansowych, ataków i awarii. Automatyzacja ich naprawy może istotnie poprawić jakość i odporność smart kontraktów.

Zakres projektu obejmuje:

• analizę możliwości narzędzi do formalnej analizy i fuzz testów dla Solidity,
• projekt interfejsu integrującego raporty tych narzędzi z LLM,
• opracowanie strategii promptowania (np. single-shot, iterative prompting, chain-of-thought),
• testowanie systemu na realnych i sztucznie przygotowanych kontraktach zawierających podatności,
• klasyfikację i pomiar skuteczności napraw generowanych przez LLM,
• próbę automatycznego hardeningu kontraktów na podstawie wiedzy modelu.

System powinien wspierać wiele cykli analizy – po każdej zaproponowanej poprawce kontrakt jest ponownie weryfikowany, a LLM otrzymuje informację zwrotną o wykrytych problemach. Umożliwia to stopniowe ulepszanie kodu oraz badanie, jak modele generatywne radzą sobie z eliminowaniem różnych klas podatności.

Efektem końcowym jest prototyp systemu półautomatycznej samooptymalizacji i samonaprawy smart kontraktów, oceniony pod kątem trafności poprawek, redukcji podatności oraz ograniczeń tego podejścia. Projekt dostarcza także wniosków na temat przyszłości LLM w analizie i bezpieczeństwie kodu blockchain.

Obszar tematyczny

Poza głównymi obszarami badawczymi istnieje wiele innych zagadnień, które mogą stanowić podstawę wartościowych projektów, eksperymentów i prac dyplomowych. Obejmują one zarówno tematy praktyczne, jak i koncepcyjne, wynikające z pojawiających się technologii, nowych narzędzi inżynierskich oraz potrzeb przemysłu.

W tej sekcji znajdują się projekty i pomysły, które nie mieszczą się bezpośrednio w pozostałych kategoriach, ale są równie interesujące i posiadają duży potencjał badawczy, aplikacyjny lub eksperymentalny. To miejsce na tematy nietypowe, interdyscyplinarne oraz takie, które pojawiają się w wyniku obserwacji bieżących trendów w informatyce.

Przykładowe tematy projektowe:

Projekt koncentruje się na rozwoju systemu ForVis, dedykowanego wizualizacji oraz analizie struktur logicznych w kontekście problemów spełnialności (SAT). Ideą rozwiązania jest tworzenie intuicyjnych reprezentacji grafowych, które ułatwiają zrozumienie zależności między zmiennymi, ocenę trudności formuły oraz analizę działania solverów SAT. System ForVis wykorzystuje architekturę trójwarstwową (frontend Angular, backend Python, baza PostgreSQL) oraz technologie takie jak Docker, Celery, RabbitMQ i Nginx, co zapewnia skalowalność i możliwość łatwego rozszerzania funkcjonalności.

Celem projektu jest rozwój i eksperymentalne zbadanie wybranych metod wizualizacji oraz ich wpływu na interpretację formuł SAT i efektywność algorytmów. Możliwe kierunki obejmują:

• Hipergrafy – wizualizacja formuł jako struktur wieloelementowych, co ułatwia analizę powiązań między klauzulami i zmiennymi.
• Osadzenia grafowe (Graph Embeddings) – badanie zależności między zmiennymi za pomocą metod redukcji wymiarowości, takich jak Node2Vec.
• Detekcja społeczności (Louvain) – identyfikacja klastrów logicznych, które mogą stanowić podstawę optymalizacji heurystyk SAT.
• Graph Attention Networks (GAT) – zastosowanie mechanizmu uwagi do oceny wpływu poszczególnych zmiennych na spełnialność.
• Solver SAT oparty na CDCL – integracja własnego solvera w celu testowania heurystyk oraz wizualizacji procesu wnioskowania.
• Wizualizacja heurystyk CDCL – analiza krok po kroku, jak solver dokonuje wyboru zmiennych i uczy się klauzul konfliktowych.

Projekt pozwala zrozumieć, jak struktura grafowa formuły wpływa na trudność problemu SAT i jak wizualizacja może wspierać analizę oraz optymalizację solverów. Może obejmować implementację nowych modułów ForVis, eksperymenty porównawcze oraz propozycje dalszego rozwoju systemu.

Projekt dotyczy połączenia dwóch kluczowych koncepcji współczesnej kryptografii i systemów rozproszonych: dowodów o zerowej wiedzy (Zero-Knowledge Proofs, ZKP) oraz problemu bizantyńskich generałów (Byzantine Fault Tolerance, BFT). Celem jest opracowanie modelu, w którym węzły systemu mogą brać udział w procesie konsensusu, ujawniając poprawność swoich decyzji bez ujawniania samych decyzji — zachowując prywatność, a jednocześnie gwarantując spójność i odporność systemu.

Wprowadzenie do problematyki obejmuje dwa niezależne obszary:

• Dowody o zerowej wiedzy (ZKP) – technika pozwalająca udowodnić posiadanie wiedzy lub poprawność obliczenia bez ujawniania tych danych.

ZKP wykorzystywane są w kryptowalutach, systemach uwierzytelniania, protokołach prywatności oraz procesach weryfikacji.

• Bizantyńska odporność na błędy (BFT) – klasyczny problem systemów rozproszonych, w którym część węzłów może działać niepoprawnie lub złośliwie.

Rozwiązania BFT są fundamentem blockchainów, systemów konsensusowych i rozproszonych baz danych.

Celem projektu jest zaprojektowanie mechanizmu, który pozwoli węzłom:

• brać udział w konsensusie bez ujawniania preferencji lub głosu,
• udowadniać, że działają zgodnie z zasadami protokołu,
• weryfikować poprawność decyzji innych węzłów,
• zachować pełną prywatność informacji wejściowych i decyzji,
• eliminuje węzły zachowujące się niepoprawnie, zgodnie z zasadami BFT.

Model może wykorzystywać różne rodzaje ZKP, m.in. SNARK, STARK, Bulletproofs lub protokoły interaktywne, w zależności od złożoności i oczekiwanego kosztu obliczeniowego. Proponowany prototyp powinien uwzględniać:

• sposób reprezentacji decyzji w formie zobowiązań (commitment schemes),
• mechanizm udowadniania poprawności decyzji bez jej ujawniania,
• integrację tych dowodów z algorytmem konsensusu BFT,
• analizę odporności na węzły złośliwe oraz zachowania odstające.

Projekt umożliwia eksperymentalne porównanie: konsensus klasyczny, konsensus z częściową prywatnością oraz konsensus wspierany ZKP. Wyniki pozwolą ocenić, w jakim stopniu ZKP mogą zwiększyć prywatność bez utraty właściwości bezpieczeństwa znanych z algorytmów BFT.

Praca stanowi połączenie kryptografii, systemów rozproszonych oraz projektowania protokołów — z dużymi możliwościami dalszych badań.

Projekt dotyczy opracowania koncepcji systemu, który umożliwia bezpieczne, zdecentralizowane i zautomatyzowane udostępnianie mocy obliczeniowej. Ideą rozwiązania jest stworzenie otwartego rynku zasobów — użytkownik może wynajmować lub udostępniać moc obliczeniową, a całość rozliczeń, weryfikacji i wyceny realizowana jest za pomocą blockchain oraz tokenizacji.

W projekcie analizowane są aktualne platformy udostępniania zasobów (takie jak Golem, Akash, iExec), ich ograniczenia technologiczne i ekonomiczne oraz możliwe kierunki ulepszeń. Na tej podstawie projekt zakłada stworzenie modelu teoretycznego obejmującego:

• mechanizmy wymiany i wynajmu mocy obliczeniowej,
• metody wyceny i rozliczeń oparte na tokenach,
• zasady bezpieczeństwa i odporności systemu,
• metody audytu i weryfikacji poprawności obliczeń w środowisku rozproszonym.

Szczególnym elementem projektu jest analiza technik potwierdzania poprawności obliczeń, m.in. poprzez koncepcje konsensusu typu „Proof of Compute” oraz inne metody zapewniania, że zewnętrzny węzeł wykonał zadanie rzetelnie.

System może być również wspierany przez modele LLM, które pełnią funkcję inteligentnych komponentów wspomagających, np.:

• klasyfikację i kategoryzację zadań obliczeniowych,
• sugerowanie optymalnego doboru zasobów,
• interpretację wyników lub wykrywanie anomalii.

Oceniana będzie także przydatność opracowanego protokołu w zastosowaniach praktycznych — zwłaszcza w trenowaniu modeli sztucznej inteligencji (w tym LLM), przetwarzaniu danych naukowych, projektach startupowych oraz jako sposób aktywizacji niewykorzystanych mocy obliczeniowych w środowiskach domowych i akademickich.

Projekt dotyczy zaprojektowania oraz stworzenia prototypowej kryptowaluty opartej na technologii blockchain. Celem jest zarówno analiza istniejących rozwiązań kryptowalutowych, jak i zaproponowanie własnego modelu działania sieci, mechanizmu konsensusu oraz zasad funkcjonowania tokena.

W pierwszym etapie przewidziany jest przegląd najważniejszych protokołów wykorzystywanych we współczesnych kryptowalutach — takich jak Bitcoin, Ethereum, Solana czy projekty klasy „layer 2”. Analiza obejmuje m.in.: modele transakcyjne (UTXO vs. konta), mechanizmy konsensusu (Proof of Work, Proof of Stake, ich warianty), sposoby zabezpieczania sieci, metody skalowania oraz architekturę inteligentnych kontraktów.

Na podstawie tej analizy opracowany zostanie projekt własnej, dedykowanej kryptowaluty, obejmujący:

• model działania sieci i sposób propagacji transakcji,
• wybór i uzasadnienie mechanizmu konsensusu,
• struktury bloków i format transakcji,
• zasady emisji i polityki tokenowej,
• ścieżki weryfikacji i walidacji,
• mechanizmy bezpieczeństwa i odporności na ataki,
• możliwość rozbudowy o smart kontrakty lub funkcje dodatkowe.

Ostatecznym celem projektu jest implementacja prototypu kryptowaluty — w formie minimalnej sieci blockchain umożliwiającej tworzenie bloków, weryfikację transakcji i przeprowadzanie podstawowych operacji. Projekt może także obejmować prosty eksplorator bloków lub demonstracyjną aplikację użytkownika.

Praca umożliwia zrozumienie kluczowych aspektów technologii blockchain oraz mechanizmów projektowania kryptowalut od podstaw.