ENSPM2021 Talk
Title: Machine Learning in Automated and Interactive Theorem Proving
Abstract: The talk will discuss the main methods that combine machine learning with automated and interactive theorem proving. This includes learningbased guidance of saturation-style and tableau-style automated theorem provers (ATPs), guiding tactical interactive theorem provers (ITPs) and using machine learning for selecting of relevant facts from large ITP libraries in the “hammer” linkups of ITPs with ATPs. I will also mention several feedback loops between proving and learning in this setting, and discuss some connections to SAT and related areas.
Josef Urban (Czech Technical University in Prague)
Josef Urban is a Principal 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 interests include Automated Reasoning, Formal Verification and Machine Learning. In particular, he is interested in development of combined inductive/learning and deductive/reasoning “strong AI” methods and systems over large formal (fully semantically specified) knowledge bases. Examples are large corpora of formally stated definitions, theorems and proofs in mathematics, software verification and related fields. He has made such corpora available to the AI methods, created the first benchmarks, and developed first approaches and systems combining learning and reasoning over such corpora in various feedback loops. The systems developed by him and his colleagues have won several competitions and the methods today assist formal verification in proof assistants. He has also co-developed first learning/reasoning systems for automated formalization of informal mathematics, and co-founded the conference on Artificial Intelligence and Theorem Proving (AITP). 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.