21 lutego 2020 16:10
Seminarium wydziałowe: Henryk Michalewski - Uczenie maszynowe i dowodzenie twierdzeń.
W imieniu Dziekana Wydziału serdecznie zapraszamy pracowników oraz studentów na kolejne seminarium wydziałowe, które odbędzie się we wtorek 25 lutego o godz. 12:30 w Instytucie Informatyki, sala 119.
Prelegentem będzie dr hab. Henryk Michalewski z Uniwersytetu Warszawskiego, który wygłosi wykład pt.
Uczenie maszynowe i dowodzenie twierdzeń.
Przed wykładem, o godz. 12:00 Dziekan zaprasza na kawę i ciastka.
Abstract:
In my talk I will describe how theorem proving can be phrased as a machine learning problem and provide experimental results with regard to various datasets consisting of mathematical problems ranging from SAT problems to simple arithmetic problems involving addition and multiplication, to theorem proving inspired by simplifications and rewritings of SQL queries and finally to general mathematical problems such as included in the Mizar Mathematical library https://en.wikipedia.org/wiki/Mizar_system. The talk will cover in particular the following topics:
- two reinforcement learning algorithms designed for theorem proving; one of them presented at NeurIPS 2018 in the paper "Reinforcement learning of Theorem Proving" (https://papers.nips.cc/paper/8098-reinforcement-learning-of-theorem-proving.pdf) runs Monte-Carlo simulations guided by policy and value functions gradually updated using previous proof attempts. The other algorithm is based on curriculum learning and is described in the paper "Towards Finding Longer Proofs" (https://arxiv.org/abs/1905.13100, project webpage: https://sites.google.com/view/atpcurr). It complements the Monte Carlo method in two respects: it may be deployed to solve just one mathematical problem and overall it is capable to produce longer proofs.
- a graph network architecture which includes sigmoidal attention (https://rlgm.github.io/papers/32.pdf) with an empirical study which shows that this kind of graph representation helps neural guidance of SAT solving algorithms.
- I will show how rewriting of SQL queries can be phrased as a theorem proving problem, explain why reinforcement learning is a suitable framework for optimization of queries and present initial experimental results obtained with Michael Benedikt and Cezary Kaliszyk.
Bio:
Henryk Michalewski's Masters and PhD theses concerned topology, mathematical logic and games. In his Habilitation, he turned to the theory of automata on trees, which plays an important role in theoretical computer science. From logic, automata, and the theory of general games, he turned to the practice of games in the usual human sense, starting from applying optimization methods to Morpion Solitaire. This was his entry point into machine learning and led to a series of papers on Atari games and Deep Reinforcement learning, including "Learning from the memory of Atari 2600" (https://arxiv.org/abs/1605.01335), "Hierarchical Reinforcement Learning with Parameters" (http://proceedings.mlr.press/v78/klimek17a/klimek17a.pdf), "Distributed Deep Reinforcement Learning: Learn how to play Atari games in 21 minutes" (https://arxiv.org/abs/1801.02852), a joint project with Google Brain on Model-Based Reinforcement Learning for Atari games https://sites.google.com/view/modelbasedrlatari/home which was accepted as a spotlight at ICLR 2020 and a joint project with Volkswagen on autonomous driving https://arxiv.org/pdf/1911.12905.pdf which was accepted for ICRA 2020.
Henryk Michalewski is a professor at the University of Warsaw. From October 2019 he is working as a Staff Visiting Faculty Researcher at Google.