|
|
GPU-Accelerated Synthesis of Probabilistic Programs
Marcin, Vladimír ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
V tejto práci sa zoberáme problémom automatizovanej syntézy pravdepodobnostných programov: majme konečnú rodinu kandidátnych programov, v ktorej chceme efektívne identifikovať program spĺňajúci danú špecifikáciu. Aj riešenie tých najjednoduchších syntéznych problémov v praxi predstavuje NP-ťažký problém. Pokrok v tejto oblasti prináša nástroj Paynt, ktorý na riešenie tohto problému používa novú integrovanú metódu syntézy pravdepodobnostných programov. Aj keď sa tento prístup dokáže efektívne vysporiadať s exponenciálnym rastom rodín kandidátnych riešení, stále tu existuje problém spôsobený exponenciálnym rastom jednotlivých členov týchto rodín. S cieľom vysporiadať sa aj s týmto problémom, sme implementovali GPU orientované algoritmy slúžiace na overovanie kandidátnych programov (modelov), ktoré danú úlohu paralelizujú na stavovej úrovni pravdepodobnostých modelov. Celkové zrýchlenie doshiahnuté týmto prístupom za určitých podmienok potom prinieslo takmer teoretický limit možného zrýchlenia syntézneho procesu.
|
|
|
Improving Robustness of Neural Networks against Adversarial Examples
Gaňo, Martin ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
Tato práce pojednává o kontradiktorních útocích na klasifikační modely neuronových sítí. Naším cílem je shrnout a demonstrovat kontradiktorní metody a ukázat, že představují vážný problém v strojovém učení. Důležitým přínosem této práce je implementace nástroje pro trénink robustního modelu na základě kontradiktorních příkladů. Náš přístup spočívá v minimalizaci maximalizace chybové funkce cílového modelu. Související práce a naše vlastní experimenty nás vedou k použití Projektovaného gradientního sestupu jako cílového útoku, proto trénujeme proti datům generovaným Projektovaným gradientním sestupem. Výsledkem použití nástroje je, že můžeme dosáhnout přesnosti více než 90% proti sofistikovaným nepřátelským útokům.
|
|
|
Employing Approximate Equivalence for Design of Approximate Circuits
Matyáš, Jiří ; Lengál, Ondřej (referee) ; Češka, Milan (advisor)
This thesis is concerned with the utilization of formal verification techniques in the design of the functional approximations of combinational circuits. We thoroughly study the existing formal approaches for the approximate equivalence checking and their utilization in the approximate circuit development. We present a new method that integrates the formal techniques into the Cartesian Genetic Programming. The key idea of our approach is to employ a new search strategy that drives the evolution towards promptly verifiable candidate solutions. The proposed method was implemented within ABC synthesis tool. Various parameters of the search strategy were examined and the algorithm's performance was evaluated on the functional approximations of multipliers and adders with operand widths up to 32 and 128 bits respectively. Achieved results show an unprecedented scalability of our approach.
|
|
|
Optimal Scheduling Systems for Outdoor Activity
Rykala, Kryštof ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
The thesis discusses technologies and approaches for implementation of information system. Its part and motivation is automatic scheduling of activities. A model for resource-contraint project scheduling is defined using mixed-integer linear programming. Part of this thesis are client, server and planning programs that form a system for management of an outdoor center with automatic scheduling of activities.
|
|
|
Counter-Example Generation in the Analysis of Markov Models
Molek, Martin ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
This thesis deals with generating counterexamples in context of probabilistic models. Counterexamples are generated for Markov models (specifically DTMC). Definitions of model properties are given by logic PCTL. Two algorithms (Best-first search and Recursive Enumration Algorithm) are used to generate these counterexamples. Thesis describes implementation of algorithms into verification tool STORM. The results of experiments show that REA is capable of handling models containg millions of states.
|
|
|
A VHDL Parser for Formal Verification
Matyáš, Jiří ; Smrčka, Aleš (referee) ; Charvát, Lukáš (advisor)
The principal goal of this bachelor thesis is to design and implement a parser of VHDL language into graph representation in VAM (Variable Assignment Language). The application is developed for formal verification purposes of VeriFIT research group of the Faculty of Information Technology, Brno University of Technology. The development of the compiler described in this thesis should provide the opportunity to use formal verification techniques to verify hardware designs described in high level design languages, such as VHDL.
|
|
|
Online route planning with open-source applications
Matyáš, Jiří ; Schneider, Michal (advisor) ; Brůha, Lukáš (referee)
The goal of this work is to create a route planning web application while using open source tools and applications. In the beginning, tools used to produce such application are briefly introduced. The the process of creating the application is described. This paper describes the proces sof getting, editing and storing data used for route planning. The proces sof creating the web mapping application itself is described, too. Data have been stored using PostgreSQL database system and its extension PostGIS. Route planning is realized using pgRouting library and the resulting route is displayed using OpenLayers library and OpenStreetMap as a base map. The application has been created using PHP and Javascript.
|
|
|
Using SAR data for wet snow monitoring
Matyáš, Jiří ; Kolář, Jan (advisor) ; Součková, Jana (referee)
Using SAR data for wet snow monitoring Abstract This paper focuses on an existing method of snow information retrieval by means of satellite SAR data. The method was first presented by Malnes and Guneriussen (2002), and has been proven to be capable of sub-pixel classification of wet snow. It is also able to classify dry snow pixels. The classification is based on change detection, so a snow-free reference image is required. Some flaws in this algorithm have been discovered during the work on this paper and are discussed, as well as a possible solution is suggested. I have also proposed a modification of the algorithm which could improve the classification results and tested the modified algorithm. Keywords: SAR, snow cover, remote sensing, wet snow
|
|
|
GPU-Accelerated Synthesis of Probabilistic Programs
Marcin, Vladimír ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
V tejto práci sa zoberáme problémom automatizovanej syntézy pravdepodobnostných programov: majme konečnú rodinu kandidátnych programov, v ktorej chceme efektívne identifikovať program spĺňajúci danú špecifikáciu. Aj riešenie tých najjednoduchších syntéznych problémov v praxi predstavuje NP-ťažký problém. Pokrok v tejto oblasti prináša nástroj Paynt, ktorý na riešenie tohto problému používa novú integrovanú metódu syntézy pravdepodobnostných programov. Aj keď sa tento prístup dokáže efektívne vysporiadať s exponenciálnym rastom rodín kandidátnych riešení, stále tu existuje problém spôsobený exponenciálnym rastom jednotlivých členov týchto rodín. S cieľom vysporiadať sa aj s týmto problémom, sme implementovali GPU orientované algoritmy slúžiace na overovanie kandidátnych programov (modelov), ktoré danú úlohu paralelizujú na stavovej úrovni pravdepodobnostých modelov. Celkové zrýchlenie doshiahnuté týmto prístupom za určitých podmienok potom prinieslo takmer teoretický limit možného zrýchlenia syntézneho procesu.
|
|
|
Improving Robustness of Neural Networks against Adversarial Examples
Gaňo, Martin ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
Tato práce pojednává o kontradiktorních útocích na klasifikační modely neuronových sítí. Naším cílem je shrnout a demonstrovat kontradiktorní metody a ukázat, že představují vážný problém v strojovém učení. Důležitým přínosem této práce je implementace nástroje pro trénink robustního modelu na základě kontradiktorních příkladů. Náš přístup spočívá v minimalizaci maximalizace chybové funkce cílového modelu. Související práce a naše vlastní experimenty nás vedou k použití Projektovaného gradientního sestupu jako cílového útoku, proto trénujeme proti datům generovaným Projektovaným gradientním sestupem. Výsledkem použití nástroje je, že můžeme dosáhnout přesnosti více než 90% proti sofistikovaným nepřátelským útokům.
|
guest ::
RSS feed.