Seminarium Wydziałowe
Jesteś tutaj: Strona główna
czwartek, luty 27, 2020
Dziekan Wydziału serdecznie zaprasza pracowników oraz studentów na
seminarium wydziałowe, które
odbędzie się we wtorek 25 lutego o godz. 12.30 (Instytut Informatyki, sala 119). Prelegentem będzie
dr hab. Henryk Michalewski z Uniwersytetu Warszawskiego, który wygłosi wykład pt.
"Machine learning and theorem proving".
Przed seminarium, o godz. 12.00, Dziekan zaprasza na kawę i ciastko.
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. The talk will cover in particular the following topics:
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, Hierarchical Reinforcement Learning with Parameters, Distributed Deep Reinforcement Learning: Learn how to play Atari games in 21 minutes, a joint project with Google Brain on Model-Based Reinforcement Learning for Atari games ( www) which was accepted as a spotlight at ICLR 2020 and a joint project with Volkswagen on autonomous driving (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.
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. 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 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, (project webpage: www). 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 ( 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.
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, Hierarchical Reinforcement Learning with Parameters, Distributed Deep Reinforcement Learning: Learn how to play Atari games in 21 minutes, a joint project with Google Brain on Model-Based Reinforcement Learning for Atari games ( www) which was accepted as a spotlight at ICLR 2020 and a joint project with Volkswagen on autonomous driving (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.
