Machine learning and theorem proving
In my talk I will describe how theorem proving can be phrased as a reinforcement 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: reinforcement learning algorithms designed for theorem proving; the HOList theorem proving system developed at Google and a graph network architecture which includes sigmoidal attention with an empirical study which shows that this kind of graph representation helps neural guidance of SAT solving algorithms.
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. Henryk Michalewski is a professor at the University of Warsaw. In this academic year Henryk is coordinating three student projects inspired by Google Research. From October 2019 Henryk is working as a Staff Visiting Faculty Researcher at Google.