Schedule
Friday, May 07, 2021
All times are in EDT (UTC -4)
| 08:55-09:00 | Introduction and Opening Remarks | |
| 09:00-09:30 | Invited Talk |
Theorem Proving and Artificial Intelligence - A Brief Introduction. Josef Urban, Czech Technical University in Prague |
| 09:30-10:00 | Invited Talk |
Reasoning with Deep Learning Architectures Based on System 2 Inductive Biases. Yoshua Bengio, Mila, Université de Montréal |
| 10:00-10:30 | Poster Session 1 | |
| 10:30-11:00 | Coffee Break | |
| 11:00-11:30 | Invited Talk |
The Relevance of Computational Creativity to Mathematical Reasoning Machines. Alison Pease, University of Dundee |
| 11:30-12:00 | Invited Talk |
Towards A Human-Like Reasoning System. Mateja Jamnik, University of Cambridge |
| 12:00-12:30 | Invited Talk |
Mathematical Reasoning in Humans. Jay McClelland, Stanford University |
| 12:30-13:00 | Coffee Break | |
| 13:00-14:00 | Discussion Panel | Mathematical Reasoning for AGI: Challenge and Implications. Yoshua Bengio, Timothy Gowers, Mateja Jamnik, Jay McClelland, Alison Pease, Christian Szegedy, Josef Urban. |
| 14:00-14:30 | Coffee Break | |
| 14:30-15:00 | Invited Talk |
From Hammer to Scalpel: Progress in Automated Theorem Proving. Markus Rabe, Google |
| 15:00-15:30 | Poster Session2 | |
| 15:30-16:00 | Coffee Break | |
| 16:00-16:30 | Invited Talk |
Formal vs Informal Mathematics, Reasoning and AGI. Stanislas Polu, OpenAI |
| 16:30-16:50 | Contributed Talk | Training a First-Order Theorem Prover from Synthetic Data. Vlad Firoiu |
| 16:50-17:10 | Contributed Talk | Proof Artifact Co-training for Theorem Proving With Language Models. Jesse Michael Han |
| 17:10-17:30 | Contributed Talk | Improving Exploration in Policy Gradient Search: Application to Symbolic Optimization. Mikel Landajuela Larma |
| 17:30-17:35 | Closing Remarks |