BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//jEvents 2.0 for Joomla//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VTIMEZONE
TZID:America/New_York
BEGIN:STANDARD
DTSTART:20241118T140000
RDATE:20250309T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20251102T010000
RDATE:20260308T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20261101T010000
RDATE:20270314T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20271107T010000
RDATE:20280312T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20281105T010000
RDATE:20290311T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:DAYLIGHT
DTSTART:20250309T030000
RDATE:20251102T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20260308T030000
RDATE:20261101T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20270314T030000
RDATE:20271107T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20280312T030000
RDATE:20281105T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:eeac768b9409b58d57f30c62b0b87bc8
CATEGORIES:Lean Seminar
CREATED:20251116T211116
SUMMARY:Auto-formalization via Joint Embeddings
LOCATION:CoRE 431
DESCRIPTION:<p><span data-olk-copy-source="MessageBody" style="color: #242424; font-siz
 e: 12pt; font-family: Aptos, Aptos_EmbeddedFont, Aptos_MSFontService, Calib
 ri, Helvetica, sans-serif;">In recent years we have witnessed a symbiotic t
 rend wherein LLMs are being combined with provers, solvers, and computer al
 gebra systems, resulting in dramatic breakthroughs in AI for math. Followin
 g this trend, we have developed two lines of work in my research group. The
  first is the idea that "good" joint embeddings (JE) can dramatically impro
 ve the efficacy of LLM-based auto-formalization tools. We say that JEs are 
 good if they respect the following invariant: semantically-equivalent forma
 lly-dissimilar objects (e.g., pairs of sematically-equivalent natural and f
 ormal language proofs) must be "close by" in the embedding space, and seman
 tically inequivalent ones "far apart". We use such JE models as part of a s
 uccessful RAG-based auto-formalization pipeline, demonstrating that such JE
 s are a critical AI-for-math technology. The second idea is Reinforcement L
 earning with Symbolic Feedback (RLSF), a class of techniques that addresses
  the LLM hallucination problem in contexts where we have access to rich sym
 bolic feedback such math, physics, and code,&nbsp;demonstrating that they t
 oo are critical to the success of AI for math.&nbsp;</span></p>
CONTACT:Vijay Ganesh
DTSTAMP:20260827T015759
DTSTART;TZID=America/New_York:20251119T140000
DTEND;TZID=America/New_York:20251119T150000
SEQUENCE:0
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR