This is a list of some projects I have made during my free time (mostly related to data analysis and deep learning) and during my PhD research (mostly related to automata theory and model-checking).
I build a model that read in movie reviews from IMDB and make prediction whether it has positive or negative sentiment. I use recurrent neural network (RNN) that also employs long short-term memory (LSTM). This make the model does not only consider individual words, but also the order they appear in. I have trained the model on 25.000 reviews. Here is the notebook.
I build a model that take a flower image and classify it over 102 types of flowers. I consider the 102-Oxford Flower dataset. In order to have a high accuracy, I used a pre-trained neural network ResNet152 and create a very deep model, i.e. >150 layers. I then use google cloud service that allows us to use its GPU computation using Tesla K80 to train the model and obtain 91% accuracy.
I perform an anomaly detection using a simple recurrent neural network. I train the model on a CPU utilization dataset and make it predict the utilisation for next 160 minutes. I compare it with the actual data and observed its mean-squared-error to conclude an indication of anomalities.
I build a model that recognise a handwritten digit using a simple multiple layer perceptron technique. I train the model on MNIST dataset which is available here and obtain 89% accuracy.
Together with my supervisor and the lead researcher in our group, we extend the framework of simulation game that is used to approximate language inclusion between two Büchi automata into Multi-Letter simulation game. This extended framework may outperform the most advanced Ramsey-based algorithms by two orders of magnitude. The result of our research is documented here and the complete tool that we have build is available here.
The core idea of Multi-Letter simulation game is in the flexibility of the second player. He does not need to give a synchronize reply and can delay his move by utilizing a buffer. We further extend this framework to the case where there is an unbounded buffer. We (me, Martin Lange, and Etienne Lozes) managed to show that deciding the winner of such a game is still possible, but is computationally very hard. This result is published here.
We further extend buffered simulation game to the case where there are multiple buffers. This then introduce the possibility to capture concurrency. We can use such a game to approximate verification of concurrent system. We managed to show that deciding the winner of such a game is not possible. It is even already highly undecidable for a very simple case. Here is our overview.