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:In recent years we have witnessed a symbiotic trend wherein LLMs are being combined with provers, solvers, and computer algebra systems, resulting in dramatic breakthroughs in AI for math. Following this trend, we have develo ped two lines of work in my research group. The first is the idea that "goo d" joint embeddings (JE) can dramatically improve the efficacy of LLM-based auto-formalization tools. We say that JEs are good if they respect the fol lowing invariant: semantically-equivalent formally-dissimilar objects (e.g. , pairs of sematically-equivalent natural and formal language proofs) must be "close by" in the embedding space, and semantically inequivalent ones "f ar apart". We use such JE models as part of a successful RAG-based auto-for malization pipeline, demonstrating that such JEs are a critical AI-for-math technology. The second idea is Reinforcement Learning with Symbolic Feedba ck (RLSF), a class of techniques that addresses the LLM hallucination probl em in contexts where we have access to rich symbolic feedback such math, ph ysics, and code, demonstrating that they too are critical to the success of AI for math. \n X-ALT-DESC;FMTTYPE=text/html:

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, demonstrating that they t oo are critical to the success of AI for math. 

CONTACT:Vijay Ganesh DTSTAMP:20260827T115846 DTSTART;TZID=America/New_York:20251119T140000 DTEND;TZID=America/New_York:20251119T150000 SEQUENCE:0 TRANSP:OPAQUE END:VEVENT END:VCALENDAR