Workshop
The Role of Mathematical Reasoning in General Artificial Intelligence
Yuhuai Wu · Kshitij Bansal · Wenda Li · Melanie Mitchell · David McAllester · John Harrison
Fri 7 May, 5:55 a.m. PDT
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: America/Los_Angeles
Schedule
|
Fri 5:55 a.m. - 6:00 a.m.
|
Introduction and Opening Remarks
(
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
)
>
SlidesLive Video |
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
)
>
SlidesLive Video |
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.
|
Poster Session 1 ( Poster Session 1 ) > link | 🔗 |
|
Fri 7:30 a.m. - 8:00 a.m.
|
Coffee 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
)
>
SlidesLive Video |
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
)
>
SlidesLive Video |
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
)
>
SlidesLive Video |
James 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
|
🔗 |
|
Fri 10:00 a.m. - 11:00 a.m.
|
Panel Discussion
(
Panel Discussion
)
>
|
Timothy Gowers 🔗 |
|
Fri 11:00 a.m. - 11:30 a.m.
|
Coffee 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
)
>
SlidesLive Video |
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.
|
Poster Session 2 ( Poster Session 2 ) > link | 🔗 |
|
Fri 12:30 p.m. - 1:00 p.m.
|
Coffee 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
)
>
SlidesLive Video |
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
)
>
SlidesLive Video |
🔗 |
|
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
)
>
SlidesLive Video |
🔗 |
|
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
)
>
SlidesLive Video |
🔗 |
|
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
(
Closing Remarks
)
>
|
🔗 |