Workshop

The Role of Mathematical Reasoning in General Artificial Intelligence

Yuhuai Wu, Kshitij Bansal, Wenda Li, Melanie Mitchell, David McAllester, John Harrison

Abstract:

In this workshop, we focus on a particular kind of reasoning ability, namely, mathematical reasoning. Advanced mathematical reasoning is unique in human intelligence, and it is also a fundamental building block for many intellectual pursuits and scientific developments. We believe that addressing this problem has the potential to shed light on a path towards general reasoning mechanisms, and hence general artificial intelligence. Therefore, we would like to bring together a group of experts from various backgrounds to discuss the role of mathematical reasoning ability towards the path of demonstrating general artificial intelligence. In addition, we hope to identify missing elements and major bottlenecks towards demonstrating mathematical reasoning ability in AI systems.

Chat is not available.

Timezone: »

Schedule

Fri 5:55 a.m. - 6:00 a.m.
Introduction and Opening Remarks
Wenda Li, Yuhuai Wu
Fri 6:00 a.m. - 6:01 a.m.
Intro: Theorem Proving and Artificial Intelligence - A Brief Introduction (Live Intro)
Fri 6:01 a.m. - 6:26 a.m.
Theorem Proving and Artificial Intelligence - A Brief Introduction (Invited Talk 1)   
Josef Urban
Fri 6:26 a.m. - 6:30 a.m.
QA: Theorem Proving and Artificial Intelligence - A Brief Introduction (QA)
Fri 6:30 a.m. - 6:31 a.m.
Intro: Reasoning with Deep Learning Architectures Based on System 2 Inductive Biases (Live Intro)
Fri 6:31 a.m. - 6:56 a.m.
Reasoning with Deep Learning Architectures Based on System 2 Inductive Biases (Invited Talk 2)   
Yoshua Bengio
Fri 6:56 a.m. - 7:00 a.m.
QA: Reasoning with Deep Learning Architectures Based on System 2 Inductive Biases (QA)
Fri 7:00 a.m. - 7:30 a.m.
 link »

https://eventhosts.gather.town/app/DnfP7ZAW3GPPfhNU/MATHAI-ICLR2021

Fri 7:30 a.m. - 8:00 a.m.
Coffee Break (Break)
Fri 8:00 a.m. - 8:01 a.m.
Intro: The Relevance of Computational Creativity to Mathematical Reasoning Machines (Live Intro)
Fri 8:01 a.m. - 8:26 a.m.
The Relevance of Computational Creativity to Mathematical Reasoning Machines (Invited Talk 3)   
Alison Pease
Fri 8:26 a.m. - 8:30 a.m.
QA: The Relevance of Computational Creativity to Mathematical Reasoning Machines (QA)
Fri 8:30 a.m. - 8:31 a.m.
Intro: Towards A Human-Like Reasoning System (Live Intro)
Fri 8:31 a.m. - 8:56 a.m.
Towards A Human-Like Reasoning System (Invited Talk 4)   
Mateja Jamnik
Fri 8:56 a.m. - 9:00 a.m.
QA: Towards A Human-Like Reasoning System (QA)
Fri 9:00 a.m. - 9:01 a.m.
Intro: Mathematical Reasoning in Humans (Live Intro)
Fri 9:01 a.m. - 9:26 a.m.
Mathematical Reasoning in Humans (Invited Talk 5)   
Jay McClelland
Fri 9:26 a.m. - 9:30 a.m.
QA: Mathematical Reasoning in Humans (QA)
Fri 9:30 a.m. - 10:00 a.m.
Coffee Break (Break)
Fri 10:00 a.m. - 11:00 a.m.
Panel Discussion
Timothy Gowers
Fri 11:00 a.m. - 11:30 a.m.
Coffee Break (Break)
Fri 11:30 a.m. - 11:31 a.m.
Intro: From Hammer to Scalpel: Progress in Automated Theorem Proving (Live Intro)
Fri 11:31 a.m. - 11:56 a.m.
From Hammer to Scalpel: Progress in Automated Theorem Proving (Invited Talk 6)   
Markus Rabe
Fri 11:56 a.m. - 12:00 p.m.
QA: From Hammer to Scalpel: Progress in Automated Theorem Proving (QA)
Fri 12:00 p.m. - 12:30 p.m.
 link »

https://eventhosts.gather.town/app/DnfP7ZAW3GPPfhNU/MATHAI-ICLR2021

Fri 12:30 p.m. - 1:00 p.m.
Coffee Break (Break)
Fri 1:00 p.m. - 1:01 p.m.
Intro: Formal vs Informal Mathematics, Reasoning and AGI (Live Intro)
Fri 1:01 p.m. - 1:26 p.m.
Formal vs Informal Mathematics, Reasoning and AGI (Invited Talk 7)   
Stanislas Polu
Fri 1:26 p.m. - 1:30 p.m.
QA: Formal vs Informal Mathematics, Reasoning and AGI (QA)
Fri 1:30 p.m. - 1:45 p.m.
Training a First-Order Theorem Prover from Synthetic Data (Contributed Talk 1)   
Fri 1:45 p.m. - 1:50 p.m.
Contributed Talk 1 QA (QA)
Fri 1:50 p.m. - 2:05 p.m.
Proof Artifact Co-training for Theorem Proving With Language Models (Contributed Talk 2)   
Fri 2:05 p.m. - 2:10 p.m.
Contributed Talk 2 QA (QA)
Fri 2:10 p.m. - 2:25 p.m.
Improving Exploration in Policy Gradient Search: Application to Symbolic Optimization (Contributed Talk 3)   
Fri 2:25 p.m. - 2:30 p.m.
Contributed Talk 3 QA (QA)
Fri 2:30 p.m. - 2:35 p.m.
Closing Remarks