|
|
GPU-Accelerated Synthesis of Probabilistic Programs
Marcin, Vladimír ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
This paper examines the problem of automatic synthesis of probabilistic programs: having a finite family of candidate programs, how can one efficiently identify a program that satisfies a given specification. Even the most straightforward synthesis problems prove to be NP-hard. An improvement to this state of practice is brought by the PAYNT tool, which tackles this problem with a novel integrated technique for synthesising probabilistic programs. Even though it efficiently deals with the exponential growth of the family size, there is still a problem with the underlying state-space explosion. To solve this problem, we have implemented GPU-oriented model-checking algorithms that takes advantage of the GPU architecture and parallelise the task at a state level of a probabilistic model. The overall acceleration that we were able to achieve with this approach was, under certain conditions, close to the theoretically possible limit of the acceleration of the whole synthesis process.
|
|
|
Improving Robustness of Neural Networks against Adversarial Examples
Gaňo, Martin ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
This work discusses adversarial attacks to image classifier neural network models. Our goal is to summarize and demonstrate adversarial methods to show that they pose a serious issue in machine learning. The important contribution of this work is the implementation of a tool for training a robust model against adversarial examples. Our approach is to minimize maximization the loss function of the target model. Related work and our own experiments leads us to use Projected gradient descent as a target attack, therefore, we train against data generated by Projected gradient descent. As a result using the framework, we can achieve accuracy more than 90% against sophisticated adversarial attacks.
|
|
|
Využití přibližné ekvivalence při návrhu přibližných obvodů
Matyáš, Jiří ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
Tato práce je zaměřena na využití formálně verifikačních technik pro návrh funkčních aproximací kombinačních obvodů. Jsou zde důkladně prostudovány existující formální přístupy pro zkoumání přibližné ekvivalence a jejich použití při vývoji aproximovaných obvodů. V rámci této práce je navržena nová metoda, která integruje vybrané formální techniky do Kartézského genetického programování. Klíčovým bodem nového přístupu je využití prohledávací strategie, která vede evoluci směrem k řešením, která lze rychleji verifikovat. Navržený algoritmus byl implementován v rámci syntézního nástroje ABC. Jeho výkonnost byla otestována na vývoji funkčních aproximací násobiček a sčítaček s šířkami vstupních operandů 32, respektive 128 bitů. Dosažené výsledky ukazují výjimečnou škálovatelnost navržené metody.
|
|
|
Optimální rozvrhovací systém pro outdoorové aktivity
Rykala, Kryštof ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
Práce se zabývá technologiemi a přístupy pro vytvoření informačního systému, jehož součástí a motivací je automatické plánování rozvrhu aktivit. Za pomocí smíšeného celočíselného lineárního programování je definován model optimalizačního problému plánování se zdroji a omezeními. Součástí práce jsou programy klientské, serverové a plánovací části, které dohromady tvoří systém pro správu outdoorového centra s podporou automatického plánování.
|
|
|
Generování protipříkladů při analýze Markovových modelů
Molek, Martin ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
Tato práce se zabývá generováním protipříkladů v kontextu verifikace pravděpodobnostních systémů. Protipříklady jsou generovány nad Markovovými modely (přesněji DTMC). Specifikace vlastností modelu jsou zadávány pomocí logiky PCTL, která je v této práci popsána. Pro generování protipříkladů byly použity dva různé algoritmy (Best-first search a Recursive Enumration Algorithm). Práce obsahuje popis implementace algoritmů do verifikačního nástroje STORM. Výsledky experimentů ukazují, že REA je schopen pracovat s modely obsahující miliony stavů.
|
|
|
Překladač jazyka VHDL pro potřeby formální verifikace
Matyáš, Jiří ; Smrčka, Aleš (oponent) ; Charvát, Lukáš (vedoucí práce)
Cílem této bakalářské práce je navrhnout a implementovat překladač, který umožňuje převod popisu hardware z jazyka VHDL do grafové reprezentace v jazyce VAM (Variable Assignment Language). Program je určen pro potřeby formální verifikace výzkumné skupiny VeriFIT Fakulty informačních technologií VUT Brno. Důvodem vypracování této práce je poskytnutí možnosti formálně verifikovat návrh hardware s využitím vysokoúrovňových návrhových jazyků, jakým je například jazyk VHDL.
|
|
|
Online plánování nejvýhodnější trasy s využitím open-source aplikací
Matyáš, Jiří ; Schneider, Michal (vedoucí práce) ; Brůha, Lukáš (oponent)
Cílem této práce je vytvoření webové mapové aplikace pro plánování nejvýhodnější trasy při využití open-source nástrojů. Na začátku práce jsou použité nástroje stručně představeny a následuje popis postupu tvorby samotné aplikace. Práce popisuje způsob získání, úpravy i uložení dat použitých pro hledání trasy. Popsán je i postup použitý při tvorbě samotné webové mapové aplikace. Pro uložení dat byl použit databázový systém PostgreSQL a jeho extenze PostGIS. Vyhledání trasy zajišťuje knihovna pgRouting a vizualizace výsedků nad mapou OpenStreetMap je realizována pomocí knihovny OpenLayers. Při tvorbě aplikace byly použity skriptovací jazyky PHP a Javascript.
|
|
|
Zjišťování mokrého sněhu z radarových dat
Matyáš, Jiří ; Kolář, Jan (vedoucí práce) ; Součková, Jana (oponent)
Zjišťování mokrého sněhu z radarových dat Abstrakt Tato práce se zaměřuje na existující metodu pro získávání informací o sněhové pokrývce z družicových radarových dat. Zkoumaná metoda byla navržena Malnesem a Guneriussenem (2002) a je schopná provést subpixelovou klasifikaci mokrého sněhu, a také klasifikovat pixely se suchým sněhem. Klasifikace je založená na detekci změn, takže je potřeba referenční snímek bez sněhové pokrývky. V průběhu zpracování byly v algoritmu objeveny některé nedostatky, které jsou v práci diskutovány, a zároveň je navrženo možné řešení. Navrhnul jsem také modifikaci tohoto algoritmu, která by mohla přispět ke zlepšení jeho přesnosti. Modifikovaný algoritmus jsem pak otestoval. Klíčová slova: SAR, sněhová pokrývka, dálkový průzkum Země, mokrý sníh
|
|
|
GPU-Accelerated Synthesis of Probabilistic Programs
Marcin, Vladimír ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
This paper examines the problem of automatic synthesis of probabilistic programs: having a finite family of candidate programs, how can one efficiently identify a program that satisfies a given specification. Even the most straightforward synthesis problems prove to be NP-hard. An improvement to this state of practice is brought by the PAYNT tool, which tackles this problem with a novel integrated technique for synthesising probabilistic programs. Even though it efficiently deals with the exponential growth of the family size, there is still a problem with the underlying state-space explosion. To solve this problem, we have implemented GPU-oriented model-checking algorithms that takes advantage of the GPU architecture and parallelise the task at a state level of a probabilistic model. The overall acceleration that we were able to achieve with this approach was, under certain conditions, close to the theoretically possible limit of the acceleration of the whole synthesis process.
|
|
|
Improving Robustness of Neural Networks against Adversarial Examples
Gaňo, Martin ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
This work discusses adversarial attacks to image classifier neural network models. Our goal is to summarize and demonstrate adversarial methods to show that they pose a serious issue in machine learning. The important contribution of this work is the implementation of a tool for training a robust model against adversarial examples. Our approach is to minimize maximization the loss function of the target model. Related work and our own experiments leads us to use Projected gradient descent as a target attack, therefore, we train against data generated by Projected gradient descent. As a result using the framework, we can achieve accuracy more than 90% against sophisticated adversarial attacks.
|
host ::
RSS.