|
|
Neurální extrakce řeči cílového řečníka
Žmolíková, Kateřina ; Erdogan, Hakan (oponent) ; Koldovský, Zbyněk (oponent) ; Černocký, Jan (vedoucí práce)
S rostoucím nasazením řečových technologií v praxi roste důležitost jejich robustnosti. Zejména zpracování řeči poškozené rušícími překrývajícími se řečníky je stále výzva. Přístupy separace řeči tento problém řeší rozkladem smíchané řeči na signály jednotlivých řečníků. Tyto metody v nedávné době výrazně pokročily s využitím vývoje v hlubokém učení. Ve spoustě aplikací, jako jsou chytré telefony nebo digitální domácí asistenti, je cílem zvýraznit řečový signál jednoho cílového řečníka, a potlačit ostatní řečníky a šum. V~této práci formulujeme tento problém jako extrakci řeči cílového řečníka a navrhujeme přímé řešení --- použití neuronové sítě, která na vstupu přijímá předregistrovanou nahrávku cílového řečníka a pozorovanou směs, a na výstupu vrací extrahovanou řeč cílového řečníka. Diskutujeme a experimentálně ukazujeme výhody tohoto přístupu ve srovnání s konvenční separací řeči. Výhody zahrnují nepotřebnost počítání řečníku ve směsi nebo lepší konzistenci výstupu pro delší nahrávky. Zkoumáme různé aspekty neurální extrakce řeči cílového řečníka, jako jsou embeddingy reprezentující řečníka, metody jak informovat neuronovou síť, vstupní a výstupní doména a ztrátová funkce. Dále demonstrujeme, jak kombinovat extrakci cílového řečníka s multi-kanálovými metodami, jako je beamforming založený na neurálních maskách nebo prostorové shlukování. Tyto kombinace využívají jak konvenčních statistických metod pro zpracování prostorové informace, tak silné modelovací schopnosti neuronových sítí. Na závěr aplikujeme extrakci řeči cílového řečníka na dva finální úkoly: automatické rozpoznávání řeči a diarizaci založenou na shlukování. Zkoumáme jak nejlépe zkombinovat předzpracování signálu s cílovými systémy včetně společné optimalizace, nebo trénování se slabou supervizí založenou na informaci o řečnících.
|
|
|
Reimplementace nástroje Combine
Vráblik, Matúš ; Rogalewicz, Adam (oponent) ; Smrčka, Aleš (vedoucí práce)
Cílem bakalářské práce je pochopení kombinačního testování, algoritmu IPOG na tvorbu kombinačních testů, jeho rozšíření o obmedzení hodnot parametrů a prototypovou implementaci v nástroji Combine vyvíjeném na FIT VUT. Následne analyzovat slabiny současné implementace, navrhnout reimplemetaci a také nástroj reimplementovat, porovnat s původní verzí a vyhodnotit novou verzi nástroje Combine.
|
|
|
Biology-inspired control of a walking robot
Žák, Marek ; Musílek, Petr (oponent) ; Ondráček, Tomáš (oponent) ; Zbořil, František (vedoucí práce)
Mobile robots have become part of everyday life. Various robots can perform a wide range of different tasks or go to places humans cannot. Their use can be found in rescue operations or in the exploration of remote or hard to reach places on Earth or in space. Walking robots form a separate category of mobile robots due to their unique features. They can negotiate rough terrain, can overcome various obstacles or use their legs to manipulate objects. Although walking robots are well suited to navigate rugged terrain, a number of factors have so far prevented their mass deployment. Their movement is relatively slow and energetically demanding, they have a limited payload, and their design is significantly more complex compared to wheeled or tracked robots. Walking robots often have dozens of joints and their control is therefore very complicated. This thesis describes a new bio-inspired hexapod robot WHexaR (Wheeled Hexapod Robot) and its controller that I designed and implemented as part of this work. The resulting robot is capable of energy-efficient movement in rugged terrain. The leg structure of the robot is inspired by the structure of an insect limb. The robot adapts its movement to the surrounding terrain. A special trochanter joint allows the entire leg of the robot to rotate parallel to gravitational acceleration, which reduces the energy consumption, increases the robot's stability and allows the robot to overcome steep hills. For movement on flat terrain, the robot is equipped with steerable wheels that allow the robot to achieve higher speeds with lower energy consumption than when using gait. The innovative biology-inspired robot controller is equipped with reflexes observed in insects that make the robot more efficient when travelling in rough terrain and improve its ability to overcome obstacles. A series of experiments were conducted to demonstrate the robot's ability to navigate rugged and sloping terrain.
|
|
|
Počítač jako inteligentní spoluhráč ve slovně-asociační hře Krycí jména
Chovancová, Kateřina ; Dočekal, Martin (oponent) ; Smrž, Pavel (vedoucí práce)
Tato práce rozšiřuje systém pro určování sémantické podobnosti slov a vytvářením slov ních asociací. K tomu je v práci využit prediktivní model fastText v kombinaci s metodou DETECT, a model založený na výpočtu Pointwise Mutual Information. Metoda DETECT využívá model Dict2vec, který je trénován na slovníkových definicích pojmů. Výsledný systém je schopen zastoupit hráče při hraní slovně asociační hry Krycí jména, a to jak na pozici člena operativy, tak v roli hlavního špiona. Zároveň byl v rámci práce vyvinut nástroj pro vytváření testů sémantické kontroly a znalosti, který pracuje se slovníkem českých synonym a slouží k výpočtu hodnoty TDS a určení četnosti výskytu slov. Poslední část práce se věnuje anlýze dat ze studie STST II., ve které bylo zkoumáno vzájemné myšlenkové napojení hráčů při hraní komunikační hry.
|
|
|
Využití formálních metod v přibližném počítání
Matyáš, Jiří ; Kubátová, Hana (oponent) ; Kumar, Akash (oponent) ; Pozzi, Laura (oponent) ; Češka, Milan (vedoucí práce)
V minulosti se výkon počítačových systémů zvyšoval hlavně díky tzv. Mooreovu zákonu - každé dva roky se počet transistorů na čipu přibližně zdvojnásobí. V současné době tento zákon přestává platit a tak se objevují a vyvíjí nové alternativní výpočetní přístupy, které mají za úkol zrychlit a zefektivnit výpočetní systémy. Jedním z těchto přístupů je tzv. aproximované počítání, které se snaží urychlit a zefektivnit výpočty za cenu přijatelných nepřesností ve výsledcích. Tento přístup je aplikovatelný hlavně v oblastech, které jsou přirozeně odolné vůči chybám - např. neuronové sítě nebo zpracování multimédií. Techniky pro aproximované počítání se postupně vyvinuly na všech úrovních výpočetních systémů. V rámci této práce se zaměřujeme na prohledávací algoritmy pro přibližný návrh hardwarových aritmetických obvodů. Aproximace aritmetických obvodů má velký potenciál, protože tyto obvody slouží jako základní stavební kameny větších systémů. Automatizované prohledávací aproximační algoritmy často pracují iterativně. V každé iteraci se nejprve vytvoří kandidátní aproximovaná řešení (pomocí komponenty zvané syntetizér), a poté se vyhodnotí jejich chyba vzhledem ke správnému řešení (komponenta analyzátor). Pro získání kvalitních aproximovaných obvodů musí prohledávací algoritmy vykonat velké množství těchto iterací. Proto je nutná vysoká efektivita syntetizéru i analyzátoru. Abychom zvýšili výkonnost těchto komponent, zapojujeme do prohledávacího algoritmu založeném na Kartézském genetickém programování (CGP) metody formální verifikace. Analyzátor je akcelerován za použití speciálního obvodu zvaného aproximační miter, který nám umožňuje převést vyhodnocení chyby obvodu na rozhodovací problém a tento problém vyřešit pomocí nástrojů zvaných SAT solvery. Další zrychlení aproximačního algoritmu přináší nově navržená strategie, která uvaluje limit na prostředky, které může SAT solver využít při vyhodnocování chyby kandidátních řešení. Díky tomuto limitu je evoluční algoritmus motivován hledat rychle verifikovatelná řešení. Výsledkem je větší množství iterací prohledávacího algoritmu a tím pádem také vyšší kvalita výsledných aproximovaných obvodů. Použitý evoluční algoritmus se může během aproximace "zaseknout" v tzv. lokálních optimech. Navržené vylepšení syntetizéru integruje CGP a optimalizaci pod-obvodů využívající SAT solver umožňuje evolučnímu algoritmu uniknout z lokálních optim. Díky tomu může algoritmus dále zlepšovat řešení i v případech, v nichž by se původní varianta CGP již dále nezlepšila. Dalším navrženým vylepšením syntetizéru je nový mutační operátor pro CGP, vytvořený speciálně pro co nejefektivnější aproximaci obvodů. Výsledky prezentované v rámci této dizertační práce výrazně vylepšují výkonnost prohledávacích algoritmů pro aproximaci aritmetických obvodů. Díky tomu můžeme získat aproximace obvodů velkých bitových šířek se složitou vnitřní strukturou (např. 32bitové násobičky nebo 128bitové sčítačky), které poskytují doposud nejlepší známý poměr mezi aproximační chybou a spotřebou elektrické energie.
|
|
|
Automata with Counting in Regular Expression Matching
Holíková, Lenka ; Meyer, Roland (oponent) ; Masopust, Tomáš (oponent) ; Holík, Lukáš (vedoucí práce)
Matching of regular expressions (regexes) is widely used, e.g., for searching, data validation, parsing, finding and replacing, data scraping, or syntax highlighting in many programming languages. It is a computationally intensive process often applied on large texts. Predictability of its efficiency has a significant impact on the overall usability of software applications in practice. A problem is that standard approaches for regex matching suffer from high worst case complexity. An unlucky combination of a regex and text may increase the matching time by orders of magnitude. This can be a doorway for the so-called Regular expression Denial of Service (ReDoS) attack in which the attacker causes a denial of service by providing a specially crafted regex or text. Automata-based matchers are the most efficient regex matching engines used nowadays in practice, especially in performance-critical industrial applications. There are years of empirical evidence showing that their performance is much more stable than that of the more traditional backtracking-based matchers. But automata matchers may run into troubles too. Bounded repetition, i.e., expressions such as [ab]{100} with a specified number of repetitions of a certain pattern, has been recognised as a major source of problems for even the fastest matchers. This thesis studies this issue systematically. In this thesis, we present a large-scale study of vulnerability of automata-based matching focused on bounded repetition. To this end, we propose a new ReDoS generator. It is the first generator capable of utilising bounded repetition to attack automata-based matchers, in fact the first generator that can attack them at all. We were then able to prove experimentally that bounded repetition indeed poses a serious security threat, for automata-based as well as backtracking-based matchers.We then propose a solution to the problem of efficient matching of regexes with bounded repetition. The approach is to compile the regexes into nondeterministic counting automata (CAs) and then to determinise them. The main problem is to find a succinct deterministic representation that can perform fast matching (naive determinisation builds a deterministic finite automata (DFAs) exponentially large to the size of the regex and of the repetition bounds in it). In the first step, we propose a determinisation algorithm based on general subset construction that generates deterministic CAs. They are exponentially more succinct than the corresponding DFAs. The main contribution of this thesis was then obtained when we elaborated the determinisation using the idea representing many counters with counting sets. We propose succinct transformation of a CA into a deterministic counting-set automaton (CsA), an automaton with a special type of registers that can hold a set of integer values. We also propose a novel compilation of regexes to CAs that generalizes the Antimirov's derivative construction. We design a framework for matching based on CsA simulation and the Antimirov's derivative construction. We compare the speed of matching of individual matching engines on a comprehensive set of real-world regexes with bounded repetition. We found that our algorithm is much more robust, outperforms the state-of-the-art matchers on regexes with bounded repetition, and is not dependent on the size of repetition bounds. It easily solves most cases in which the existing matchers struggle due to bounded repetition.
|
|
|
Mapping of packet processing from P4 Language to FPGA Technology
Kekely, Michal ; Fišer, Petr (oponent) ; Zilberman, Noa (oponent) ; Kořenek, Jan (vedoucí práce)
This thesis deals with the design of novel hardware architectures for packet classification. The main goal is to propose general and flexible hardware approaches capable of classifying packets on high-speed computer networks. The approaches need to be configurable via P4 language description and need to be scaleable to 100 Gbps and faster networks. The thesis starts with an analysis of the current state of the art in packet classification on high-speed networks. Based on the analysis, new architectures for packet classification are proposed. The architectures are designed with scalability, flexibility, and memory efficiency in mind. The goal is to achieve high throughput while maintaining P4-programmability and the ability to carry out general packet classification. Proposed approaches are further optimized and extended to be as efficient as possible. The first architecture uses the DCFL algorithm extended by a parallel TCAM memory, memory duplication and ruleset analysis. The goal is to achieve general packet classification, which has small memory requirements and offer a trade-off between the achieved throughput and the memory requirements. The second proposed approach is more specialized. It optimizes exact match packet classification by leveraging the distributed memories on FPGAs to speed up the Cuckoo hashing algorithm. The main goal is to achieve very high throughputs efficiently. Both approaches are further extended by proposing a caching mechanism that enables efficient external memory usage. Finally, all of the proposed mechanisms are evaluated on real network data, and the achieved results are shown.
|
|
|
Static Analysis of C Programs
Malík, Viktor ; Zuleger, Florian (oponent) ; Strejček, Jan (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis proposes several original contributions to the area of static analysis of software with focus on low-level systems code written in C. The contributions are split into two parts, each related to a different area of static analysis, namely formal verification of (low-level) C code and static analysis of semantic equivalence of different versions of the same software. The first part proposes new analyses suitable for verification engines that perform automatic invariant inference using an SMT solver. The proposed solution includes two abstract template domains that use logical formulae over bit-vectors to encode the shape of the program heap and the contents of the program arrays. The shape domain is based on computing a points-to relation between pointers and symbolic addresses of abstract memory objects. The array domain is based on splitting the arrays into several non-overlapping contiguous segments and computing a different invariant for each of them. Both domains can be combined with value domains in a straightforward manner, which particularly allows our approach to reason about shapes and contents of heap and array structures at the same time. The information obtained from the analyses can be used to prove memory safety and reachability properties, expressed by user assertions, of programs manipulating data structures. All of the proposed solutions have been implemented in the 2LS framework and compared against state-of-the-art tools that perform the best in the relevant categories of the well-known Software Verification Competition (SV-COMP). Results show that 2LS outperforms these tools on benchmarks requiring combined reasoning about unbounded data structures and their numerical contents. The second part of the thesis is motivated by existence of software projects that undergo regular refactorings and modifications and yet need to ensure semantic stability of some of their core parts. This part proposes a highly-scalable approach for automatically checking semantic equivalence of different versions of large, real-world C projects, with a particular focus on the Linux kernel. The proposed method uses a novel combination of pattern matching with light-weight static analysis and control-flow transformations. The method checks preservation of the semantics of functions forming the API of the project being analyzed as well as of the semantics of its global variables, which typically hold various control parameters. For the latter, a specialised slicing procedure is proposed to slice out code influenced by these variables and concentrate the further analysis on that code only. Although the method cannot prove equivalence on heavily refactored code, it can compare thousands of functions in the order of minutes while producing a low number of false non-equality verdicts as our experiments show. The method has been implemented over the LLVM infrastructure in a tool called DiffKemp. Our results show that DiffKemp, unlike other existing tools, gives practically useful results even on projects of the size of the Linux kernel.
|
|
|
Automata in Software Verification and Testing
Hruška, Martin ; Rezine, Ahmed (oponent) ; Kofroň, Jan (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis focuses on applications of automata theory to software quality. In the first part, we focus on shape analysis which can be used for formal verification of programs manipulating dynamic data structures. Particularly, we develop an approach of backward program execution along possible counterexamples tracesvand counterexample-guided refinement for shape analysis based on forest automata. We also introduce a new approach based on automata over graphs with a bounded tree width which is more general than forest automata but still has feasible computation properties. In the second part, we introduce a method for automated testing of manufacturing execution systems (MES) in digital twin. We are able to orchestrate a digital twin to reproduce behaviour of a real-world setting in which MES is deployed and so provide a safe environment for testing. Moreover, we can generate new test cases by applying automata and abstraction over them in this context.
|
|
|
Evolutionary Synthesis of Complex Digital Circuits
Kocnová, Jitka ; Fišer, Petr (oponent) ; Trefzer,, Martin (oponent) ; Vašíček, Zdeněk (vedoucí práce)
The research presented in this thesis focuses on the field of evolutionary optimization of complex combinational circuits. The work begins with a study of the existing conventional and nonconventional approaches to the optimization of combinational circuits. Features and issues connected with the internal circuit representations commonly used by present synthesis tools. Boolean networks and their scalability were discussed. Attention was also paid to the evolutionary synthesis, with focus on the CGP (Cartesian Genetic Programming). A new approach to the evolutionary optimization of combinational circuits was proposed. By extracting a sub-circuit containing a suitable number of gates of the original circuit and by optimizing this sub-circuit by the CGP, it was possible to reduce the number of gates of the circuit significantly more than by optimizing the whole circuit by the CGP. For the extraction phase, three methods were proposed. The first method is based on the cut computing algorithm. This method was able to reduce the number of gates of every benchmark circuit and it overcame the results of the globally working CGP in majority of cases. The second method is based on the windowing algorithm. This allows to expand the sub-circuit selection with the gates in the output direction of the root node of the selection and not only with the gates in its input direction. This method significantly improved the results obtained by using the cut-based method. It also overcame the issue of the cut-based method with selecting the sub-circuit near the primary inputs of the circuit and thus creating a selection too small for a subsequent optimization. The third method is based on the reconvergent-paths selection algorithm. The existence of a reconvergent-path in the sub-circuit increases the probability of presence of don't care nodes and thus the higher efficiency of the optimization. Also, an evolutionary optimization method targeting the non-uniform delay on the sub-circuit's inputs. By using this method, it is possible to extract and optimize a sub-circuit without an influence on the delay of the whole circuit. By applying the principle of local evolutionary optimization, a significantly better gate reduction of the circuits was achieved then by applying the CGP optimization on whole cir- cuits. However, it is important to choose the sub-circuit's root node carefuly with respect to its position in the circuit. Also, it is necessary to set the parameters of evolution, extraction and the whole optimization process carefully (e.g. the number of gates in each sub-circuit, number of CGP generations and number of sub-circuits that should be optimized).
|
host ::
RSS.