BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Artificial Intelligence Research Group Talks (Comp
uter Laboratory)
SUMMARY:Neural Sequence Models for Mathematical Reasoning
- Yuhuai(Tony) Wu\, Stanford University &\; Goo
gle
DTSTART;TZID=Europe/London:20220614T160000
DTEND;TZID=Europe/London:20220614T170000
UID:TALK171794AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/171794
DESCRIPTION:"Join us on Zoom":https://zoom.us/j/99166955895?pw
d=SzI0M3pMVEkvNmw3Q0dqNDVRalZvdz09\n\nAdvanced mat
hematical reasoning is unique in human intelligenc
e\, and it is a fundamental building block for man
y intellectual pursuits and scientific development
s. In this talk\, I will describe generic approach
es to mathematical reasoning using neural sequence
models. Unlike previous approaches with highly co
nstrained action spaces\, sequence models allow th
e prover to freely synthesize arbitrary proof step
s\, including the synthesis of conjectures\, lemma
s\, and definitions. We created a tool that can he
lp formal mathematicians prove theorems in Lean\,
and our model made contributions accepted by profe
ssional mathematicians\, adding new proofs to the
Lean Mathlib library. The aforementioned work high
lights the power of modern sequence models for aut
omated theorem proving. However\, there are still
major reasoning capabilities that are missing. Fir
st\, for reasoning tasks such as theorem proving o
r program synthesis\, one must be able to work wit
h large and continuously changing theorem database
s and code repositories. I introduced a new transf
ormer architecture that can memorize the internal
representations of past inputs\, allowing the util
ization of newly added facts or codes without the
need for retraining. Second\, reasoning is often t
he result of extended chains of thought\, while cu
rrent models mostly perform fast\, intuitive patte
rn matching. I introduced a learning algorithm tha
t enables models to generate explicit rationales w
hen tackling challenging reasoning problems\, by b
ootstrapping from a pre-trained large language mod
el. I will conclude my talk with future research d
irections towards the goal of building a strong ma
thematical reasoning model.\n\n*Bio:*\n\nYuhuai To
ny Wu is a Postdoctoral Scholar at Stanford Univer
sity working with Percy Liang and Jay McClelland\,
and a Research Scientist at Google. His long-term
research interest is to build a machine that can
automate mathematics. Towards this goal\, his curr
ent research focuses on building fundamental reaso
ning architectures as well as improving the reason
ing capabilities of large language models. During
his Ph.D at University of Toronto\, he was awarded
a Google PhD Fellowship. \n\n
LOCATION:Zoom
CONTACT:Mateja Jamnik
END:VEVENT
END:VCALENDAR