2014
2015
2016
2017

The twenty-fifth meeting of the Prague computer science seminar

Josef Urban

Artificial Intelligence and Theorem Proving

The talk will cover several AI methods used to learn proving of conjectures over large formal mathematical corpora. This includes (i) machine-learning methods that learn from previous proofs how to suggest the most relevant lemmas for proving the next conjectures, (ii) methods that guide low-level proof-search algorithms based on previous proof traces, and (iii) methods that automatically invent suitable theorem-proving strategies on classes of problems.

January 26, 2017

4:00pm

Auditorium S5, MFF UK
Malostranské nám. 25, Praha 1
Show on the map

Lecture annotation

The talk will cover several AI methods used to learn proving of conjectures over large formal mathematical corpora. This includes (i) machine-learning methods that learn from previous proofs how to suggest the most relevant lemmas for proving the next conjectures, (ii) methods that guide low-level proof-search algorithms based on previous proof traces, and (iii) methods that automatically invent suitable theorem-proving strategies on classes of problems.

I will show examples of AI systems implementing positive feedback loops between induction and deduction, and show the performance of the current methods over large libraries of existing proof assistants such as Isabelle, Mizar, and HOL. Finally, I will mention emerging AI systems that combine statistical parsing of informal mathematics with such strong theorem proving methods.

Lecturer

Josef Urban

Josef Urban is a senior researcher at the Czech Institute of Informatics, Robotics and Cybernetics (CIIRC) of the Czech Technical University in Prague where he is heading the ERC-funded project AI4REASON. His main interest is development of combined inductive and deductive AI methods over large formal (fully semantically specified) knowledge bases, such as large corpora of formally stated mathematical definitions, theorems and proofs. His systems have won several competitions in this field. He received his MSc in Mathematics and PhD in Computers Science from the Charles University in Prague, worked as an assistant professor in Prague, and as a researcher at the University of Miami and Radboud University Nijmegen.

ABOUT THE PRAGUE COMPUTER SCIENCE SEMINAR

The seminar takes place on the 4th Thursday of each month at 4:00pm (except June, July, August and December) alternately in the buildings of Faculty of Electrical Engineering, Czech Technical University, Karlovo nám. 13, Praha 2 and Faculty of Mathematics and Physics, Charles University, Malostranské nám. 25, Praha 1.

Its program consists of a one-hour lecture followed by a discussion. The lecture is based on an (internationally) exceptional or remarkable achievement of the lecturer, presented in a way which is comprehensible and interesting to a broad computer science community. The lectures is in English.

The seminar is organized by the organizational committee consisting of Roman Barták (Charles University, Faculty of Mathematics and Physics), Michal Chytil (Czech Academy of Sciences, Computer Science Institute), Pavel Kordík (Czech Tech. Univ., Faculty of Information Technologies), Jan Kybic (Czech Tech. Univ., Faculty of Electrical Engineering), Michal Pěchouček (Czech Tech. Univ., Faculty of Electrical Engineering), Jiří Sgall (Charles University, Faculty of Mathematics and Physics), Vojtěch Svátek (University of Economics, Faculty of Informatics and Statistics), Michal Šorel (Czech Academy of Sciences, Institute of Information Theory and Automation), Tomáš Werner (Czech Tech. Univ., Faculty of Electrical Engineering), and Filip Železný (Czech Tech. Univ., Faculty of Electrical Engineering)

The idea to organize this seminar emerged in discussions of the representatives of several research institutes on how to avoid the undesired fragmentation of the Czech computer science community.

Supporters

Contact