Obhájené dizertační práce

Nízká evolvabilita strukturovaných dokumentů, jako jsou plány správy dat (PSD), omezuje jejich přizpůsobivost měnícím se požadavkům. Tato disertační práce se zabývá tímto problémem aplikací teorie normalizovaných systémů a integrací strojového zpracování k redesignu tvorby a správy dokumentů. S využitím metodologie Design Science vyvíjíme transformační rámec schopný vývoje a změn, který zajišťuje udržitelnou konverzi mezi strojově čitelnými a lidsky orientovanými formáty, čímž zlepšuje modularitu a škálovatelnost. Výzkum se zaměřuje na řešení měnících se požadavků, přizpůsobení PSD různým oborům a organizacím, zajištění bezproblémové migrace mezi šablonami, automatizaci hodnocení a poskytování strukturovaného vedení pro výzkumníky. Náš přístup transformuje tradiční PSD do strojově zpracovatelných formátů, což umožňuje automatizované hodnocení pomocí předdefinovaných metrik, snižuje manuální pracovní zátěž a zlepšuje postupy správy dat. Navržené řešení je teoreticky vyhodnoceno a jeho efektivita v oblasti plánování správy dat je demonstrována prostřednictvím prototypové implementace a případové studie.

Klientské aplikace jsou klíčovou součástí moderních softwarových systémů, jelikož slouží jako hlavní rozhraní mezi uživateli a digitální infrastrukturou. Výrazně ovlivňují vnímanou kvalitu systému, jeho použitelnost i celkový úspěch. Jejich vývoj však komplikuje rychlý technologický vývoj, roztříštěnost ekosystému a těsná provázanost sémantické struktury, vizuálního návrhu a platformní implementace, což vede k horší údržbě, omezené evoluci a citlivosti na řetězové efekty při změnách. Přestože nástroje jako design systémy a front-endové frameworky se v praxi rozšířily, současné vývojové postupy často postrádají formální základy a modulární architektury nezbytné pro dlouhodobou udržitelnost. Stávající modelovací jazyky i softwarové architektury často nedokážou nabídnout strojově zpracovatelné reprezentace a opakovaně využitelné sémantické popisy. Vzniká tak významná mezera mezi teoretickými přístupy a praktickými potřebami klientského vývoje. V této disertační práci navrhujeme nový přístup, který kombinuje principy Teorie Normalizovaných Systémů (NST) se sémantickými technologiemi a formálním modelováním uživatelských rozhraní a design systémů. Tato integrace umožňuje vytvářet strukturované a evolvovatelné reprezentace, které podporují automatizovanou generaci udržitelného kódu. Uplatněním konstrukčních principů NST a mechanismů tzv. expanderů v oblasti front-endového vývoje - která je v rámci NST zatím nedostatečně prozkoumána - usilujeme o podporu modularity a eliminaci řetězových efektů. Výzkum probíhal dle metodiky Design Science Research a zahrnoval pět propojených vývojových cyklů. Ty zahrnovaly systematickou revizi modelovacích jazyků pro UI, návrh formálních ontologií pro popis UI a design systémů, metodiku udržitelného psaní front-endového kódu a návrh a implementaci tzv. expanderů pro transformaci modelů do produkčního kódu. Navržený přístup byl validován v rámci reálných scénářů a pomocí analýz evolvovatelnosti. Přínosy této práce ukazují, že kombinací principů NST a formálních sémantických popisů je možné navrhovat a generovat udržitelné a dlouhodobě evolvovatelné klientské aplikace. Získané výsledky rozšiřují oblast použití NST směrem k vývoji uživatelských rozhraní a otevírají cestu k dalšímu výzkumu v oblasti modelově řízeného vývoje, automatizované generace kódu a návrhu multiplatformních aplikací.

Dynamicky typované jazyky, jako je Pharo, postrádají explicitní typové informace, což omezuje nástroje pro vývojáře například navigaci, doplňování, reverzní inženýrství a generování třídních diagramů. Tato práce navrhuje jednotný způsob, jak shromažďovat a kombinovat různé náznaky typu (statické analýzy, pozorování za běhu a lehké indicie odvozené z názvů) za jediným dotazovacím rozhraním s jasně vyjádřenými kompromisy mezi latencí a pokrytím. Přístup je realizován v rozšiřitelném rámce pro kombinování se sledováním původu, řazením kandidátů a konfigurovatelnými politikami (řetězení a fúze). Doplňuje jej datová pipeline těžící rozsáhlé pravidelnosti názevtyp z reálného kódu. Výsledky jsou předvedeny v prototypových IDE nástrojích (prezenter stromu typů, chytřejší seznamy odesilatelů/implementátorů a rozšířené doplňování) a v průzkumném generátoru UML pro dávkové zpracování. Vyhodnocení na reprezentativních balíčcích pro Pharo se zaměřuje na vhodnost pro praxi: jak se zlepšuje pokrytí v reálných časových limitech, jak profily zpřehledňují kompromisy a kde zůstávají omezení a hrozby pro validitu. Rámec i vytěžené priority jsou míněny jako znovupoužitelné stavební prvky pro tvůrce nástrojů a přenositelné do příbuzných dynamických prostředí.

Kolektivní rozhodování leží v základech multiagentních systémů, sociálních věd i ekonomie. Příklady takových procesů sahají od volební teorie, přes rozdělování zdrojů, až po formování týmů. Všechny tyto problémy mají společnou strukturu: skupina agentů má preference ohledně možných kolektivních rozhodnutí a cílem je tyto preference agregovat a zvolit nejlepší možné rozhodnutí. Oblast (výpočetní) sociální volby poskytuje matematickou formalizaci těchto procesů a různých ideálů nejlepších rozhodnutí a zkoumá, jak náročné je tyto žádoucí výsledky algoritmicky nalézt. Není příliš překvapivé, že mnoho problémů v této oblasti je výpočetně velmi složitých, jelikož zahrnují potenciálně protichůdné preference a velmi komplikované požadavky na kvalitu výsledků. Jelikož se však jedná o problémy důležité v reálném životě, musíme je být schopni řešit. Existují různé přístupy, jak se s touto složitostí vypořádat. V této dizertační práci vycházíme z jednoduché myšlenky, že ne všechny instance výpočetně složitého problému jsou stejně náročné. Konkrétně využíváme parametrizovanou složitost, teoretický framework poskytující formální nástroje ke zkoumání podmínek, za nichž lze daný problém efektivně řešit. Přínosem této práce je podrobná parametrizovaná analýza pěti základních problémů v oblasti výpočetní sociální volby. Začínáme studiem manipulace skrze mazání projektů v participativním rozpočtování, což je zobecnění voleb komisí. Následně se věnujeme spravedlivému rozdělování doručovacích zakázek v dnešní sdílené ekonomice. Poté se zaměříme na dvě třídy her formování koalic, z nichž každá zdůrazňuje odlišné aspekty kolektivního rozhodování. Závěrem představujeme výpočetní model vhodný pro ubytování uprchlíků v komunitě respektující preference jak nově příchozích, tak stávajících obyvatel města.

Virtuální realita je jedním z nejrychleji rostoucích oborů v oblasti technologií. Vizuální kvalita, zorné pole, time-warping, to všechno se každým dnem zlepšuje. Existuje však také jeden další důležitý aspekt virtuální reality, o kterém se tak často nemluví, a přesto by se mělo -- uživatelské rozhraní. Po několika desetiletích, co jsme závislí pouze na myši a klávesnici -- zařízeních, která dlouhou dobu jako ovladače pro počítače převládala --, můžeme konečně využít další způsoby, jak svoje cíle do počítače převést. K ovládání virtuálního prostředí můžeme dokonce použít jiné části těla než ruce -- například můžeme interagovat s prostředím pomocí pohybu očí nebo prostě po virtuálním světě chodit, jako bychom byli na procházce v lese. Tato odborná studie se zabývá ovladači pro virtuální realitu, které jsou založeny na sledování pohybu rukou. Cílem je vytvořit intuitivní ovladač s využitím optických senzorů, aby uživatel nemusel držet nebo mít na sobě přidělané žádné zařízení pro interakci s~virtuálním světem. Navrhli jsme a implementovali sadu algoritmů pro fúzi trackovacích dat z více optických senzorů pro sledování ruky, čímž jsme docílili větší přesnosti a nových možností trackování, než by dokázal jeden optický senzor. Náš přístup jsme otestovali jak z hlediska přesnosti a rychlosti algoritmů, tak jeho použitelnosti v reálných scénářích. Ve všech testech náš přístup předčil současné nejmodernější přístupy.

Všude je spousta dat, na internetu, ve vědě atd. Samotná neanotovaná data však mají jen malou hodnotu. Cílem této disertace je zdokonalit aktivní hlubokého učení pro efektivní a spolehlivé anotování velkých datových množin se zvláštním důrazem na astronomická spektra. Abychom ověřili vhodnost aktivního hlubokého učení pro velké datové množiny astronomických spekter, použili jsme metodu aktivního hlubokého učení ke hledání vzácných astronomických objektů. Tato metoda, která spojuje konvoluční neuronovou síť s aktivním učením, úspěšně objevila řadu nových objektů, a to přestože jsme neměli k dispozici velkou a reprezentativní trénovací množinu. Úspěšnost aktivního hlubokého učení závisí na prediktivních nejistotách, proto jsme v návaznosti zkoumali metody pro jejich kvantifikaci. Vyvinuli jsme dvě pravděpodobnostní metody: jednu pro predikci spektroskopického rudého posuvu pomocí metody Monte Carlo dropout a druhou pro predikci atmosférických vlastností exoplanet pomocí metody deep ensemble. Avšak prediktivní nejistoty musí být spolehlivé. Proto jsme vytvořili metodu, která usnadňuje diagnostiku příčin možných problémů těchto prediktivních nejistot. Tato metoda využívá interpreter histogramu pravděpodobnostní integrální transformace k usnadnění této diagnostiky. Celkově tato disertační práce posouvá oblast aktivního hlubokého učení a vyhodnocování prediktivních nejistot s možnými aplikacemi přesahujícími rámec astronomie do jakékoli oblasti s velkými datovými množinami.

Doporučovací systémy hrají zásadní roli při správě a personalizaci obrovského množství dat napříč doménami, jako jsou internetové obchody, multimediální platformy a sociální média. Tato práce se zabývá dvěma kritickými výzvami v moderních doporučovacích systémech: škálovatelností lineárních modelů a integrací interakční a atributové podobnosti pomocí architektury Transformer. V návaznosti na Embarassingly Shallow Autoencoder (EASE) představuje ELSA, škálo- vatelnou variantu EASE, směřující k překonání omezení EASE na datasetech s velkým kata- logem. Využitím faktorizace matice vah a optimalizace založené na gradientním sestupu prokazuje ELSA pozoruhodnou škálovatelnost a použitelnost na reálná data v průmyslové praxi. Druhá část práce rozšiřuje použití ELSA pro trénink modelů založených na architektuře Transformer a představuje beeFormer, framework pro trénink Trnsformerů na interačních datech. beeFormer efektivně kombinuje interakční data s popisy a obrázky produktů, což vede k lepším doporučením v porovnání nejen s attributovými modely, ale i tradičním kolaborativním filtrováním. Práce se dále zaměřuje na doporučování napříč různými doménami a odhaluje potenciál modelů Transformer pro přenos znalostí při doporučování napříč oblastmi, jako jsou knihy, filmy nebo móda. Rovněž ukazuje, že využití popisů generovaných pomocí modelů typu Large Language Model (LLM) významně zlepšuje kvalitu doporučení napříč jednotlivými doménami.

Tato disertační práce pojednává o formální verifikaci systémů založených na strojovém kódu pomocí techniky kontroly modelu s použitím abstrakce. Je prezentován současný stav poznání v tomto oboru a je poukázáno na slabá místa předchozích přístupů. Autorův výzkum popsaný v této disertační práci a předchozích článcích v konferenčních sbornících prezentuje nové způsoby řešení problémů předchozího výzkumu: systémy jsou popsány v programovacím jazyce Rust a samy o sobě simulovatelné, jsou automaticky konvertovány do verifikačních ekvivalentů a verifikovány v originální konstrukci založené na zjemňování trojhodnotové abstrakce. Pro účinnou verifikaci je speciálně zacházeno s proměnnými založenými na bitových vektorech. Autor práce vytvořil nástroj pro formální verifikaci, který implementuje představené techniky, a jeho schopnosti jsou v práci vyhodnoceny. Nástroj může být použit pro verifikaci libovolných konečných číslicových systémů, se zaměřením na systémy, kde je chování určeno programy ve strojovém kódu. Vytvořený nástroj je bezplatně a veřejně dostupný, s otevřeným zdrojovým kódem.