BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CMSA - ECPv6.15.18//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:CMSA
X-ORIGINAL-URL:https://cmsa.fas.harvard.edu
X-WR-CALDESC:Events for CMSA
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:America/New_York
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20230312T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20231105T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20240310T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20241103T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20250309T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20251102T060000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20241113T100000
DTEND;TZID=America/New_York:20241113T230000
DTSTAMP:20260412T075829
CREATED:20241017T141250Z
LAST-MODIFIED:20241115T175125Z
UID:10003613-1731492000-1731538800@cmsa.fas.harvard.edu
SUMMARY:Frontier of Formal Theorem Proving with Large Language Models: Insights from the DeepSeek-Prover Series
DESCRIPTION:New Technologies in Mathematics Seminar \nSpeaker: Huajian Xin\, DeepSeek \nTitle: Frontier of Formal Theorem Proving with Large Language Models: Insights from the DeepSeek-Prover Series \nAbstract: Recent advances in large language models have markedly influenced mathematical reasoning and automated theorem proving within artificial intelligence. Yet\, despite their success in natural language tasks\, these models face notable obstacles in formal theorem proving environments such as Lean and Isabelle\, where exacting derivations must adhere to strict formal specifications. Even state-of-the-art models encounter difficulty generating accurate and complex formal proofs\, revealing the unique blend of mathematical rigor required in this domain. In the DeepSeek-Prover series (V1 and V1.5)\, we have explored specialized methodologies aimed at addressing these challenges. This talk will delve into three foundational areas: the synthesis of training data through autoformalization\, reinforcement learning that utilizes feedback from proof assistants\, and test-time optimization using Monte Carlo tree search. I will also provide insights into current model capabilities\, persistent challenges\, and the future potential of large language models in automated theorem proving.
URL:https://cmsa.fas.harvard.edu/event/newtech_111324/
LOCATION:Virtual
CATEGORIES:New Technologies in Mathematics Seminar
ATTACH;FMTTYPE=image/png:https://cmsa.fas.harvard.edu/media/CMSA-NTM-Seminar-11.13.24.png
END:VEVENT
END:VCALENDAR