Obhájené dizertační práce

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.