Témata dizertačních prací

Vizuální navigace má mnoho aplikací v robotice: od manipulace, přes mobilní robotiku až po autonomní vozidla. Hluboké učení s posilováním (deep reinforcement learning) je elegantní přístup k vizuální navigaci bez použití map. Tato metoda integruje zpracování obrazu, lokalizaci a plánování do jednoho modulu, který lze trénovat a tedy optimalizovat pro dané prostředí. Zabýváme se výzkumnými problémy od syntetického generování a zobrazování prostředí až po řízení robotů v reálném čase.

Obsahem práce bude výzkum algoritmů pro klasifikaci šifrovaného síťového provozu a detekci bezpečnostních hrozeb ve vysokorychlostních počítačových sítích a tvorba automaticky anotovaných datových sad. Šifrovaný provoz představuje v současné době velkou výzvu pro standardní monitorovací nástroje, které doposud pracovaly především s nešifrovanými informacemi extrahovanými z paketů, vědeckou komunitu v oblasti síťové bezpečnosti i pro odbornou veřejnost. Většina síťového provozu je již šifrovaná a proto je potřeba hledat nové zdroje informací o dění na síti. Tyto informace jsou důležité jak pro operátory sítí tak i pro bezpečnostní analytiky.

Cílem tohoto rámcového tématu dizertační práce je výzkum vhodných statických vlastností provozu, které je možné počítat v reálném čase na linkách o rychlostech přes 100Gb/s (s využitím hardwarové akcelerace), výzkum klasifikačních a detekčních algoritmů založených na strojovém učení pro zpracování síťových toků obohacených o nové statistiky a v neposlední řadě experimentální vyhodnocování těchto vyvíjených algoritmů na reálném vysokorychlostním provozu.

Dizertabilita tématu je založena na faktech, že jde o řešení velmi netriviálních problémů, kterými jsou zpracování a filtrace velkých objemů dat společně s modelováním síťového provozu, hledání odchylek, identifikace útočníků a správné řízení mitigace těchto problémů. V oblasti analýzy šifrovaného provozu se začínají objevovat výzkumné výsledky z celosvětové vědecké komunity, avšak zatím nebylo publikováno dostatečně použitelné řešení. Základem bude výzkum v oblasti možností využití statistických metod, pravděpodobnostních modelů a využití algoritmů umělé inteligence.

Vzhledem k současným rychlostem síťových přenosů a požadavkům na on-line monitorování je nutné algoritmy navrhovat a realizovat s využitím dekompozice na hardwarovou a softwarovou část a s použitím vhodných technologií hardwarové akcelerace (např. FPGA).

Se stále zvyšujícím se počtem tranzistorů na čipu se také zvyšuje množství dat potřebné pro jeho testování. Integrované obvody jsou poprvé testovány při výrobě, před zapouzdřením. Zde jsou testovací vektory generovány tzv. ATE (Automated Test Equipment) zařízením a přenášeny do čipu. Množství dat je zde obrovské, paměť v ATE je extrémně drahá, to samé platí o době testu. Je tudíž nutné tato data komprimovat. Poměr nákladů vynaložených na test čipu a na jeho návrh se stále zvyšuje. Komprese testovacích vektorů je tedy aktuální téma a stále více nabývá na významu. Je tedy zapotřebí intenzivního výzkumu v této oblasti a pokoušet se překonat stávající kompresní techniky.

Bylo navrženo mnoho kompresních technik, některé se používají v průmyslové praxi [1], [2]. Většina z nich je založená na kombinaci pseudo-náhodného testu (který může být implementován na čipu) a deterministického testu. Deterministické vektory jsou algoritmicky zkomprimované a uložené v ATE a posléze dekomprimované na čipu.

Cílem doktorského studia bude navrhnout nové metody pro kompresi a dekompresi testu pro pokročilé design-for-testability (DFT) architektury [3]. To bude zahrnovat návrh nových dekompresních architektur, algoritmů pro kompresi testu a návrh celkové HW architektury.

Tento výzkum bude (může) volně navazovat na dokončenou dizertační práci [4], [5].

• [1] J. Rajski et al. “Embedded Deterministic Test”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 23, no. 5, pp. 776-792, 2004.
• [2] Y. Huang, S. Milewski, J. Rajski, J. Tyszer and C. Wang, “Low Cost Hypercompression of Test Data,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 39, no. 10, pp. 2964-2975, 2020.
• [3] R. Dorsch, H. Wunderlich, “Reusing Scan Chains for Test Pattern Decompression”, Journal of Electronic Testing: Theory and Applications, vol. 18, no. 2, pp. 231-240, 2002.
• [4] J. Balcárek, P. Fišer, and J. Schmidt, “Techniques for SAT-based Constrained Test Pattern Generation,” in Microprocessors and Microsystems, Elsevier, Vol. 37, Issue 2, March 2013, pp. 185-195. [5] J. Balcárek, „Implicit Representations in Testing and Dependability of Digital Circuits“, Ph.D. Thesis, CTU in Prague, 2016.
• [5] J. Balcárek, „Implicit Representations in Testing and Dependability of Digital Circuits“, Ph.D. Thesis, CTU in Prague, 2016.

Algoritmy používané při návrhu logických obvodů (EDA algoritmy) jsou typicky hladové povahy. Lokální rozhodnutí se provádějí náhodně, dle topologického uspořádání, anebo dle zkušeností autora algoritmu. Tato rozhodnutí nemusí být vždy správná a mohou vést k nekvalitním výsledkům. Jedním z možných řešení tohoto problému je použití umělé inteligence (AI). AI se učí při běhu algoritmu a posléze napomáhá zvolit správné cesty.

Cílem výzkumu je prozkoumat možnosti použití AI v logické syntéze a vytvořit nové algoritmy používající AI pro řízení provádění lokálních rozhodnutí.

Současné nástroje pro logickou syntézu a optimalizaci (komerční i akademické) z převážné míry kladou důraz na rychlost, na úkor kvality. Nedávný výzkum ukázal, že tyto nástroje mají tendenci uváznout v hlubokých lokálních minimech a často produkují velice suboptimální výsledky (plocha, zpoždění). Jedním z důvodů je deterministická povaha používaných algoritmů. Randomizované iterativní algoritmy se ukázaly být jedním z řešení tohoto problému [1], [2] – nabízejí možnost zlepšit kvalitu řešení za cenu delšího výpočetního času.

Současné studie navíc ukazují, že většina nástrojů pro logickou syntézu a optimalizaci je velice citlivá na „náhodnost“ vnesenou zvnějšku, samotným návrhářem [3], [4]. Syntéza pak při nepatrné změně zdrojového kódu (při zachování funkční ekvivalence) produkuje kvalitativně značně odlišné výsledky. Toto chování není příliš žádoucí. Je tedy záhodno analyzovat toto chování, identifikovat jeho příčiny a navrhnout efektivnější algoritmy.

Cílem výzkumu bude analýza chování dostupných nástrojů (algoritmů) pro logickou syntézu a optimalizaci [5], identifikace příčin výše zmíněného chování, identifikace bodů algoritmu, kam lze explicitně vložit náhodnost a randomizace těchto algoritmů. Bude analyzován vliv náhodnosti a navrženy algoritmy, které vliv náhodnosti minimalizují, případně ji využijí v pozitivním smyslu [1], [2]. Dále mohou být navrženy nové algoritmy, které budou minimálně citlivé na náhodnost zanešenou zvenku, při zachování akceptovatelné výpočetní složitosti.

• [1] P. Fišer and J. Schmidt, “Improving the Iterative Power of Resynthesis,” in Proc. of 15th IEEE Symposium on Design and Diagnostics of Electronic Systems (DDECS), Tallinn (Estonia), April 18-20, 2012, pp. 30-33.
• [2] P. Fišer and J. Schmidt, “On Using Permutation of Variables to Improve the Iterative Power of Resynthesis,” in Proc. of 10th Int. Workshop on Boolean Problems (IWSBP), Freiberg (Germany), September 19-21, 2012, pp. 107-114.
• [3] A. Puggelli, T. Welp, A. Kuehlmann, and A. Sangiovanni-Vincentelli, “Are Logic Synthesis Tools Robust?,” in Proc. of the 48th ACM/EDAC/IEEE Design Automation Conference (DAC), 5-9 June 2011, pp. 633-638.
• [4] P. Fišer, J. Schmidt, and J. Balcárek, “On Robustness of EDA Tools,” in Proc. of 17th Euromicro Conference on Digital Systems Design (DSD), Verona (Italy), August 27-29, 2014, pp. 427-434.
• [5] Berkeley Logic Synthesis and Verification Group, “ABC: A System for Sequential Synthesis and Verification” [Online]. Available: http://www.eecs.berkeley.edu/alanmi/abc/.

Návrh tzv. aproximativních logických obvodů je jedním z dnešních mainstreamů. Zde logické obvody nemusí vykonávat požadovanou funkci přesně, je tolerována jistá chyba. Výsledné obvody jsou pak značně menší a mají menší spotřebu. Aproximativní obvody nacházejí aplikaci ve zpracovávání/rozpoznávání obrazu/zvuku, neuronových sítích, data-miningu, atd.

Testování aproximativních obvodů se stává dalším úkolem k řešení. Nabízí se zde více stupňů volnosti: test nemusí být úplný, ne všechny poruchy musí být testovány, aby obvod stále vyhovoval požadavkům. Výsledkem je pak kratší test.

Cílem výzkumu je navrhnout nové algoritmy pro generování testů (ATPG) pro aproximativní obvody.

Současné nástroje pro logickou syntézu a optimalizaci (komerční i akademické) z převážné míry kladou důraz na rychlost, na úkor kvality. Nedávný výzkum ukázal, že tyto nástroje mají tendenci uváznout v hlubokých lokálních minimech a často produkují velice suboptimální výsledky (plocha, zpoždění). Jedním z důvodů je deterministická povaha používaných algoritmů. Randomizace algoritmů [1], [2] se ukázala být pouze částečným řešením tohoto problému. Druhým, důležitějším důvodem, je chybějící řízení syntézních algoritmů na nejvyšší úrovni. Současná logická syntéza je většinou iterativní proces, ve kterém se jednotlivé syntézní kroky spouštějí spekulativně. Zavedení pokročilejších technik řízení by mohlo značně vylepšit celý syntézní proces.

Cílem výzkumu je prozkoumat chování jednotlivých kroků logické syntézy (např. v nástroji ABC [3]), zjistit jejich závislost a ortogonalitu a navrhnout algoritmus pro efektivní řízení celého procesu.

• [1] P. Fišer and J. Schmidt, “Improving the Iterative Power of Resynthesis,” in Proc. of 15th IEEE Symposium on Design and Diagnostics of Electronic Systems (DDECS), Tallinn (Estonia), April 18-20, 2012, pp. 30-33.
• [2] P. Fišer and J. Schmidt, “On Using Permutation of Variables to Improve the Iterative Power of Resynthesis,” in Proc. of 10th Int. Workshop on Boolean Problems (IWSBP), Freiberg (Germany), September 19-21, 2012, pp. 107-114.
• [3] Berkeley Logic Synthesis and Verification Group, “ABC: A System for Sequential Synthesis and Verification” [Online]. Available: http://www.eecs.berkeley.edu/alanmi/abc/.

Cílem práce je analyzovat vnímání povrchových materiálů za proměnných světelných a pozorovacích podmínek. Práce bude mít za úkol nalezení vhodných statických i dynamických vizuálních stimulů a psychofyzikální ověření jejich relativního významu pro lidské vnímání a rozpoznávání odlišných materiálů.

Práce je zaměřena na výzkum metod rozpoznávání a modelování tvaru těles z videozáznamu pro aplikace virtuální reality. Navrhněte a realizujte vhodnou metodu automatického odhadování 3D modelu z naměřených dat pomocí videokamery. Ověřte metodu na vybraných modelech soch a budov.

Práce je zaměřena na studium metod odhadu pokročilých reprezentací vizuálních vlastností povrchových materiálů (BTF, SVBRDF) přímo měřením 3D objektů v přirozeném osvětlení. Navrhněte a realizujte vhodnou metodu automatického odhadování vizuální reprezentace povrchového materiálu z naměřených dat pomocí ručního snímání videokamerou. Ověřte metodu na vybraných povrchových materiálech.

Stanovení kvality modelovaných vizuálních dat je stále nevyřešený problém, protože chybí matematické kritérium umožňující vhodně aproximovat lidské vnímání. Cílem práce bude nalezení takového kritéria, které umožní porovnávat a řadit podle podobnosti syntetické výsledky s jejich měřenými vzory. Kritérium bude použitelné i na texturních datech.

Práce je zaměřena na studium metod modelování osvětlení z naměřené obrazové informace pro aplikace modelování BTF textur v modelech virtuální reality. Navrhněte a realizujte vhodnou metodu tvorby osvětlení z naměřených obrazových dat. Ověřte metodu na modelu osvětlení interiéru a exteriéru při proměnném osvětlení.

Návrh a implementace vhodného statistického modelu, který umožní modelování a predikci šíření virové infekce mezi jednotlivými sousedícími zeměpisnými oblastmi. Model dále umožní hodnotit některá vybraná epidemiologická opatření a jejich vliv na rychlost šíření virové infekce. Vyvinutý markovský model bude verifikován na datech koronavirové infekce COVID-19.

Vzhled reálných materiálů se významně mění se změnou osvětlení a pohledu. Proto současné nejvyspělejší texturní reprezentace (BTF) vyžadují modelovat odrazivost v širokém rozsahu parametrů osvětlení a umístění kamery pomocí složitých matematických modelů. Cílem práce bude vyvinout a ověřit nový BTF model založený na teorii markovských náhodných polí, který zlepší současný stav fyzikálně správného modelování povrchů materiálů.

Návrh vhodných multispektrálních texturních příznaků pro analýzu povrchových materiálů vizuálních scén s proměnlivými podmínkami pozorování. Příznaky budou odvozeny od vícerozměrových statistických modelů, navrženy jejich invariantní modifikace, porovnány se současnými nejlepšími publikovanými alternativními texturními příznaky a aplikovány na BTF data.

Cílem práce je kriticky zhodnotit současný stav neřízené segmentace obrazových dat a vyvinutí algoritmu pro neřízenou segmentaci dynamických barevných / multispektrálních / BTF obrazů do jednotlivých homogenních oblastí. Algoritmus bude založen na vícerozměrných markovských modelech a testován na PTSB benchmarku.

Melanom kůže, jako nejnebezpečnější forma rakoviny kůže, je rostoucím nebezpečím v posledních desetiletích díky svému stále zvyšujícímu se výskytu. Jeho efektivní léčba vyžaduje jeho rozpoznání a chirurgické odstranění v co nejranější fázi. Cílem práce je nalezení diskriminativních obrazových příznaků a vhodného klasifikátoru, který umožní rozpoznání rakoviny kůže z barevných obrazů kůže a zároveň umožní monitorování pokroku léčby ze sekvence časově proměnných obrazů nádoru.

Uvažovaným základním problémem je RCPSP (Resource-Constrained Project Scheduling Problem). Je dán množinou činností, které mají být naplánovány. Pořadí těchto činností je částečně definováno relacemi následností. Každá činnost vyžaduje určité množství obnovitelných zdrojů (např. stroje, zaměstnance), přičemž každý zdroj má plánovanou kapacitu a určitou energii (tj. spotřební zdroj s limity danými 15minutovými smlouvami). Cílem je najít posloupnost činností přiřazených ke zdrojům (tj. rozvrh) a kapacitu zdrojů s ohledem na dvě kritéria. Jedním z cílů je minimalizovat penalizaci za včasnost/zdržení (náklady vzniklé dokončením některých zakázek před nebo po termínu jejich splatnosti). Druhým cílem je minimalizace nákladů spojených se zvyšováním kapacity zdrojů (např. přijímání více zaměstnanců nebo práce přesčas). Pak by řešení problému mohlo uvažovat o lineární kombinaci nebo o Pareto optimu s ohledem na tyto dva cíle.

Problém můžeme dále rozšířit při zvažování alternativ nebo módů provádění procesů. Nakonec bychom mohli prozkoumat využití strojového učení k urychlení našich algoritmů, například k urychlení výpočtu objektivní funkce v algoritmu provádějícím časté záměny úloh, jak se ukázalo jako užitečné v naší předchozí práci zabývající se rozpisem sester ve směnném provozu.

• Čapek, R. - Šůcha, P. - Hanzálek, Z.: Production Scheduling with Alternative Process Plans, European Journal of Operational Research, Volume 217, Issue 2, March 2012, Pages 300–311.
• Módos, I. - Šůcha, P. - Hanzálek, Z.: Algorithms for robust production scheduling with energy consumption limits, Computers & Industrial Engineering, Volume 112, October 2017, Pages 391-408.
• Václavík, R. - Šůcha, P. - Hanzálek, Z.: Roster evaluation based on classifiers for the nurse rostering problem, Journal of Heuristics, October 2016, Volume 22, Issue 5, Pages 667–697

Vzhledem k tomu, že počet úloh a zdrojů v mnoha aplikacích rychle roste, je výpočet časového plánu (TT) velmi obtížný. I u velmi základních modelů je známo, že tyto problémy jsou NP-těžké. U rozsáhlých problémů je proto první výzvou získat rozumné řešení v rozumném čase. Nejběžnějším přístupem je modelování problému rozvrhování pomocí určitého formalismu, obvykle SMT nebo ILP, a nalezení proveditelného řešení pomocí univerzálního řešiče. Nevýhodou tohoto přístupu je jeho omezený výkon. Pro dosažení dostatečné škálovatelnosti je třeba vyvinout specifický algoritmus.

Máme zájem vyvinout efektivní a škálovatelné algoritmy, které budou schopny vypočítat rozvrhy (např. časem spouštěné komunikace v IEEE 802.1Qbv Time-Sensitive Networks) s desítkami tisíc úloh (tj. zpráv) pokrývajících stovky zdrojů (tj. komunikační kanály). Kromě toho se očekává, že algoritmy budou během vyhledávání uchovávat některé cenné informace, označované jako kontext, které pak budou využity k urychlení procesu vývoje plánu v reakci na měnící se požadavky.

Můžeme dále rozšířit naše algoritmy, aby společně zpracovávaly TT a Event-Triggered (ET) komunikace, čímž zlepšíme vlastnosti systémového časování. Nakonec bychom mohli prozkoumat použití strojového učení k urychlení našich algoritmů. Nedávno jsme navrhli hlubokou neuronovou síť kombinovanou s Lawlerovým rozkladem pro problém zpožděných dokončení na jednom stroji. Výsledky ukazují, že náš algoritmus založený na datech překonal dřívější moderní heuristiku a my vidíme velký potenciál rozšířit jej na další problémy se známým dekompozičním pravidlem.

• Vlk, M. - Brejchova, K. - Hanzalek, Z. - Tang, S.: Large-Scale Periodic Scheduling in Time-Sensitive Networks, Computers & Operations Research, Volume 137, January 2022.
• Minaeva, A. - Hanzalek, Z.: Survey on Periodic Scheduling for Time-Triggered Hard Real-Time Systems, ACM Computing Surveys, Volume 54, Issue 1, March 2021, Article 23, Pages 23:1-23:32.
• Bouška, M., Novák, A., Šůcha, P., Módos, I., Hanzálek, Z.: Data-driven Algorithm for Scheduling with Total Tardiness. In: Proceedings of the 9th International Conference on Operations Research and Enterprise Systems, ICORES 2020.

Rozvrhování výpočetních a komunikačních úloh v systémech, jako jsou například real-time časem řízené vestavěné jednotky (TTRES) v automatizovaných automobilech, se řídí předem definovaným statickým rozvrhem. Pro jeho nalezení je potřeba navrhnout komplexní rozvrhovací algoritmus. Tradiční časem řízené paradigma je však příliš rigidní a nezohledňuje vývoj konfigurace TTRES během jejího životního cyklu. Na základě našich zkušeností se domníváme, že současné algoritmy pro TTRES se nedokáží: (i) přizpůsobit změnám při přidávání dalších úloh do rozvrhu a (ii) zlepšit strategii vyhledávání o informace automaticky získané z řešení příbuzných problémů a instancí. Algoritmy řešící nedostatky (i) a (ii) lze řídit vstupními daty problému, jejichž charakter má vliv na omezení a kritéria daného rozvrhovacího problému. Věříme, že jde o významný nevyužitý potenciál v rozvrhovacích algoritmech. Naším cílem je uvolnit tento potenciál s využitím strojového učení a navázat na naše předchozí výsledky kombinující strojové učení a kombinatorickou optimalizaci.

Optimalizační úlohy, se kterými se setkáváme v reálných aplikacích, stále častěji optimalizují cíle, kterými nejsou matematické funkce, ale výsledky počítačových simulací nebo experimentálních měření. Tento druh optimalizace, označovaný jako black-box optimalizace, představuje dvě velké výzvy: 1. lze získat pouze hodnoty takového black-box cíle, nikoliv jeho gradient nebo vyšší derivace, 2. vyhodnocení cíle je typicky časově náročné a/nebo drahé. Pokud jde o první výzvu, v uplynulých desetiletích se velmi úspěšnými při otimalizaci používající pouze hodnoty cíle ukázaly být evoluční algoritmy. Ty však typicky vyžadují velké množství vyhodnocování, což je v konfliktu s druhou výzvou. Tento konflikt v uplynulém desetiletí podnítil intenzivní výzkum evoluční black-box optimalizace, který s sebou přináší široké spektrum dizertabilních témat.

Jako black-box označujeme optimalizaci, při které se nepoužívá matematické vyjádření optimalizované funkce (typicky z důvodu, že žádné takové vyjádření není známo), ale optimalizační algoritmus má k dispozici pouze její hodnoty v konkrétních bodech. Tyto hodnoty se obvykle získávají empiricky měřením nebo pomocí experimentů, ať už probíhají fyzicky nebo v podobě simulací. Pro black-box optimalizaci se používají algoritmy, které nemají skoro žádné předpoklady o matematických vlastnostech optimalizované funkce, nejčastěji evoluční algoritmy a další přírodou inspirované algoritmy jako roje částic. Protože tyto algoritmy pracují pouze s funkčními hodnotami optimalizované funkce, blíží s k jejímu optimu podstatně pomaleji než optimalizační metody pro hladké funkce, které využívají rovněž informace o gradientu optimalizované funkce, případně o jejích druhých derivacích. Tato vlastnost je zvláště nepříjemná ve spojení se skutečností, že empirické získání hodnoty optimalizované funkce bývá obvykle značně nákladné i časově náročné. Evoluční algoritmy však lze podstatně urychlit tím, že při vyhodnocování funkční hodnoty optimalizované funkce používají empirickou black-box funkci jen občas, zatímco většinou vyhodnocují pouze její dostatečně přesný regresní model. Mezi regresními modely používanými k tomuto účelu jsou už zhruba 20 let i umělé neuronové sítě, nejdříve vícevrstvé perceptrony a později pak sítě s radiálními bázovými funkcemi. Pod vlivem současné popularity moderních typů neuronových sítí, často označovaných jako hluboké neuronové sítě, byly nicméně v posledních letech navrženy nové přístupy použitelné k urychlení black-box optimalizace, jako jsou hluboké Gaussovské procesy, použití bayesovských neuronových sítí, optimalizaci v latentním prostoru nižší dimenze, zobrazovaném generativní neuronovou sítí do prostoru, v němž leží vstupy optimalizované black-box funkce, nebo využití sítí typu GAN (generative adversarial network), jejichž dvě komponenty se používají pro explorační a exploatační složku optimalizace.

Grafová data se používají k uchovávání znalostí o mnoha důležitých oblastech současného světa, jako jsou např. počí-tačové sítě, sociální sítě, chemické molekuly, komunikační systémy, průmyslové procesy či textové dokumenty. Metody pro analýzu dat a modelování založené na datech, jako jsou klasifikace, regrese a shlukování, však byly dosud vyvíjeny primárně pro vektorová data a grafová data je pro použití těchto metod zapotřebí nejprve reprezentovat v nějakém vektorovém prostoru. Nejúspěšnější při takové reprezentaci jsou umělé neuronové sítě. Díky potřebě učení reprezenta-cí grafů se objevil specifický typ neuronových sítí, nazývaný grafové neuronové sítě. Avšak i grafové neuronové sítě mají vlastnost naprosté většiny umělých neuronových sítí, že transformace vstupů sítě na její výstupy je black-box zob-razení, které pro daný vstup sítě neumožňuje vysvětlit její výstup. V souvislosti s tradičními neuronovými sítěmi, přede-vším vícevrstevnými perceptrony a sítěmi s radiálními bázovými funkcemi, se již od devadesátých let věnuje pozornost metodám umožňujícím popsat závislost výstupu sítě na jejím vstupu pomocí logických implikací a ekvivalencí, případně jiným způsobem vysvětlit hodnotu výstupu pro daný vstup. V případě grafových neuronových sítí je však výzkum vysvět-lovacích metod teprve v začátcích. Příspěvkem k němu by měla být i navrhovaná práce.

Evoluční algoritmy jsou v posledních 20 letech jednou z nejúspěšnějších metod pro řešení netradičních optimalizačních problémů, jako např. hledání nejvhodnějších dokumentů obsahujících požadované informace, objevování nejzajímvějších informací v dostupných datech či další typy optimalizačních úloh, při nichž lze hodnoty cílové funkce získat pouze empiricky. Protože evoluční algoritmy pracují pouze s funkčními hodnotami optimalizované funkce, blíží s k jejímu optimu podstatně pomaleji než optimalizační metody pro hladké funkce, které využívají rovněž informace o gradientu optimalizované funkce, případně o jejích druhých derivacích. Tato vlastnost evolučních algoritmů je zvláště nepříjemná ve spojení se skutečností, že empirické získání hodnoty optimalizované funkce bývá obvykle značně nákladné i časově náročné. Evoluční algoritmy však lze podstatně urychlit tím, že při vyhodnocování funkční hodnoty optimalizované funkce používají empirickou optimalizovanou funkci jen občas, zatímco většinou vyhodnocují pouze její dostatečně přesný regresní model. Právě přesnost modelu určuje, jak úspěšnou náhražkou původní empirické funkce bude. Proto se po získání každé nové generace bodů, v nichž byla empirická funkce vyhodnocena, model zpřesňuje opakovaným učením zahrnujícím tyto body. Lze však jít ještě dále a již při volbě bodů pro empirické vyhodnocení brát kromě hodnoty empirické funkce také v úvahu, jak při opakovaném učení modelu přispějí k jeho zpřesnění. Takový přístup se označuje jako aktivní učení. Používání aktivního učení k urychlení evolučních algoritmů je však teprve v úplných začátcích a měla by ho podpořit i navržená práce.

Levná technologie pro sekvenování genomu odstartovala obrovský nárůst dat, která je potřeba uložit a zpracovat. Takto obrovský objem dat je potřeba pro personalizovanou medicínu, pro výzkum pangenomu nebo pro hledání biomarkerů pro různé nemoci. Tradiční indexy umožňující efektivní vyhledávání tentokrát selhávají kvůli překročení dostupné paměti. Také nevyužívají důležitou vlastnost vysoké podobnosti sekvencí lidského genomu.

Poslední vývoj v oblasti stringologie přinesl různé komprimované indexy založené na Burrows-Wheelerově transformaci. Cílem projektu je nalézt efektivnější metody pro ukládání a indexování dat pro různé úlohy v bioinformatice.

Claude Shannon provedl experiment v roce 1951 a dospěl k závěru, že entropie anglického textu je 0,6-1,3 bitů na znak. Model takového experimentu zahrnuje znalost anglické gramatiky, anglické slovní zásoby a nejběžnějších anglických frází.

Cílem práce je zvýšit efektivitu komprese textů přirozeného jazyka pomocí relaxace výše uvedeného modelu. Několik fází analýzy přirozeného jazyka bude použito jak k porozumění textu, tak k efektivnější kompresi textu.

Datový formát XML byl zaveden před mnoha lety a dnes je široce používán jako defacto standard pro reprezentaci a výměnu dat přes WWW. Bylo vyvinuto mnoho technik komprese XML. Některé neumožňují dotazy bez dekomprese celého XML dokumentu, některé ano. Nejnovější vývoj ve stringologii nám však přinesl rychlé a komprimované datové struktury pro ukládání dat na základě Burrows-Wheelerovy transformace. Cílem dizertační práce je nalézt efektivnější metody pro ukládání a dotazování dat ve formátu XML. Tyto metody by měly zachovat snadný a rychlý přístup k uloženým datům a zároveň zlepšit složitost paměti.

Školitel-specialista: Ing. Hana Najmanová, Ph.D., prof. RNDr. Pavel Surynek, Ph.D.

Multiagentní (MA) modely pohybu chodců se stávají slibným nástrojem využívaným v požárním inženýrství pro posouzení bezpečné evakuace osob. Chodec je v takovém modelu reprezentován agentem, jehož parametry, dynamika a interakční pravidla jsou inspirována fyzickými, kognitivními a psychickými procesy lidí v davu. Nedávné studie ukazují, že velmi důležitým, ale zřídka uvažovaným aspektem ovlivňujícím proces evakuace, je heterogenita davu různých úrovní. Velkou (a dosud málo pojednanou) výzvou je simulace davu složeného z chodců s podstatně odlišnými rolemi a kompetencemi během evakuace (poslouchání vs. udílení instrukcí, organizace a řízení jiných chodců) jako např. evakuace školy (žáci vs. učitelé) nebo kulturní akce (návštěvníci vs. personál).

Cílem práce je zaplnit tuto mezeru v současném stavu poznání některými z následujících způsobů:

• Důkladné prozkoumání vlivu podstatné heterogenity na důležité charakteristiky toku chodců a procesu evakuace v nejběžnějších MA modelech (celulární, založené na sociální síle nebo pravidlech).
• Vývoj nových nebo modifikace stávajících MA modelů tak, aby byla umožněna výše zmíněná hierarchická heterogenita, vazby mezi agenty a formace.
• Organizace a analýza evakuačních experimentů zabývajících se výše uvedenými otázkami. Porovnání experimentů a simulací, vývoj metrik kvantifikujících shodu heterogenity v modelech a realitě.
• Využití nástrojů multiagentního hledání cest a plánování pro prozkoumání možných strategií řídících chodců/agentů a vlivu těchto strategií na proces evakuace.

Práce by měla být konzultována s odborníkem na požární inženýrství a s odborníkem na multiagentní plánovací procesy.

Cílem DP je naevrhnout metodu analýzy vibrací způsobených nerovnostmi vozovky a na jejím základě porovnat efektivitu různých strategií řízení pérování automobilů. Strategie budou porovnávány a vyhodnoceny na základě software-in-the-loop simulací v platformě Matlab popř. jinou metodou navrženou doktorandem. Porovnávány budou výsledky simulací pérování čtvrtinového modelu automobilu pro různé typy nerovností vozovky. Strategie tlumení je kompromisem mezi dvěma protichůdnými požadavky: držení vozidla na vozovce a jízdní komfort cestujícího. Tato kritéria budou ve studii zohledněna. Srovnání bude provedeno jak pro skupinu čistě aktivního tak pro skupinu semiaktivního pérování. Součástí práce bude i rešerše současného stavu problematiky.

Metody moderních IoT musí podporovat spolupráci koncových prvků s aktuálními P2P metodami distribuovaných aplikací a databází opírajících se o výkonné výpočetní systémy s virtuální a cloud architekturou a o vysokorychlostní Internet.

Samotné provozní prvky IoT (sensory, ovladače a prvky kombinující obě tyto funkce) přitom musí respektovat řadu omezení parametrů (energetické limity sensorů, vliv mobility na komunikační limity bezdrátové komunikace, apod).

Cílem disertační práce je návrh a analýza algoritmických metod pro zajištění spolehlivé a efektivní spolupráce jak IoT prvků navzájem tak mezi IOT prvky a centrální infrastrukturou cloudového systému.

Splnitelnost modulo teorie (SMT) se zaměřuje na poskytování technologie pro řešení těžkých problémů pocházejících z praxe, které lze formalizovat v matematické logice. Zdroje aplikací jsou například testování nebo verifikace softwaru. Moderní SMT řešiče se však z řešení jednoho problému nedozvědí žádné nové informace, které by se daly přenést na jiný problém. Naproti tomu, moderní techniky strojového učení (ML) umožňují zdokonalování algoritmů v průběhu času. Tématem této práce je navázat na existující SMT algoritmy a rozšířit je o ML techniky pro kvalitativní vylepšení nejmodernějších řešitelů.

Formální stromové jazyky, formalismy pro jejich generování a popis, a výpočetní modely pro zpracování stromových jazyků tvoří jednu z oblastí teorie formálních jazyků a automatů. Praktickými souvisejícími tématy výzkumu jsou také efektivní algoritmy pro různé úlohy zpracování stromů, jako jsou vyhledávání, indexování nebo výpočet repetic ve stromech. Mezi různé typy uvažovaných stromů patří například seřazené a neseřazené stromy, nebo ohodnocené a neohodnocené stromy. Mezi uvažované třídy formálních stromových jazyků patří například regulární nebo bezkontextové stromové jazyky. Modely výpočtů pro zpracování stromových jazyků zahrnují různé typy stromových automatů nebo zásobníkové automaty, které čtou lineární zápisy stromů. Cílem studia je rozvíjet teorii formálních stromových jazyků a efektivních algoritmů pro sekvenční a paralelní zpracování stromů.

Výzkum v oblasti reliability v kontextu hlubokého učení ukazuje, že neexistuje shoda ohledně toho, jak by se měla reliabilita vyhodnocovat. Do nově vzniklé oblasti výzkumu reliability pro hluboké učení patří např. statistické postupy založené na jednoduchých myšlenkách jako verifikace naučené sítě pro data, která pocházející z jiného rozdělení než trénovací data. Mezi silnější nástroje patří vyčíslení vlivu škodlivých vzorů [1], vyčíslení neurčitosti v algoritmech hlubokého učení [3], nebo výpočetní metody pro propagaci chyby skrz sítě [2]. Mezi teoretické přístupy vycházející z teorie pravděpodobnosti patří statistické testování reliability pro klasifikátor [4]. V dizertaci budou navrženy nové nástroje pro vyčíslení reliability pro natrénovanou hlubokou síť. Teoreticky bude studováno vyčíslení vlivu chyb (neurčitost, chyby měření, nebo odlehlé hodnoty) na výsledky natrénované hluboké sítě. Další cíl je odvodit diagnostické nástroje pro ověření pravděpodobnostních předpokladů hluboké sítě. Přitom bude využito nástrojů, mezi něž patří bootstrap anebo neparametrická kombinace testů hypotéz.

• [1] Alshemali B., Kalita J. (2020). Improving the reliability of deep neural networks in NLP: A review. Knowledge-based systems 191, 105210.
• [2] Bosio A., Bernardi P., Ruospo A., Sanchez E. (2019). A reliability analysis of a deep neural network. IEEE Latin American Test Symposium LATS 2019, 1-6.
• [3] Caldeira J., Nord B. (2021). Deeply uncertain: Comparing methods of uncertainty quantification in deep learning algorithms. Machine Learning: Science and Technology 2, 015002.
• [4] Gweon H. (2022). A power-controlled reliability assessment for multi-class probabilistic classifiers. Advances in Data Analysis and Classification. Online first.
• [5] Martensson G., Ferreira D., Granberg T., Cavallin L., Oppedal K. et al. (2020). The reliability of a deep learning model in clinical out-of-distribution MRI data: A multicohort study. Medical Image Analysis 66, 101714.

Lineární diskriminační analýza (LDA) představuje populární statistickou klasifikační metodu. Byla navržena řada různých regularizovaných verzí LDA pro vysoce dimenzionální data, tj. data s počtem proměnných převyšujícím (i řádově) počet pozorování. Nedávno navržené robustní regularizované verze LDA jsou rezistentní vůči přítomnosti odlehlých hodnot v datech. Tyto metody využívají robustních odhadů střední hodnoty a varianční matice mnohorozměrných dat. Cílem dizertace bude navrhnout a studovat nové verze robustní regularizované LDA a provést rozsáhlé simulace, které ověří jejich vlastnosti. Nové metody využijí nových robustních odhadů varianční matice: Jedna myšlenka je využít odhad MRWCD [1], který minimalizuje determinant regularizované vážené varianční matice. Druhá myšlenka je využít odhad, který je založen na metodách numerické lineární algebry, zejména odhad založený na minimalizaci součinu malého počtu největších vlastních čísel varianční matice [2].

• [1] Kalina J., Tichavský J. (2022): The minimum weighted covariance determinant estimator for high-dimensional data. Advances in Data Analysis and Classification 16, 977-999.
• [2] Kalina J. (2020): The minimum weighted covariance determinant estimator revisited. Communications in Statistics Simulation and Computation 51, 3888-3900.

Školitel-specialista: Ing. Petra Pavlíčková, Ph.D.

V ekonomice podniku je v současné době generováno množství dat, následně uložených v podnikových informačních systémech (ERP). Takto získaná a uložená data jsou vhodným podkladem pro rozhodování manažerů na všech stupních řízení podniku. Pro podporu manažerského rozhodování je žádoucí vhodně formalizovat expertní znalosti z oblasti finančního zdraví podniku a řízení hlavních ekonomických procesů v podniku tak, aby došlo k jejich zefektivnění a zvýšení zisku podniku. Rámcové téma disertační práce se proto zaměřuje na nalezení vhodné metody reprezentace znalostní báze z oblasti řízení ekonomických procesů podniku, zejména s využitím nástrojů modelování používaných při modelování medicínských znalostí (GLIF, znalostní ontologie). Hlavní směr zkoumání bude orientován na modelování znalostní báze ekonomických procesů primárně pomocí metodik OntoUML.

Mnoho témat studovaných v rámci výpočetní sociální volby nalezlo v současné době již nespočet aplikací. Abychom vyjmenovali jen několik z nich: doporučovací systémy nebo rozdělování prostředků z potravinových bank. S tím, jak rostou nároky na používané systémy, zároveň roste potřeba efektivních algoritmů pro tyto a příbuzné problémy; speciálně pak podrobné studium jejich vlastností a výpočetní složitosti. Hlavním paradigmatem pro toto studium bude tzv. parametrizovaná složitost (též známá jako multivarietní analýza složitosti algoritmů), která se již řadu let úspěšně používá nejen v tomto oboru. Zároveň je třeba se zaměřit na praktická řešení na reálných datech, na které zle očekávat úspěšné nasazení dlouhodobě vyvíjených nástrojů jakými bezpochyby jsou ILP či SAT řešiče. Zároveň je dobré podotknout, že toto odvětví skrývá i velké výzvy v podobě problémů, které jsou úplné pro “vyšší třídy” polynomiální hierarchie. Takovým problémem je například tzv. Judgement Aggregation.

U doporučovacích systémů v současné době zaměřujeme výzkum na několik otevřených problémů, které mají hluboké teoretické základy, ale jejichž řešení mají současně velmi konkrétní praktické aplikace. Zkoumáme využitenost hlubokých neuronových sítí pro redukci cold start problému doporučovacího systému, konstrukci transformerů pro predikci nákupních košíků. V oblasti obecného strojového učení se zaměřujeme na posilované učení pro optimalizaci dlouhodobějších metrik, jako je spokojenost uživatele, na metody transfer learningu pro začlenění nových doporučovacích databází, a na využití AutoML pro optimalizaci architektury a hyperparametrů doporučovacího systému.

Analýza dat se obvykle provádí složením řady diskrétních nástrojů a knihoven do datově-analytických kanálů. Ty jsou jádrem datových věd, které dnes zažívají strmý růst počtu výpočetních metod a objemu analyzovaných dat. Díky tomu vznikají problémy se škálovatelností těchto kanálů a důvěryhodností jejich výsledků.

Obsahem této disertační práce je výzkum škálovatelnosti (přizpůsobivosti se rostoucí velikosti dat a výpočetním potřebám) a důvěryhodnosti (usnadňují auditování výsledku) datově-analytických kanálů. Výzkum bude probíhat ve dvou rovinách. První se zaměří na možnosti rozšíření programovacího jazyka R umožňující transparentní vertikální a horizontální škálování. Druhá rovina bude výzkum kombinací technik statické a dynamické analýzy programů k získání informací o typech a závažnosti programovacích chyb, které se vyskytují v kódech datově-analytických kanálů a následně návrh algoritmů pro jejich detekci a možné automatické odstranění.

Extrakce informací z textu se používá v mnoha oborech k redukci textu vynecháním jeho částí, které nenesou informaci relevantní pro uživatele. Patří sem např. sumarizace textu. Téma je z oblasti text mining, což je obor plný otevřených problémů. V našich publikovaných pracích jsme používali techniky linguistické analýzy vět (angl.. part-of-speech tagging) a clustrování podle podmnožin vět (angl. chunking) pro účely analýzy textů funkčních požadavků na softwarový produkt. Na základě textů jsme generovali dotazy, jejichž cílem bylo analýzou odpovědí zpřesňovat specifikaci funkčních požadavků. Cílem práce je použít vyzkoušené techniky z našich publikací v oblasti extrakce textů, porovnat je se současnými výsledky publikovaných metod a nalézt dokonalejší nové metody.

Školitel-specialista: Ing. Tomáš Čejka, Ph.D.

Obsahem práce bude výzkum algoritmů pro detekci, identifikaci a mitigaci bezpečnostních hrozeb a anomálií v počítačových sítích se zaměřením na oblast tzv. Internetu věcí (IoT). Z pohledu síťové bezpečnosti je nutné nahlížet na oblast IoT jako na hrozbu a to jak pro samotné IoT, tak i pro další zařízení, kdy IoT se může stát zdrojem hrozby. Je proto důležité sledovat komunikaci v těchto sítích, odvozovat z významných událostí v komunikaci další meta informace a tyto informace používat pro identifikaci zdroje hrozeb, mitigaci hrozeb a řízení strategie mitigace.

Cílem dizertační práce bude nalezení vhodných možností, jak vytvářet modely dlouhodobě uchovávající negativní či pozitivní události v komunikaci, a jak na základě těchto modelů co nejrychleji (s minimální latencí) tyto detekovat, identifikovat a odstranit zdroje problémů. Dizertabilita tématu je založena na faktech, že jde o řešení velmi netriviálních problémů, kterými jsou zpracování a filtrace velkých objemů dat společně s modelováním síťového provozu, hledání odchylek,identifikace zdrojů problémů a správné řízení mitigace těchto problémů. Na rozdíl od klasických IP sítí, IoT prostředí navíc významně využívá specifických fyzických vrstev v podobě specializovaných komunikačních protokolů, což s sebou přináší nové potenciální vektory útoků, které jsou běžnou analýzou IP provozu nedetekovatelné. Z tohoto důvodu je potřeba hledat nové způsoby monitorování IoT provozu. Základem bude výzkum v oblasti možností využití statistických metod, pravděpodobnostních modelů a využití algoritmů umělé inteligence.

Vzhledem k současným rychlostem síťových přenosů a požadavkům na on-line monitorování je nutné algoritmy navrhovat a realizovat s využitím dekompozice na hardwarovou a softwarovou část a s použitím vhodných technologií hardwarové akcelerace (např. FPGA).

Výzkum možností využití formálních metod (Petriho sítě, Markovské řetězce, UML diagramy) pro zjednodušení návrhu číslicového systému a jeho automatizaci. Předpokládejme spojení s verifikací a výpočty spolehlivostních ukazatelů ve všech návrhových fázích a úpravu a optimalizaci řešení podle různých parametrů. Cílem by měla být i vzájemná kombinace různých typů modelů a podrobný výzkum vztahů a automatizovaného přechodu mezi nimi. Dílčí výsledky a navržené metody budou průběžně ověřovány na reálných aplikacích a benchmarcích. Nedílnou součástí tématu je i studium možných nových modelů používaných v průmyslu a/nebo ve výzkumu.

Výzkum způsobů a postupů v návrhu systému s předem danými spolehlivostními parametry na bázi programovatelného hardwaru (FPGA i procesorů). Výzkum vlivu redundance na různých úrovních (v prostoru, čase, SW, HW) na odolnost proti útokům. Zahrnutí možné automatizace postupů včetně vytvoření spolehlivostních modelů a výpočtů spolehlivostních parametrů. Předpokládá se průběžné ověřování výsledků na reálných aplikacích a benchmarcích.

Školitel-specialista: Ing. Martin Kohlík, Ph.D.

Současné spolehlivostní modely často využívají zjednodušené postupy vedoucí k nerealistickým odhadům spolehlivosti a životnosti modelovaných systémů [1], nebo používají hrubé pesimistické odhady [2]. Cílem práce by měla být metodologie návrhu spolehlivostního modelu, který umožní rychlé a přesné výpočty spolehlivostních parametrů systému. Metodologie by měla zohlednit změny systému v čase (např. stárnutí, údržbu, opravy), strukturu systému (jednotlivé bloky a jejich případné zabezpečení proti poruchám) a možnosti získávání spolehlivostních ukazatelů z reálných dat [3].

• [1] Electronic Reliability Design Handbook - MIL-HDBK-338B. US Department of Defense, 1998.
• [2] M. Kohlík, "Hierarchical Dependability Models Based on Markov Chains", Dissertation thesis, Czech Technical University in Prague, 2015.
• [3] Daňhel, M.: "Prediction and Analysis of Mission Critical Systems Dependability", Dissertation thesis, Czech Technical University in Prague, 2018.

Školitel-specialista: Ing. Pavel Kubalík, Ph.D.

Cílem tohoto výzkumu je:

- návrh architektur založených na on-line detekci a opravě chyb pro FPGA obvody, které budou použitelné pro mission-critical systémy (inteligentní auta apod.), tedy systémy, u kterých je nutné dodržet požadovanou úroveň spolehlivostních parametrů, spolu se zajištěním minimální velikosti, pracovní frekvence (real-time), a tudíž i spotřeby.

- návrh vhodných metod, které by automatizovaně vybraly vhodný typ zabezpečení s ohledem na konkrétní aplikaci, její požadavky a nutná omezení (design constrains), včetně rychlosti návrhu.

- využití existujících modelů a jejich úprava, které by tento problém řešily na systémové úrovni a jejich propojení s hierarchickými modely spolehlivosti, vytvářenými na katedře.

Cílovou platformou bude FPGA obvod umožňující zotavení po poruše a případně i možnost změny funkce celého implementovaného systému. Výzkum klade důraz zejména na využití nových a upravených typů bezpečnostních kódů pro optimalizovanou architekturu s detekcí a opravou chyb vhodnou pro FPGA. Klasické struktury odolné proti poruchám (TMR, duplex) budou také zohledněny a případně využity.

Vytvořené architektury budou v průběhu výzkumu ověřovány na reálných benchmarcích a vlastní sadě obvodů. Hodnotícím parametrem bude (kromě velikosti) realistický výpočet dosažených spolehlivostních parametrů.

Školitel-specialista: Mgr. Peter Kálnai, Ph.D.

Obsahem tématu je výzkum ověření možností, jak dosáhnout (a garantovat) předem určená omezení při návrhu systému (velikost, spotřebu, požadované ukazatele spolehlivosti, odolnost proti poruchám/útokům) vhodnou kombinací výběru a poměru hardwaru a softwaru. Předpokládáme využití systému pro návrh procesorů Codasip a otevřeného procesoru RISC-V (RISC-V byl specielně navržen pro široké použití nejen, pro vestavné systémy s důrazem na výkon i na spotřebu). Systém Codasip (https://codasip.com/) umožňuje navrhovat a upravovat specializované procesory, a to včetně verifikačních nástrojů.

Součástí výzkumu bude i použití a případná úprava vhodných spolehlivostních modelů pro ověření dosažení požadovaných parametrů s hlavním cílem určení nejlepší realizace vzhledem k původním požadavkům, tzn. například úprava instrukční sady přidáním kryptografických instrukcí, přidání dalšího bloku, použití více specializovaných procesorů apod.

Ověření výsledků bude možné jednak simulací a jednak implementací ve vhodné FPGA technologii.

Školitel-specialista: RNDr. Petra Vidnerová, Ph.D.

Hluboké sítě se staly v současné době nejpoužívanější metodou v oblasti rozpoznávání obrazů, zejména vizuálních a klasifikačních úloh. Několik nedávných studií ale ukázalo, že se některé hluboké sítě dají snadno zmást malou, pro lidské oko nepostřehnutelnou, změnou obrázku, která vede k tomu, že je obrázek klasifikován jako něco úplně jiného. Je proto potřebné zkoumat robustnost neuronových sítí vzhledem k matoucím vzorům.

Cílem dizertace je navrhnout multiobjektivní algoritmy generující nepostřehnutelné perturbace obrázků vedoucí k jejich nesprávné klasifikaci. Budou vyvinuty evoluční algoritmy pro generování matoucích obrázků, které maximalizují chyby klasifikace a zachovávají co největší podobnost originálním trénovacím vzorům. Bude analyzována role hloubky sítě a lokálních vlastností výpočetních jednotek. Budou zkoumány metody pro zvýšení robustnosti neuronových sítí vzhledem k matoucím vzorům.

Vzdáleně ležící pozorování (nebo „outlier“) je takové, které se významně odlišuje od ostatních prvků ve vzorku, kde se objevuje. Termín „anomálie“ označuje různé problémy v různých oblastech. Je velmi důležité detekovat anomálie co nejdříve, aby nedošlo k velkým ztrátám či problémům, ať už jde o poruchu stroje, nádor v lidském těle, apod.

Ve většině oblastí mají sbíraná/měřená data charakter streamovaných časových řad. Díky jejich inherentním vlastnostem, jako jsou periodicita, trendy, sezónnost a nepravidelnost, představuje přesná detekce anomálií velký problém. Navíc ve většině reálných scénářů je prakticky nemožné anotovat ohromné množství dat. Proto se často používají metody učení bez učitele jako shlukování. Ty však nezohledňují parametr času, který je v časových řadách neoddělitelným kontextem. Proto neumožňují nalézt anomálie, které se objevují v cyklech.

Cílem práce bude navrhnout, implementovat a otestovat metodu učení bez učitele, která bude zohledňovat kontext, sezónnost a trendy při detekci anomálií. Metoda má být adaptovatelná pro různé scénáře a případy a schopná zpracovávat data z různých oblastí.

Velká data s sebou přinášejí celou řadu otázek, z nichž mezi nejdůležitější patří rozpoznání a správné využití různých typů závislostí a také kontextu, který zpravidla nese využitelné informace. Typickým příkladem je prostorové uspořádání zdrojů dat, například senzory pro sběr environmentálních dat v různých prostředích. Tento kontext, společně s měřenými časovými řadami, reprezentuje velmi významný zdroj informace pro predikci výstupu.

V úlohách strojového učení hraje klíčovou roli výběr příznaků. V mnoha případech je však výběr příznaků mnohem složitější než identifikace jedné podmnožiny vstupních proměnných, které společně vysvětlují výstup. Mohou totiž existovat interakce, které závisejí na kontextové informaci, tj. proměnné, která se ukáže relevantní pouze za určitých specifických podmínek. Základní problém k řešení je identifikace vstupních proměnných, jejichž relevance nebo irelevance pro predikci výstupu platí pouze za specifických podmínek, kdy se předpokládá, že tyto podmínky mohou být vyjádřeny pomocí specifické kontextové proměnné. Tato kontextová proměnná může být např. standardní vstupní proměnná, pak je cílem kontextové analýzy lépe pochopit, jak tato proměnná interaguje s ostatními vstupy při predikci výstupu. Kontextem může být také externí proměnná, která nepatří k původním vstupům, ale přesto může ovlivnit jejich relevantnost ve vztahu k výstupu.

Cílem práce bude navrhnout, implementovat a otestovat metodu učení s učitelem, která bude kontextovou informaci využívat pro efektivnější predikci výstupu. Metoda má být adaptovatelná pro různé scénáře a případy a schopná zpracovávat data z různých oblastí.

Kryptoměny jsou novým fenoménem, který je založený na decentralizaci a umožňuje nám anonymní platby. V dnešní době existuje přes tisíc kryptoměn, které jsou založené na různých konceptech, jako jsou např. proof-of-work nebo proof-of-stake. Cílem bude navrhnout novou kryptoměnu, která by splňovala bezpečnostní požadavky i požadavky trhu jako jsou škálovatelnost, dostatečná rychlost zpracování transakcí, nízká latence a byla by šetrná k životnému prostředí.

Škodlivý kód neboli malware patří v dnešní době mezi největší bezpečnostní hrozby. Každodenně se vygeneruje ohromné množství nového škodlivého kódu, a protože není možné analyzovat každý vzorek zvlášť, je potřeba vyvinout automatické mechanismy, které by ho dokázaly detekovat. Ukazuje se, že algoritmy strojového učení jsou vhodným nástrojem pro automatickou detekci malware. Pomocí nich je možné detekovat i zero-day malware, avšak na rozdíl od standardních postupů, jako je detekce založena na signaturách, dosahují vyšší false positive (FP). Cílem dizertační práce bude vyvinout automatický systém pro detekci malware dosahující solidní přesnost klasifikace a mající minimální FP.

Řešení celočíselné soustavy lineárních rovnic (SLR) bez zaokrouhlovacích chyb lze provést pomocí rozdělení řešení do soustav lineárních kongruencí (SLK) a následného převodu výsledků do množiny řešení původní SLR. K tomuto převodu se používá tzv. MRC algoritmus, který má složitost O(nm2), kde n je dimenze matice a m je počet použitých SLK (modulů).

Cílem práce je nalézt efektivnější způsob použití MRC algoritmu, který těží ze znalosti vzájemné datové závislosti řešení SLR. Rovněž je možné navrhnout zparalelnění nově navrženého algoritmu. Výsledkem je metoda založená na MRC pracující s menší složitostí než O(nm2) pro řešení zpětného převodu výsledků SLK na výsledky SLR.

Chování různých obvodů založených na polovodičích je kromě jiných faktorů závislé taktéž na prostředí, ve kterém jsou provozovány. Žádanou informací pro uživatele různých HW zařízení je spolehlivost těchto zařízení v závislosti na stáří, a s tím do určité míry související odolnost polovodičových komponent vůči ionizujícímu záření.

Téma dizertační práce je matematické modelování chování HW polovodičových komponent na různé technologické úrovni v závislosti na ozáření ionizujícím/korpuskulárním zářením. Cílem práce je vytvořit model chování HW zařízení zahrnující faktory stárnutí a degradace materiálů vlivem ozařování. Výsledky budou využitelné pro určení spolehlivosti/doby bezchybné funkcionality obvodů vystavených ozáření nebo dlouhodobému používání.

Studium vhodných post-kvantových kryptosystémů je již dlouhodobě v zájmu kryptologů. Důvodem jsou zdárně se rozvíjející technologie kvantových počítačů, které by mohly svými vlastnostmi za použití vhodných faktorizačních algoritmů ohrozit bezpečnost asymetrických kryptosystémů.

Téma dizertační práce je studium a analýza stávajících a návrh nových metod kryptografických post-kvantových algoritmů. Cílem je vytvořit takový asymetrický kryptosystém, který by byl odolný vůči útokům za použití kvantových počítačů a byl by implementačně jednoduchý a bezpečný.

Jedním z kandidátů post-kvantových kryptosystémů vhodných pro analýzu a případnou úpravu je asymetrický šifrovací algoritmus McEliece založený na binárních Goppa kódech. Tento algoritmus vyhovuje bezpečnostním požadavkům kladeným na asymetrické kryptosystémy dnešní doby, avšak je zde problém s jeho velkou prostorovou složitostí. Snaha o zkrácení velikosti klíčů u tohoto algoritmu muže být dobrou počáteční výzvou pro další výzkum.

Cílem je návrh a implementace specializovaných hardwarových architektur pro výpočet modulárních aritmetických operací. Výsledky jsou použitelné v kryptografii eliptických křivek, stejně jako i v jiných systémech, které využívají modulární aritmetiku.

Současné hardwarové komponenty kryptografických systémů se neobejdou bez kvalitních TRNG. Rovněž jsou žádané spolehlivé generátory klíčů, které jsou založené na PUF. Takové generování klíčů je z hlediska bezpečnosti velmi žádané, a to proto, že tímto způsobem vygenerovaný klíč zůstává „tajemstvím“ samotného hardware kryptosystému.

Téma dizertační práce je studium chování navržených PUF a TRNG z hlediska jejich dlouhodobé stabilní odezvy. Cílem práce je prozkoumat stávající a navrhnout nová řešení PUF a TRNG, která jsou vhodná pro účely dlouhodobého generování kvalitního výstupu u TRNG, a která dávají rovněž garanci stabilního generování klíčů vycházejícího z odezev PUF. Práce zahrnuje studium a pochopení chování těchto komponent na statistické úrovni a taktéž na úrovni fyziklální/technologické.

Analýza postranních kanálů je významnou kapitolou v oblasti počítačové bezpečnosti, neboť dává útočníkovi do rukou nástroj, s jehož pomocí lze získat důvěrná data i přes využití kryptograficky bezpečných algoritmů. Ačkoli jsou útoky postranními kanály známé již více než dvacet let, stále nabízí spoustu výzev ke zkoumání. Mezi aktuální témata patří například útoky na nastupující postkvantové kryptografické algoritmy, ale i doposud méně zkoumané algoritmy, jako jsou například ty založené na ARX. Dalším aktuálním tématem pak je využití umělé inteligence v analýze postranních kanálů. V oblasti protiopatření pak čekají aktuální témata v podobě non-interference a kompozice, či implementace pomocí vysokoúrovňové syntézy. Tyto výzvy a související oblasti budou tématem navrhované disertační práce.

Výzkum metod implementace a akcelerace vybraných kryptologických operací a schémat ve vestavných systémech a v rekonfigurovatelných obvodech, zejména pak v programovatelných hradlových polích.

Geometrie kamer je důležitou oblastí počítačového vidění a robotiky, která poskytuje pochopení základů oboru. Tato oblast však zatím nebyla příliš ovlivněna nedávnými pokroky ve strojovém učení a zejména geometrickém strojovém učení. Naším cílem je použít strojového učení k řešení problémů v geometrii kamer, které nebyly vyřešeny tradičními technikami. Například současné metody pro výpočet geometrie kamery z obrazových korespondencí se mohou efektivně vypořádat pouze s relativně jednoduchými problémy, jako je geometrie dvou pohledů. Například neexistují žádné skutečně účinné výpočetní metody ani pro geometrii tří kalibrovaných kamer. Klasický přístup k návrhu takových metod vede v tomto případě k velmi komplikovaným výpočetním postupům kvůli snaze řešit exaktní algebraické problémy. Nedávné pokroky v numerické algebraické geometrii začínají poskytovat praktickou alternativu k přístupům založeným na eliminaci. Věříme, že tyto přístupy lze výrazně zlepšit z pohledu účinnosti a robustnosti učením se optimálním strategiím řešení, efektivní analýze problémů a přizpůsobení problému datům. Naším plánem je vyvinout nový přístup k řešení obtížných problémů v geometrii více kamer, který by využíval strojové učení a přizpůsoboval techniky řešení konkrétním datům.[MB] M. Bronstein et alt. “Geometric deep learning: going beyond Euclidean data”. IEEE Signal Processing Magazine, vol. 34, no. 4, pp. 18-42, 2017.

• [MB] M. Bronstein et alt. “Geometric deep learning: going beyond Euclidean data”. IEEE Signal Processing Magazine, vol. 34, no. 4, pp. 18-42, 2017.
• [NS] D. Nister and F. Schaffalitzky. “Four Points in Two or Three Calibrated Views: Theory and Practice”. International Journal of Computer Vision (IJCV), vol. 67, pp. 211-231, 2006.
• [Fal] R Fabbri et al. “TRPLP – Trifocal Relative Pose From Lines at Points”. IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pp. 12070-12080, 2020.
• [PLMPl] T Duff et al. “PLMP - Point-Line Minimal Problems in Complete Multi-View Visibility”. IEEE International Conference on Computer Vision (ICCV), pp. 1675-1684, 2019.
• [PL1P] T Duff et al. “PL1P - Point-line Minimal Problems under Partial Visibility in Three Views”. European Conference on Computer Vision (ECCV), pp. 175-192, 2020.
• [BGrob] V Larsson et al. "Beyond Grobner Bases: Basis Selection for Minimal Solvers". IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pp. 3945-3954, 2018.
• [Pfeifer] D Peifer et al. “Learning selection strategies in Buchberger's algorithm”. International Conference on Machine Learning (ICML), pp. 7575-7585, 2020.
• [Bernal] E. Bernal et al. “Machine learning the real discriminant locus”. ArXiv preprint, June 2020.
• [DSAC] E Brachmann et al. "DSAC – Differentiable RANSAC for Camera Localization", CVPR 2017.
• [Ranftl] R Ranftl, V Koltun. Deep Fundamental Matrix Estimation. ECCV 2018.
• [Rolinek] M Vlastelica et al. DIFFERENTIATION OF BLACKBOX COMBINATORIAL SOLVERS. ICLR 2020.

Školitel-specialista: Ing. Michal Valenta, Ph.D.

Grafové databáze se v posledních letech intenzivně rozvíjí a využívají v různých oblastech (data lineage, umělá inteligence, optimalizace dodavatelských řetězců, datové analýzy, ...). Reprezentace dat pomocí orientovaných i neorientovaných grafů zdůrazňuje vzájemné propojení dat a umožňuje je nahlížet z různých perspektiv. S využitím grafových databází roste potřeba výzkumu a rozvoje metod konceptuálního modelování cíleného na následnou implementaci konceptuálních schémat v grafových databázích. Dizertační práce se bude zabývat výzkumem metod konceptuálního modelování a implementací konceptuálních modelů s velkou vyjadřovací schopností (například OntoUML) v grafových databázích.

Jeden z nedostatků klasických metod pro specifikaci softwarových požadavků je obtížnost ověření konzistence a adekvátnosti specifikací. Softwarové inženýrství reagovalo na tuto skutečnost různými metodami (např. model based software engineering, agile software development, executable algebraic specification), které umožňují vidět praktické chování specifikací ve vývojovém procesu co nejdříve. Tyto metody ale dělají kompromisy ohledně jiných aspektů, týkajících se např. expresivity anebo preciznosti. V rámci tohoto tématu student navrhne formální jazyk, který splní dva na první pohled protichůdné cíle:

• Jazyk má expresivitu tak vysokou, aby mohl sloužit k pohodlnému psaní specifikací

• Specifikace v tomto jazyku se dají provést podobně jako programy v obvyklém programovacím jazyku

Klíčem pro současné splnění obou cílů budou anotace, kterými uživatel jazyku poskytuje informaci o vykonávání specifikace tak, aby zvýšená snaha o psaní anotací měla za důsledek zvýšenou účinnost vykonávání. Prvním krokem bude vývoj nástroje pro výuku, který dovoluje studentům, kteří píšou specifikace jako úkol ve cvičení, jejich řešení hned i spustit a otestovat.

Vyvíjíme software, teorii a algoritmy, které umí řešit matematické formule obsahující nelineární rovnice a nerovnice, konjunkce, disjunkce, a logické kvantifikátory. Aplikujeme výslednou technologii v několika oblastech (např. verifikace složitých systémů, výpočet Lyapunových funkcí). Nabízíme velké množství témat v této oblasti.

Více informací:

• http://www.cs.cas.cz/~ratschan/theses/en/constraint_solving.html

Vlak Pendolino z Prahy do Ostravy měl na začátku vážné problémy: občas zastavoval během jízdy kvůli chybě v softwaru. Podobné chyby způsobovaly vážná neštěstí, například havárii raketoplánu Ariane 5 v roce 1996. Náš výzkum je zaměřen na pomoc s tím, aby se v budoucnosti bylo možné takovým problémům vyhýbat. Nabízíme velké množství témat v této oblasti.

Více informací:

• http://www.cs.cas.cz/~ratschan/theses/cz/verification.html

Současný průmyslový návrh a verifikace číslicových obvodů klade důraz na trvání vývoje. Obvyklý požadavek je stylu „o 1% lepší výsledek za čas delší o 1%“. V této situaci se jeví účelným použití akcelerace výpočtu. Standardně používané algoritmy byly navrženy pro sekvenční zpracování a jsou to obvykle složité, mnohovrstevné iterativní heuristiky. Akcelerovat takový výpočet vyžaduje nalézt i v těchto algoritmech (například, založených na metodě větví a hranic) paralelismus, případně nahradit některé části výpočtu lépe paralelizovatelnými postupy. Dále, je třeba stanovit, jaké architektury a granularity akcelerátorů nejlépe odpovídají navrženým výpočtům, a studovat jejich work-optimalitu, neboť ta se promítá do energetické efektivnosti výpočtu.

Přibližné výpočty jsou metodou, jak plnit praktický účel konstruovaného zařízení s podstatně sníženými nároky (příkon, velikost, atd.) na implementaci. Používají se v zásadě dvě metriky přibližnosti: aritmetická diference (pokud se vektor binárních hodnot interpretuje jako číslo) a Hammingova vzdálenost, tedy počet binárních signálů odlišných od původní specifikace. Pro tyto dvě metriky jsou vyvíjeny postupy návrhu. Metrika přibližnosti ovšem vyplývá z účelu výpočtu. V případě obrazové informace diference zpravidla vyhovuje, v ostatních případech tomu obecně být nemusí. Dále, v aplikacích se objevují tvrdá omezení, tedy specifikace, které porušeny být nesmí. Většina současných postupů v návrhu číslicových systémů nedovoluje zavést libovolné, aplikačně specifické metriky, ani aplikačně specifická omezení. Cílem práce je vyvíjet takové postupy a doložit cenu, kterou je případně nutno za univerzálnost zaplatit.

Školitel-specialista: Ing. Daniel Langr, Ph.D.

Použitý formát řídkých matic nebo tenzorů podstatně ovlivňuje výkonnost a škálovatelnost algoritmů v numerické lineární algebře.

Ideální formát zaručuje minimální paměťové nároky, ale zároveň maximální vytížení ALU jednotek, cache pamětí a optimální vyvažování zátěže jednotlivých uzlů HPC systému.

Bylo sice vyvinuto dosti různých formátů, ale tyto mají svoje nevýhody: jsou náročné na převod, jsou použitelné jen pro omezenou množinu operací, případně nepodporují možnost přidání nebo odebrání nenulového prvku.

Cílem práce tedy bude výzkum formátů řídkých matic a tenzorů vhodných pro masivně paralelní algoritmy v numerické lineární algebře s cílem odstranění jejich nedostatků a návrh heuristik pro zvolení optimálního formátu pro danou cílovou architekturu.

Školitel-specialista: Ing. Jan Rohlíček, Ph.D.

Rentgenová strukturní analýza z dat získaných práškovou difrakcí je významná analytická metoda pro určení struktury chemických látek v případě, kdy látka neposkytuje tzv. monokrystal. Pro aplikaci metody je klíčová indexace dat – určení mřížkových parametrů. Existující algoritmy a postupy pro indexaci mají problém indexovat méně kvalitní data a směsi látek. Cílem práce je vyvinout efektivnější paralelní algoritmy než jsou stávající algoritmy, pro řešení těchto problémů.

Simulace molekulární dynamiky (MD) umožňují analyzovat fyzikální pohyby biomolekul. Generovaná data jsou sekvence snímků (řádově statisíce) simulovaných v předem definovaném časovém kroku. Každý snímek se skládá z pozic všech atomů proteinu (řádově desetitisíce), které jsou simulovány pomocí silového pole molekulární mechaniky. Analýza tak obrovského množství dat je často náročná zejména pro molekuly s konformační heterogenitou, jako je neuspořádaný Abeta peptid relevantní pro Alzheimerovu chorobu (AD). Abeta peptid je charakteristickým znakem onemocnění a vyskytuje se v různých konformacích. Pochopení dynamických vlastností proteinu Abeta je klíčem k určení účinků potenciálních léků na léčbu Alzheimerovy choroby. Cílem této práce je navázat na nedávné pokroky ve strojovém učení z video sekvencí a vyvinout nové metody pro automatickou analýzu simulací molekulární dynamiky a obecněji pro proteinové inženýrství. Toto téma bude řešeno společně s Dr. Stanislavem Mazurenkem a prof. Jiřím Damborským (Loschmidt Laboratories, Masarykova univerzita).

Více informací:

• https://loschmidt.chemi.muni.cz/peg/
• http://impact.ciirc.cvut.cz
• https://ellis.ciirc.cvut.cz/4-students/

• S Mazurenko, Z Prokop, J Damborsky. Machine learning in enzyme engineering, In ACS Catalysis, 10 (2), 1210-1223, 2020.
• A Miech, D Zhukov, JB Alayrac, M Tapaswi, I Laptev, J Sivic, Howto100m: Learning a text-video embedding by watching hundred million narrated video clips, In Proceedings of the IEEE/CVF International Conference on Computer Vision and Pattern Recognition, 2019.
• J-B Alayrac, P Bojanowski, N Agrawal, J Sivic, I Laptev, S Lacoste-Julien, Learning from Narrated Instruction Videos, IEEE Transactions on Pattern Analysis and Machine Intelligence, 2017.
• A Mardt, L Pasquali, H Wu, F Noe, VAMPnets for deep learning of molecular kinetics. In Nature Communications, 9, 5, 2018.

Lidé řeší efektivně a bezpečně každodenní manipulační úlohy. Jen na základě několika málo interakcí se naučí používat nástroje, aniž by předem znali jejich přesné fyzikální vlastnosti nebo vlastnosti okolního prostředí. Příklady takových úloh je zatloukání hřebíků, odhrnování sněhu, hrabání listí nebo vrtání děr do různých materiálů. V současné době neexistuje inteligentní autonomní systém s podobnou úrovní vizuomotorických schopností.

Cílem této práce je vyvinout modely strojového učení založené na fyzické a geometrické struktuře okolního prostředí, které umožní bezpečné automatické učení vizuomotorických dovedností pro robotickou manipulaci v nových prostředích.

Více informací:

• http://impact.ciirc.cvut.cz/
• http://ellisprague.eu/4-students

• Z Li, J Sedlar, J Carpentier, I Laptev, N Mansard, J Sivic, Estimating 3D Motion and Forces of Person-Object Interactions From Monocular Video, IEEE Conference on Computer Vision and Pattern Recognition (CVPR) (2019).
• Y Labbe, S Zagoruyko, I Kalevatykh, I Laptev, J Carpentier, M Aubry, J Sivic, Monte-Carlo Tree Search for Efficient Visually Guided Rearrangement Planning, IEEE Robotics and Automation Letters (2020).
• Y Labbe, J Carpentier, M Aubry, J Sivic, CosyPose: Consistent multi-view multi-object 6D pose estimation, European Conference on Computer Vision (ECCV) (2020).

Vytvořit stroje, které rozumí komplexním obrazovým vstupům, je jeden ze základních problémů umělé inteligence s aplikacemi v autonomní robotice, automatické průmyslové výrobě nebo zdravotnictví. Je to ale obtížný problém, protože vizuální svět je složitý a proměnlivý. Nedávné úspěchy vizuálního rozpoznáváni jsou z velké části kombinací reprezentací založených na neuronových sítích, technik strojového učení a rozsáhlých manuálně anotovaných obrazových dat. Dalším zásadním otevřeným problémem je vývoj vizuálních reprezentací, které nevyžadují pro učení detailní anotace ve formě vstupů a cílových výstupů, ale jsou učitelné pouze ze slabých, zašuměných a jen částečných anotací. Tato práce bude tento otevřený problém řešit.

Více informací:

• http://impact.ciirc.cvut.cz/
• http://ellisprague.eu/4-students

• Alayrac, J.-B., Bojanowski, P., Agrawal, N., Laptev, I., Sivic, J. and Lacoste-Julien, S., Learning from narrated instruction videos IEEE Transactions on Pattern Analysis and Machine Intelligence, 40 (9), 2194-2208 (2018)

Složitost vyhledávacích systémů nové generace vychází z požadavku organizovat masivní a stále rostoucí objemy heterogenních dat a metadat spolu s potřebou poskytovat distribuovanou správu převážně založenou na podobnostním vyhledávání. Problém začíná získáváním slabě strukturovaných nebo zcela nestrukturovaných dat, jako jsou obrázky a video, pro které jsou nutně potřeba inovativní techniky pro extrakci a klasifikaci informací, aby se zvýšila jejich vyhledatelnost. Nalezitelnost objektu a vlastní proces vyhledávání v zásadě považujeme za dva zásadní a synergické aspekty vyhledávání. Oba představují výzvy v oblasti efektivity, které vyžadují inovativní teorie a technologie, a musí být studovány společně, aby se sblížily s kvalitativně novými vyhledávacími nástroji budoucnosti. Téma disertační práce má povahu základního výzkumu, protože se zabývá teoretickými limity vyhledávání podle podobnosti v kontextu problému velkých dat. Cílem práce je hledání a vývoj škálovatelných řešení.

Umělá inteligence a strojové učení stále více uplatňuje v reálných aplikacích a tím významně proniká do oblasti vestavných a zejména kyberfyzikálních systémů. Typickým příkladem je subsystém analýzy obrazu pro samořiditelná auta nebo inteligentní senzory. Na rozdíl od oblasti big data disponují tyto systémy omezeným výpočetním výkonem a mají vysokou variabilitu v architektuře hardwaru, a navíc jsou na tyto systémy kladeny další požadavky zejména na zpracování v reálném čase, bezpečnost a spolehlivost, explainability, spotřebu a velikost čipu. Z těchto hledisek musí být výsledná implementace optimalizována tak, aby minimalizovala hardwarové zdroje při zachování funkčnosti a spolehlivosti pro splnění ekonomických cílů. Automatizovaný převod modelů strojového učení například hlubokých neuronových sítí do hardwaru ASIC a zejména pak programovatelného (FPGA) je v současné době velmi aktuálním tématem.

Předmětem navrhovaného tématu je výzkum algoritmů, postupů, metodik a nástrojů pro syntézu modelů umělé inteligence a strojového učení do programovatelného hardwaru. Aktuální je výzkum v oblasti aproximativních výpočtů, optimalizace hardware s využitím omezené přesnosti cílené dle hodnot jednotlivých parametrů včetně dalších aspektů mapování na cílovou platformu (spotřeba, velikost čipu, časování). Předmětem výzkumu nebude jen prosté mapování naučeného modelu na hardware, ale i optimalizace AI modelu s ohledem na implementaci v hardwaru, což vyžaduje těsnější provázání nástrojů pro AI s nástroji pro vysokoúrovňovou a logickou syntézu. Téma je možné rozšířit na syntézu sítí se spiking modely neuronů a o integraci učících algoritmů do hardwaru, což se v současné době neřešená nebo málo řešená problematika.

• [1] Shubham Raif, et al. Logic Synthesis Meets Machine Learning: Trading Exactness for Generalization. arXiv:2012.02530v2 [cs.LG] 15 Dec 2020.
• [2] Chia-Chih Chi and Jie-Hong R. Jiang. Logic Synthesis of Binarized Neural Networks for Efficient Circuit Implementation. In IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN (ICCAD ’18), November 5–8, 2018, San Diego, CA, USA. ACM, New York, NY, USA, 7 pages. https://doi.org/10.1145/3240765.3240822
• [3] Yifan Qian, et al.: Approximate Logic Synthesis in the Loop for Designing Low-Power Neural Network Accelerator. 2021 IEEE International Symposium on Circuits and Systems (ISCAS) | 978-1-7281-9201-7/20/$31.00 ©2021 IEEE | DOI: 10.1109/ISCAS51556.2021.9401451

Optické sítě se sice primárně používají pro datové přenosy, ale v současné době poskytují i vhodnou a perspektivní platformu pro další aplikace včetně přenosu vysoce stabilní frekvence a přesného času z atomových hodin na vzdálenosti až tisíců kilometrů. Výhodou optické linky je, že umožňuje současný obousměrný přenos v tomtéž vlákně a tedy rušivé vlivy lze kompenzovat, neboť se uplatňují stejnou měrou v obou směrech. Používané metody přenosu času a frekvence pracují na různých síťových vrstvách, ty nejpřesnější z nich na linkové a fyzické vrstvě. Student se bude muset detailně seznámit s existujícími metodami, měřit a vyhodnotit jejich parametry. Výzkum bude zaměřen na návrh nových protokolů, způsobů kódování přenášené informace a modulace nosného signálu s cílem zlepšit přesnost a spolehlivost přenášeného času a frekvence. Jedná se o komplexní téma, které je interdisciplinární a pohybuje se na rozhraní počítačových sítí a programování obvodů FPGA s možným přesahem do návrhu elektronických obvodů a případně i opto-elektronických obvodů.

Mezi nekonečná slova generovaná morfismy patří jednak pevné body morfismů, slova vzniklá z S-adických systémů [1] a L-systémů [2]. Cílem práce je výzkum kombinatorických vlastnostní těchto struktur, jmenovitě například jejich faktorové/palindromické/abelovské komplexity a vlastností, které jsou zachovány v případě, že generující morfismy jsou rozpoznatelné. Možností je navíc zaměření na návrh relevantních efektivních algoritmů a/nebo formalizaci v generickém dokazovacím asistentu Isabelle/HOL [3].

• [1] Berthé, V., Delecroix, V.: Beyond substitutive dynamical systems: S-adic expansions, RIMS Lecture note ‘Kokyuroku Bessatu’ B46, pp. 81–123 (2014)
• [2] Rozenberg, G. Salomaa, A.: The Book of L, Springer Berlin Heidelberg, 1986
• [3] https://isabelle.in.tum.de/

Není pochyb o tom, že včasná diagnóza pacientů trpících nemocemi, jako je ischemická choroba srdeční a mrtvice nebo vážné případy infekce COVID-19, je nesmírně důležitá pro neodkladné zahájení léčby, případně odvrácení smrti. Z tohoto důvodu musí být moderní laboratoře schopné co nejrychleji analyzovat vzorek a poskytnout výsledek. Důležitým ukazatelem měřícím, jak rychle laboratoř dokáže vyhodnotit vzorek, je takzvaný TAT (Turn Around Time). Jeho hodnota je zásadně ovlivněna tím, jak jsou v procesu vzorky řazeny. Toto téma se zabývá rozvrhovacímy problémy, které se váží k procesu zpracování vzorků. Naše analýza laboratoří a rešerše odborné literatury ukázala, že tento problém doposud nebyl dostatečně studován, přičemž správné rozvrhování vzorků může výrazně snížit TAT prioritních vzorků pacientů.

Cílem této disertační práce je navrhnout nové matematické modely pro rozvrhování procesu vyhodnocování laboratorních vzorků a navrhnout efektivní optimalizační algoritmy kde prohledávání prostoru řešení je urychleno metodami strojového učení.

• [1] ATLAS Collaboration, "ATLAS Software and Computing HL-LHC Roadmap", https://cds.cern.ch/record/280291

V automatickém plánování je úkolem najít posloupnost akcí, které vedou ke splnění určitého cíle [1,2]. Plánování probíhá na abstraktní úrovni, kdy je plánovací prostředí, ve kterém se úloha odehrává, popsáno pomocí množin logických atomů. Akce postupně mění za splnění daných předpokladů prostředí pomocí množinových operací. Plánování pro robotické agenty představuje speciální případ plánování, kdy na rozdíl od obecného plánování, které v principu umožňuje akce měnící prostředí libovolně, je třeba uvažovat o topologii prostředí a vykonávání akcí jedním či více robotickými agenty. U robotických agentů přitom předpokládáme lokalizaci v rámci prostředí, tedy omezený dosah jejich efektorů, případnou nutnost přesunu na místo vykonání akce a obsazení prostoru jinými agenty [3,4]. Otevřenou otázkou je návrh centrálních algoritmů pro efektivní a robustní plánování uvažující jak jedno-robotický případ, tak více spolupracujících robotických agentů.

• [1] Malik Ghallab, Dana S. Nau, Paolo Traverso: Automated Planning and Acting. Cambridge University Press 2016, ISBN 978-1-107-03727-4
• [2] Malik Ghallab, Dana S. Nau, Paolo Traverso: Automated planning - theory and practice. Elsevier 2004, ISBN 978-1-55860-856-6, pp. I-XXVIII, 1-635
• [3] Ron Alterovitz, Sven Koenig, Maxim Likhachev: Robot Planning in the Real World: Research Challenges and Opportunities. AI Magazine 37(2): 76-84 (2016
• [4] Yawen Deng, Yiwen Hua, Nils Napp, Kirstin Petersen: A Compiler for Scalable Construction by the TERMES Robot Collective. Robotics Auton. Syst. 121 (2019)

V automatickém plánování je úkolem najít posloupnost akcí, které po jejich vykonání vedou ke splnění určitého cíle [1, 2]. Speciálně se toto téma zaměřuje na kompilaci plánovací úlohy do jiného formalismu, jako je například splňování omezení (CSP) [3] nebo výroková splnitelnost (SAT) [4]. Potenciál představuje zejména líná kompilace, kdy je úloha zakódována do cílového formalismu neúplně a ke zpřesnění jejího zakódování dochází až ve spolupráci s řešičem pomocí generování protipříkladů. Technika líné kompilace byla úspěšně použita ve speciální doméně multi-agentního hledání cest [5]. Zobecnění líné kompilace pro klasické plánování je ovšem stále otevřenou otázkou.

• [1] Malik Ghallab, Dana S. Nau, Paolo Traverso: Automated Planning and Acting. Cambridge University Press 2016, ISBN 978-1-107-03727-4
• [2] Malik Ghallab, Dana S. Nau, Paolo Traverso: Automated planning - theory and practice. Elsevier 2004, ISBN 978-1-55860-856-6, pp. I-XXVIII, 1-635
• [3] Rina Dechter: Constraint processing. Elsevier Morgan Kaufmann 2003, ISBN 978-1-55860-890-0
• [4] Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications 185, IOS Press 2009, ISBN 978-1-58603-929-5
• [5] Pavel Surynek: Unifying Search-based and Compilation-based Approaches to Multi-agent Path Finding through Satisfiability Modulo Theories. Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI 2019), pp. 1916-1922, Macau, China, International Joint Conferences on Artificial Intelligence, 2019, ISBN (Online): 978-0-9992411-4-1

Školitel-specialista: doc. Dipl.-Ing. Dr. techn. Stefan Ratschan

Multi-agentní hledání cest (MAPF) je problém výpočtu bezkolizních cest z daných výchozích pozic do cílových pozic pro sadu agentů [1,2]. Problém MAPF je motivován řadou reálných aplikací, agenty mohou například modelovat roboty pro přepravu zboží ve skladech. Tradiční řešení tohoto problému jsou založené na modelech, kde čas i prostor jsou diskrétní. Spojité modely by však byly realističtější. Současný stav poznání v této oblasti umožňuje agentům pohybovat se spojitě po lineárních trajektoriích [3,4]. Cílem této práce je přispět k obecnějším technikám, například umožnit agentům pohyb po nelineárních trajektoriích, nebo modelovat určité kinematické vlastnosti agentů, jako je zrychlení, či další vlastnosti, které se projevují ve spojitém modelu problému.

• [1] David Silver: Cooperative Pathfinding. AIIDE 2005: 117-122
• [2] Ko-Hsin Cindy Wang, Adi Botea: MAPP: a Scalable Multi-Agent Path Planning Algorithm with Tractability and Completeness Guarantees. J. Artif. Intell. Res. 42: 55-90 (2011)
• [3] Thayne T. Walker, Nathan R. Sturtevant, Ariel Felner: Extended Increasing Cost Tree Search for Non-Unit Cost Domains. IJCAI 2018: 534-540
• [4] Anton Andreychuk, Konstantin S. Yakovlev, Pavel Surynek, Dor Atzmon, Roni Stern: Multi-agent pathfinding with continuous time. Artif. Intell. 305: 103662 (2022)

Plánování pohybu v robotice představuje jeden z klíčových kroků k realizaci abstraktního plánu zadaného jako posloupnost akcí prostřednictvím fyzického působení robota v prostředí [1,2]. Pohybový plán pro každý spojitý časový okamžik určuje prostorové nastavení jednotlivých částí a efektorů robota tzv. konfiguraci. Techniky plánování pohybu zpravidla pracují se spojitým mnoha-dimenzionálním prostorem všech možných konfigurací robota, kde nalezení plánu pro pohyb odpovídá nalezení spojité trajektorie v konfiguračním prostoru [1,3]. Výzvu představuje zejména případ, kdy je plánován pohyb více robotů s potenciálem k prostorové kolizi, jelikož s rostoucím počtem robotů prudce narůstá dimenze spojeného konfiguračního prostoru a tím obtížnost nalezení nekolidujících trajektorií [4]. Zajímavou otázkou je rovněž vykonávání pohybu skutečnými roboty a reakce na případné selhání vykonávání u jednoho či více robotů.

• [1] M. LaValle, S.: Planning Algorithms. Cambridge University Press, 2006
• [2] Malik Ghallab, Dana S. Nau, Paolo Traverso: Automated Planning and Acting. Cambridge University Press 2016, ISBN 978-1-107-03727-4
• [3] Choset, H., Lynch, K. M., Hutchinson, S., Kantor, G., Burgard, W., Kavraki, L. E., Thrun, S.: Principles of Robot Motion: Theory, Algorithms, and Implementations. MIT Press, 2005
• [4] Duong Le, Erion Plaku: Cooperative, Dynamics-based, and Abstraction-Guided Multi-robot Motion Planning. J. Artif. Intell. Res. 63: 361-390 (2018)

Protipříklady řízené zpřesňování abstrakcí (counterexample guided abstraction refinement – CEGAR) je úspěšná technika v ověřování modelů [1,2]. V rámci navrhovaného tématu je úkolem prozkoumat možnosti použití techniky CEGAR v plánování pro mnoho robotů [3,4]. Plánování s mnoha roboty nabízí velký prostor pro návrh abstrakcí problému, které přinášejí vhodná zjednodušení a umožňují řešícímu systému problém snadněji vyřešit, například lze některé roboty v problému ignorovat, ovšem za cenu nepřesností ve výsledném řešení. Návrh, vyhledání a ověření protipříkladů pro multi-robotický systém, pomocí nichž by bylo možné nepřesnosti v řešení eliminovat, představuje další zajímavou výzvu. Určitého pokroku bylo dosaženo v plánování cest pro mnoho robotů, kde zpřesnění abstrakce probíhalo vůči srážkám mezi roboty. Abstrakce pro plánování cest ale představují pouze speciální případ, přičemž v rámci tohoto tématu bychom chtěli návrh abstrakcí posunout dál směrem k obecnějším multi-robotickým systémům, kde je škála činností robotů širší. Zajímavým směrem je i obohacení techniky CEGAR abstrakcemi, které produkují nepřesnost v řešení, vůči kterým je multi-robotický systém robustní, a není tedy třeba provádět jejich zpřesnění.

• [1] Edmund M. Clarke, Anubhav Gupta, Ofer Strichman: SAT-based counterexample-guided abstraction refinement. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 23(7): 1113-1123 (2004)
• [2] Anubhav Gupta, Edmund M. Clarke: Reconsidering CEGAR: Learning Good Abstractions without Refinement. ICCD 2005: 591-598
• [3] Teng Guo, Si Wei Feng, Jingjin Yu: Polynomial Time Near-Time-Optimal Multi-Robot Path Planning in Three Dimensions with Applications to Large-Scale UAV Coordination. IROS 2022: 10074-10080
• [4] Lydia E. Kavraki, Steven M. LaValle: Motion Planning. Springer Handbook of Robotics, 2nd Ed. 2016: 139-162

Výzkum v rámci tohoto tématu bude zaměřen na hledání řešení vybraných problémů v umělé inteligenci pomocí redukce na problém splnitelnosti [1]. Mezi problémy, které přestavují vhodné kandidáty pro tento způsob řešení, patří doménově závislé plánování (například hledání cest, plánování pro roboty) [2], rozvrhování, návrh obvodů, nebo kombinatorické úlohy. Pojem splnitelnost zde chápeme v širším smyslu, tj. nikoli pouze jako základní výrokovou splnitelnost (problém SAT), ale zahrnujeme i obecnější splňování podmínek (constraint satisfaction) [3], či kombinace splnitelnosti v různých logických teoriích (SAT-modulo theory – SMT) [4].

• [1] Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications 185, IOS Press 2009.
• [2] Pavel Surynek: Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems. Ann. Math. Artif. Intell. 81(3-4): pp. 329-375, 2017.
• [3] Francesca Rossi, Peter van Beek, Toby Walsh: Handbook of Constraint Programming. Foundations of Artificial Intelligence 2, Elsevier 2006.
• [4] Daniel Kroening, Ofer Strichman: Decision Procedures - An Algorithmic Point of View, Second Edition. Texts in Theoretical Computer Science. An EATCS Series, Springer 2016.

Cílem výzkumu je návrh nových konceptů a souvisejících řešících algoritmů pro multi-agentní hledání cest (Multi-Agent Path Finding) [1]. V základní variantě problému MAPF hledáme cesty pro agenty pohybující se po neorientovaném grafu tak, aby každý agent dorazil do svého cíle ze zadané počáteční pozice, a přitom se nesrazil s žádným jiným agentem. Současné řešící techniky pro MAPF zahrnují škálu metod od sub-optimálních polynomiálních algoritmů [2] přes optimální algoritmy založené na prohledávání stavového prostoru [3] po transformace do jiných formalismů jako je SAT [4]. Otevřené otázky nabízejí zejména zobecněné varianty problému MAPF, kde uvažujeme navíc například komplexnější vzájemné vyhýbání, udržování formací, souvislostí či jiných globálních vlastností (vlastnost, jež zahrnuje všechny agenty), zobecněné cenové funkce či více nezávislých (soupeřících) týmů agentů.

• [1] David Silver, “Cooperative pathfinding,” Proceedings of AIIDE, pp. 117–122, 2005.
• [2] Boris de Wilde, Adriaan ter Mors, Cees Witteveen: Push and Rotate: a Complete Multi-agent Pathfinding Algorithm. J. Artif. Intell. Res. 51: pp. 443-492, 2014.
• [3] Guni Sharon, Roni Stern, Meir Goldenberg, Ariel Felner: The increasing cost tree search for optimal multi-agent pathfinding. Artif. Intell. 195, pp. 470-495, 2013.
• [4] Pavel Surynek, Ariel Felner, Roni Stern, Eli Boyarski: Efficient SAT Approach to Multi-Agent Path Finding Under the Sum of Costs Objective. Proceedings of ECAI, pp. 810-818, 2016.

Školitel-specialista: Ing. Jan Fesl, Ph.D.

Typickými úlohami, které je třeba řešit ve vysokorychlostních počítačových sítích internetu, jsou řízení toku (flow control) a ochrana proti zahlcení (congestion control). Obě zmíněné úlohy řeší síťové protokoly různých vrstev modelu OSI/OSI.

Komunikační sítě datových center (DC) jsou v porovnání s internetem specifické svými podmínkami a z hlediska řízení toku či ochrany proti zahlcení se významně odlišují. Komunikačních linky mají vyšší rychlost a propustnost a vysoká spolehlivost. Především je ale v sítích DC oproti Internetu reálná možnost zpracovávat globálnější informace o stavu a vytíženosti komunikačních linek či síťových prvků (jejich výpočetních zdrojů), popř. možnost adaptivní rekonfigurace celé sítě DC dle aktuálních komunikačních požadavků.

V rámci dizertační práce analyzujte vlastnosti publikovaných algoritmů pro řízení toku a pro ochranu proti zahlcení v komunikačních sítích DC. Vytvořte realistický model komunikační sítě DC a pomocí něho prozkoumejte liḿitace těchto algoritmů. Vypracujte metodiku hodnocení kvality těchto algoritmů vycházející ze specifických požadavků na komunikační sítě DC. Na základě této analytické rešerše navrhněte dokonalejší adaptivní algoritmy pro řízení toku a pro ochranu proti zahlcení v sítích DC využívající globální informaci o síťovém provozu. Vaše návrhy algoritmů pak ověřujte testováním v rámci modelu a vyhodnoťte dle své metodiky jejich kvalitu.

Školitel-specialista: Ing. Jan Fesl, Ph.D.

Datová centra (DC) hrají díky narůstající důležitosti cloud computingu velkou roli v mnoha různých odvětvích, avšak jejich efektivní správa či optimální řízení představují netriviální algoritmické problémy. Významným příkladem je problém optimálního rozmístění virtuálních strojů (VM) (příp. kontejnerů) napříč virtualizačními uzly. Některé varianty tohoto problému lze formulovat jako vícerozměrný bin packing problém, který patří do skupiny NP-těžkých problémů, které lze přibližně řešit pomocí optimalizačních heuristik, jako jsou genetické algoritmy, tabu prohledávání, simulované žíhání, a pod. Problém lze i řešit převodem na jiný výpočetně ekvivalentní problém, např. SAT, kdy lze využít existující pokročilé řešiče.

Navrhněte metodiku pro nastavení různých optimalizačních kritérií, jako např. energetická náročnost běhu infrastruktury DC, zatížení sítě, latence komunikačních operací běžících aplikací, zaručení vysoké dostupnosti, atd. Zkonstruujte model DC pro simulaci a testování vlastností optimalizačních algoritmů pro rozmístění VM na virtualizační uzly DC. V tomto modelu analyzujte pomocí této metodiky vlastnosti existujících algoritmů pro řešení problému optimálního rozmístění VM na virtualizační uzly, identifikujte jejich nedostatky a navrhněte, validujte a vyhodnoťte nové algoritmy.

Školitel-specialista: Ing. Jan Fesl, Ph.D.

Klasické Intrusion Detection Systems (IDS) hrají v zabezpečení počítačových sítí či datových center již řadu let důležitou roli. V případě sítí s ultra-vysokým průtokem dat již klasický koncept IDS použít nelze kvůli jeho omezenému lokálnímu výpočetnímu výkonu. Jeden ze způsobů řešení jsou distribuované IDS (DIDS). Úkolem disertační práce bude studium algoritmů a metod, které budou využitelné jednak pro rozdělování zátěže mezi sondami síťového provozu a dále i pro samotnou analýzu síťového provozu v rámci konkrétního DIDS. Pro zvýšení účinnosti resp. pro zpřesňování úspěšnosti predikce konkrétní síťové aktivity se jeví jako perspektivní použití kolaborativního strojového učení, které svojí podstatou odpovídá konceptu DIDS.

Školitel-specialista: Ing. Jan Fesl, Ph.D.

Distribuované útoky typu DDOS (klasické či pomalé) představují velkou hrozbu jak v dnešním Internetu, tak i softwarově definovaných sítích či v cloudech. Účinnou obranou proti takovýmto útokům je jejich včasná a spolehlivá detekce, která je ovšem netriviální vzhledem k množství parametrů, které je třeba zohlednit. Tématem disertační práce je výzkum matematických modelů umožňujících návrh algoritmů pro detekci obou zmíněných typů DDOS útoků. Jako perspektivní se aktuálně jeví modely založené kombinaci strojového učení a tradičních analytických statistických metod, které umožňují rychlé předzpracování dat a tím dokáží podstatně zkrátit dobu pro učinění rozhodnutí, která je v případě DDOS útoků zcela zásadní.

Konfigurace efektivně fungujících počítačových sítí uspořádaných do složitých topologií je v dnešní době považována za netriviální problém. Nezřídka kdy se stává, že změna konfigurace konkrétního prvku v rámci počítačové sítě má vliv i na její další části (např. z hlediska dostupnosti, latence, kvality služeb, atd.). V době aktivace konfigurace však nemusí být její vliv ihned zřejmý a je tudíž vhodné možné účinky konfigurace nejprve verifikovat. Úkolem disertační práce je vývoj algoritmů a metod pro formální verifikaci stavu síťových prvků, které dokáží ještě před samotnou aktivací konfigurace upozornit na potenciální problém.

Školitel-specialista: Lasse Blaauwbroek, MSc.

Strojové učení pro interaktivní dokazování vět je téma, o které je rostoucí zájem. Je řada individuálních projektů, které v posledních letech zaznamenaly značný úspěch. Stále však zbývá mnoho práce, aby se strojové učení stalo prakticky užitečným. Jednou z překážek je, že většina projektů existuje v rámci svého individuálního sila a nelze je přímo porovnávat s ostatními. Tento problém se již řeší v širší oblasti strojového učení prostřednictvím iniciativ, jako je platforma OpenML [1, 2], která umožňuje vytvářet datové sady a odpovídající úlohy a nahrávat je na platformu. Po nahrání datové sady a úlohy může kdokoli vytvořit a nahrát modely, které se pokusí úlohu vyřešit. Platforma pak automaticky vyhodnotí a porovná všechny odeslané modely a vytvoří interaktivní vizualizace, které zdůrazní relativní silné a slabé stránky modelů. Kolaborativní platformy přinášejí značné výhody, z nichž nejdůležitější je možnost snadno porovnávat různé modely učení prostřednictvím spravedlivých a konzistentních srovnávacích testů, které reprezentují reálné podmínky. V současné době si každý projekt strojového učení vyvíjí vlastní techniku hodnocení, z nichž mnohé nereprezentují reálné podmínky. Výzkumy v oblasti spolupráce člověka s počítačem navíc ukázaly, že "gamifikace" obtížných problémů výrazně napomáhá kompetitivnímu zapojení komunity [3]. Bohužel data, metody vyhodnocování a modely spojené s dokazováním vět jsou příliš složité na to, aby se vešly do obecného rámce iniciativ, jako je OpenML. Proto vyvineme speciální platformu pro interaktivní dokazování vět. Předchozí pokusy o vývoj centrálizované platformy pro dokazování tvrzení [4, 5, 14] se příliš neujaly kvůli absenci interaktivní složky. Poskytují jedinou statickou sadu dat a kód k provedení vyhodnocení, ale chybí jim možnost automaticky, spravedlivě a interaktivně porovnávat různé modely. Tato práce je na pomezí několika témat, včetně strojového učení, dokazování vět, interakce člověka s počítačem, webových technologií a počítačového inženýrství. Vývoj úspěšné platformy zahrnuje různé výzkumné úhly pohledu a různé technické komponenty.

Více informací:

• DocsGoogle

Školitel-specialista: RNDr. Martin Suda, Ph.D.

Cílem automatizovaného dokazování tvrzení je automatizace matematicky přesného deduktivního usuzování s aplikacemi ve formální verifikaci kritických bezpečnostních systémů nebo ve formalizaci matematiky. Výzkum praktických automatických dokazovačů kombinuje vývoj logických kalkulů s jejich efektivní implementací a empirickým vyhodnocením na relevantních množinách problémů. Neméně důležitou roli hrají účinné heuristiky, které pomáhají řídit hledání důkazu. Nedávné pokroky v umělé inteligenci, zejména strojové učení a neuronové sítě, umožňují automatické objevování takových heuristik, a to buď na základě předchozích zkušeností s dokazováním, nebo v rámci zpětnovazebního učení (reinforcement learning). Cílem práce bude posunout stav poznání v této oblasti a vyvinout nové metody pro automatické objevování heuristik pro hledání důkazů.

Školitel-specialista: Dr. Adam Pease

Budete trénovat moderní jazykové modely, které budou překládat výroky přirozeného jazyka, jako například "Šálek je na stole", na výroky formální logiky. Ty budou nakonec použity dnešními automatizovanými dokazovači vět (ATP), jako jsou Vampire a E prover, k odvození závěrů z těchto výroků. V tomto výzkumu budeme používat jazyk a formální ontologii SUMO (https://www.ontologyportal.org/). Například předchozí výrok bude v SUMO vypadat následovně:

(exists (?X ?Y)
   (a
      (instance ?X Table)
      (instance ?Y Cup)
      (orientace ?Y ?X On)))

Jazykový překlad bude doplněn sémantickými nástroji, jako je např. syntaktická a sémantická kontrola v SUMO. Dále budou vyvinuty metody rozšiřování dat s cílem zvětšit velikost trénovacího korpusu pro NLP metody. To zahrnuje například generování syntetických dat pomocí tzv. logic-to-language překladače SUMO, přímého překladu do různých přirozených jazyků a generování tranzitivních dat prostřednictvím NLP metod, jako je překladač Google Translate. Konečným cílem je automatické obohacování znalostní báze SUMO o velké množství comon-sense faktů vyjádřených v přirozeném jazyce. To následně umožní automatizované uvažování o rostoucím množství každodenních témat.

Infrastruktury systémů, které dnes zahrnují operační systémy, síťové komunikační prvky, webové servery, prvky pro vyvažování zátěže, aplikační servery, atd. produkují během provozu systémů obrovské množství provozních dat. Výzkum v oblasti datových věd využívající provozní data má za cíl vylepšit metody strojového učení k lepšímu rozpoznání různých vzorů chování systémů, korelací a podobností mezi daty za účelem vylepšit správu systémů ale i jejich změny v návrhu nebo analýzu důvodů vzniku incidentů. Tyto úkoly zahrnují predikci chování a simulaci systémů při vzniku plánovaných i neplánovaných událostí jako jsou např. výpadky spojení, chyby serverů nebo nárůst pracovní zátěže systémů. Tento výzkum vylepší metody učení známé jako “supervised” a “unsupervised” learning přizpůsobené pro podmínky provozu systémů a bude zahrnovat širokou škálu metod pro klasifikaci, clusterování nebo regresi.

Jádra monolitických operačních systémů jsou v současnosti pravděpodobně nejsložitější centralizované programy, které podstupují proces neustáleho vývoje a ladění jak funkčnosti tak výkonnosti. Mají architekturu řádově stovek modulů. V současné době je k dispozici řadu nástrojů pro diagnostiku funkcionality a výkonnosti těchto jader, ale úroveň využitelnosti výstupů těchto nástrojů pro efektivní ladění jader je výrazně závislá na lidském faktoru, na vyspělosti a zkušenosti týmu vývojářů.

Cílem dizertační práce je výzkum metod automatického zjišťování příčin výkonnostních problémů jádra operačního systému a škálovatelnosti jader pro víceprocesorové počítačové systémy. Prozkoumejte, které známé techniky umělé inteligenne a strojového učení lze využít pro automatizaci těchto metod.