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: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:20250331T100000 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:0a6d970d06a5856041b4184078625e52 CATEGORIES:Lean Seminar CREATED:20260330T141754 SUMMARY:From solving formal systems to building theories (and back) LOCATION:Hill 705 DESCRIPTION:A famous essay by Gowers, “The two cultures of mathematics”, highlights a c ontrast between two attitudes towards mathematics: the problem-solving view where the point of “understanding” is to improve one’s ability to tackle p roblems, and the theory-building angle that sees the point of solving probl ems as improving one’s understanding (and mathematical theories). AI, for m athematics and arguably most domains, largely focuses on problem-solving gi ven an existing background theory, but building theories themselves is comp arably underexplored. This talk will consider what theory building can look like in two AI systems. First, we will consider the problem of tactic indu ction: given a set of formal proofs, find high-level tactics that simplify them, as measured by a compression objective. We’ll consider both a case st udy on learning tactics from educational algebra problems from Khan Academy , as well as tactics in the Rocq theorem prover. Learned tactics reveal dom ain-specific patterns in solutions and we show that they can help LLM-based provers. Then, we will describe ongoing work on Formal Disco, an open-ende d system where complete new verified programs, from ideation to specificati on, implementation and proofs, are synthesized by LLM agents. Using open mo dels over 10 days, our system generated the largest dataset of verified pro grams in the Dafny language to date, and we show how the data is useful to improve models at verification-relevant tasks, such as annotating methods w ith assertions and loops invariants. Although the evaluations of both syste ms will focus on pragmatic tasks, we will speculate further on implications of more powerful automated theory building systems. X-ALT-DESC;FMTTYPE=text/html:

A famous essay by Gowers, “T he two cultures of mathematics”, highlights a contrast between two attitude s towards mathematics: the problem-solving view where the point of “underst anding” is to improve one’s ability to tackle problems, and the theory-building angle that sees the point of solving problems as improving one’ s understanding (and mathematical theories). AI, for mathematics and arguab ly most domains, largely focuses on problem-solving given an existing backg round theory, but building theories themselves is comparably underexplored. This talk will consider what theory building can look like in two AI syste ms. First, we will consider the problem of tactic induction: giv en a set of formal proofs, find high-level tactics that simplify them, as m easured by a compression objective. We’ll consider both a case study on lea rning tactics from educational algebra problems from Khan Academy, as well as tactics in the Rocq theorem prover. Learned tactics reveal domain-specific p atterns in solutions and we show that they can help LLM-based provers. Then , we will describe ongoing work on Formal Disco, an open-ended system where complete new verified programs, from ideation to specification, implementa tion and proofs, are synthesized by LLM agents. Using open models over 10 d ays, our system generated the largest dataset of verified programs in the D afny language to date, and we show how the data is useful to improve models at verification-relevant tasks, such as annotating methods with asser tions and loops invariants. Although the evaluations of both systems w ill focus on pragmatic tasks, we will speculate further on implication s of more powerful automated theory building systems.

CONTACT:Gabriel Poesia DTSTAMP:20260828T001806 DTSTART;TZID=America/New_York:20260401T100000 DTEND;TZID=America/New_York:20260401T110000 SEQUENCE:0 TRANSP:OPAQUE END:VEVENT END:VCALENDAR