The workshop takes inspiration from the successful series of PIWo inter-reasoning workshops organised by the Automated Reasoning Group in Prague and the follow up VINO workshop in Vienna. In a similar spirit, it will combine high-quality invited presentations with informal discussions and a cultural networking programme.
The main topic of the workshop will be the combination of automated reasoning and machine learning.
Alfréd Rényi Institute for Mathematics, Reáltanoda utca 13-15, Budapest, 1053, Hungary
Schedule:
Monday, 24th of September
10:00-11:30: Discussion on the role of ATP in formal verification of complicated mathematical statements.
12:00- 13:00: Martin Suda - Anatomy of the Vampire Theorem Prover
14:30 - 15:30: Konstantin Korovin - Instantiation based Theorem Proving and Abstraction-Refinement
16:00 - 16:30: Jan Jabukuv - Instantiation based Theorem Proving and Abstraction-Refinement
16:30 - 17:30: Zarathustra Goertzel - Machine Learning and Watchlist Guidance for E prover
Tuesday, 25th of September
10:00 - 10:30: Zsolt Zombori - Longer Proofs by Curriculum Learning
10:30- 11:00: Henryk Michalewski - DeepSAT
11:00 - 11:30: Bartosz Piotrowski - Machine Learning of Premise Selection
12:00 - 13:00: Chad Brown - The AIM Conjecture and Proof Checking
14:30 - 15:30: Shawn Wang: Progress in Autoformalization of Mathematics
16:00 - 16:30 Thibault Gauthier - Machine Learning for Tactical Guidance
16:30 - 17:00: Michael Rawson - Strategy Learning for Vampire
Wednesday, 26th of September
10:00-11:00: Christian Szegedy: Deep Learning for HOL-light
11:30 -12:30: Balazs Szegedy: Machine Learning over tensor networks.
Afternoon: Cultural program
Thursday 27th of September
10:00 - 11:00: Lasse Blaauwbroek - Experiments with Learning of Tactical Guidance for Coq
11:30 - 13:00: Discussions, wrap up.