|
|
Using Reinforcement learning and inductive synthesis for designing robust controllers in POMDPs
Hudák, David ; Holík, Lukáš (oponent) ; Češka, Milan (vedoucí práce)
A significant challenge in sequential decision-making involves dealing with uncertainty, which arises from inaccurate sensors or only a partial knowledge of the agent's environment. This uncertainty is formally described through the framework of partially observable Markov decision processes (POMDPs). Unlike Markov decision processes (MDP), POMDPs only provide limited information about the exact state through imprecise observations. Decision-making in such settings requires estimating the current state, and generally, achieving optimal decisions is not tractable. There are two primary strategies to address this issue. The first strategy involves formal methods that concentrate on computing belief MDPs or synthesizing finite state controllers, known for their robustness and verifiability. However, these methods often struggle with scalability and require to know the underlying model. Conversely, informal methods like reinforcement learning offer scalability but lack verifiability. This thesis aims to merge these approaches by developing and implementing various techniques for interpreting and integrating the results and communication strategies between both methods. In this thesis, our experiments show that this symbiosis can improve both approaches, and we also show that our implementation overcomes other RL implementations for similar tasks.
|
|
|
Formal Analysis of Neural Networks
Hudák, David ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
Today, the area where we can use deep learning is becoming broader. It includes safety-critical domains such as traffic or healthcare, and the need for its verification grows. However, sufficient verification toolkits for neural networks, the leading deep learning approach, are still in development. State-of-the-art algorithms now can not verify commonly used deep networks. In this paper, we focus on one of the state-of-the-art solutions, VeriNet. More generally, we focused on the symbolic approach of local robustness analysis. This approach usually relies on creating, processing, and refining the neural network representation, and we focused on the refinement phase. We primarily dealt with the branch and bound algorithm, which in this toolkit splits node inputs in a network to create smaller sub-problems. For this algorithm, we proposed and implemented new split node selection strategies. Specifically, we designed memory-based, alternating, and semi-hierarchical strategies. We achieved significant improvements in the scalability of the VeriNet toolkit. One of our approaches can solve more complex cases and significantly improve already solved cases' performance. Moreover, we discovered an anomaly in the behavior of the verification algorithm we named branch implosions, which led to extreme speed up for some cases. In addition, we extended the set of performed network benchmarks with models from the Marabou package.
|
|
|
Formal Analysis of Neural Networks
Hudák, David ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
Today, the area where we can use deep learning is becoming broader. It includes safety-critical domains such as traffic or healthcare, and the need for its verification grows. However, sufficient verification toolkits for neural networks, the leading deep learning approach, are still in development. State-of-the-art algorithms now can not verify commonly used deep networks. In this paper, we focus on one of the state-of-the-art solutions, VeriNet. More generally, we focused on the symbolic approach of local robustness analysis. This approach usually relies on creating, processing, and refining the neural network representation, and we focused on the refinement phase. We primarily dealt with the branch and bound algorithm, which in this toolkit splits node inputs in a network to create smaller sub-problems. For this algorithm, we proposed and implemented new split node selection strategies. Specifically, we designed memory-based, alternating, and semi-hierarchical strategies. We achieved significant improvements in the scalability of the VeriNet toolkit. One of our approaches can solve more complex cases and significantly improve already solved cases' performance. Moreover, we discovered an anomaly in the behavior of the verification algorithm we named branch implosions, which led to extreme speed up for some cases. In addition, we extended the set of performed network benchmarks with models from the Marabou package.
|
host ::
RSS.