University of Warsaw | H.Michalewski@mimuw.edu.pl |

2 Banacha St. | +48 669 669 860 |

Warsaw, Poland | office 1560 |

- 2015
**Habilitation in computer science**, University of Warsaw.**Title: Investigations of automata and related logics using methods of set theory**.- Winter 2002
**internship**in the Fields Institute, Toronto, Canada, applications of set theory in other areas of mathematics- 1998-2002
**PhD in Mathematics**, University of Warsaw**Thesis title: Function spaces with topology of pointwise convergence**- 1993-1998
**MA in Mathematics**, University of Warsaw

- 2019-
**Visiting Professor**at Google (Staff Visiting Faculty Researcher at Google)- 2018-2019
**Visiting Professor**at the Department of Computer Science of the University of Oxford- 2017-2018
**Assistant Professor**at the Mathematical Institute of Polish Academy of Sciences- 2017
**Invited Professor**at the École normale supérieure de Lyon- 2016-2019
- research and business projects with deepsense.ai related to machine learning
- 2012-2013
**Assistant Professor**at the Mathematical Institute of Polish Academy of Sciences- 2007-present
**Assistant Professor**at the Department of Mathematics, Informatics and Mechanics of the University of Warsaw- 2004-2007
**Postdoc**at the Department of Mathematics of the Ben Gurion University, Israel. Working on topics related to logic and foundations of mathematics- 2002-2004
**Teaching Assistant**at the Department of Mathematics, Informatics and Mechanics of the University of Warsaw

My Masters and PhD theses concerned mathematical logic and games. Representative papers are Game-theoretic approach to the hereditary Baire property of C_{p}(N_{F}) and Condensation of projective sets onto compacta. The importance of games in set theory is linked to the set-theoretical notion of descriptive complexity of sets. Namely, many classes of sets can be characterized using so called **game quantifiers**. With such a quantifier applied to a parametrized family of two-person games we can select parameters where the first player has a winning strategy.

In my Habilitation I turned to the theory of automata on trees, which plays a fundamental role in computer science, applying ideas from game quantification. Measure Properties of Game Tree Languages proved that sets defined by automata on trees correspond to sets defined with game quantifiers over games with universes being boolean combinations of *F*_{σ} sets. This is useful since Kolomogorov proved that such sets are **tame** in several senses -- for example, they are Lebesgue measurable. In On the Decidability of MSO+U on Infinite Trees we combined definability arguments with prior undecidability results to show the first undecidability result for a logic on trees, MSO+U. How unprovable is Rabin's decidability theorem? dealt with the interaction of automata theory and proof theory; the paper provides a fine-grained analysis of the axioms needed to prove a fundamantal decidability results in automata and logic, Rabin's theorem.

From logic, automata, and the theory of general games, I turned to the practice of games in the usual human sense. In 485 - a new upper bound for Morpion Solitaire we reduced the problem of finding the upper bound in the Morpion Solitaire game to a number of linear optimization tasks, which are amenable to computational solutions. This was my entry point into AI, and led to a series of papers on Atari games and Deep Reinforcement learning, including Learning from the memory of Atari 2600, Hierarchical Reinforcement Learning with Parameters, Reinforcement learning of theorem proving, Neural heuristics for SAT solving Towards Finding Longer Proofs. In 2018 I have started a business collaboration with Volkswagen which resulted in an experiment Simulation-based reinforcement learning for real-world autonomous driving - we have trained our agents in simulation and tested on a full-size passenger vehicle.

- Pierre Pradic, 2016-2019, joint PhD program with the École normale supérieure de Lyon, thesis co-supervisied by Colin Riba; main topic: reverse mathematics of algorithms.
- Bartosz Piotrowski, 2017-2021, joint PhD program with the Technical University in Prague, thesis co-supervised by Josef Urban; main topic: machine learning for theorem proving.
- Błażej Osiński, 2017-2021, a former Googler, main topic: machine learning and robotics, a lead researcher in the VW project.
- Michał Garmulewicz, 2018-2022, currently working as a research intern at Brain Corporation, San Diego on problems related to planning and imitation learning.

- Machine learning and automatic theorem proving, 2019-2022, principal investigator.

- an invited speaker at the Annual Meeting of the Swiss Society for Logic and Philosophy of Science (SSLPS), Lausanne, Switzerland, November 2015.
- an invited talk on reinforcement learning at the Google office in Warsaw, Poland, Feb, 2018.
- an invited talk on reinforcement learning and theorem proving at Google Research, Mountain View, USA, November, 2018.
- an invited talk on reinforcement learning and theorem proving at DeepMind, London, UK, July, 2019.
- an invited talk on reinforcement learning and theorem proving at the Cambridge Computer Laboratory, UK, August, 2019.
- an invited talk on reinforcement learning and theorem proving at the Cambridge Math Department, UK, November, 2019.

- machine learning: a course run jointly with Jan Lasek and Piotr Migdał from deepsense.ai for consultants of the Boston Consulting Group, including a kaggle-style machine learning comptetition organized on a machine learning platform neptune.ml
- optimization: a novel course at the University of Warsaw on linear optimization combining precise exposition of theory and practical classes in programming
- advanced courses at the University of Warsaw: practical machine learning run jointly with withy deepsense.ai, computer aided verification, logic and type theory - programming in Coq, artificial intelligence and games (a research seminar, which led to 2 papers on optimization), automata on infinite structures, mu-calculus, information theory, algorithmic aspects of game theory, functional analysis, descriptive set theory, tropical geometry and linear optimization

- Markdown, Madoko and Natural Deduction as tools in teaching an introductory course in logic
- Live computing - a collaboration with Intel on alternative ways of teaching basics of computer science.

- Błażej Osiński, Adam Jakubowski, Paweł Zięcina, Piotr Miłoś, Christopher Galias, Silviu Homoceanu and Henryk Michalewski, Simulation-based reinforcement learning for real-world autonomous driving, presented at Machine Learning for Autonomous Driving NeurIPS 2019 Workshop, accepted to ICRA 2020. This is a joint project with Volkswagen, see the press release.
- Sebastian Jaszczur, Michał Łuszczyk, Henryk Michalewski, Neural heuristics for SAT solving, oral presentation at the Representation Learning on Graphs and Manifold Workshop, ICLR 2019.
- Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban, Towards finding longer proofs, presented at Knowledge Representation & Reasoning Meets Machine Learning NeurIPS 2019 Workshop (selected oral presentation).
- Lukasz Kaiser, Mohammad Babaeizadeh, Piotr Milos, Blazej Osinski, Roy H Campbell, Konrad Czechowski, Dumitru Erhan, Chelsea Finn, Piotr Kozakowski, Sergey Levine, Afroz Mohiuddin, Ryan Sepassi, George Tucker, Henryk Michalewski, Model-Based Reinforcement Learning for Atari, accepted as a spotlight presentation at ICLR 2020 (5% acceptance rate).
- Igor Adamski, Robert Adamski, Tomasz Grel, Adam Jędrych, Kamil Kaczmarek, Henryk Michalewski, Distributed Deep Reinforcement Learning: Learn how to play Atari games in 21 minutes, presented at ISC HPC conference 2018.
- Henryk Michalewski, Piotr Miłoś, Błażej Osiński, Learning to Run challenge solutions: Adapting reinforcement learning methods for neuromusculoskeletal environments, competition track at NIPS 2017, 6th place out of 450, some videos
- Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olšák, Reinforcement learning of theorem proving, NeurIPS 2018.
- Maciej Klimek, Henryk Michalewski, Piotr Miłoś, Hierarchical Reinforcement Learning with Parameters, presented at CoRL 2017, paper, videos
- Robert Adamski, Tomasz Grel, Maciej Klimek, Henryk Michalewski: Atari games and Intel processors; CGW@IJCAI 2017, animations from various stages of learning for Breakout, Space Invaders and Boxing
- Filippo Cavallari, Henryk Michalewski, Michał Skrzypczak: A characterisation of G
_{delta}regular tree languages, MFCS 2017. - Mikolaj Bojańczyk, Henryk Michalewski: Some connections between universal algebra and logics for trees, preprint 2017
- Henryk Michalewski,Matteo Mio, Michal Skrzypczak: Monadic Second Order Logic with Measure and Category Quantifiers, Logical Methods in Computer Science 14(2) (2018)
- Jakub Sygnowski, Henryk Michalewski: Learning from the memory of Atari 2600, CGW@IJCAI 2016, implementation
- Oskar Skibski, Henryk Michalewski, Andrzej Nagórko, Tomasz Michalak, Andrew Dowell, Talal Rahwan, Michael Wooldridge, Non-Utilitarian Coalition Structure Generation, ECAI 2016, implementation
- Leszek Aleksander Kolodziejczyk, Henryk Michalewski, Pierre Pradic, Michal Skrzypczak: The Logical Strength of Büchi's Decidability Theorem, CSL 2016: 36:1-36:16
- Leszek Aleksander Kolodziejczyk, Henryk Michalewski: How unprovable is Rabin's decidability theorem?, LICS 2016: 788-797
- Henryk Michalewski, Andrzej Nagórko, Jakub Pawlewicz, An upper bound of 84 for Morpion Solitaire 5D, CCCG 2016 proceedings, implementation
- Henryk Michalewski, Michal Skrzypczak: Unambiguous Büchi Is Weak, DLT 2016: 319-331
- Henryk Michalewski, Matteo Mio, Mikolaj Bojańczyk: On the Regular Emptiness Problem of Subzero Automata, ICE 2016: 1-23
- Henryk Michalewski, Matteo Mio, Measure Quantiﬁer in Monadic Second Order Logic, LFCS 2016: 267-282.
- Henryk Michalewski, Matteo Mio, On the Problem of Computing the Probability of Regular Sets of Trees, FSTTCS 2015: 489-502
- Henryk Michalewski, Matteo Mio. Baire Category Quantifier in Monadic Second Order Logic, ICALP (2) 2015: 362-374
- Henryk Michalewski, Andrzej Nagórko, Jakub Pawlewicz, 485 - a new upper bound for Morpion Solitaire, CGW@IJCAI 2015, implementation
- André Arnold, Henryk Michalewski, Damian Niwinski, On the Separation Question for Tree Languages, Theory Comput. Syst. 55(4): 833-855 (2014)
- Alessandro Facchini, Henryk Michalewski, Deciding the Borel Complexity of Regular Tree Languages, CiE 2014: 163-172
- Mikolaj Bojańczyk, Tomasz Gogacz, Henryk Michalewski, Michal Skrzypczak, On the Decidability of MSO+U on Infinite Trees, ICALP (2) 2014: 50-61
- Tomasz Gogacz, Henryk Michalewski, Matteo Mio, Michal Skrzypczak, Measure Properties of Game Tree Languages, MFCS (1) 2014: 303-314
- Henryk Michalewski, Damian Niwinski, On Topological Completeness of Regular Tree Languages, Logic and Program Semantics 2012: 165-179
- André Arnold, Henryk Michalewski, Damian Niwinski, On the separation question for tree languages, STACS 2012: 396-407
- Szczepan Hummel, Henryk Michalewski, Damian Niwinski, On the Borel Inseparability of Game Tree Languages, STACS 2009: 565-575
- Menachem Kojman, Henryk Michalewski, Borel extensions of Baire measures in ZFC, Fund. Math. 211 (2011), no. 3, 197-223
- Andrzej Komisarski, Henryk Michalewski, Pawel Milewski, Functions equivalent to Borel measurable ones, Bull. Pol. Acad. Sci. Math. 58 (2010), no. 1, 55-64
- Adam Krawczyk, Witold Marciszewski, Henryk Michalewski, Remarks on the set of G
_{delta}-points in Eberlein and Corson compact spaces, Topology Appl. 156 (2009), no. 9, 1746-1748. - Wieslaw Kubiś, Henryk Michalewski, Small Valdivia compact spaces, Topology and its Applications 153 (14), 2560-2573
- Adam Krawczyk, Henryk Michalewski, An example of a topological group, Topology Appl. 127 (2003), no. 3, 325-330
- Adam Krawczyk, Henryk Michalewski, Linear metric spaces close to being sigma–compact, preprint, 2003
- Henryk Michalewski, Condensation of projective sets onto compact, Proc. AMS 131, (2003), 3601-3606
- Henryk Michalewski, An answer to a question of Arhangelskii, Comment. Math. Univ. Carolin. 42 (2001), no. 3, 545-550
- Henryk Michalewski, Homogeneity of K(Q), Tsukuba J. Math. 24 (2000), no. 2, 297-302
- Henryk Michalewski, Game-theoretic approach to the hereditary Baire property of C
_{p}(N_{F}), Bull. Polish Acad. Sci. Math. 46 (1998), no. 2, 135-140 - Henryk Michalewski, Roman Pol, On a Hurewicz-type theorem and a selection theorem of Michael, Bull. Polish Acad. Sci. Math. 43 (1995), no. 4, 273-275 (1996)