2014

2015

2016

2017

2018

2019

2020

2022

2023

2024

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.

Annotation Lecturer

2024
2023
2022
2020
2019
2018
2017
2016
2015
2014

Play record

January 26, 2017

4:00pm

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

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.

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.

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 are in English.

The seminar is organized by the organizational committee consisting of Roman Barták (Charles University, Faculty of Mathematics and Physics), Jaroslav Hlinka (Czech Academy of Sciences, Computer Science Institute), Michal Chytil, Pavel Kordík (CTU in Prague, Faculty of Information Technologies), Michal Koucký (Charles University, Faculty of Mathematics and Physics), Jan Kybic (CTU in Prague, Faculty of Electrical Engineering), Michal Pěchouček (CTU in Prague, 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 (CTU in Prague, Faculty of Electrical Engineering), and Filip Železný (CTU in Prague, 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.